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 | |
| 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)
}
| -rw-r--r-- | Source/Dafny/Cloner.cs | 37 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 50 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 118 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 260 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 60 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 867 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 52 | ||||
| -rw-r--r-- | Test/dafny0/NestedMatch.dfy | 59 | ||||
| -rw-r--r-- | Test/dafny0/NestedMatch.dfy.expect | 2 |
9 files changed, 1157 insertions, 348 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 9f83bf09..f729d411 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -300,9 +300,8 @@ namespace Microsoft.Dafny var e = (ExprDotName)expr;
return new ExprDotName(Tok(e.tok), CloneExpr(e.Lhs), e.SuffixName, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));
} else if (expr is ApplySuffix) {
- var e = (ApplySuffix)expr;
- return new ApplySuffix(Tok(e.tok), CloneExpr(e.Lhs), e.Args.ConvertAll(CloneExpr));
-
+ var e = (ApplySuffix) expr;
+ return CloneApplySuffix(e);
} else if (expr is MemberSelectExpr) {
var e = (MemberSelectExpr)expr;
return new MemberSelectExpr(Tok(e.tok), CloneExpr(e.Obj), e.MemberName);
@@ -411,7 +410,7 @@ namespace Microsoft.Dafny } else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
return new MatchExpr(Tok(e.tok), CloneExpr(e.Source),
- e.Cases.ConvertAll(c => new MatchCaseExpr(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))), e.UsesOptionalBraces);
+ e.Cases.ConvertAll(CloneMatchCaseExpr), e.UsesOptionalBraces);
} else if (expr is NegationExpression) {
var e = (NegationExpression)expr;
@@ -422,6 +421,22 @@ namespace Microsoft.Dafny }
}
+ public MatchCaseExpr CloneMatchCaseExpr(MatchCaseExpr c) {
+ Contract.Requires(c != null);
+ if (c.Arguments != null) {
+ Contract.Assert(c.CasePatterns == null);
+ return new MatchCaseExpr(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body));
+ } else {
+ Contract.Assert(c.Arguments == null);
+ Contract.Assert(c.CasePatterns != null);
+ return new MatchCaseExpr(Tok(c.tok), c.Id, c.CasePatterns.ConvertAll(CloneCasePattern), CloneExpr(c.Body));
+ }
+ }
+
+ public virtual Expression CloneApplySuffix(ApplySuffix e) {
+ return new ApplySuffix(Tok(e.tok), CloneExpr(e.Lhs), e.Args.ConvertAll(CloneExpr));
+ }
+
public virtual CasePattern CloneCasePattern(CasePattern pat) {
Contract.Requires(pat != null);
if (pat.Var != null) {
@@ -530,7 +545,7 @@ namespace Microsoft.Dafny } else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
r = new MatchStmt(Tok(s.Tok), Tok(s.EndTok), CloneExpr(s.Source),
- s.Cases.ConvertAll(c => new MatchCaseStmt(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), c.Body.ConvertAll(CloneStmt))), s.UsesOptionalBraces);
+ s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);
} else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
@@ -562,6 +577,18 @@ namespace Microsoft.Dafny return r;
}
+ public MatchCaseStmt CloneMatchCaseStmt(MatchCaseStmt c) {
+ Contract.Requires(c != null);
+ if (c.Arguments != null) {
+ Contract.Assert(c.CasePatterns == null);
+ return new MatchCaseStmt(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), c.Body.ConvertAll(CloneStmt));
+ } else {
+ Contract.Assert(c.Arguments == null);
+ Contract.Assert(c.CasePatterns != null);
+ return new MatchCaseStmt(Tok(c.tok), c.Id, c.CasePatterns.ConvertAll(CloneCasePattern), c.Body.ConvertAll(CloneStmt));
+ }
+ }
+
public CalcStmt.CalcOp CloneCalcOp(CalcStmt.CalcOp op) {
if (op is CalcStmt.BinaryCalcOp) {
return new CalcStmt.BinaryCalcOp(((CalcStmt.BinaryCalcOp) op).Op);
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;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 99dfecd6..a94b9a1b 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4710,8 +4710,8 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullElements(MissingCases));
}
- public readonly Expression Source;
- public readonly List<MatchCaseStmt> Cases;
+ private Expression source;
+ private List<MatchCaseStmt> cases;
public readonly List<DatatypeCtor> MissingCases = new List<DatatypeCtor>(); // filled in during resolution
public readonly bool UsesOptionalBraces;
@@ -4721,14 +4721,31 @@ namespace Microsoft.Dafny { Contract.Requires(endTok != null);
Contract.Requires(source != null);
Contract.Requires(cce.NonNullElements(cases));
- this.Source = source;
- this.Cases = cases;
+ this.source = source;
+ this.cases = cases;
this.UsesOptionalBraces = usesOptionalBraces;
}
+ public Expression Source {
+ get { return source; }
+ }
+
+ public List<MatchCaseStmt> Cases {
+ get { return cases; }
+ }
+
+ // should only be used in desugar in resolve to change the cases of the matchexpr
+ public void UpdateSource(Expression source) {
+ this.source = source;
+ }
+
+ public void UpdateCases(List<MatchCaseStmt> cases) {
+ this.cases = cases;
+ }
+
public override IEnumerable<Statement> SubStatements {
get {
- foreach (var kase in Cases) {
+ foreach (var kase in cases) {
foreach (var s in kase.Body) {
yield return s;
}
@@ -4745,7 +4762,7 @@ namespace Microsoft.Dafny { public class MatchCaseStmt : MatchCase
{
- public readonly List<Statement> Body;
+ private List<Statement> body;
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -4759,7 +4776,25 @@ namespace Microsoft.Dafny { Contract.Requires(id != null);
Contract.Requires(cce.NonNullElements(arguments));
Contract.Requires(cce.NonNullElements(body));
- this.Body = body;
+ this.body = body;
+ }
+
+ public MatchCaseStmt(IToken tok, string id, [Captured] List<CasePattern> cps, [Captured] List<Statement> body)
+ : base(tok, id, cps) {
+ Contract.Requires(tok != null);
+ Contract.Requires(id != null);
+ Contract.Requires(cce.NonNullElements(cps));
+ Contract.Requires(cce.NonNullElements(body));
+ this.body = body;
+ }
+
+ public List<Statement> Body {
+ get { return body; }
+ }
+
+ // should only be called by resolve to reset the body of the MatchCaseExpr
+ public void UpdateBody(List<Statement> body) {
+ this.body = body;
}
}
@@ -6806,8 +6841,8 @@ namespace Microsoft.Dafny { }
public class MatchExpr : Expression { // a MatchExpr is an "extended expression" and is only allowed in certain places
- public readonly Expression Source;
- public readonly List<MatchCaseExpr> Cases;
+ private Expression source;
+ private List<MatchCaseExpr> cases;
public readonly List<DatatypeCtor> MissingCases = new List<DatatypeCtor>(); // filled in during resolution
public readonly bool UsesOptionalBraces;
@@ -6823,15 +6858,32 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null);
Contract.Requires(source != null);
Contract.Requires(cce.NonNullElements(cases));
- this.Source = source;
- this.Cases = cases;
+ this.source = source;
+ this.cases = cases;
this.UsesOptionalBraces = usesOptionalBraces;
}
+ public Expression Source {
+ get { return source; }
+ }
+
+ public List<MatchCaseExpr> Cases {
+ get { return cases; }
+ }
+
+ // should only be used in desugar in resolve to change the source and cases of the matchexpr
+ public void UpdateSource(Expression source) {
+ this.source = source;
+ }
+
+ public void UpdateCases(List<MatchCaseExpr> cases) {
+ this.cases = cases;
+ }
+
public override IEnumerable<Expression> SubExpressions {
get {
yield return Source;
- foreach (var mc in Cases) {
+ foreach (var mc in cases) {
yield return mc.Body;
}
}
@@ -6913,12 +6965,13 @@ namespace Microsoft.Dafny { public readonly IToken tok;
public readonly string Id;
public DatatypeCtor Ctor; // filled in by resolution
- public readonly List<BoundVar> Arguments;
+ public List<BoundVar> Arguments; // created by the resolver.
+ public List<CasePattern> CasePatterns; // generated from parsers. It should be converted to List<BoundVar> during resolver. Invariant: CasePatterns != null ==> Arguments == null
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(tok != null);
Contract.Invariant(Id != null);
- Contract.Invariant(cce.NonNullElements(Arguments));
+ Contract.Invariant(cce.NonNullElements(Arguments) || cce.NonNullElements(CasePatterns));
}
public MatchCase(IToken tok, string id, [Captured] List<BoundVar> arguments) {
@@ -6929,24 +6982,51 @@ namespace Microsoft.Dafny { this.Id = id;
this.Arguments = arguments;
}
+
+ public MatchCase(IToken tok, string id, [Captured] List<CasePattern> cps) {
+ Contract.Requires(tok != null);
+ Contract.Requires(id != null);
+ Contract.Requires(cce.NonNullElements(cps));
+ this.tok = tok;
+ this.Id = id;
+ this.CasePatterns = cps;
+ }
}
public class MatchCaseExpr : MatchCase
{
- public readonly Expression Body;
+ private Expression body;
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Body != null);
+ Contract.Invariant(body != null);
}
public MatchCaseExpr(IToken tok, string id, [Captured] List<BoundVar> arguments, Expression body)
- : base(tok, id, arguments)
- {
+ : base(tok, id, arguments) {
Contract.Requires(tok != null);
Contract.Requires(id != null);
Contract.Requires(cce.NonNullElements(arguments));
Contract.Requires(body != null);
- this.Body = body;
+ this.body = body;
+ }
+
+ public MatchCaseExpr(IToken tok, string id, [Captured] List<CasePattern> cps, Expression body)
+ : base(tok, id, cps)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(id != null);
+ Contract.Requires(cce.NonNullElements(cps));
+ Contract.Requires(body != null);
+ this.body = body;
+ }
+
+ public Expression Body {
+ get { return body; }
+ }
+
+ // should only be called by resolve to reset the body of the MatchCaseExpr
+ public void UpdateBody(Expression body) {
+ this.body = body;
}
}
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 9e283ef5..d0924169 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -2884,31 +2884,76 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void 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 = "";
Expect(31);
x = t;
- Ident(out id);
- if (la.kind == 48) {
+ if (la.kind == 1) {
+ Ident(out id);
+ name = id.val;
+ if (la.kind == 48) {
+ Get();
+ CasePattern(out pat);
+ arguments.Add(pat);
+ while (la.kind == 21) {
+ Get();
+ CasePattern(out pat);
+ arguments.Add(pat);
+ }
+ Expect(49);
+ }
+ } else if (la.kind == 48) {
Get();
- IdentTypeOptional(out bv);
- arguments.Add(bv);
+ CasePattern(out pat);
+ arguments.Add(pat);
while (la.kind == 21) {
Get();
- IdentTypeOptional(out bv);
- arguments.Add(bv);
+ CasePattern(out pat);
+ arguments.Add(pat);
}
Expect(49);
- }
+ } else SynErr(202);
Expect(27);
- while (!(StartOf(28))) {SynErr(202); Get();}
+ while (!(StartOf(28))) {SynErr(203); Get();}
while (IsNotEndOfCase()) {
Stmt(body);
- while (!(StartOf(28))) {SynErr(203); Get();}
+ while (!(StartOf(28))) {SynErr(204); Get();}
+ }
+ c = new MatchCaseStmt(x, name, arguments, body);
+ }
+
+ void CasePattern(out CasePattern pat) {
+ IToken id; List<CasePattern> arguments;
+ BoundVar bv;
+ pat = null;
+
+ if (IsIdentParen()) {
+ Ident(out id);
+ Expect(48);
+ arguments = new List<CasePattern>();
+ if (la.kind == 1) {
+ CasePattern(out pat);
+ arguments.Add(pat);
+ while (la.kind == 21) {
+ Get();
+ CasePattern(out pat);
+ arguments.Add(pat);
+ }
+ }
+ Expect(49);
+ pat = new CasePattern(id, id.val, arguments);
+ } else if (la.kind == 1) {
+ IdentTypeOptional(out bv);
+ pat = new CasePattern(bv.tok, bv);
+
+ } else SynErr(205);
+ if (pat == null) {
+ pat = new CasePattern(t, "_ParseError", new List<CasePattern>());
}
- c = new MatchCaseStmt(x, id.val, arguments, body);
+
}
void QuantifierDomain(out List<BoundVar> bvars, out Attributes attrs, out Expression range) {
@@ -3005,7 +3050,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; binOp = BinaryExpr.Opcode.Exp;
break;
}
- default: SynErr(204); break;
+ default: SynErr(206); break;
}
if (k == null) {
op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
@@ -3020,7 +3065,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 110) {
Get();
- } else SynErr(205);
+ } else SynErr(207);
}
void ImpliesOp() {
@@ -3028,7 +3073,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 112) {
Get();
- } else SynErr(206);
+ } else SynErr(208);
}
void ExpliesOp() {
@@ -3036,7 +3081,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 114) {
Get();
- } else SynErr(207);
+ } else SynErr(209);
}
void AndOp() {
@@ -3044,7 +3089,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 116) {
Get();
- } else SynErr(208);
+ } else SynErr(210);
}
void OrOp() {
@@ -3052,7 +3097,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 118) {
Get();
- } else SynErr(209);
+ } else SynErr(211);
}
void NegOp() {
@@ -3060,7 +3105,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 120) {
Get();
- } else SynErr(210);
+ } else SynErr(212);
}
void Forall() {
@@ -3068,7 +3113,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 121) {
Get();
- } else SynErr(211);
+ } else SynErr(213);
}
void Exists() {
@@ -3076,7 +3121,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 123) {
Get();
- } else SynErr(212);
+ } else SynErr(214);
}
void QSep() {
@@ -3084,7 +3129,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 24) {
Get();
- } else SynErr(213);
+ } else SynErr(215);
}
void EquivExpression(out Expression e0, bool allowSemi, bool allowLambda) {
@@ -3118,7 +3163,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LogicalExpression(out e1, allowSemi, allowLambda);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1);
}
- } else SynErr(214);
+ } else SynErr(216);
}
}
@@ -3148,7 +3193,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo RelationalExpression(out e1, allowSemi, allowLambda);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
}
- } else SynErr(215);
+ } else SynErr(217);
}
}
@@ -3366,7 +3411,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(216); break;
+ default: SynErr(218); break;
}
}
@@ -3388,7 +3433,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 126) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(217);
+ } else SynErr(219);
}
void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda) {
@@ -3441,7 +3486,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (IsSuffix()) {
Suffix(ref e);
}
- } else SynErr(218);
+ } else SynErr(220);
}
void MulOp(out IToken x, out BinaryExpr.Opcode op) {
@@ -3455,7 +3500,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 128) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(219);
+ } else SynErr(221);
}
void MapDisplayExpr(IToken/*!*/ mapToken, bool finite, out Expression e) {
@@ -3493,7 +3538,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 104) {
HashCall(id, out openParen, out typeArgs, out args);
} else if (StartOf(30)) {
- } else SynErr(220);
+ } else SynErr(222);
e = new ExprDotName(id, e, id.val, typeArgs);
if (openParen != null) {
e = new ApplySuffix(openParen, e, args);
@@ -3546,7 +3591,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee);
}
- } else SynErr(221);
+ } else SynErr(223);
} else if (la.kind == 135) {
Get();
anyDots = true;
@@ -3554,7 +3599,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out ee, true, true);
e1 = ee;
}
- } else SynErr(222);
+ } else SynErr(224);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -3598,7 +3643,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(49);
e = new ApplySuffix(openParen, e, args);
- } else SynErr(223);
+ } else SynErr(225);
}
void LambdaExpression(out Expression e, bool allowSemi) {
@@ -3627,7 +3672,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
Expect(49);
- } else SynErr(224);
+ } else SynErr(226);
while (la.kind == 42 || la.kind == 43) {
if (la.kind == 42) {
Get();
@@ -3702,7 +3747,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo NamedExpr(out e, allowSemi, allowLambda);
break;
}
- default: SynErr(225); break;
+ default: SynErr(227); break;
}
}
@@ -3717,7 +3762,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 104) {
HashCall(id, out openParen, out typeArgs, out args);
} else if (StartOf(30)) {
- } else SynErr(226);
+ } else SynErr(228);
e = new NameSegment(id, id.val, typeArgs);
if (openParen != null) {
e = new ApplySuffix(openParen, e, args);
@@ -3746,7 +3791,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
e = new SeqDisplayExpr(x, elements);
Expect(47);
- } else SynErr(227);
+ } else SynErr(229);
}
void MultiSetExpr(out Expression e) {
@@ -3770,7 +3815,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, true, true);
e = new MultiSetFormingExpr(x, e);
Expect(49);
- } else SynErr(228);
+ } else SynErr(230);
}
void ConstAtomExpression(out Expression e, bool allowSemi, bool allowLambda) {
@@ -3866,7 +3911,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ParensExpression(out e, allowSemi, allowLambda);
break;
}
- default: SynErr(229); break;
+ default: SynErr(231); break;
}
}
@@ -3895,7 +3940,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo n = BigInteger.Zero;
}
- } else SynErr(230);
+ } else SynErr(232);
}
void Dec(out Basetypes.BigDec d) {
@@ -3939,7 +3984,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 28) {
Get();
oneShot = true;
- } else SynErr(231);
+ } else SynErr(233);
}
void MapLiteralExpressions(out List<ExpressionPair> elements) {
@@ -4002,7 +4047,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo CaseExpression(out c, allowSemi, allowLambda);
cases.Add(c);
}
- } else SynErr(232);
+ } else SynErr(234);
e = new MatchExpr(x, e, cases, usesOptionalBrace);
}
@@ -4020,7 +4065,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 122 || la.kind == 123) {
Exists();
x = t;
- } else SynErr(233);
+ } else SynErr(235);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body, allowSemi, allowLambda);
@@ -4072,7 +4117,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssumeStmt(out s);
} else if (la.kind == 30) {
CalcStmt(out s);
- } else SynErr(234);
+ } else SynErr(236);
}
void LetExpr(out Expression e, bool allowSemi, bool allowLambda) {
@@ -4116,7 +4161,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- } else SynErr(235);
+ } else SynErr(237);
Expression(out e, false, true);
letRHSs.Add(e);
while (la.kind == 21) {
@@ -4143,16 +4188,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new NamedExpr(x, d.val, expr);
}
- void CasePattern(out CasePattern pat) {
- IToken id; List<CasePattern> arguments;
- BoundVar bv;
- pat = null;
+ void CaseExpression(out MatchCaseExpr c, bool allowSemi, bool allowLambda) {
+ Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id;
+ List<CasePattern/*!*/> arguments = new List<CasePattern/*!*/>();
+ CasePattern/*!*/ pat;
+ Expression/*!*/ body;
+ string/*!*/ name = "";
- if (IsIdentParen()) {
+ Expect(31);
+ x = t;
+ if (la.kind == 1) {
Ident(out id);
- Expect(48);
- arguments = new List<CasePattern>();
- if (la.kind == 1) {
+ name = id.val;
+ if (la.kind == 48) {
+ Get();
CasePattern(out pat);
arguments.Add(pat);
while (la.kind == 21) {
@@ -4160,43 +4209,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo CasePattern(out pat);
arguments.Add(pat);
}
+ Expect(49);
}
- Expect(49);
- pat = new CasePattern(id, id.val, arguments);
- } else if (la.kind == 1) {
- IdentTypeOptional(out bv);
- pat = new CasePattern(bv.tok, bv);
-
- } else SynErr(236);
- if (pat == null) {
- pat = new CasePattern(t, "_ParseError", new List<CasePattern>());
- }
-
- }
-
- void 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;
- Expression/*!*/ body;
-
- Expect(31);
- x = t;
- Ident(out id);
- if (la.kind == 48) {
+ } else if (la.kind == 48) {
Get();
- IdentTypeOptional(out bv);
- arguments.Add(bv);
+ CasePattern(out pat);
+ arguments.Add(pat);
while (la.kind == 21) {
Get();
- IdentTypeOptional(out bv);
- arguments.Add(bv);
+ CasePattern(out pat);
+ arguments.Add(pat);
}
Expect(49);
- }
+ } else SynErr(238);
Expect(27);
Expression(out body, allowSemi, allowLambda);
- c = new MatchCaseExpr(x, id.val, arguments, body);
+ c = new MatchCaseExpr(x, name, arguments, body);
}
void HashCall(IToken id, out IToken openParen, out List<Type> typeArgs, out List<Expression> args) {
@@ -4258,7 +4286,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 42) {
Get();
x = t;
- } else SynErr(237);
+ } else SynErr(239);
}
@@ -4532,42 +4560,44 @@ public class Errors { case 199: s = "this symbol not expected in LoopSpec"; break;
case 200: s = "this symbol not expected in LoopSpec"; break;
case 201: s = "invalid LoopSpec"; break;
- case 202: s = "this symbol not expected in CaseStatement"; break;
+ case 202: s = "invalid CaseStatement"; break;
case 203: s = "this symbol not expected in CaseStatement"; break;
- case 204: s = "invalid CalcOp"; break;
- case 205: s = "invalid EquivOp"; break;
- case 206: s = "invalid ImpliesOp"; break;
- case 207: s = "invalid ExpliesOp"; break;
- case 208: s = "invalid AndOp"; break;
- case 209: s = "invalid OrOp"; break;
- case 210: s = "invalid NegOp"; break;
- case 211: s = "invalid Forall"; break;
- case 212: s = "invalid Exists"; break;
- case 213: s = "invalid QSep"; break;
- case 214: s = "invalid ImpliesExpliesExpression"; break;
- case 215: s = "invalid LogicalExpression"; break;
- case 216: s = "invalid RelOp"; break;
- case 217: s = "invalid AddOp"; break;
- case 218: s = "invalid UnaryExpression"; break;
- case 219: s = "invalid MulOp"; break;
- case 220: s = "invalid Suffix"; break;
- case 221: s = "invalid Suffix"; break;
+ case 204: s = "this symbol not expected in CaseStatement"; break;
+ case 205: s = "invalid CasePattern"; break;
+ case 206: s = "invalid CalcOp"; break;
+ case 207: s = "invalid EquivOp"; break;
+ case 208: s = "invalid ImpliesOp"; break;
+ case 209: s = "invalid ExpliesOp"; break;
+ case 210: s = "invalid AndOp"; break;
+ case 211: s = "invalid OrOp"; break;
+ case 212: s = "invalid NegOp"; break;
+ case 213: s = "invalid Forall"; break;
+ case 214: s = "invalid Exists"; break;
+ case 215: s = "invalid QSep"; break;
+ case 216: s = "invalid ImpliesExpliesExpression"; break;
+ case 217: s = "invalid LogicalExpression"; break;
+ case 218: s = "invalid RelOp"; break;
+ case 219: s = "invalid AddOp"; break;
+ case 220: s = "invalid UnaryExpression"; break;
+ case 221: s = "invalid MulOp"; break;
case 222: s = "invalid Suffix"; break;
case 223: s = "invalid Suffix"; break;
- case 224: s = "invalid LambdaExpression"; break;
- case 225: s = "invalid EndlessExpression"; break;
- case 226: s = "invalid NameSegment"; break;
- case 227: s = "invalid DisplayExpr"; break;
- case 228: s = "invalid MultiSetExpr"; break;
- case 229: s = "invalid ConstAtomExpression"; break;
- case 230: s = "invalid Nat"; break;
- case 231: s = "invalid LambdaArrow"; break;
- case 232: s = "invalid MatchExpression"; break;
- case 233: s = "invalid QuantifierGuts"; break;
- case 234: s = "invalid StmtInExpr"; break;
- case 235: s = "invalid LetExpr"; break;
- case 236: s = "invalid CasePattern"; break;
- case 237: s = "invalid DotSuffix"; break;
+ case 224: s = "invalid Suffix"; break;
+ case 225: s = "invalid Suffix"; break;
+ case 226: s = "invalid LambdaExpression"; break;
+ case 227: s = "invalid EndlessExpression"; break;
+ case 228: s = "invalid NameSegment"; break;
+ case 229: s = "invalid DisplayExpr"; break;
+ case 230: s = "invalid MultiSetExpr"; break;
+ case 231: s = "invalid ConstAtomExpression"; break;
+ case 232: s = "invalid Nat"; break;
+ case 233: s = "invalid LambdaArrow"; break;
+ case 234: s = "invalid MatchExpression"; break;
+ case 235: s = "invalid QuantifierGuts"; break;
+ case 236: s = "invalid StmtInExpr"; break;
+ case 237: s = "invalid LetExpr"; break;
+ case 238: s = "invalid CaseExpression"; break;
+ case 239: s = "invalid DotSuffix"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index bf42c71a..0259f12c 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -901,17 +901,7 @@ namespace Microsoft.Dafny { wr.WriteLine();
Indent(caseInd);
wr.Write("case {0}", mc.Id);
- if (mc.Arguments.Count != 0) {
- string sep = "(";
- foreach (BoundVar bv in mc.Arguments) {
- wr.Write("{0}{1}", sep, bv.DisplayName);
- if (bv.Type is NonProxyType) {
- wr.Write(": {0}", bv.Type);
- }
- sep = ", ";
- }
- wr.Write(")");
- }
+ PrintMatchCaseArgument(mc);
wr.Write(" =>");
foreach (Statement bs in mc.Body) {
wr.WriteLine();
@@ -1199,17 +1189,7 @@ namespace Microsoft.Dafny { bool isLastCase = i == e.Cases.Count - 1;
Indent(ind);
wr.Write("case {0}", mc.Id);
- if (mc.Arguments.Count != 0) {
- string sep = "(";
- foreach (BoundVar bv in mc.Arguments) {
- wr.Write("{0}{1}", sep, bv.DisplayName);
- if (bv.Type is NonProxyType) {
- wr.Write(": {0}", bv.Type);
- }
- sep = ", ";
- }
- wr.Write(")");
- }
+ PrintMatchCaseArgument(mc);
wr.WriteLine(" =>");
PrintExtendedExpr(mc.Body, ind + IndentAmount, isLastCase, isLastCase && (parensNeeded || endWithCloseParen));
i++;
@@ -1246,6 +1226,33 @@ namespace Microsoft.Dafny { }
}
+ public void PrintMatchCaseArgument(MatchCase mc) {
+ if (mc.Arguments != null) {
+ if (mc.Arguments.Count != 0) {
+ string sep = "(";
+ foreach (BoundVar bv in mc.Arguments) {
+ wr.Write("{0}{1}", sep, bv.DisplayName);
+ if (bv.Type is NonProxyType) {
+ wr.Write(": {0}", bv.Type);
+ }
+ sep = ", ";
+ }
+ wr.Write(")");
+ }
+ } else {
+ Contract.Assert(mc.CasePatterns != null);
+ if (mc.CasePatterns.Count != 0) {
+ string sep = "(";
+ foreach (var cp in mc.CasePatterns) {
+ wr.Write(sep);
+ PrintCasePattern(cp);
+ sep = ", ";
+ }
+ wr.Write(")");
+ }
+ }
+ }
+
public void PrintExpression(Expression expr, bool isFollowedBySemicolon) {
Contract.Requires(expr != null);
PrintExpr(expr, 0, false, true, isFollowedBySemicolon, -1);
@@ -1859,14 +1866,7 @@ namespace Microsoft.Dafny { foreach (var mc in e.Cases) {
bool isLastCase = i == e.Cases.Count - 1;
wr.Write(" case {0}", mc.Id);
- if (mc.Arguments.Count != 0) {
- string sep = "(";
- foreach (BoundVar bv in mc.Arguments) {
- wr.Write("{0}{1}", sep, bv.DisplayName);
- sep = ", ";
- }
- wr.Write(")");
- }
+ PrintMatchCaseArgument(mc);
wr.Write(" => ");
PrintExpression(mc.Body, isRightmost && isLastCase, !parensNeeded && isFollowedBySemicolon);
i++;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index f7ec135b..be348311 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -5185,106 +5185,381 @@ namespace Microsoft.Dafny Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == s.Hints.Count);
} else if (stmt is MatchStmt) {
- MatchStmt s = (MatchStmt)stmt;
- bool bodyIsSpecOnly = specContextOnly;
- int prevErrorCount = ErrorCount;
- ResolveExpression(s.Source, new ResolveOpts(codeContext, true, specContextOnly));
- Contract.Assert(s.Source.Type != null); // follows from postcondition of ResolveExpression
- bool successfullyResolved = ErrorCount == prevErrorCount;
- if (!specContextOnly && successfullyResolved) {
- bodyIsSpecOnly = UsesSpecFeatures(s.Source);
- }
- UserDefinedType sourceType = null;
- DatatypeDecl dtd = null;
- if (s.Source.Type.IsDatatype) {
- sourceType = (UserDefinedType)s.Source.Type.NormalizeExpand();
- dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);
+ ResolveMatchStmt(stmt, specContextOnly, codeContext);
+ } else if (stmt is SkeletonStatement) {
+ var s = (SkeletonStatement)stmt;
+ Error(s.Tok, "skeleton statements are allowed only in refining methods");
+ // nevertheless, resolve the underlying statement; hey, why not
+ if (s.S != null) {
+ ResolveStatement(s.S, specContextOnly, codeContext);
}
- var subst = new Dictionary<TypeParameter, Type>();
- Dictionary<string, DatatypeCtor> ctors;
- if (dtd == null) {
- Error(s.Source, "the type of the match source expression must be a datatype (instead found {0})", s.Source.Type);
- ctors = null;
- } else {
- Contract.Assert(sourceType != null); // dtd and sourceType are set together above
- ctors = datatypeCtors[dtd];
- Contract.Assert(ctors != null); // dtd should have been inserted into datatypeCtors during a previous resolution stage
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException();
+ }
+ }
- // build the type-parameter substitution map for this use of the datatype
- for (int i = 0; i < dtd.TypeArgs.Count; i++) {
- subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
- }
+ void ResolveMatchStmt(Statement stmt, bool specContextOnly, ICodeContext codeContext) {
+ MatchStmt s = (MatchStmt)stmt;
+ DesugarMatchStmtWithTupleExpression(s);
+
+ bool bodyIsSpecOnly = specContextOnly;
+ int prevErrorCount = ErrorCount;
+ ResolveExpression(s.Source, new ResolveOpts(codeContext, true, specContextOnly));
+ Contract.Assert(s.Source.Type != null); // follows from postcondition of ResolveExpression
+ bool successfullyResolved = ErrorCount == prevErrorCount;
+ if (!specContextOnly && successfullyResolved) {
+ bodyIsSpecOnly = UsesSpecFeatures(s.Source);
+ }
+ UserDefinedType sourceType = null;
+ DatatypeDecl dtd = null;
+ if (s.Source.Type.IsDatatype) {
+ sourceType = (UserDefinedType)s.Source.Type.NormalizeExpand();
+ dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);
+ }
+ var subst = new Dictionary<TypeParameter, Type>();
+ Dictionary<string, DatatypeCtor> ctors;
+ if (dtd == null) {
+ Error(s.Source, "the type of the match source expression must be a datatype (instead found {0})", s.Source.Type);
+ ctors = null;
+ } else {
+ Contract.Assert(sourceType != null); // dtd and sourceType are set together above
+ ctors = datatypeCtors[dtd];
+ Contract.Assert(ctors != null); // dtd should have been inserted into datatypeCtors during a previous resolution stage
+
+ // build the type-parameter substitution map for this use of the datatype
+ for (int i = 0; i < dtd.TypeArgs.Count; i++) {
+ subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
}
- s.IsGhost = bodyIsSpecOnly;
+ }
+ s.IsGhost = bodyIsSpecOnly;
- ISet<string> memberNamesUsed = new HashSet<string>();
- foreach (MatchCaseStmt mc in s.Cases) {
- DatatypeCtor ctor = null;
- if (ctors != null) {
- Contract.Assert(dtd != null);
- if (!ctors.TryGetValue(mc.Id, out ctor)) {
- Error(mc.tok, "member {0} does not exist in datatype {1}", mc.Id, dtd.Name);
+ // convert CasePattern in MatchCaseExpr to BoundVar and flatten the MatchCaseExpr.
+ Type type = new InferredTypeProxy();
+ string name = FreshTempVarName("_mc#", codeContext);
+ BoundVar bv = new BoundVar(s.Tok, name, type);
+ List<CasePattern> patternSubst = new List<CasePattern>();
+ DesugarMatchCaseStmt(s, dtd, bv, patternSubst);
+
+ ISet<string> memberNamesUsed = new HashSet<string>();
+ foreach (MatchCaseStmt mc in s.Cases) {
+ DatatypeCtor ctor = null;
+ if (ctors != null) {
+ Contract.Assert(dtd != null);
+ if (!ctors.TryGetValue(mc.Id, out ctor)) {
+ Error(mc.tok, "member {0} does not exist in datatype {1}", mc.Id, dtd.Name);
+ } else {
+ Contract.Assert(ctor != null); // follows from postcondition of TryGetValue
+ mc.Ctor = ctor;
+ if (ctor.Formals.Count != mc.Arguments.Count) {
+ Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.Arguments.Count, ctor.Formals.Count);
+ }
+ if (memberNamesUsed.Contains(mc.Id)) {
+ Error(mc.tok, "member {0} appears in more than one case", mc.Id);
} else {
- Contract.Assert(ctor != null); // follows from postcondition of TryGetValue
- mc.Ctor = ctor;
- if (ctor.Formals.Count != mc.Arguments.Count) {
- Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.Arguments.Count, ctor.Formals.Count);
- }
- if (memberNamesUsed.Contains(mc.Id)) {
- Error(mc.tok, "member {0} appears in more than one case", mc.Id);
- } else {
- memberNamesUsed.Add(mc.Id); // add mc.Id to the set of names used
- }
+ memberNamesUsed.Add(mc.Id); // add mc.Id to the set of names used
}
}
- scope.PushMarker();
- int i = 0;
- foreach (BoundVar v in mc.Arguments) {
- if (!scope.Push(v.Name, v)) {
- Error(v, "Duplicate parameter name: {0}", v.Name);
- }
- ResolveType(v.tok, v.Type, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
- if (ctor != null && i < ctor.Formals.Count) {
- Formal formal = ctor.Formals[i];
- Type st = SubstType(formal.Type, subst);
- if (!UnifyTypes(v.Type, st)) {
- Error(stmt, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
- }
- v.IsGhost = formal.IsGhost;
+ }
+ scope.PushMarker();
+ int i = 0;
+ foreach (BoundVar v in mc.Arguments) {
+ if (!scope.Push(v.Name, v)) {
+ Error(v, "Duplicate parameter name: {0}", v.Name);
+ }
+ ResolveType(v.tok, v.Type, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
+ if (ctor != null && i < ctor.Formals.Count) {
+ Formal formal = ctor.Formals[i];
+ Type st = SubstType(formal.Type, subst);
+ if (!UnifyTypes(v.Type, st)) {
+ Error(stmt, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
}
- i++;
+ v.IsGhost = formal.IsGhost;
}
+ i++;
+ }
+ foreach (Statement ss in mc.Body) {
+ ResolveStatement(ss, bodyIsSpecOnly, codeContext);
+ }
+ // substitute body to replace the case pat with v. This needs to happen
+ // after the body is resolved so we can scope the bv correctly.
+ if (patternSubst.Count > 0) {
+ MatchCaseExprSubstituteCloner cloner = new MatchCaseExprSubstituteCloner(patternSubst, bv);
+ List<Statement> list = new List<Statement>();
foreach (Statement ss in mc.Body) {
- ResolveStatement(ss, bodyIsSpecOnly, codeContext);
+ Statement clone = cloner.CloneStmt(ss);
+ // resolve it again since we just cloned it.
+ ResolveStatement(clone, bodyIsSpecOnly, codeContext);
+ list.Add(clone);
+ }
+ mc.UpdateBody(list);
+ }
+
+ scope.PopMarker();
+ }
+ if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) {
+ // We could complain about the syntactic omission of constructors:
+ // Error(stmt, "match statement does not cover all constructors");
+ // but instead we let the verifier do a semantic check.
+ // So, for now, record the missing constructors:
+ foreach (var ctr in dtd.Ctors) {
+ if (!memberNamesUsed.Contains(ctr.Name)) {
+ s.MissingCases.Add(ctr);
+ }
+ }
+ Contract.Assert(memberNamesUsed.Count + s.MissingCases.Count == dtd.Ctors.Count);
+ }
+ if (!s.IsGhost) {
+ s.IsGhost = s.Cases.All(cs => cs.Body.All(ss => ss.IsGhost));
+ }
+ }
+
+ /*
+ * Convert
+ * match (x, y)
+ * case (Zero, _) => Zero
+ * case (Suc(_), Zero) => x
+ * case (Suc(a), Suc(b)) => minus(a, b)
+ * To:
+ * match x
+ * case Zero => match y
+ * case _ => zero
+ * case Suc(_) => match y
+ * case Zero => x
+ * case Suc(a) => match y
+ * case (b) => minus(a,b)
+ */
+ void DesugarMatchStmtWithTupleExpression(MatchStmt me) {
+ // (x, y) is treated as a 2-tuple constructor
+ if (me.Source is DatatypeValue) {
+ var e = (DatatypeValue)me.Source;
+ Contract.Assert(e.Arguments.Count >= 1);
+ Expression source = e.Arguments[0];
+ List<MatchCaseStmt> cases = new List<MatchCaseStmt>();
+ foreach (MatchCaseStmt mc in me.Cases) {
+ Contract.Assert(mc.CasePatterns != null);
+ Contract.Assert(mc.CasePatterns.Count == e.Arguments.Count);
+ CasePattern cp = mc.CasePatterns[0];
+ List<CasePattern> patterns;
+ if (cp.Arguments != null) {
+ patterns = cp.Arguments;
+ } else {
+ patterns = new List<CasePattern>();
+ }
+
+ List<Statement> body = mc.Body;
+ for (int i = e.Arguments.Count; 1 <= --i; ) {
+ // others go into the body
+ body = CreateMatchCaseStmtBody(mc.tok, e.Arguments[i], mc.CasePatterns[i], body);
}
- scope.PopMarker();
+ cases.Add(new MatchCaseStmt(cp.tok, cp.Id, patterns, body));
+ }
+ me.UpdateSource(source);
+ me.UpdateCases(cases);
+ }
+ }
+
+ List<Statement> CreateMatchCaseStmtBody(Boogie.IToken tok, Expression source, CasePattern cp, List<Statement> body) {
+ List<MatchCaseStmt> cases = new List<MatchCaseStmt>();
+ List<CasePattern> patterns;
+ if (cp.Var != null) {
+ var bv = cp.Var;
+ if (LocalVariable.HasWildcardName(bv)) {
+ return body;
+ } else {
+ patterns = new List<CasePattern>();
}
- if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) {
- // We could complain about the syntactic omission of constructors:
- // Error(stmt, "match statement does not cover all constructors");
- // but instead we let the verifier do a semantic check.
- // So, for now, record the missing constructors:
- foreach (var ctr in dtd.Ctors) {
- if (!memberNamesUsed.Contains(ctr.Name)) {
- s.MissingCases.Add(ctr);
+ } else {
+ patterns = cp.Arguments;
+ }
+ cases.Add(new MatchCaseStmt(cp.tok, cp.Id, patterns, body));
+ List<Statement> list = new List<Statement>();
+ // endTok??
+ list.Add(new MatchStmt(tok, tok, source, cases, false));
+ return list;
+ }
+
+
+ /*
+ * Convert
+ * match xs
+ * case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
+ * case Cons(y, Nil) => y
+ * To
+ * match xs
+ * case Cons(y, ys) => match ys
+ * case Nil => y
+ * case Cons(z, zs) => last(ys)
+ */
+ void DesugarMatchCaseStmt(MatchStmt s, DatatypeDecl dtd, BoundVar sourceVar, List<CasePattern> patterns) {
+ Contract.Assert(dtd != null);
+ Dictionary<string, DatatypeCtor> ctors = datatypeCtors[dtd];
+ foreach (MatchCaseStmt mc in s.Cases) {
+ if (mc.Arguments != null) {
+ // already desugared. This happens during the second pass resolver after cloning.
+ Contract.Assert(mc.CasePatterns == null);
+ return;
+ }
+
+ Contract.Assert(mc.Arguments == null);
+ Contract.Assert(mc.CasePatterns != null);
+ DatatypeCtor ctor = null;
+ if (ctors != null) {
+ if (!ctors.TryGetValue(mc.Id, out ctor)) {
+ Error(mc.tok, "member {0} does not exist in datatype {1}", mc.Id, dtd.Name);
+ } else {
+ Contract.Assert(ctor != null); // follows from postcondition of TryGetValue
+ mc.Ctor = ctor;
+ if (ctor.Formals.Count != mc.CasePatterns.Count) {
+ Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.Arguments.Count, ctor.Formals.Count);
}
}
- Contract.Assert(memberNamesUsed.Count + s.MissingCases.Count == dtd.Ctors.Count);
}
- if (!s.IsGhost) {
- s.IsGhost = s.Cases.All(cs => cs.Body.All(ss => ss.IsGhost));
+ scope.PushMarker();
+ List<BoundVar> arguments = new List<BoundVar>();
+ foreach (CasePattern pat in mc.CasePatterns) {
+ // Find the constructor in the given datatype
+ // If what was parsed was just an identifier, we will interpret it as a datatype constructor, if possible
+ ctor = null;
+ if (pat.Var == null || (pat.Var != null && pat.Var.Type is TypeProxy && dtd != null)) {
+ if (datatypeCtors[dtd].TryGetValue(pat.Id, out ctor)) {
+ pat.Ctor = ctor;
+ pat.Var = null;
+ }
+ }
+ if (pat.Var != null) {
+ BoundVar v = pat.Var;
+ arguments.Add(v);
+ if (!scope.Push(v.Name, v)) {
+ Error(v, "Duplicate name: {0}", v.Name);
+ }
+ } else {
+ DesugarMatchCasePattern(mc, pat, sourceVar);
+ patterns.Add(pat);
+ arguments.Add(sourceVar);
+ }
}
+ mc.Arguments = arguments;
+ mc.CasePatterns = null;
+ scope.PopMarker();
+ }
- } else if (stmt is SkeletonStatement) {
- var s = (SkeletonStatement)stmt;
- Error(s.Tok, "skeleton statements are allowed only in refining methods");
- // nevertheless, resolve the underlying statement; hey, why not
- if (s.S != null) {
- ResolveStatement(s.S, specContextOnly, codeContext);
+ List<MatchCaseStmt> newCases = new List<MatchCaseStmt>();
+
+ // need to consolidate the cases.
+ // Convert
+ // match xs
+ // case Cons(y, #mc#0) => match #mc#0
+ // case Cons((z, zs) => body
+ // case Cons(y, #mc#0) => match #mc#0
+ // case Nil => y
+ // into
+ // match xs
+ // case Cons(y, #mc#0) => match #mc#0
+ // case Cons((z, zs) => body
+ // case Nil => y
+ bool thingsChanged = false;
+ Dictionary<string, MatchCaseStmt> caseMap = new Dictionary<string, MatchCaseStmt>();
+ List<MatchCaseStmt> mcWithWildCard = new List<MatchCaseStmt>();
+ foreach (MatchCaseStmt mc in s.Cases) {
+ // check each CasePattern to see if it has wildcard.
+ if (CaseExprHasWildCard(mc)) {
+ mcWithWildCard.Add(mc);
+ } else {
+ thingsChanged |= CombineMatchCaseStmt(mc, newCases, caseMap);
+ }
+ }
+
+ foreach (MatchCaseStmt mc in mcWithWildCard) {
+ // now process with cases with wildcard
+ thingsChanged |= CombineMatchCaseStmt(mc, newCases, caseMap);
+ }
+
+ if (thingsChanged) {
+ s.UpdateCases(newCases);
+ }
+ }
+
+ void DesugarMatchCasePattern(MatchCaseStmt mc, CasePattern pat, BoundVar v) {
+ // convert
+ // case Cons(y, Cons(z, zs)) => body
+ // to
+ // case Cons(y, #mc#) => match #mc#
+ // case Cons(z, zs) => body
+
+ Expression source = new NameSegment(pat.tok, v.Name, null);
+ List<MatchCaseStmt> cases = new List<MatchCaseStmt>();
+ cases.Add(new MatchCaseStmt(pat.tok, pat.Id, pat.Arguments == null ? new List<CasePattern>() : pat.Arguments, mc.Body));
+ List<Statement> list = new List<Statement>();
+ // endTok??
+ list.Add(new MatchStmt(pat.tok, pat.tok, source, cases, false));
+ mc.UpdateBody(list);
+ }
+
+ bool CombineMatchCaseStmt(MatchCaseStmt mc, List<MatchCaseStmt> newCases, Dictionary<string, MatchCaseStmt> caseMap) {
+ bool thingsChanged = false;
+ MatchCaseStmt old_mc;
+ if (caseMap.TryGetValue(mc.Id, out old_mc)) {
+ // already has a case with the same ctor, try to consolidate the body.
+ List<Statement> oldBody = old_mc.Body;
+ List<Statement> body = mc.Body;
+ if ((oldBody.Count == 1) && (oldBody[0] is MatchStmt)
+ && (body.Count == 1) && (body[0] is MatchStmt)) {
+ // both only have on statement and the statement is MatchStmt
+ MatchStmt old = (MatchStmt) oldBody[0];
+ MatchStmt current = (MatchStmt) body[0];
+ if (SameMatchCase(old_mc, mc)) {
+ foreach (MatchCaseStmt c in current.Cases) {
+ old.Cases.Add(c);
+ }
+ thingsChanged = true;
+ }
+ } else {
+ // duplicate cases, do nothing for now. The error will be reported during resolving
}
} else {
- Contract.Assert(false); throw new cce.UnreachableException();
+ // it is a new case.
+ newCases.Add(mc);
+ caseMap.Add(mc.Id, mc);
+ }
+ return thingsChanged;
+ }
+
+ bool SameMatchCase(MatchCaseStmt one, MatchCaseStmt other) {
+ // this method is called after all the CasePattern in the match cases are converted
+ // into BoundVars.
+ Contract.Assert(one.CasePatterns == null && one.Arguments != null);
+ Contract.Assert(other.CasePatterns == null && other.Arguments != null);
+ // In order to combine the two match cases, the bodies need to be a MatchExpr and
+ // the arguments and the source of the body are the same.
+ // We do string equals since they should be in the same scope.
+ if (one.Arguments.Count != other.Arguments.Count) {
+ return false;
+ }
+ List<Statement> body1 = one.Body;
+ List<Statement> body2 = other.Body;
+ if ((body1.Count != 1) || (body2.Count != 1)) {
+ return false;
+ }
+ if (!(body1[0] is MatchStmt) || !(body2[0] is MatchStmt)) {
+ return false;
+ }
+ var source1 = ((MatchStmt)body1[0]).Source;
+ var source2 = ((MatchStmt)body2[0]).Source;
+ if (!(source1 is NameSegment) || !(source2 is NameSegment)) {
+ return false;
}
+ if (!((NameSegment)source1).Name.Equals(((NameSegment)source2).Name)) {
+ return false;
+ }
+ for (int i = 0; i < one.Arguments.Count; i++) {
+ BoundVar bv1 = one.Arguments[i];
+ BoundVar bv2 = other.Arguments[i];
+ if (!LocalVariable.HasWildcardName(bv1) && !LocalVariable.HasWildcardName(bv2) &&
+ !bv1.Name.Equals(bv2.Name)) {
+ return false;
+ }
+ }
+ return true;
}
void FillInDefaultLoopDecreases(LoopStmt loopStmt, Expression guard, List<Expression> theDecreases, ICallable enclosingMethod) {
@@ -7324,99 +7599,365 @@ namespace Microsoft.Dafny }
} else if (expr is MatchExpr) {
- var me = (MatchExpr)expr;
- ResolveExpression(me.Source, opts);
- Contract.Assert(me.Source.Type != null); // follows from postcondition of ResolveExpression
- UserDefinedType sourceType = null;
- DatatypeDecl dtd = null;
- if (me.Source.Type.IsDatatype) {
- sourceType = (UserDefinedType)me.Source.Type.NormalizeExpand();
- dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);
- }
- var subst = new Dictionary<TypeParameter, Type>();
- Dictionary<string, DatatypeCtor> ctors;
- if (dtd == null) {
- Error(me.Source, "the type of the match source expression must be a datatype (instead found {0})", me.Source.Type);
- ctors = null;
- } else {
- Contract.Assert(sourceType != null); // dtd and sourceType are set together above
- ctors = datatypeCtors[dtd];
- Contract.Assert(ctors != null); // dtd should have been inserted into datatypeCtors during a previous resolution stage
+ ResolveMatchExpr(expr, opts);
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
+ }
- // build the type-parameter substitution map for this use of the datatype
- for (int i = 0; i < dtd.TypeArgs.Count; i++) {
- subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
- }
+ if (expr.Type == null) {
+ // some resolution error occurred
+ expr.Type = new InferredTypeProxy();
+ }
+ }
+
+ void ResolveMatchExpr(Expression expr, ResolveOpts opts) {
+ var me = (MatchExpr)expr;
+ DesugarMatchExprWithTupleExpression(me);
+
+ ResolveExpression(me.Source, opts);
+ Contract.Assert(me.Source.Type != null); // follows from postcondition of ResolveExpression
+ UserDefinedType sourceType = null;
+ DatatypeDecl dtd = null;
+ if (me.Source.Type.IsDatatype) {
+ sourceType = (UserDefinedType)me.Source.Type.NormalizeExpand();
+ dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);
+ }
+ var subst = new Dictionary<TypeParameter, Type>();
+ Dictionary<string, DatatypeCtor> ctors;
+ if (dtd == null) {
+ Error(me.Source, "the type of the match source expression must be a datatype (instead found {0})", me.Source.Type);
+ ctors = null;
+ } else {
+ Contract.Assert(sourceType != null); // dtd and sourceType are set together above
+ ctors = datatypeCtors[dtd];
+ Contract.Assert(ctors != null); // dtd should have been inserted into datatypeCtors during a previous resolution stage
+
+ // build the type-parameter substitution map for this use of the datatype
+ for (int i = 0; i < dtd.TypeArgs.Count; i++) {
+ subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
}
+ }
- ISet<string> memberNamesUsed = new HashSet<string>();
- expr.Type = new InferredTypeProxy();
- foreach (MatchCaseExpr mc in me.Cases) {
- DatatypeCtor ctor = null;
- if (ctors != null) {
- Contract.Assert(dtd != null);
- if (!ctors.TryGetValue(mc.Id, out ctor)) {
- Error(mc.tok, "member {0} does not exist in datatype {1}", mc.Id, dtd.Name);
+ // convert CasePattern in MatchCaseExpr to BoundVar and flatten the MatchCaseExpr.
+ Type type = new InferredTypeProxy();
+ string name = FreshTempVarName("_mc#", opts.codeContext);
+ BoundVar bv = new BoundVar(me.tok, name, type);
+ List<CasePattern> patternSubst = new List<CasePattern>();
+ DesugarMatchCaseExpr(me, dtd, bv, patternSubst);
+
+ ISet<string> memberNamesUsed = new HashSet<string>();
+ expr.Type = new InferredTypeProxy();
+ foreach (MatchCaseExpr mc in me.Cases) {
+ DatatypeCtor ctor = null;
+ if (ctors != null) {
+ Contract.Assert(dtd != null);
+ if (!ctors.TryGetValue(mc.Id, out ctor)) {
+ Error(mc.tok, "member {0} does not exist in datatype {1}", mc.Id, dtd.Name);
+ } else {
+ Contract.Assert(ctor != null); // follows from postcondition of TryGetValue
+ mc.Ctor = ctor;
+ if (ctor.Formals.Count != mc.Arguments.Count) {
+ Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.Arguments.Count, ctor.Formals.Count);
+ }
+ if (memberNamesUsed.Contains(mc.Id)) {
+ Error(mc.tok, "member {0} appears in more than one case", mc.Id);
} else {
- Contract.Assert(ctor != null); // follows from postcondition of TryGetValue
- mc.Ctor = ctor;
- if (ctor.Formals.Count != mc.Arguments.Count) {
- Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.Arguments.Count, ctor.Formals.Count);
- }
- if (memberNamesUsed.Contains(mc.Id)) {
- Error(mc.tok, "member {0} appears in more than one case", mc.Id);
- } else {
- memberNamesUsed.Add(mc.Id); // add mc.Id to the set of names used
- }
+ memberNamesUsed.Add(mc.Id); // add mc.Id to the set of names used
}
}
- scope.PushMarker();
- int i = 0;
- foreach (BoundVar v in mc.Arguments) {
- if (!scope.Push(v.Name, v)) {
- Error(v, "Duplicate parameter name: {0}", v.Name);
- }
- ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
- if (ctor != null && i < ctor.Formals.Count) {
- Formal formal = ctor.Formals[i];
- Type st = SubstType(formal.Type, subst);
- if (!UnifyTypes(v.Type, st)) {
- Error(expr, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
- }
- v.IsGhost = formal.IsGhost;
+ }
+ scope.PushMarker();
+ int i = 0;
+ foreach (BoundVar v in mc.Arguments) {
+ if (!scope.Push(v.Name, v)) {
+ Error(v, "Duplicate parameter name: {0}", v.Name);
+ }
+ ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
+ if (ctor != null && i < ctor.Formals.Count) {
+ Formal formal = ctor.Formals[i];
+ Type st = SubstType(formal.Type, subst);
+ if (!UnifyTypes(v.Type, st)) {
+ Error(expr, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
}
- i++;
+ v.IsGhost = formal.IsGhost;
}
+ i++;
+ }
+ ResolveExpression(mc.Body, opts);
+ // substitute body to replace the case pat with v. This needs to happen
+ // after the body is resolved so we can scope the bv correctly.
+ if (patternSubst.Count > 0) {
+ MatchCaseExprSubstituteCloner cloner = new MatchCaseExprSubstituteCloner(patternSubst, bv);
+ mc.UpdateBody(cloner.CloneExpr(mc.Body));
+ // resolve it again since we just cloned it.
ResolveExpression(mc.Body, opts);
- Contract.Assert(mc.Body.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(expr.Type, mc.Body.Type)) {
- Error(mc.Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", mc.Body.Type, expr.Type);
+ }
+
+ Contract.Assert(mc.Body.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(expr.Type, mc.Body.Type)) {
+ Error(mc.Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", mc.Body.Type, expr.Type);
+ }
+ scope.PopMarker();
+ }
+ if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) {
+ // We could complain about the syntactic omission of constructors:
+ // Error(expr, "match expression does not cover all constructors");
+ // but instead we let the verifier do a semantic check.
+ // So, for now, record the missing constructors:
+ foreach (var ctr in dtd.Ctors) {
+ if (!memberNamesUsed.Contains(ctr.Name)) {
+ me.MissingCases.Add(ctr);
+ }
+ }
+ Contract.Assert(memberNamesUsed.Count + me.MissingCases.Count == dtd.Ctors.Count);
+ }
+ }
+
+ /*
+ * Convert
+ * match (x, y)
+ * case (Zero, _) => Zero
+ * case (Suc(_), Zero) => x
+ * case (Suc(a), Suc(b)) => minus(a, b)
+ * To:
+ * match x
+ * case Zero => match y
+ * case _ => zero
+ * case Suc(_) => match y
+ * case Zero => x
+ * case Suc(a) => match y
+ * case (b) => minus(a,b)
+ */
+ private void DesugarMatchExprWithTupleExpression(MatchExpr me) {
+ // (x, y) is treated as a 2-tuple constructor
+ if (me.Source is DatatypeValue) {
+ var e = (DatatypeValue)me.Source;
+ Contract.Assert(e.Arguments.Count >= 1);
+ Expression source = e.Arguments[0];
+ List<MatchCaseExpr> cases = new List<MatchCaseExpr>();
+ foreach (MatchCaseExpr mc in me.Cases) {
+ Contract.Assert(mc.CasePatterns != null);
+ Contract.Assert(mc.CasePatterns.Count == e.Arguments.Count);
+ CasePattern cp = mc.CasePatterns[0];
+ List<CasePattern> patterns;
+ if (cp.Arguments != null) {
+ patterns = cp.Arguments;
+ } else {
+ patterns = new List<CasePattern>();
+ }
+
+ Expression body = mc.Body;
+ for (int i = e.Arguments.Count; 1 <= --i; ) {
+ // others go into the body
+ body = CreateMatchCaseExprBody(mc.tok, e.Arguments[i], mc.CasePatterns[i], body);
+ }
+ cases.Add(new MatchCaseExpr(cp.tok, cp.Id, patterns, body));
+ }
+ me.UpdateSource(source);
+ me.UpdateCases(cases);
+ }
+ }
+
+ Expression CreateMatchCaseExprBody(Boogie.IToken tok, Expression source, CasePattern cp, Expression body) {
+ List<MatchCaseExpr> cases = new List<MatchCaseExpr>();
+ List<CasePattern> patterns;
+ if (cp.Var != null) {
+ var bv = cp.Var;
+ if (LocalVariable.HasWildcardName(bv)) {
+ return body;
+ } else {
+ patterns = new List<CasePattern>();
+ }
+ } else {
+ patterns = cp.Arguments;
+ }
+ cases.Add(new MatchCaseExpr(cp.tok, cp.Id, patterns, body));
+ return new MatchExpr(tok, source, cases, false);
+ }
+
+ /*
+ * Convert
+ * match xs
+ * case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
+ * case Cons(y, Nil) => y
+ * To
+ * match xs
+ * case Cons(y, ys) => match ys
+ * case Nil => y
+ * case Cons(z, zs) => last(ys)
+ * */
+ void DesugarMatchCaseExpr(MatchExpr me, DatatypeDecl dtd, BoundVar sourceVar, List<CasePattern> patterns) {
+ Contract.Assert(dtd != null);
+ Dictionary<string, DatatypeCtor> ctors = datatypeCtors[dtd];
+ foreach (MatchCaseExpr mc in me.Cases) {
+ if (mc.Arguments != null) {
+ // already desugared. This happens during the second pass resolver after cloning.
+ Contract.Assert(mc.CasePatterns == null);
+ return;
+ }
+
+ Contract.Assert(mc.Arguments == null);
+ Contract.Assert(mc.CasePatterns != null);
+ DatatypeCtor ctor = null;
+ if (ctors != null) {
+ if (!ctors.TryGetValue(mc.Id, out ctor)) {
+ Error(mc.tok, "member {0} does not exist in datatype {1}", mc.Id, dtd.Name);
+ } else {
+ Contract.Assert(ctor != null); // follows from postcondition of TryGetValue
+ mc.Ctor = ctor;
+ if (ctor.Formals.Count != mc.CasePatterns.Count) {
+ Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.CasePatterns.Count, ctor.Formals.Count);
+ }
}
- scope.PopMarker();
}
- if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) {
- // We could complain about the syntactic omission of constructors:
- // Error(expr, "match expression does not cover all constructors");
- // but instead we let the verifier do a semantic check.
- // So, for now, record the missing constructors:
- foreach (var ctr in dtd.Ctors) {
- if (!memberNamesUsed.Contains(ctr.Name)) {
- me.MissingCases.Add(ctr);
+ scope.PushMarker();
+ List<BoundVar> arguments = new List<BoundVar>();
+ foreach (CasePattern pat in mc.CasePatterns) {
+ // Find the constructor in the given datatype
+ // If what was parsed was just an identifier, we will interpret it as a datatype constructor, if possible
+ ctor = null;
+ if (pat.Var == null || (pat.Var != null && pat.Var.Type is TypeProxy && dtd != null)) {
+ if (datatypeCtors[dtd].TryGetValue(pat.Id, out ctor)) {
+ pat.Ctor = ctor;
+ pat.Var = null;
+ }
+ }
+ if (pat.Var != null) {
+ BoundVar v = pat.Var;
+ arguments.Add(v);
+ if (!scope.Push(v.Name, v)) {
+ Error(v, "Duplicate name: {0}", v.Name);
}
+ } else {
+ DesugarMatchCasePattern(mc, pat, sourceVar);
+ patterns.Add(pat);
+ arguments.Add(sourceVar);
}
- Contract.Assert(memberNamesUsed.Count + me.MissingCases.Count == dtd.Ctors.Count);
}
- } else {
- Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
+ mc.Arguments = arguments;
+ mc.CasePatterns = null;
+ scope.PopMarker();
}
- if (expr.Type == null) {
- // some resolution error occurred
- expr.Type = new InferredTypeProxy();
+ List<MatchCaseExpr> newCases = new List<MatchCaseExpr>();
+
+ // need to consolidate the cases.
+ // Convert
+ // match xs
+ // case Cons(y, #mc#0) => match #mc#0
+ // case Cons((z, zs) => body
+ // case Cons(y, #mc#0) => match #mc#0
+ // case Nil => y
+ // into
+ // match xs
+ // case Cons(y, #mc#0) => match #mc#0
+ // case Cons((z, zs) => body
+ // case Nil => y
+ bool thingsChanged = false;
+ Dictionary<string, MatchCaseExpr> caseMap = new Dictionary<string, MatchCaseExpr>();
+ List<MatchCaseExpr> mcWithWildCard = new List<MatchCaseExpr>();
+ foreach (MatchCaseExpr mc in me.Cases) {
+ // check each CasePattern to see if it has wildcard.
+ if (CaseExprHasWildCard(mc)) {
+ mcWithWildCard.Add(mc);
+ } else {
+ thingsChanged |= CombineMatchCaseExpr(mc, newCases, caseMap);
+ }
+ }
+
+ foreach (MatchCaseExpr mc in mcWithWildCard) {
+ // now process with cases with wildcard
+ thingsChanged |= CombineMatchCaseExpr(mc, newCases, caseMap);
+ }
+
+ if (thingsChanged) {
+ me.UpdateCases(newCases);
}
}
+ void DesugarMatchCasePattern(MatchCaseExpr mc, CasePattern pat, BoundVar v) {
+ // convert
+ // case Cons(y, Cons(z, zs)) => body
+ // to
+ // case Cons(y, #mc#) => match #mc#
+ // case Cons(z, zs) => body
+
+ Expression source = new NameSegment(pat.tok, v.Name, null);
+ List<MatchCaseExpr> cases = new List<MatchCaseExpr>();
+ cases.Add(new MatchCaseExpr(pat.tok, pat.Id, pat.Arguments == null ? new List<CasePattern>() : pat.Arguments, mc.Body));
+ MatchExpr e = new MatchExpr(pat.tok, source, cases, false);
+ mc.UpdateBody(e);
+ }
+
+
+ bool CaseExprHasWildCard(MatchCase mc) {
+ foreach (BoundVar bv in mc.Arguments) {
+ if (LocalVariable.HasWildcardName(bv)) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ bool CombineMatchCaseExpr(MatchCaseExpr mc, List<MatchCaseExpr> newCases, Dictionary<string, MatchCaseExpr> caseMap) {
+ bool thingsChanged = false;
+ MatchCaseExpr old_mc;
+ if (caseMap.TryGetValue(mc.Id, out old_mc)) {
+ // already has a case with the same ctor, try to consolidate the body.
+ Expression oldBody = old_mc.Body;
+ Expression body = mc.Body;
+ if (SameMatchCase(old_mc, mc)) {
+ MatchExpr old = (MatchExpr)oldBody;
+ MatchExpr current = (MatchExpr)body;
+ foreach (MatchCaseExpr c in current.Cases) {
+ old.Cases.Add(c);
+ }
+ thingsChanged = true;
+ } else {
+ // duplicate cases, do nothing for now. The error will be reported during resolving
+ }
+ } else {
+ // it is a new case.
+ newCases.Add(mc);
+ caseMap.Add(mc.Id, mc);
+ }
+ return thingsChanged;
+ }
+
+ bool SameMatchCase(MatchCaseExpr one, MatchCaseExpr other) {
+ // this method is called after all the CasePattern in the match cases are converted
+ // into BoundVars.
+ Contract.Assert(one.CasePatterns == null && one.Arguments != null);
+ Contract.Assert(other.CasePatterns == null && other.Arguments != null);
+ // In order to combine the two match cases, the bodies need to be a MatchExpr and
+ // the arguments and the source of the body are the same.
+ // We do string equals since they should be in the same scope.
+ if (one.Arguments.Count != other.Arguments.Count) {
+ return false;
+ }
+ if (!(one.Body is MatchExpr) || !(other.Body is MatchExpr)) {
+ return false;
+ }
+ var source1 = ((MatchExpr)one.Body).Source;
+ var source2 = ((MatchExpr)other.Body).Source;
+ if (!(source1 is NameSegment) || !(source2 is NameSegment)) {
+ return false;
+ }
+ if (!((NameSegment)source1).Name.Equals(((NameSegment)source2).Name)) {
+ return false;
+ }
+ for (int i = 0; i < one.Arguments.Count; i++) {
+ BoundVar bv1 = one.Arguments[i];
+ BoundVar bv2 = other.Arguments[i];
+ if (!LocalVariable.HasWildcardName(bv1) && !LocalVariable.HasWildcardName(bv2) &&
+ !bv1.Name.Equals(bv2.Name)) {
+ return false;
+ }
+ }
+ return true;
+ }
+
void ResolveCasePattern(CasePattern pat, Type sourceType, ICodeContext context) {
Contract.Requires(pat != null);
Contract.Requires(sourceType != null);
@@ -7463,13 +8004,15 @@ namespace Microsoft.Dafny }
// recursively call ResolveCasePattern on each of the arguments
var j = 0;
- foreach (var arg in pat.Arguments) {
- if (j < ctor.Formals.Count) {
- var formal = ctor.Formals[j];
- Type st = SubstType(formal.Type, subst);
- ResolveCasePattern(arg, st, context);
+ if (pat.Arguments != null) {
+ foreach (var arg in pat.Arguments) {
+ if (j < ctor.Formals.Count) {
+ var formal = ctor.Formals[j];
+ Type st = SubstType(formal.Type, subst);
+ ResolveCasePattern(arg, st, context);
+ }
+ j++;
}
- j++;
}
if (j == ctor.Formals.Count) {
pat.AssembleExpr(udt.TypeArgs);
@@ -9009,8 +9552,10 @@ namespace Microsoft.Dafny var s = FreeVariables(e.Source);
foreach (MatchCaseExpr mc in e.Cases) {
var t = FreeVariables(mc.Body);
- foreach (var bv in mc.Arguments) {
- t.Remove(bv);
+ foreach (var cp in mc.CasePatterns) {
+ foreach (var bv in cp.Vars) {
+ t.Remove(bv);
+ }
}
s.UnionWith(t);
}
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 72649b5f..1361ad85 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -1118,6 +1118,58 @@ namespace Microsoft.Dafny }
}
+
+
+ class MatchCaseExprSubstituteCloner : Cloner
+ {
+ private List<CasePattern> patternSubst;
+ private BoundVar var;
+
+ // the cloner is called after resolving the body of matchexpr, trying
+ // to replace casepattern in the body that has been replaced by bv
+ public MatchCaseExprSubstituteCloner(List<CasePattern> subst, BoundVar var) {
+ this.patternSubst = subst;
+ this.var = var;
+ }
+
+ public override Expression CloneApplySuffix(ApplySuffix e) {
+ // if the ApplySuffix matches the CasePattern, then replace it with the BoundVar.
+ if (FindMatchingPattern(e)) {
+ return new NameSegment(e.tok, this.var.Name, null);
+ } else {
+ return new ApplySuffix(Tok(e.tok), CloneExpr(e.Lhs), e.Args.ConvertAll(CloneExpr));
+ }
+ }
+
+ private bool FindMatchingPattern(ApplySuffix e) {
+ Expression lhs = e.Lhs;
+ if (!(lhs is NameSegment)) {
+ return false;
+ }
+ string applyName = ((NameSegment)lhs).Name;
+ foreach (CasePattern cp in patternSubst) {
+ string ctorName = cp.Id;
+ if (!(applyName.Equals(ctorName)) || (e.Args.Count != cp.Arguments.Count)) {
+ continue;
+ }
+ bool found = true;
+ for (int i = 0; i < e.Args.Count; i++) {
+ var arg1 = e.Args[i];
+ var arg2 = cp.Arguments[i];
+ if (arg1.Resolved is IdentifierExpr) {
+ var bv1 = ((IdentifierExpr)arg1.Resolved).Var;
+ if (bv1 != arg2.Var) {
+ found = false;
+ }
+ }
+ }
+ if (found) {
+ return true;
+ }
+ }
+ return false;
+ }
+ }
}
diff --git a/Test/dafny0/NestedMatch.dfy b/Test/dafny0/NestedMatch.dfy new file mode 100644 index 00000000..e6e7c489 --- /dev/null +++ b/Test/dafny0/NestedMatch.dfy @@ -0,0 +1,59 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Nat = Zero | Suc(Nat)
+
+predicate Even(n: Nat)
+{
+ match n
+ case Zero => true
+ case Suc(Zero) => false
+ case Suc(Suc(p)) => Even(p)
+}
+
+
+method checkEven(n: Nat) {
+ assert Even(Zero) == true;
+ assert Even(Suc(Zero)) == false;
+ assert Even(Suc(Suc(n))) == Even(n);
+}
+
+datatype List<T> = Nil | Cons(T, List<T>)
+
+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))
+}
+
+method checkLast(y: T) {
+ assert last(Cons(y, Nil)) == y;
+ assert last(Cons(y, Cons(y, Nil))) == last(Cons(y, Nil));
+}
+
+
+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)
+}
+
+method checkMinus(x:Nat, y: Nat) {
+ assert minus(Suc(x), Suc(y)) == minus(x,y);
+}
+
+
+// nested match statement
+method Last<T>(xs: List<T>) returns (x: T)
+ requires xs != Nil
+{
+
+ match xs {
+ case Cons(y, Nil) => x:= y;
+ case Cons(y, Cons(z, zs)) => x:=Last(Cons(z, zs));
+ }
+}
diff --git a/Test/dafny0/NestedMatch.dfy.expect b/Test/dafny0/NestedMatch.dfy.expect new file mode 100644 index 00000000..f3a9c95f --- /dev/null +++ b/Test/dafny0/NestedMatch.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 11 verified, 0 errors
|