diff options
| author |  qunyanm <unknown> | 2015-05-14 15:44:39 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2015-05-14 15:44:39 -0700 |
| commit | 454909184e73582e425cad56a526956d91b88dcc (patch) | |
| tree | 7a77a99216dff39bd0aa862327e3c158694a9da1 /Source/Dafny/Dafny.atg | |
| parent | c13c4f3fbeae61ff152eaeeb4ae8bde9d01206be (diff) | |
Allow MatchExpr and MatchStmt to have nested patterns. Such as
function last<T>(xs: List<T>): T
requires xs != Nil
{
match xs
case Cons(y, Nil) => y
case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
}
And
function minus(x: Nat, y: Nat): Nat
{
match (x, y)
case (Zero, _) => Zero
case (Suc(_), Zero) => x
case (Suc(a), Suc(b)) => minus(a, b)
}
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 50 |
1 files changed, 32 insertions, 18 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index c03f5ce0..3f684ff6 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1794,17 +1794,24 @@ MatchStmt<out Statement/*!*/ s> CaseStatement<out MatchCaseStmt/*!*/ c>
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ x, id;
- List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
- BoundVar/*!*/ bv;
+ List<CasePattern/*!*/> arguments = new List<CasePattern/*!*/>();
+ CasePattern/*!*/ pat;
List<Statement/*!*/> body = new List<Statement/*!*/>();
+ string/*!*/ name = "";
.)
"case" (. x = t; .)
- Ident<out id>
- [ "("
- IdentTypeOptional<out bv> (. arguments.Add(bv); .)
- { "," IdentTypeOptional<out bv> (. arguments.Add(bv); .)
- }
- ")" ]
+ ( Ident<out id> (. name = id.val; .)
+ [ "("
+ CasePattern<out pat> (. arguments.Add(pat); .)
+ { "," CasePattern<out pat> (. arguments.Add(pat); .)
+ }
+ ")" ]
+ | "("
+ CasePattern<out pat> (. arguments.Add(pat); .)
+ { "," CasePattern<out pat> (. arguments.Add(pat); .)
+ }
+ ")"
+ )
"=>"
SYNC /* this SYNC and the one inside the loop below are used to avoid problems with the IsNotEndOfCase test. The SYNC will
* skip until the next symbol that can legally occur here, which is either the beginning of a Stmt or whatever is allowed
@@ -1814,7 +1821,7 @@ CaseStatement<out MatchCaseStmt/*!*/ c> Stmt<body>
SYNC /* see comment about SYNC above */
}
- (. c = new MatchCaseStmt(x, id.val, arguments, body); .)
+ (. c = new MatchCaseStmt(x, name, arguments, body); .)
.
/*------------------------------------------------------------------------*/
AssertStmt<out Statement/*!*/ s>
@@ -2584,19 +2591,26 @@ MatchExpression<out Expression e, bool allowSemi, bool allowLambda> .
CaseExpression<out MatchCaseExpr c, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id;
- List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
- BoundVar/*!*/ bv;
+ List<CasePattern/*!*/> arguments = new List<CasePattern/*!*/>();
+ CasePattern/*!*/ pat;
Expression/*!*/ body;
+ string/*!*/ name = "";
.)
"case" (. x = t; .)
- Ident<out id>
- [ "("
- IdentTypeOptional<out bv> (. arguments.Add(bv); .)
- { "," IdentTypeOptional<out bv> (. arguments.Add(bv); .)
- }
- ")" ]
+ ( Ident<out id> (. name = id.val; .)
+ [ "("
+ CasePattern<out pat> (. arguments.Add(pat); .)
+ { "," CasePattern<out pat> (. arguments.Add(pat); .)
+ }
+ ")" ]
+ | "("
+ CasePattern<out pat> (. arguments.Add(pat); .)
+ { "," CasePattern<out pat> (. arguments.Add(pat); .)
+ }
+ ")"
+ )
"=>"
- Expression<out body, allowSemi, allowLambda> (. c = new MatchCaseExpr(x, id.val, arguments, body); .)
+ Expression<out body, allowSemi, allowLambda> (. c = new MatchCaseExpr(x, name, arguments, body); .)
.
CasePattern<out CasePattern pat>
= (. IToken id; List<CasePattern> arguments;
|