diff options
| -rw-r--r-- | Source/Dafny/Dafny.atg | 15 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 126 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 25 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 25 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 141 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 44 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy | 53 |
8 files changed, 320 insertions, 115 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index c4955a6a..0d815bf4 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -666,6 +666,9 @@ MatchExpression<out Expression/*!*/ e> .)
"match" (. x = t; .)
Expression<out e>
+ /* Note: The following gives rise to a '"case" is start & successor of deletable structure' error,
+ but it's okay, because we want this closer match expression to bind as much as possible--use
+ parens around it to limit its scope. */
{ CaseExpression<out c> (. cases.Add(c); .)
}
(. e = new MatchExpr(x, e, cases); .)
@@ -686,10 +689,20 @@ CaseExpression<out MatchCaseExpr/*!*/ c> }
")" ]
"=>"
- Expression<out body> (. c = new MatchCaseExpr(x, id.val, arguments, body);
+ MatchOrExpr<out body> (. c = new MatchCaseExpr(x, id.val, arguments, body);
parseVarScope.PopMarker(); .)
.
+/* Note, '(' is start of more than one alternative in MatchOrExpr, but the first intentionally hides
+ the third alternative in this regard, in order to also allow match expressions to be parenthesized. */
+MatchOrExpr<out Expression/*!*/ e>
+= (. e = dummyExpr; .)
+ ( "(" MatchOrExpr<out e> ")"
+ | MatchExpression<out e>
+ | Expression<out e>
+ )
+ .
+
/*------------------------------------------------------------------------*/
BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 290609fc..d49c78c6 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -977,11 +977,24 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(31);
}
Expect(43);
- Expression(out body);
+ MatchOrExpr(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
parseVarScope.PopMarker();
}
+ void MatchOrExpr(out Expression/*!*/ e) {
+ e = dummyExpr;
+ if (la.kind == 30) {
+ Get();
+ MatchOrExpr(out e);
+ Expect(31);
+ } else if (la.kind == 41) {
+ MatchExpression(out e);
+ } else if (StartOf(9)) {
+ Expression(out e);
+ } else SynErr(118);
+ }
+
void Stmt(List<Statement/*!*/>/*!*/ ss) {
Contract.Requires(cce.NonNullElements(ss)); Statement/*!*/ s;
IToken bodyStart, bodyEnd;
@@ -995,7 +1008,7 @@ List<Expression/*!*/>/*!*/ decreases) { ss.Add(s);
} else if (la.kind == 11 || la.kind == 16) {
VarDeclStmts(ss);
- } else SynErr(118);
+ } else SynErr(119);
}
void OneStmt(out Statement/*!*/ s) {
@@ -1073,7 +1086,7 @@ List<Expression/*!*/>/*!*/ decreases) { s = new ReturnStmt(x);
break;
}
- default: SynErr(119); break;
+ default: SynErr(120); break;
}
}
@@ -1246,7 +1259,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(120);
+ } else SynErr(121);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -1354,7 +1367,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 51) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else SynErr(121);
+ } else SynErr(122);
Expect(8);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1393,7 +1406,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(9)) {
Expression(out e);
ee = new List<Expression>(); ee.Add(e);
- } else SynErr(122);
+ } else SynErr(123);
if (ee == null && ty == null) { ee = new List<Expression>(); ee.Add(dummyExpr); }
}
@@ -1403,7 +1416,7 @@ List<Expression/*!*/>/*!*/ decreases) { IdentOrFuncExpression(out e);
} else if (la.kind == 30 || la.kind == 96 || la.kind == 97) {
ObjectExpression(out e);
- } else SynErr(123);
+ } else SynErr(124);
while (la.kind == 49 || la.kind == 92) {
SelectOrCallSuffix(ref e);
}
@@ -1449,7 +1462,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(9)) {
Expression(out ee);
e = ee;
- } else SynErr(124);
+ } else SynErr(125);
Expect(31);
}
@@ -1492,7 +1505,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 30 || la.kind == 96 || la.kind == 97) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else SynErr(125);
+ } else SynErr(126);
while (la.kind == 49 || la.kind == 92) {
SelectOrCallSuffix(ref e);
}
@@ -1506,7 +1519,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(9)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else SynErr(126);
+ } else SynErr(127);
}
void EquivExpression(out Expression/*!*/ e0) {
@@ -1536,7 +1549,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 66) {
Get();
- } else SynErr(127);
+ } else SynErr(128);
}
void LogicalExpression(out Expression/*!*/ e0) {
@@ -1574,7 +1587,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 68) {
Get();
- } else SynErr(128);
+ } else SynErr(129);
}
void RelationalExpression(out Expression/*!*/ e0) {
@@ -1592,7 +1605,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 70) {
Get();
- } else SynErr(129);
+ } else SynErr(130);
}
void OrOp() {
@@ -1600,7 +1613,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 72) {
Get();
- } else SynErr(130);
+ } else SynErr(131);
}
void Term(out Expression/*!*/ e0) {
@@ -1676,7 +1689,7 @@ List<Expression/*!*/>/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(131); break;
+ default: SynErr(132); break;
}
}
@@ -1698,7 +1711,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 83) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(132);
+ } else SynErr(133);
}
void UnaryExpression(out Expression/*!*/ e) {
@@ -1717,7 +1730,7 @@ List<Expression/*!*/>/*!*/ decreases) { SelectExpression(out e);
} else if (StartOf(16)) {
ConstAtomExpression(out e);
- } else SynErr(133);
+ } else SynErr(134);
}
void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
@@ -1731,7 +1744,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 85) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(134);
+ } else SynErr(135);
}
void NegOp() {
@@ -1739,7 +1752,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 87) {
Get();
- } else SynErr(135);
+ } else SynErr(136);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -1830,7 +1843,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(50);
break;
}
- default: SynErr(136); break;
+ default: SynErr(137); break;
}
}
@@ -1885,9 +1898,9 @@ List<Expression/*!*/>/*!*/ decreases) { QuantifierGuts(out e);
} else if (StartOf(9)) {
Expression(out e);
- } else SynErr(137);
+ } else SynErr(138);
Expect(31);
- } else SynErr(138);
+ } else SynErr(139);
}
void SelectOrCallSuffix(ref Expression/*!*/ e) {
@@ -1937,12 +1950,12 @@ List<Expression/*!*/>/*!*/ decreases) { multipleIndices.Add(ee);
}
- } else SynErr(139);
+ } else SynErr(140);
} else if (la.kind == 95) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else SynErr(140);
+ } else SynErr(141);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
} else {
@@ -1964,7 +1977,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
Expect(50);
- } else SynErr(141);
+ } else SynErr(142);
}
void QuantifierGuts(out Expression/*!*/ q) {
@@ -1982,7 +1995,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 100 || la.kind == 101) {
Exists();
x = t;
- } else SynErr(142);
+ } else SynErr(143);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -2010,7 +2023,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 99) {
Get();
- } else SynErr(143);
+ } else SynErr(144);
}
void Exists() {
@@ -2018,7 +2031,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 101) {
Get();
- } else SynErr(144);
+ } else SynErr(145);
}
void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -2031,7 +2044,7 @@ List<Expression/*!*/>/*!*/ decreases) { es = new List<Expression/*!*/>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else SynErr(145);
+ } else SynErr(146);
Expect(8);
}
@@ -2040,7 +2053,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 103) {
Get();
- } else SynErr(146);
+ } else SynErr(147);
}
void AttributeBody(ref Attributes attrs) {
@@ -2234,35 +2247,36 @@ public class Errors { case 115: s = "invalid FunctionBody"; break;
case 116: s = "invalid PossiblyWildFrameExpression"; break;
case 117: s = "invalid PossiblyWildExpression"; break;
- case 118: s = "invalid Stmt"; break;
- case 119: s = "invalid OneStmt"; break;
- case 120: s = "invalid IfStmt"; break;
- case 121: s = "invalid ForeachStmt"; break;
- case 122: s = "invalid AssignRhs"; break;
- case 123: s = "invalid SelectExpression"; break;
- case 124: s = "invalid Guard"; break;
- case 125: s = "invalid CallStmtSubExpr"; break;
- case 126: s = "invalid AttributeArg"; break;
- case 127: s = "invalid EquivOp"; break;
- case 128: s = "invalid ImpliesOp"; break;
- case 129: s = "invalid AndOp"; break;
- case 130: s = "invalid OrOp"; break;
- case 131: s = "invalid RelOp"; break;
- case 132: s = "invalid AddOp"; break;
- case 133: s = "invalid UnaryExpression"; break;
- case 134: s = "invalid MulOp"; break;
- case 135: s = "invalid NegOp"; break;
- case 136: s = "invalid ConstAtomExpression"; break;
- case 137: s = "invalid ObjectExpression"; break;
+ case 118: s = "invalid MatchOrExpr"; break;
+ case 119: s = "invalid Stmt"; break;
+ case 120: s = "invalid OneStmt"; break;
+ case 121: s = "invalid IfStmt"; break;
+ case 122: s = "invalid ForeachStmt"; break;
+ case 123: s = "invalid AssignRhs"; break;
+ case 124: s = "invalid SelectExpression"; break;
+ case 125: s = "invalid Guard"; break;
+ case 126: s = "invalid CallStmtSubExpr"; break;
+ case 127: s = "invalid AttributeArg"; break;
+ case 128: s = "invalid EquivOp"; break;
+ case 129: s = "invalid ImpliesOp"; break;
+ case 130: s = "invalid AndOp"; break;
+ case 131: s = "invalid OrOp"; break;
+ case 132: s = "invalid RelOp"; break;
+ case 133: s = "invalid AddOp"; break;
+ case 134: s = "invalid UnaryExpression"; break;
+ case 135: s = "invalid MulOp"; break;
+ case 136: s = "invalid NegOp"; break;
+ case 137: s = "invalid ConstAtomExpression"; break;
case 138: s = "invalid ObjectExpression"; break;
- case 139: s = "invalid SelectOrCallSuffix"; break;
+ case 139: s = "invalid ObjectExpression"; break;
case 140: s = "invalid SelectOrCallSuffix"; break;
case 141: s = "invalid SelectOrCallSuffix"; break;
- case 142: s = "invalid QuantifierGuts"; break;
- case 143: s = "invalid Forall"; break;
- case 144: s = "invalid Exists"; break;
- case 145: s = "invalid AttributeOrTrigger"; break;
- case 146: s = "invalid QSep"; break;
+ case 142: s = "invalid SelectOrCallSuffix"; break;
+ case 143: s = "invalid QuantifierGuts"; break;
+ case 144: s = "invalid Forall"; break;
+ case 145: s = "invalid Exists"; break;
+ case 146: s = "invalid AttributeOrTrigger"; break;
+ case 147: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 0b93a1dc..6b97b471 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -239,7 +239,7 @@ namespace Microsoft.Dafny { if (f.Body != null) {
Indent(indent);
wr.WriteLine("{");
- PrintExtendedExpr(f.Body, ind);
+ PrintExtendedExpr(f.Body, ind, true, false);
Indent(indent);
wr.WriteLine("}");
}
@@ -560,7 +560,9 @@ namespace Microsoft.Dafny { }
wr.WriteLine(" =>");
foreach (Statement bs in mc.Body) {
+ Indent(caseInd + IndentAmount);
PrintStatement(bs, caseInd + IndentAmount);
+ wr.WriteLine();
}
}
Indent(indent);
@@ -604,7 +606,7 @@ namespace Microsoft.Dafny { // ----------------------------- PrintExpression -----------------------------
- public void PrintExtendedExpr(Expression expr, int indent) {
+ public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, bool endWithCloseParen) {
Contract.Requires(expr != null);
Indent(indent);
if (expr is ITEExpr) {
@@ -613,7 +615,7 @@ namespace Microsoft.Dafny { wr.Write("if ");
PrintExpression(ite.Test);
wr.WriteLine(" then");
- PrintExtendedExpr(ite.Thn, indent + IndentAmount);
+ PrintExtendedExpr(ite.Thn, indent + IndentAmount, true, false);
expr = ite.Els;
if (expr is ITEExpr) {
Indent(indent); wr.Write("else ");
@@ -621,7 +623,7 @@ namespace Microsoft.Dafny { Indent(indent); wr.WriteLine("else");
Indent(indent + IndentAmount);
PrintExpression(expr);
- wr.WriteLine();
+ wr.WriteLine(endWithCloseParen ? ")" : "");
return;
}
}
@@ -629,7 +631,10 @@ namespace Microsoft.Dafny { MatchExpr me = (MatchExpr)expr;
wr.Write("match ");
PrintExpression(me.Source);
+ wr.WriteLine();
+ int i = 0;
foreach (MatchCaseExpr mc in me.Cases) {
+ bool isLastCase = i == me.Cases.Count - 1;
Indent(indent);
wr.Write("case {0}", mc.Id);
if (mc.Arguments.Count != 0) {
@@ -640,12 +645,18 @@ namespace Microsoft.Dafny { }
wr.Write(")");
}
- wr.WriteLine(" =>");
- PrintExtendedExpr(mc.Body, indent + IndentAmount);
+ bool parensNeeded = !isLastCase && mc.Body is MatchExpr;
+ if (parensNeeded) {
+ wr.WriteLine(" => (");
+ } else {
+ wr.WriteLine(" =>");
+ }
+ PrintExtendedExpr(mc.Body, indent + IndentAmount, isLastCase, parensNeeded || (isLastCase && endWithCloseParen));
+ i++;
}
} else {
PrintExpression(expr, indent);
- wr.WriteLine();
+ wr.WriteLine(endWithCloseParen ? ")" : "");
}
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 1e27c4db..57fe4f77 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -624,7 +624,8 @@ namespace Microsoft.Dafny { // any type is fine
}
if (f.Body != null) {
- ResolveExpression(f.Body, false, f.IsGhost);
+ List<IVariable> matchVarContext = new List<IVariable>(f.Formals);
+ ResolveExpression(f.Body, false, f.IsGhost, matchVarContext);
Contract.Assert(f.Body.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(f.Body.Type, f.ResultType)) {
Error(f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type);
@@ -1713,7 +1714,11 @@ namespace Microsoft.Dafny { /// <summary>
/// "twoState" implies that "old" and "fresh" expressions are allowed
/// </summary>
- void ResolveExpression(Expression expr, bool twoState, bool specContext){
+ void ResolveExpression(Expression expr, bool twoState, bool specContext) {
+ ResolveExpression(expr, twoState, specContext, null);
+ }
+
+ void ResolveExpression(Expression expr, bool twoState, bool specContext, List<IVariable> matchVarContext) {
Contract.Requires(expr != null);
Contract.Requires(currentClass != null);
Contract.Ensures(expr.Type != null);
@@ -2207,6 +2212,7 @@ namespace Microsoft.Dafny { dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);
}
Dictionary<string,DatatypeCtor> ctors;
+ IVariable goodMatchVariable = null;
if (dtd == null) {
Error(me.Source, "the type of the match source expression must be a datatype");
ctors = null;
@@ -2216,8 +2222,12 @@ namespace Microsoft.Dafny { Contract.Assert(ctors != null); // dtd should have been inserted into datatypeCtors during a previous resolution stage
IdentifierExpr ie = me.Source as IdentifierExpr;
- if (ie == null || !(ie.Var is Formal)) {
- Error(me.Source.tok, "match source expression must be a formal parameter of the enclosing function");
+ if (ie == null || !(ie.Var is Formal || ie.Var is BoundVar)) {
+ Error(me.Source.tok, "match source expression must be a formal parameter of the enclosing function or an enclosing match expression");
+ } else if (!matchVarContext.Contains(ie.Var)) {
+ Error(me.Source.tok, "match source expression '{0}' has already been used as a match source expression in this context", ie.Var.Name);
+ } else {
+ goodMatchVariable = ie.Var;
}
// build the type-parameter substitution map for this use of the datatype
@@ -2270,7 +2280,12 @@ namespace Microsoft.Dafny { }
i++;
}
- ResolveExpression(mc.Body, twoState, specContext);
+ List<IVariable> innerMatchVarContext = new List<IVariable>(matchVarContext);
+ if (goodMatchVariable != null) {
+ innerMatchVarContext.Remove(goodMatchVariable); // this variable is no longer available for matching
+ }
+ innerMatchVarContext.AddRange(mc.Arguments);
+ ResolveExpression(mc.Body, twoState, specContext, innerMatchVarContext);
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);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 08800623..c3eec272 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -445,17 +445,11 @@ namespace Microsoft.Dafny { Function f = (Function)member;
AddFunction(f);
if (f.Body is MatchExpr) {
- MatchExpr me = (MatchExpr)f.Body;
- Formal formal = (Formal)((IdentifierExpr)me.Source).Var; // correctness of casts follows from what resolution checks
- foreach (MatchCaseExpr mc in me.Cases) {
- Contract.Assert(mc.Ctor != null); // the field is filled in by resolution
- Bpl.Axiom ax = FunctionAxiom(f, mc.Body, new List<Expression>(), formal, mc.Ctor, mc.Arguments);
- sink.TopLevelDeclarations.Add(ax);
- }
- Bpl.Axiom axPost = FunctionAxiom(f, null, f.Ens, null, null, null);
+ AddFunctionAxiomCase(f, (MatchExpr)f.Body, null);
+ Bpl.Axiom axPost = FunctionAxiom(f, null, f.Ens, null);
sink.TopLevelDeclarations.Add(axPost);
} else {
- Bpl.Axiom ax = FunctionAxiom(f, f.Body, f.Ens, null, null, null);
+ Bpl.Axiom ax = FunctionAxiom(f, f.Body, f.Ens, null);
sink.TopLevelDeclarations.Add(ax);
}
if (f.IsRecursive && !f.IsUnlimited) {
@@ -492,16 +486,81 @@ namespace Microsoft.Dafny { }
}
- Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, Expression body, List<Expression/*!*/>/*!*/ ens,
- Formal specializationFormal,
- DatatypeCtor ctor, List<BoundVar/*!*/> specializationReplacementFormals){
+ void AddFunctionAxiomCase(Function f, MatchExpr me, Specialization prev) {
+ Contract.Requires(f != null);
+ Contract.Requires(me != null);
+ IVariable formal = ((IdentifierExpr)me.Source).Var; // correctness of casts follows from what resolution checks
+ foreach (MatchCaseExpr mc in me.Cases) {
+ Contract.Assert(mc.Ctor != null); // the field is filled in by resolution
+ Specialization s = new Specialization(formal, mc, prev);
+ if (mc.Body is MatchExpr) {
+ AddFunctionAxiomCase(f, (MatchExpr)mc.Body, s);
+ } else {
+ Bpl.Axiom ax = FunctionAxiom(f, mc.Body, new List<Expression>(), s);
+ sink.TopLevelDeclarations.Add(ax);
+ }
+ }
+ }
+
+ class Specialization
+ {
+ public readonly List<Formal/*!*/> Formals;
+ public readonly List<Expression/*!*/> ReplacementExprs;
+ public readonly List<BoundVar/*!*/> ReplacementFormals;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(Formals));
+ Contract.Invariant(cce.NonNullElements(ReplacementExprs));
+ Contract.Invariant(Formals.Count == ReplacementExprs.Count);
+ Contract.Invariant(cce.NonNullElements(ReplacementFormals));
+ }
+
+ public Specialization(IVariable formal, MatchCase mc, Specialization prev) {
+ Contract.Requires(formal is Formal || formal is BoundVar);
+ Contract.Requires(mc != null);
+ Contract.Requires(prev == null || formal is BoundVar || !prev.Formals.Contains((Formal)formal));
+
+ List<Expression> rArgs = new List<Expression>();
+ foreach (BoundVar p in mc.Arguments) {
+ IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);
+ ie.Var = p; ie.Type = ie.Var.Type; // resolve it here
+ rArgs.Add(ie);
+ }
+ // create and resolve datatype value
+ var r = new DatatypeValue(mc.tok, mc.Ctor.EnclosingDatatype.Name, mc.Ctor.Name, rArgs);
+ r.Ctor = mc.Ctor;
+ r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List<Type>()/*this is not right, but it seems like it won't matter here*/);
+
+ Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
+ substMap.Add(formal, r);
+
+ // Fill in the fields
+ Formals = new List<Formal>();
+ ReplacementExprs = new List<Expression>();
+ ReplacementFormals = new List<BoundVar>();
+ if (prev != null) {
+ Formals.AddRange(prev.Formals);
+ foreach (var e in prev.ReplacementExprs) {
+ ReplacementExprs.Add(Substitute(e, null, substMap));
+ }
+ foreach (var rf in prev.ReplacementFormals) {
+ if (rf != formal) {
+ ReplacementFormals.Add(rf);
+ }
+ }
+ }
+ if (formal is Formal) {
+ Formals.Add((Formal)formal);
+ ReplacementExprs.Add(r);
+ }
+ ReplacementFormals.AddRange(mc.Arguments);
+ }
+ }
+
+ Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, Expression body, List<Expression/*!*/>/*!*/ ens, Specialization specialization) {
Contract.Requires(f != null);
- Contract.Requires(specializationFormal == null || body != null);
Contract.Requires(ens != null);
- Contract.Requires(cce.NonNullElements(specializationReplacementFormals));
Contract.Requires(predef != null);
- Contract.Requires((specializationFormal == null) == (ctor == null));
- Contract.Requires((specializationFormal == null) == (specializationReplacementFormals == null));
Contract.Requires(f.EnclosingClass != null);
ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
@@ -523,12 +582,12 @@ namespace Microsoft.Dafny { // f(args)-has-the-expected-type);
//
// The variables "formals" are the formals of function "f"; except, if a specialization is provided, then
- // "specializationFormal" (which is expected to be among the formals of "f") is excluded and replaced by
- // "specializationReplacementFormals".
+ // "specialization.Formals" (which are expected to be among the formals of "f") are excluded and replaced by
+ // "specialization.ReplacementFormals".
// The list "args" is the list of formals of function "f"; except, if a specialization is provided, then
- // "specializationFormal" is replaced by the expression "ctor(specializationReplacementFormals)".
- // If a specialization is provided, occurrences of "specializationFormal" in "body", "f.Req", and "f.Ens"
- // are also replaced by that expression.
+ // each of the "specialization.Formals" is replaced by the corresponding expression in "specialization.ReplacementExprs".
+ // If a specialization is provided, occurrences of "specialization.Formals" in "body", "f.Req", and "f.Ens"
+ // are also replaced by those corresponding expressions.
//
// The translation of "body" uses the #limited form whenever the callee is in the same SCC of the call graph.
//
@@ -562,25 +621,18 @@ namespace Microsoft.Dafny { etran.GoodRef(f.tok, bvThisIdExpr, thisType));
ante = Bpl.Expr.And(ante, wh);
}
- DatatypeValue r = null;
- if (specializationReplacementFormals != null) {
- Contract.Assert(ctor != null); // follows from if guard and the precondition
- List<Expression> rArgs = new List<Expression>();
- foreach (BoundVar p in specializationReplacementFormals) {
+ if (specialization != null) {
+ foreach (BoundVar p in specialization.ReplacementFormals) {
bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
formals.Add(bv);
- IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);
- ie.Var = p; ie.Type = ie.Var.Type; // resolve it here
- rArgs.Add(ie);
// add well-typedness conjunct to antecedent
Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, bv), p.Type, etran);
if (wh != null) { ante = Bpl.Expr.And(ante, wh); }
}
- r = new DatatypeValue(f.tok, cce.NonNull(ctor.EnclosingDatatype).Name, ctor.Name, rArgs);
- r.Ctor = ctor; r.Type = new UserDefinedType(f.tok, ctor.EnclosingDatatype.Name, new List<Type>()/*this is not right, but it seems like it won't matter here*/); // resolve it here
}
foreach (Formal p in f.Formals) {
- if (p != specializationFormal) {
+ int i = specialization == null ? -1 : specialization.Formals.FindIndex(val => val == p);
+ if (i == -1) {
bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
formals.Add(bv);
Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv);
@@ -589,8 +641,7 @@ namespace Microsoft.Dafny { Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran);
if (wh != null) { ante = Bpl.Expr.And(ante, wh); }
} else {
- Contract.Assert(r != null); // it is set above
- args.Add(etran.TrExpr(r));
+ args.Add(etran.TrExpr(specialization.ReplacementExprs[i]));
// note, well-typedness conjuncts for the replacement formals has already been done above
}
}
@@ -606,9 +657,11 @@ namespace Microsoft.Dafny { etran.InMethodContext())));
Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
- if (specializationFormal != null) {
- Contract.Assert(r != null);
- substMap.Add(specializationFormal, r);
+ if (specialization != null) {
+ Contract.Assert(specialization.Formals.Count == specialization.ReplacementExprs.Count);
+ for (int i = 0; i < specialization.Formals.Count; i++) {
+ substMap.Add(specialization.Formals[i], specialization.ReplacementExprs[i]);
+ }
}
Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType));
Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), args);
@@ -649,8 +702,12 @@ namespace Microsoft.Dafny { if (whr != null) { meat = Bpl.Expr.And(meat, whr); }
Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, meat));
string comment = "definition axiom for " + f.FullName;
- if (specializationFormal != null) {
- comment = string.Format("{0}, specialized for '{1}'", comment, specializationFormal.Name);
+ if (specialization != null) {
+ string sep = "{0}, specialized for '{1}'";
+ foreach (var formal in specialization.Formals) {
+ comment = string.Format(sep, comment, formal.Name);
+ sep = "{0}, '{1}'";
+ }
}
return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax), comment);
}
@@ -1831,11 +1888,7 @@ namespace Microsoft.Dafny { Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
Bpl.Expr ct = CtorInvocation(mc, etran, locals, b);
// generate: if (src == ctor(args)) { assume args-is-well-typed; mc.Body is well-formed; assume Result == TrExpr(case); } else ...
- CheckWellformed(mc.Body, options, null, locals, b, etran);
- if (result != null) {
- b.Add(new Bpl.AssumeCmd(mc.tok, Bpl.Expr.Eq(result, etran.TrExpr(mc.Body))));
- b.Add(new Bpl.AssumeCmd(mc.tok, CanCallAssumption(mc.Body, etran)));
- }
+ CheckWellformed(mc.Body, options, result, locals, b, etran);
ifcmd = new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), ifcmd, els);
els = null;
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 018a29e2..9501d26d 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -408,7 +408,9 @@ Modules0.dfy(62,6): Error: inter-module calls must follow the module import rela Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts
-8 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(133,10): Error: match source expression 'tree' has already been used as a match source expression in this context
+Modules0.dfy(172,12): Error: match source expression 'l' has already been used as a match source expression in this context
+10 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0
@@ -585,7 +587,7 @@ Execution trace: (0,0): anon24_Else
(0,0): anon25_Then
-Dafny program verifier finished with 11 verified, 1 error
+Dafny program verifier finished with 17 verified, 1 error
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(34,13): Error: assertion violation
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index a7ac03d9..998b20bc 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -93,3 +93,47 @@ method TestAllocatednessAxioms(a: List<Node>, b: List<Node>, c: List<AnotherNode }
}
}
+
+class NestedMatchExpr {
+ function Cadr<T>(a: List<T>, default: T): T
+ {
+ match a
+ case Nil => default
+ case Cons(x,t) =>
+ match t
+ case Nil => default
+ case Cons(y,tail) => y
+ }
+ // CadrAlt is the same as Cadr, but it writes its two outer cases in the opposite order
+ function CadrAlt<T>(a: List<T>, default: T): T
+ {
+ match a
+ case Cons(x,t) => (
+ match t
+ case Nil => default
+ case Cons(y,tail) => y)
+ case Nil => default
+ }
+ method TestNesting0()
+ {
+ var x := 5;
+ var list := #List.Cons(3, #List.Cons(6, #List.Nil));
+ assert Cadr(list, x) == 6;
+ match (list) {
+ case Nil => assert false;
+ case Cons(h,t) => assert Cadr(t, x) == 5;
+ }
+ }
+ method TestNesting1(a: List<NestedMatchExpr>)
+ ensures Cadr(a, this) == CadrAlt(a, this);
+ {
+ match (a) {
+ case Nil =>
+ case Cons(x,t) =>
+ match (t) {
+ case Nil =>
+ case Cons(y,tail) =>
+ }
+ }
+ }
+}
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index 3e8d1e25..adce71a8 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -120,3 +120,56 @@ class Ghosty { method Callee(a: int, ghost b: int) { }
ghost method Theorem(a: int) { }
}
+
+// ---------------------- illegal match expressions ---------------
+
+datatype Tree { Nil; Cons(int, Tree, Tree); }
+
+function NestedMatch0(tree: Tree): int
+{
+ match tree
+ case Nil => 0
+ case Cons(h,l,r) =>
+ match tree // error: cannot match on "tree" again
+ case Nil => 0
+ case Cons(hh,ll,rr) => hh
+}
+
+function NestedMatch1(tree: Tree): int
+{
+ match tree
+ case Nil => 0
+ case Cons(h,l,r) =>
+ match l
+ case Nil => 0
+ case Cons(h0,l0,r0) =>
+ match r
+ case Nil => 0
+ case Cons(h1,l1,r1) => h + h0 + h1
+}
+
+function NestedMatch2(tree: Tree): int
+{
+ match tree
+ case Nil => 0
+ case Cons(h,l,r) =>
+ match l
+ case Nil => 0
+ case Cons(h,l0,tree) => // fine to declare another "h" and "tree" here
+ match r
+ case Nil => 0
+ case Cons(h1,l1,r1) => h + h1
+}
+
+function NestedMatch3(tree: Tree): int
+{
+ match tree
+ case Nil => 0
+ case Cons(h,l,r) =>
+ match l
+ case Nil => 0
+ case Cons(h0,l0,r0) =>
+ match l // error: cannot match on "l" again
+ case Nil => 0
+ case Cons(h1,l1,r1) => h + h0 + h1
+}
|