Skip to content

Commit

Permalink
Allow _ in match patterns
Browse files Browse the repository at this point in the history
  • Loading branch information
titzer committed Jun 26, 2024
1 parent 76f4080 commit 41a7fe2
Show file tree
Hide file tree
Showing 44 changed files with 372 additions and 9 deletions.
2 changes: 1 addition & 1 deletion aeneas/src/main/Version.v3
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,6 @@

// Updated by VCS scripts. DO NOT EDIT.
component Version {
def version: string = "III-7.1742";
def version: string = "III-7.1743";
var buildData: string;
}
8 changes: 5 additions & 3 deletions aeneas/src/ssa/VstSsaGen.v3
Original file line number Diff line number Diff line change
Expand Up @@ -603,11 +603,13 @@ class VstSsaGen extends VstVisitor<VstSsaEnv, SsaInstr> {
var ta = [keyType], args = [newKey], i = 0;
var ic = ir.makeIrClass(newKeyType);
for (pl = p.params.list; pl != null; pl = pl.tail) { // XXX: mark and skip unused params
var fieldRef = IrSpec.new(newKeyType, ta, ic.fields[i++]);
pl.head.ssa = VstSsaVar.new();
var vdecl = pl.head, field = ic.fields[i++];
if (vdecl.isUnderscore()) continue; // unused part of a match
var fieldRef = IrSpec.new(newKeyType, ta, field);
vdecl.ssa = VstSsaVar.new();
var op = V3Op.newVariantGetField(fieldRef);
var load = env.add(op, [newKey], fieldRef.member.facts);
pl.head.ssa.instr = load;
vdecl.ssa.instr = load;
if (load.inputs.length == 1 && load.input0() == newKey) {
// loads of non-default variants don't need null checks
if (p.decl().variantTag > 0) load.facts |= Fact.O_NO_NULL_CHECK;
Expand Down
6 changes: 4 additions & 2 deletions aeneas/src/vst/Parser.v3
Original file line number Diff line number Diff line change
Expand Up @@ -774,8 +774,10 @@ component Parser {
return MatchPattern.new(expr, params);
}
def parseMatchParam(p: ParserState) -> VarDecl {
var id = parseIdentVoid(p);
var v = VarDecl.new(id.name, null, null);
var token: Token;
if (p.curByte == '_') token = p.token(1);
else token = parseIdentVoid(p).name;
var v = VarDecl.new(token, null, null);
v.isReadOnly = true;
return v;
}
Expand Down
9 changes: 6 additions & 3 deletions aeneas/src/vst/Verifier.v3
Original file line number Diff line number Diff line change
Expand Up @@ -1220,7 +1220,7 @@ class TypeChecker(ERROR: ErrorGen, file: VstFile) extends VstVisitor<Type, Type>
}
if (mv.variantType != null) return checkVariantPattern(mv, pat);
if (mv.enumType != null) return checkEnumPattern(mv, pat);
if (pat.params != null) return errAtRange(pat.params.range()).MatchError("match pattern cannot have parameters");
if (pat.params != null) return errAtRange(pat.params.range()).MatchError(Strings.format1("match on type %s cannot have parameters", TYPE(mv.etype)));
typeCheckExpr(e, mv.etype, "match case");
if (!VarExpr.?(e)) return errAtExpr(e).MatchError("match expression is not a constant");
var ve = VarExpr.!(e);
Expand Down Expand Up @@ -1257,13 +1257,16 @@ class TypeChecker(ERROR: ErrorGen, file: VstFile) extends VstVisitor<Type, Type>
var ll = pat.params.list, pl = pat.decl().params.list;
var typeArgs = vt.getTypeArgs();
while (ll != null) {
var vdecl = ll.head;
if (pl == null) {
var msg = Strings.format2("case %q.%s", vt.render, pat.decl().name());
errAtToken(ll.head.token).ArityMismatch(msg, Lists.length(pat.decl().params.list), Lists.length(pat.params.list));
return;
}
ll.head.vtype = pl.head.vtype.substitute(typeArgs);
methodEnv.bindVar(ll.head);
if (!vdecl.isUnderscore()) {
vdecl.vtype = pl.head.vtype.substitute(typeArgs);
methodEnv.bindVar(vdecl);
}
ll = ll.tail;
pl = pl.tail;
}
Expand Down
1 change: 1 addition & 0 deletions aeneas/src/vst/Vst.v3
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,7 @@ class Decl(token: Token) {
def render(buf: StringBuilder) -> StringBuilder {
return buf.puts(token.image);
}
def isUnderscore() -> bool { return Strings.equal("_", token.image); } // XXX: make a boolean field?
}
// Parsed parameter
class ParamDecl extends VarDecl {
Expand Down
1 change: 1 addition & 0 deletions doc/aeneas-issues.txt
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,7 @@ ______ ______ __ _ ______ ______ ______ _____ ______ ______ _ _ ______ _
debugger: allow fuzzy match of files / line
immutable arrays
-- done -------
* Allow _ in match patterns
* wasm target allows omitting main
* off-heap Range<byte>
* stray updateVar for phis
Expand Down
6 changes: 6 additions & 0 deletions test/core/parser/match_underscore00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@parse
def m() {
match (m) {
A(_) => ;
}
}
6 changes: 6 additions & 0 deletions test/core/parser/match_underscore01.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@parse
def m() {
match (m) {
A(x, _) => ;
}
}
6 changes: 6 additions & 0 deletions test/core/parser/match_underscore02.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@parse = ParseError @ 4:19
def m() {
match (m) {
_ _ => ;
}
}
7 changes: 7 additions & 0 deletions test/core/parser/match_underscore03.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
//@parse
def m() {
match (m) {
A(_, _) => ;
_ => ;
}
}
9 changes: 9 additions & 0 deletions test/core/parser/match_underscore04.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
//@parse
def m() {
match (m) {
A(_, _) => ;
x: T => ;
A(_, _) => ;
_ => ;
}
}
6 changes: 6 additions & 0 deletions test/core/parser/match_underscore05.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@parse = ParseError @ 4:20
def m() {
match (m) {
x: _ => ;
}
}
6 changes: 6 additions & 0 deletions test/core/parser/match_underscore06.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@parse
def m() {
match (m) {
x: T => _;
}
}
6 changes: 6 additions & 0 deletions test/core/parser/match_underscore07.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@parse = ParseError @ 4:21
def m() {
match (m) {
x() _ => ;
}
}
6 changes: 6 additions & 0 deletions test/core/parser/match_underscore08.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@parse = ParseError @ 4:21
def m() {
match (m) {
x(_ _) => ;
}
}
6 changes: 6 additions & 0 deletions test/core/parser/match_underscore09.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@parse = ParseError @ 4:21
def m() {
match (m) {
x(__) => ;
}
}
6 changes: 6 additions & 0 deletions test/core/parser/match_underscore10.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@parse = ParseError @ 4:21
def m() {
match (m) {
x(_,) => ;
}
}
6 changes: 6 additions & 0 deletions test/core/parser/match_underscore11.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@parse = ParseError @ 4:21
def m() {
match (m) {
x(_a) => ;
}
}
6 changes: 6 additions & 0 deletions test/core/parser/match_underscore12.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@parse
def m() {
match (m) {
x(a_) => ;
}
}
6 changes: 6 additions & 0 deletions test/core/parser/match_underscore13.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@parse
def m() {
match (m) {
x(a_b) => ;
}
}
8 changes: 8 additions & 0 deletions test/fail/match_cover00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
//@seman
type T(x: int);

def m(t: T) {
match (t) {
T(_) => ;
}
}
8 changes: 8 additions & 0 deletions test/fail/match_cover01.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
//@seman
type T(x: int);

def m(t: T) {
match (t) {
T => ;
}
}
8 changes: 8 additions & 0 deletions test/fail/match_cover02.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
//@seman
type T(x: int);

def m(t: T) {
match (t) {
x: T => ;
}
}
10 changes: 10 additions & 0 deletions test/variants/match_underscore00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
//@execute 0=3; -3=0; 66=69
type T {
case A(x: int);
}

def main(a: int) -> int {
match (T.A(a)) {
A(_) => return a + 3;
}
}
10 changes: 10 additions & 0 deletions test/variants/match_underscore01.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
//@execute 0=3; -3=0; 66=69
type T {
case A(x: int, y: int);
}

def main(a: int) -> int {
match (T.A(a, 11)) {
A(x, _) => return x + 3;
}
}
12 changes: 12 additions & 0 deletions test/variants/match_underscore02.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
//@execute 0=3; -3=0; 66=69
type T {
case A(x: int, y: int);
}

def make: (int, int) -> T = T.A;

def main(a: int) -> int {
match (make(a, 11)) {
A(x, _) => return x + 3;
}
}
12 changes: 12 additions & 0 deletions test/variants/match_underscore03.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
//@execute 0=15; -3=15; 66=15
type T {
case A(x: int, y: int);
}

def make: (int, int) -> T = T.A;

def main(a: int) -> int {
match (make(a, 12)) {
A(_, x) => return x + 3;
}
}
13 changes: 13 additions & 0 deletions test/variants/match_underscore04.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
//@execute 0=100; 55=155
type T {
case A(x: int, y: int, z: int);
}

def make: (int, int, int) -> T = T.A;

def main(a: int) -> int {
var t = make(a + 100, a + 200, a + 300);
match (t) {
A(x, _, _) => return x;
}
}
13 changes: 13 additions & 0 deletions test/variants/match_underscore05.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
//@execute 0=200; 55=255
type T {
case A(x: int, y: int, z: int);
}

def make: (int, int, int) -> T = T.A;

def main(a: int) -> int {
var t = make(a + 100, a + 200, a + 300);
match (t) {
A(_, x, _) => return x;
}
}
13 changes: 13 additions & 0 deletions test/variants/match_underscore06.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
//@execute 0=300; 55=355
type T {
case A(x: int, y: int, z: int);
}

def make: (int, int, int) -> T = T.A;

def main(a: int) -> int {
var t = make(a + 100, a + 200, a + 300);
match (t) {
A(_, _, x) => return x;
}
}
13 changes: 13 additions & 0 deletions test/variants/match_underscore07.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
//@execute 0=400; 55=510
type T {
case A(x: int, y: int, z: int);
}

def make: (int, int, int) -> T = T.A;

def main(a: int) -> int {
var t = make(a + 100, a + 200, a + 300);
match (t) {
A(x, _, z) => return x + z;
}
}
13 changes: 13 additions & 0 deletions test/variants/match_underscore08.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
//@execute 0=100; 55=155
type T {
case A(x: int, y: (int, int));
}

def make: (int, (int, int)) -> T = T.A;

def main(a: int) -> int {
var t = make(a + 100, (a + 200, a + 300));
match (t) {
A(x, _) => return x;
}
}
13 changes: 13 additions & 0 deletions test/variants/match_underscore09.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
//@execute 0=500; 55=610
type T {
case A(x: int, y: (int, int));
}

def make: (int, (int, int)) -> T = T.A;

def main(a: int) -> int {
var t = make(a + 100, (a + 200, a + 300));
match (t) {
A(_, y) => return y.0 + y.1;
}
}
10 changes: 10 additions & 0 deletions test/variants/seman/match_underscore00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
//@seman
type T {
case A(x: int);
}

def m(t: T) {
match (t) {
A(_) => ;
}
}
10 changes: 10 additions & 0 deletions test/variants/seman/match_underscore01.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
//@seman
type T {
case A(x: int, y: int);
}

def m(t: T) -> int {
match (t) {
A(x, _) => return x;
}
}
10 changes: 10 additions & 0 deletions test/variants/seman/match_underscore02.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
//@seman
type T {
case A(x: int, y: int);
}

def m(t: T) -> int {
match (t) {
A(_, y) => return y;
}
}
10 changes: 10 additions & 0 deletions test/variants/seman/match_underscore03.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
//@seman
type T {
case A(x: int, y: int);
}

def m(t: T) -> int {
match (t) {
A(_, z) => return z;
}
}
10 changes: 10 additions & 0 deletions test/variants/seman/match_underscore04.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
//@seman = TypeError @ 8:22
type T {
case A(x: int, y: int);
}

def m(t: T) -> bool {
match (t) {
A(_, z) => return z;
}
}
Loading

0 comments on commit 41a7fe2

Please sign in to comment.