diff options
| author |  rustanleino <unknown> | 2009-11-20 23:04:27 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-20 23:04:27 +0000 |
| commit | 9ed23deb0a3db4b61cf07fc6b551e10bc5436837 (patch) | |
| tree | 23f152c4938c27ff110dae14c1f0bea039a9ae09 | |
| parent | 797711ee7fb126a081e00d8b247c0cfa83ddd3f2 (diff) | |
Added resolution and translation of algebraic datatypes and (in function bodies) match expressions.
Addressed a couple of todos, including checking the well-formedness of quantifiers and if-then-else expressions in function bodies.
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 5 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.ssc | 96 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 58 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.ssc | 48 | ||||
| -rw-r--r-- | Source/Dafny/DafnyMain.ssc | 2 | ||||
| -rw-r--r-- | Source/Dafny/Parser.ssc | 574 | ||||
| -rw-r--r-- | Source/Dafny/Printer.ssc | 43 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.ssc | 133 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.ssc | 204 | ||||
| -rw-r--r-- | Source/Dafny/Translator.ssc | 407 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.ssc | 2 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 8 | ||||
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 14 | ||||
| -rw-r--r-- | Test/dafny0/Termination.dfy | 18 | ||||
| -rw-r--r-- | Test/dafny0/TypeParameters.dfy | 35 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 |
16 files changed, 1144 insertions, 505 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 4e524175..06b33b86 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -192,6 +192,11 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } type DatatypeType;
+type DtCtorId;
+function DatatypeCtorId(DatatypeType) returns (DtCtorId);
+
+function DtRank(DatatypeType) returns (int);
+
// ---------------------------------------------------------------
type Field alpha;
diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc index 5fb97548..c0158d13 100644 --- a/Source/Core/AbsyCmd.ssc +++ b/Source/Core/AbsyCmd.ssc @@ -868,11 +868,11 @@ namespace Microsoft.Boogie }
public override void Emit(TokenTextWriter! stream, int level)
{
- if (this.Comment.Contains("\n")) {
- stream.WriteLine(this, level, "/* {0} */", this.Comment);
- } else {
- stream.WriteLine(this, level, "// {0}", this.Comment);
- }
+ if (this.Comment.Contains("\n")) {
+ stream.WriteLine(this, level, "/* {0} */", this.Comment);
+ } else {
+ stream.WriteLine(this, level, "// {0}", this.Comment);
+ }
}
public override void Resolve(ResolutionContext! rc) { }
public override void AddAssignedVariables(VariableSeq! vars) { }
@@ -1320,18 +1320,18 @@ namespace Microsoft.Boogie {
stream.Write(this, level, "call ");
string sep = "";
- if (Outs.Count > 0) {
- foreach (Expr arg in Outs) {
- stream.Write(sep);
- sep = ", ";
- if (arg == null) {
- stream.Write("*");
- } else {
- arg.Emit(stream);
- }
- }
- stream.Write(" := ");
- }
+ if (Outs.Count > 0) {
+ foreach (Expr arg in Outs) {
+ stream.Write(sep);
+ sep = ", ";
+ if (arg == null) {
+ stream.Write("*");
+ } else {
+ arg.Emit(stream);
+ }
+ }
+ stream.Write(" := ");
+ }
stream.Write(TokenTextWriter.SanitizeIdentifier(callee));
stream.Write("(");
sep = "";
@@ -1572,46 +1572,46 @@ namespace Microsoft.Boogie Requires! req = (!) this.Proc.Requires[i];
if (!req.Free) {
if (hasWildcard) {
- Expr pre = Substituter.Apply(s, req.Condition);
- if (preConjunction == null) {
- preConjunction = pre;
- } else {
- preConjunction = Expr.And(preConjunction, pre);
- }
+ Expr pre = Substituter.Apply(s, req.Condition);
+ if (preConjunction == null) {
+ preConjunction = pre;
+ } else {
+ preConjunction = Expr.And(preConjunction, pre);
+ }
} else {
- Requires! reqCopy = (Requires!) req.Clone();
- reqCopy.Condition = Substituter.Apply(s, req.Condition);
- AssertCmd! a = new AssertRequiresCmd(this, reqCopy);
- a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
- newBlockBody.Add(a);
+ Requires! reqCopy = (Requires!) req.Clone();
+ reqCopy.Condition = Substituter.Apply(s, req.Condition);
+ AssertCmd! a = new AssertRequiresCmd(this, reqCopy);
+ a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
+ newBlockBody.Add(a);
}
}
}
if (hasWildcard) {
- if (preConjunction == null) {
- preConjunction = Expr.True;
- }
- Expr! expr = new ExistsExpr(tok, wildcardVars, preConjunction);
+ if (preConjunction == null) {
+ preConjunction = Expr.True;
+ }
+ Expr! expr = new ExistsExpr(tok, wildcardVars, preConjunction);
AssertCmd! a = new AssertCmd(tok, expr);
- a.ErrorDataEnhanced = AssertCmd.GenerateBoundVarMiningStrategy(expr);
- newBlockBody.Add(a);
+ a.ErrorDataEnhanced = AssertCmd.GenerateBoundVarMiningStrategy(expr);
+ newBlockBody.Add(a);
}
#endregion
#region assume Pre[ins := cins] with formal paramters
if (hasWildcard) {
- s = Substituter.SubstitutionFromHashtable(substMap);
- for (int i = 0; i < this.Proc.Requires.Length; i++)
- {
- Requires! req = (!) this.Proc.Requires[i];
- if (!req.Free) {
- Requires! reqCopy = (Requires!) req.Clone();
- reqCopy.Condition = Substituter.Apply(s, req.Condition);
- AssumeCmd! a = new AssumeCmd(tok, reqCopy.Condition);
- newBlockBody.Add(a);
- }
- }
- }
+ s = Substituter.SubstitutionFromHashtable(substMap);
+ for (int i = 0; i < this.Proc.Requires.Length; i++)
+ {
+ Requires! req = (!) this.Proc.Requires[i];
+ if (!req.Free) {
+ Requires! reqCopy = (Requires!) req.Clone();
+ reqCopy.Condition = Substituter.Apply(s, req.Condition);
+ AssumeCmd! a = new AssumeCmd(tok, reqCopy.Condition);
+ newBlockBody.Add(a);
+ }
+ }
+ }
#endregion
#region cframe := frame (to hold onto frame values in case they are referred to in the postcondition)
@@ -1922,8 +1922,8 @@ namespace Microsoft.Boogie #region assume (forall wildcardVars :: Pre ==> Post);
Expr body = postConjunction;
if (couts.Length > 0) {
- body = new ExistsExpr(tok, couts, body);
- }
+ body = new ExistsExpr(tok, couts, body);
+ }
body = Expr.Imp(preConjunction, body);
if (wildcardVars.Length != 0) {
TypeVariableSeq! typeParams = Type.FreeVariablesIn((!)InstantiatedTypes);
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index f68b59e1..2bf7c1e3 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -390,7 +390,7 @@ FunctionDecl<out Function! f> ( ";"
{ FunctionSpec<reqs, reads> }
| { FunctionSpec<reqs, reads> }
- ExtendedExpr<out bb> (. body = bb; .)
+ FunctionBody<out bb> (. body = bb; .)
)
(. parseVarScope.PopMarker();
f = new Function(id, id.val, use, typeArgs, formals, returnType, reqs, reads, body, attrs);
@@ -410,6 +410,16 @@ ReadsClause<List<Expression!\>! reads> ";"
.
+FunctionBody<out Expression! e>
+= (. e = dummyExpr; .)
+ "{"
+ ( IfThenElseExpr<out e>
+ | MatchExpression<out e>
+ | Expression<out e>
+ )
+ "}"
+ .
+
ExtendedExpr<out Expression! e>
= (. e = dummyExpr; .)
"{"
@@ -430,6 +440,43 @@ IfThenElseExpr<out Expression! e> ) (. e = new ITEExpr(x, e, e0, e1); .)
.
+MatchExpression<out Expression! e>
+= (. Token! x;
+ List<MatchCase!> cases = new List<MatchCase!>();
+ .)
+ "match" (. x = token; .)
+ Expression<out e>
+ ( "{" CaseExpressions<cases> "}" /* curly braces are optional; in the future, when match expressions can be nested, this will be handy */
+ | CaseExpressions<cases>
+ )
+ (. e = new MatchExpr(x, e, cases); .)
+ .
+
+CaseExpressions<List<MatchCase!\>! cases>
+= (. MatchCase! c; .)
+ { CaseExpression<out c> (. cases.Add(c); .)
+ }
+ .
+
+CaseExpression<out MatchCase! c>
+= (. Token! x, id, arg;
+ List<BoundVar!> arguments = new List<BoundVar!>();
+ Expression! body;
+ .)
+ "case" (. x = token; parseVarScope.PushMarker(); .)
+ Ident<out id>
+ [ "("
+ Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
+ parseVarScope.Push(arg.val, arg.val); .)
+ { "," Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
+ parseVarScope.Push(arg.val, arg.val); .)
+ }
+ ")" ]
+ "=>"
+ Expression<out body> (. c = new MatchCase(x, id.val, arguments, body);
+ parseVarScope.PopMarker(); .)
+ .
+
/*------------------------------------------------------------------------*/
BlockStmt<out Statement! block>
@@ -827,13 +874,20 @@ UnaryExpression<out Expression! e> NegOp = "!" | '\u00ac'.
ConstAtomExpression<out Expression! e>
-= (. Token! x; int n; List<Expression!>! elements;
+= (. Token! x, dtName, id; int n; List<Expression!>! elements;
e = dummyExpr;
.)
( "false" (. e = new LiteralExpr(token, false); .)
| "true" (. e = new LiteralExpr(token, true); .)
| "null" (. e = new LiteralExpr(token); .)
| Nat<out n> (. e = new LiteralExpr(token, n); .)
+ | "#" (. x = token; .)
+ Ident<out dtName>
+ "."
+ Ident<out id> (. elements = new List<Expression!>(); .)
+ [ "("
+ [ Expressions<elements> ]
+ ")" ] (. e = new DatatypeValue(token, dtName.val, id.val, elements); .)
| "fresh" (. x = token; .)
"(" Expression<out e> ")" (. e = new FreshExpr(x, e); .)
| "|" (. x = token; .)
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc index 92854bc5..831cc424 100644 --- a/Source/Dafny/DafnyAst.ssc +++ b/Source/Dafny/DafnyAst.ssc @@ -361,6 +361,14 @@ namespace Microsoft.Dafny this.Formals = formals;
base(tok, name, attributes);
}
+
+ public string! FullName {
+ get
+ requires EnclosingDatatype != null;
+ {
+ return "#" + EnclosingDatatype.Name + "." + Name;
+ }
+ }
}
public abstract class MemberDecl : Declaration {
@@ -833,6 +841,20 @@ namespace Microsoft.Dafny }
}
+ public class DatatypeValue : Expression {
+ public readonly string! DatatypeName;
+ public readonly string! MemberName;
+ public readonly List<Expression!>! Arguments;
+ public DatatypeCtor Ctor; // filled in by resolution
+
+ public DatatypeValue(Token! tok, string! datatypeName, string! memberName, [Captured] List<Expression!>! arguments) {
+ this.DatatypeName = datatypeName;
+ this.MemberName = memberName;
+ this.Arguments = arguments;
+ base(tok);
+ }
+ }
+
public class ThisExpr : Expression {
public ThisExpr(Token! tok) {
base(tok);
@@ -1078,6 +1100,32 @@ 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<MatchCase!>! Cases;
+
+ public MatchExpr(Token! tok, Expression! source, [Captured] List<MatchCase!>! cases) {
+ this.Source = source;
+ this.Cases = cases;
+ base(tok);
+ }
+ }
+
+ public class MatchCase {
+ public readonly Token! tok;
+ public readonly string! Id;
+ public DatatypeCtor Ctor; // filled in by resolution
+ public readonly List<BoundVar!>! Arguments;
+ public readonly Expression! Body;
+
+ public MatchCase(Token! tok, string! id, [Captured] List<BoundVar!>! arguments, Expression! body) {
+ this.tok = tok;
+ this.Id = id;
+ this.Arguments = arguments;
+ this.Body = body;
+ }
+ }
+
public class ITEExpr : Expression { // an ITEExpr is an "extended expression" and is only allowed in certain places
public readonly Expression! Test;
public readonly Expression! Thn;
diff --git a/Source/Dafny/DafnyMain.ssc b/Source/Dafny/DafnyMain.ssc index 9bf132d3..2cccc08e 100644 --- a/Source/Dafny/DafnyMain.ssc +++ b/Source/Dafny/DafnyMain.ssc @@ -59,7 +59,7 @@ namespace Microsoft.Dafny { }
}
- if (Bpl.CommandLineOptions.Clo.NoResolve) { return null; }
+ if (Bpl.CommandLineOptions.Clo.NoResolve || Bpl.CommandLineOptions.Clo.NoTypecheck) { return null; }
Dafny.Resolver r = new Dafny.Resolver();
r.ResolveProgram(program);
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index 83665027..7a5f78ef 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -5,7 +5,7 @@ using Microsoft.Contracts; namespace Microsoft.Dafny {
public class Parser {
- const int maxT = 88;
+ const int maxT = 92;
const bool T = true;
const bool x = false;
@@ -226,7 +226,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { mm.Add(m);
} else if (t.kind == 14) {
FrameDecl();
- } else Error(89);
+ } else Error(93);
}
static void FieldDecl(List<MemberDecl!>! mm) {
@@ -283,9 +283,9 @@ public static int Parse (List<TopLevelDecl!>! classes) { while (t.kind == 19 || t.kind == 30) {
FunctionSpec(reqs, reads);
}
- ExtendedExpr(out bb);
+ FunctionBody(out bb);
body = bb;
- } else Error(90);
+ } else Error(94);
parseVarScope.PopMarker();
f = new Function(id, id.val, use, typeArgs, formals, returnType, reqs, reads, body, attrs);
@@ -327,7 +327,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
BlockStmt(out bb);
body = bb;
- } else Error(91);
+ } else Error(95);
parseVarScope.PopMarker();
m = new Method(id, id.val, typeArgs, ins, outs, req, mod, ens, body, attrs);
@@ -459,7 +459,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { } else if (t.kind == 1 || t.kind == 27) {
ReferenceType(out tok, out ty);
- } else Error(92);
+ } else Error(96);
}
static void Formals(bool incoming, List<Formal!>! formals) {
@@ -507,8 +507,8 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expression(out e);
Expect(8);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else Error(93);
- } else Error(94);
+ } else Error(97);
+ } else Error(98);
}
static void BlockStmt(out Statement! block) {
@@ -530,7 +530,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void Expression(out Expression! e0) {
Token! x; Expression! e1;
ImpliesExpression(out e0);
- while (t.kind == 49 || t.kind == 50) {
+ while (t.kind == 52 || t.kind == 53) {
EquivOp();
x = token;
ImpliesExpression(out e1);
@@ -565,7 +565,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else Error(95);
+ } else Error(99);
}
static void FunctionSpec(List<Expression!>! reqs, List<Expression!>! reads) {
@@ -577,17 +577,19 @@ public static int Parse (List<TopLevelDecl!>! classes) { reqs.Add(e);
} else if (t.kind == 30) {
ReadsClause(reads);
- } else Error(96);
+ } else Error(100);
}
- static void ExtendedExpr(out Expression! e) {
+ static void FunctionBody(out Expression! e) {
e = dummyExpr;
Expect(5);
if (t.kind == 31) {
IfThenElseExpr(out e);
+ } else if (t.kind == 33) {
+ MatchExpression(out e);
} else if (StartOf(5)) {
Expression(out e);
- } else Error(97);
+ } else Error(101);
Expect(6);
}
@@ -623,10 +625,73 @@ public static int Parse (List<TopLevelDecl!>! classes) { IfThenElseExpr(out e1);
} else if (t.kind == 5) {
ExtendedExpr(out e1);
- } else Error(98);
+ } else Error(102);
e = new ITEExpr(x, e, e0, e1);
}
+ static void MatchExpression(out Expression! e) {
+ Token! x;
+ List<MatchCase!> cases = new List<MatchCase!>();
+
+ Expect(33);
+ x = token;
+ Expression(out e);
+ if (t.kind == 5) {
+ Get();
+ CaseExpressions(cases);
+ Expect(6);
+ } else if (t.kind == 6 || t.kind == 34) {
+ CaseExpressions(cases);
+ } else Error(103);
+ e = new MatchExpr(x, e, cases);
+ }
+
+ static void ExtendedExpr(out Expression! e) {
+ e = dummyExpr;
+ Expect(5);
+ if (t.kind == 31) {
+ IfThenElseExpr(out e);
+ } else if (StartOf(5)) {
+ Expression(out e);
+ } else Error(104);
+ Expect(6);
+ }
+
+ static void CaseExpressions(List<MatchCase!>! cases) {
+ MatchCase! c;
+ while (t.kind == 34) {
+ CaseExpression(out c);
+ cases.Add(c);
+ }
+ }
+
+ static void CaseExpression(out MatchCase! c) {
+ Token! x, id, arg;
+ List<BoundVar!> arguments = new List<BoundVar!>();
+ Expression! body;
+
+ Expect(34);
+ x = token; parseVarScope.PushMarker();
+ Ident(out id);
+ if (t.kind == 21) {
+ Get();
+ Ident(out arg);
+ arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
+ parseVarScope.Push(arg.val, arg.val);
+ while (t.kind == 10) {
+ Get();
+ Ident(out arg);
+ arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
+ parseVarScope.Push(arg.val, arg.val);
+ }
+ Expect(22);
+ }
+ Expect(35);
+ Expression(out body);
+ c = new MatchCase(x, id.val, arguments, body);
+ parseVarScope.PopMarker();
+ }
+
static void Stmt(List<Statement!>! ss) {
Statement! s;
while (t.kind == 5) {
@@ -638,7 +703,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { ss.Add(s);
} else if (t.kind == 9) {
VarDeclStmts(ss);
- } else Error(99);
+ } else Error(105);
}
static void OneStmt(out Statement! s) {
@@ -646,11 +711,11 @@ public static int Parse (List<TopLevelDecl!>! classes) { s = dummyStmt; /* to please the compiler */
switch (t.kind) {
- case 47: {
+ case 50: {
AssertStmt(out s);
break;
}
- case 48: {
+ case 51: {
AssumeStmt(out s);
break;
}
@@ -658,15 +723,15 @@ public static int Parse (List<TopLevelDecl!>! classes) { UseStmt(out s);
break;
}
- case 1: case 2: case 5: case 21: case 46: case 67: case 70: case 71: case 72: case 73: case 74: case 75: case 76: case 80: case 81: {
+ case 1: case 2: case 5: case 21: case 49: case 70: case 73: case 74: case 75: case 76: case 77: case 78: case 80: case 81: case 84: case 85: {
AssignStmt(out s);
break;
}
- case 38: {
+ case 41: {
HavocStmt(out s);
break;
}
- case 43: {
+ case 46: {
CallStmt(out s);
break;
}
@@ -674,15 +739,15 @@ public static int Parse (List<TopLevelDecl!>! classes) { IfStmt(out s);
break;
}
- case 39: {
+ case 42: {
WhileStmt(out s);
break;
}
- case 44: {
+ case 47: {
ForeachStmt(out s);
break;
}
- case 33: {
+ case 36: {
Get();
x = token;
Ident(out id);
@@ -690,7 +755,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { s = new LabelStmt(x, id.val);
break;
}
- case 34: {
+ case 37: {
Get();
x = token;
if (t.kind == 1) {
@@ -701,14 +766,14 @@ public static int Parse (List<TopLevelDecl!>! classes) { s = new BreakStmt(x, label);
break;
}
- case 35: {
+ case 38: {
Get();
x = token;
Expect(8);
s = new ReturnStmt(x);
break;
}
- default: Error(100); break;
+ default: Error(106); break;
}
}
@@ -727,7 +792,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void AssertStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(47);
+ Expect(50);
x = token;
Expression(out e);
Expect(8);
@@ -736,7 +801,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void AssumeStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(48);
+ Expect(51);
x = token;
Expression(out e);
Expect(8);
@@ -760,7 +825,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { s = dummyStmt;
LhsExpr(out lhs);
- Expect(36);
+ Expect(39);
x = token;
AssignRhs(out rhs, out ty);
if (rhs != null) {
@@ -775,7 +840,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void HavocStmt(out Statement! s) {
Token! x; Expression! lhs;
- Expect(38);
+ Expect(41);
x = token;
LhsExpr(out lhs);
Expect(8);
@@ -788,10 +853,10 @@ public static int Parse (List<TopLevelDecl!>! classes) { List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
List<VarDecl!> newVars = new List<VarDecl!>();
- Expect(43);
+ Expect(46);
x = token;
CallStmtSubExpr(out e);
- if (t.kind == 10 || t.kind == 36) {
+ if (t.kind == 10 || t.kind == 39) {
if (t.kind == 10) {
Get();
e = ConvertToLocal(e);
@@ -810,7 +875,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
}
- Expect(36);
+ Expect(39);
CallStmtSubExpr(out e);
} else {
Get();
@@ -856,7 +921,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { } else if (t.kind == 5) {
BlockStmt(out s);
els = s;
- } else Error(101);
+ } else Error(107);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -869,18 +934,18 @@ public static int Parse (List<TopLevelDecl!>! classes) { List<Expression!> decreases = new List<Expression!>();
Statement! body;
- Expect(39);
+ Expect(42);
x = token;
Guard(out guard);
assume guard == null || Owner.None(guard);
- while (t.kind == 18 || t.kind == 40 || t.kind == 41) {
- if (t.kind == 18 || t.kind == 40) {
+ while (t.kind == 18 || t.kind == 43 || t.kind == 44) {
+ if (t.kind == 18 || t.kind == 43) {
isFree = false;
if (t.kind == 18) {
Get();
isFree = true;
}
- Expect(40);
+ Expect(43);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(8);
@@ -909,7 +974,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { AssignStmt bodyAssign = null;
parseVarScope.PushMarker();
- Expect(44);
+ Expect(47);
x = token;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
@@ -920,20 +985,20 @@ public static int Parse (List<TopLevelDecl!>! classes) { Get();
Type(out ty);
}
- Expect(45);
+ Expect(48);
Expression(out collection);
parseVarScope.Push(boundVar.val, boundVar.val);
- if (t.kind == 46) {
+ if (t.kind == 49) {
Get();
Expression(out range);
}
Expect(22);
Expect(5);
- while (t.kind == 29 || t.kind == 47 || t.kind == 48) {
- if (t.kind == 47) {
+ while (t.kind == 29 || t.kind == 50 || t.kind == 51) {
+ if (t.kind == 50) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- } else if (t.kind == 48) {
+ } else if (t.kind == 51) {
AssumeStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -944,10 +1009,10 @@ public static int Parse (List<TopLevelDecl!>! classes) { if (StartOf(5)) {
AssignStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else if (t.kind == 38) {
+ } else if (t.kind == 41) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else Error(102);
+ } else Error(108);
Expect(6);
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
parseVarScope.PopMarker();
@@ -961,14 +1026,14 @@ public static int Parse (List<TopLevelDecl!>! classes) { Token! x; Expression! ee; Type! tt;
e = null; ty = null;
- if (t.kind == 37) {
+ if (t.kind == 40) {
Get();
ReferenceType(out x, out tt);
ty = tt;
} else if (StartOf(5)) {
Expression(out ee);
e = ee;
- } else Error(103);
+ } else Error(109);
if (e == null && ty == null) { e = dummyExpr; }
}
@@ -983,7 +1048,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Type(out ty);
optionalType = ty;
}
- if (t.kind == 36) {
+ if (t.kind == 39) {
Get();
AssignRhs(out rhs, out newType);
}
@@ -1002,13 +1067,13 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void Guard(out Expression e) {
Expression! ee; e = null;
Expect(21);
- if (t.kind == 42) {
+ if (t.kind == 45) {
Get();
e = null;
} else if (StartOf(5)) {
Expression(out ee);
e = ee;
- } else Error(104);
+ } else Error(110);
Expect(22);
}
@@ -1016,11 +1081,11 @@ public static int Parse (List<TopLevelDecl!>! classes) { e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 21 || t.kind == 80 || t.kind == 81) {
+ } else if (t.kind == 21 || t.kind == 84 || t.kind == 85) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else Error(105);
- while (t.kind == 76 || t.kind == 78) {
+ } else Error(111);
+ while (t.kind == 79 || t.kind == 81) {
SelectOrCallSuffix(ref e);
}
}
@@ -1028,7 +1093,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void ImpliesExpression(out Expression! e0) {
Token! x; Expression! e1;
LogicalExpression(out e0);
- if (t.kind == 51 || t.kind == 52) {
+ if (t.kind == 54 || t.kind == 55) {
ImpliesOp();
x = token;
ImpliesExpression(out e1);
@@ -1037,23 +1102,23 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
static void EquivOp() {
- if (t.kind == 49) {
+ if (t.kind == 52) {
Get();
- } else if (t.kind == 50) {
+ } else if (t.kind == 53) {
Get();
- } else Error(106);
+ } else Error(112);
}
static void LogicalExpression(out Expression! e0) {
Token! x; Expression! e1;
RelationalExpression(out e0);
if (StartOf(8)) {
- if (t.kind == 53 || t.kind == 54) {
+ if (t.kind == 56 || t.kind == 57) {
AndOp();
x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (t.kind == 53 || t.kind == 54) {
+ while (t.kind == 56 || t.kind == 57) {
AndOp();
x = token;
RelationalExpression(out e1);
@@ -1064,7 +1129,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (t.kind == 55 || t.kind == 56) {
+ while (t.kind == 58 || t.kind == 59) {
OrOp();
x = token;
RelationalExpression(out e1);
@@ -1075,11 +1140,11 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
static void ImpliesOp() {
- if (t.kind == 51) {
+ if (t.kind == 54) {
Get();
- } else if (t.kind == 52) {
+ } else if (t.kind == 55) {
Get();
- } else Error(107);
+ } else Error(113);
}
static void RelationalExpression(out Expression! e0) {
@@ -1093,25 +1158,25 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
static void AndOp() {
- if (t.kind == 53) {
+ if (t.kind == 56) {
Get();
- } else if (t.kind == 54) {
+ } else if (t.kind == 57) {
Get();
- } else Error(108);
+ } else Error(114);
}
static void OrOp() {
- if (t.kind == 55) {
+ if (t.kind == 58) {
Get();
- } else if (t.kind == 56) {
+ } else if (t.kind == 59) {
Get();
- } else Error(109);
+ } else Error(115);
}
static void Term(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (t.kind == 66 || t.kind == 67) {
+ while (t.kind == 69 || t.kind == 70) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1121,7 +1186,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void RelOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
switch (t.kind) {
- case 57: {
+ case 60: {
Get();
x = token; op = BinaryExpr.Opcode.Eq;
break;
@@ -1136,59 +1201,59 @@ public static int Parse (List<TopLevelDecl!>! classes) { x = token; op = BinaryExpr.Opcode.Gt;
break;
}
- case 58: {
+ case 61: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 59: {
+ case 62: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- case 60: {
+ case 63: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 61: {
+ case 64: {
Get();
x = token; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 45: {
+ case 48: {
Get();
x = token; op = BinaryExpr.Opcode.In;
break;
}
- case 62: {
+ case 65: {
Get();
x = token; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 63: {
+ case 66: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 64: {
+ case 67: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 65: {
+ case 68: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- default: Error(110); break;
+ default: Error(116); break;
}
}
static void Factor(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (t.kind == 42 || t.kind == 68 || t.kind == 69) {
+ while (t.kind == 45 || t.kind == 71 || t.kind == 72) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1197,23 +1262,23 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void AddOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 66) {
+ if (t.kind == 69) {
Get();
x = token; op = BinaryExpr.Opcode.Add;
- } else if (t.kind == 67) {
+ } else if (t.kind == 70) {
Get();
x = token; op = BinaryExpr.Opcode.Sub;
- } else Error(111);
+ } else Error(117);
}
static void UnaryExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 67) {
+ if (t.kind == 70) {
Get();
x = token;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (t.kind == 70 || t.kind == 71) {
+ } else if (t.kind == 73 || t.kind == 74) {
NegOp();
x = token;
UnaryExpression(out e);
@@ -1222,59 +1287,59 @@ public static int Parse (List<TopLevelDecl!>! classes) { SelectExpression(out e);
} else if (StartOf(11)) {
ConstAtomExpression(out e);
- } else Error(112);
+ } else Error(118);
}
static void MulOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 42) {
+ if (t.kind == 45) {
Get();
x = token; op = BinaryExpr.Opcode.Mul;
- } else if (t.kind == 68) {
+ } else if (t.kind == 71) {
Get();
x = token; op = BinaryExpr.Opcode.Div;
- } else if (t.kind == 69) {
+ } else if (t.kind == 72) {
Get();
x = token; op = BinaryExpr.Opcode.Mod;
- } else Error(113);
+ } else Error(119);
}
static void NegOp() {
- if (t.kind == 70) {
+ if (t.kind == 73) {
Get();
- } else if (t.kind == 71) {
+ } else if (t.kind == 74) {
Get();
- } else Error(114);
+ } else Error(120);
}
static void SelectExpression(out Expression! e) {
Token! id; e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 21 || t.kind == 80 || t.kind == 81) {
+ } else if (t.kind == 21 || t.kind == 84 || t.kind == 85) {
ObjectExpression(out e);
- } else Error(115);
- while (t.kind == 76 || t.kind == 78) {
+ } else Error(121);
+ while (t.kind == 79 || t.kind == 81) {
SelectOrCallSuffix(ref e);
}
}
static void ConstAtomExpression(out Expression! e) {
- Token! x; int n; List<Expression!>! elements;
+ Token! x, dtName, id; int n; List<Expression!>! elements;
e = dummyExpr;
switch (t.kind) {
- case 72: {
+ case 75: {
Get();
e = new LiteralExpr(token, false);
break;
}
- case 73: {
+ case 76: {
Get();
e = new LiteralExpr(token, true);
break;
}
- case 74: {
+ case 77: {
Get();
e = new LiteralExpr(token);
break;
@@ -1284,7 +1349,24 @@ public static int Parse (List<TopLevelDecl!>! classes) { e = new LiteralExpr(token, n);
break;
}
- case 75: {
+ case 78: {
+ Get();
+ x = token;
+ Ident(out dtName);
+ Expect(79);
+ Ident(out id);
+ elements = new List<Expression!>();
+ if (t.kind == 21) {
+ Get();
+ if (StartOf(5)) {
+ Expressions(elements);
+ }
+ Expect(22);
+ }
+ e = new DatatypeValue(token, dtName.val, id.val, elements);
+ break;
+ }
+ case 80: {
Get();
x = token;
Expect(21);
@@ -1293,12 +1375,12 @@ public static int Parse (List<TopLevelDecl!>! classes) { e = new FreshExpr(x, e);
break;
}
- case 46: {
+ case 49: {
Get();
x = token;
Expression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
- Expect(46);
+ Expect(49);
break;
}
case 5: {
@@ -1311,17 +1393,17 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expect(6);
break;
}
- case 76: {
+ case 81: {
Get();
x = token; elements = new List<Expression!>();
if (StartOf(5)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(77);
+ Expect(82);
break;
}
- default: Error(116); break;
+ default: Error(122); break;
}
}
@@ -1360,10 +1442,10 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void ObjectExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 80) {
+ if (t.kind == 84) {
Get();
e = new ThisExpr(token);
- } else if (t.kind == 81) {
+ } else if (t.kind == 85) {
Get();
x = token;
Expect(21);
@@ -1376,9 +1458,9 @@ public static int Parse (List<TopLevelDecl!>! classes) { QuantifierGuts(out e);
} else if (StartOf(5)) {
Expression(out e);
- } else Error(117);
+ } else Error(123);
Expect(22);
- } else Error(118);
+ } else Error(124);
}
static void SelectOrCallSuffix(ref Expression! e) {
@@ -1386,7 +1468,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expression e0 = null; Expression e1 = null; Expression! ee; bool anyDots = false;
bool func = false;
- if (t.kind == 78) {
+ if (t.kind == 79) {
Get();
Ident(out id);
if (t.kind == 21) {
@@ -1399,14 +1481,14 @@ public static int Parse (List<TopLevelDecl!>! classes) { e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (t.kind == 76) {
+ } else if (t.kind == 81) {
Get();
x = token;
if (StartOf(5)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 36 || t.kind == 79) {
- if (t.kind == 79) {
+ if (t.kind == 39 || t.kind == 83) {
+ if (t.kind == 83) {
Get();
anyDots = true;
if (StartOf(5)) {
@@ -1419,11 +1501,11 @@ public static int Parse (List<TopLevelDecl!>! classes) { e1 = ee;
}
}
- } else if (t.kind == 79) {
+ } else if (t.kind == 83) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else Error(119);
+ } else Error(125);
assert !anyDots ==> e0 != null;
if (anyDots) {
assert e0 != null || e1 != null;
@@ -1436,8 +1518,8 @@ public static int Parse (List<TopLevelDecl!>! classes) { e = new SeqUpdateExpr(x, e, e0, e1);
}
- Expect(77);
- } else Error(120);
+ Expect(82);
+ } else Error(126);
}
static void QuantifierGuts(out Expression! q) {
@@ -1450,13 +1532,13 @@ public static int Parse (List<TopLevelDecl!>! classes) { Triggers trigs = null;
Expression! body;
- if (t.kind == 82 || t.kind == 83) {
+ if (t.kind == 86 || t.kind == 87) {
Forall();
x = token; univ = true;
- } else if (t.kind == 84 || t.kind == 85) {
+ } else if (t.kind == 88 || t.kind == 89) {
Exists();
x = token;
- } else Error(121);
+ } else Error(127);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -1480,27 +1562,27 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
static void Forall() {
- if (t.kind == 82) {
+ if (t.kind == 86) {
Get();
- } else if (t.kind == 83) {
+ } else if (t.kind == 87) {
Get();
- } else Error(122);
+ } else Error(128);
}
static void Exists() {
- if (t.kind == 84) {
+ if (t.kind == 88) {
Get();
- } else if (t.kind == 85) {
+ } else if (t.kind == 89) {
Get();
- } else Error(123);
+ } else Error(129);
}
static void QSep() {
- if (t.kind == 86) {
+ if (t.kind == 90) {
Get();
- } else if (t.kind == 87) {
+ } else if (t.kind == 91) {
Get();
- } else Error(124);
+ } else Error(130);
}
static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -1513,7 +1595,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else Error(125);
+ } else Error(131);
Expect(6);
}
@@ -1545,7 +1627,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { } else if (StartOf(5)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else Error(126);
+ } else Error(132);
}
@@ -1597,100 +1679,106 @@ public static int Parse (List<TopLevelDecl!>! classes) { case 30: s = "reads expected"; break;
case 31: s = "if expected"; break;
case 32: s = "else expected"; break;
- case 33: s = "label expected"; break;
- case 34: s = "break expected"; break;
- case 35: s = "return expected"; break;
- case 36: s = ":= expected"; break;
- case 37: s = "new expected"; break;
- case 38: s = "havoc expected"; break;
- case 39: s = "while expected"; break;
- case 40: s = "invariant expected"; break;
- case 41: s = "decreases expected"; break;
- case 42: s = "* expected"; break;
- case 43: s = "call expected"; break;
- case 44: s = "foreach expected"; break;
- case 45: s = "in expected"; break;
- case 46: s = "| expected"; break;
- case 47: s = "assert expected"; break;
- case 48: s = "assume expected"; break;
- case 49: s = "<==> expected"; break;
- case 50: s = "\\u21d4 expected"; break;
- case 51: s = "==> expected"; break;
- case 52: s = "\\u21d2 expected"; break;
- case 53: s = "&& expected"; break;
- case 54: s = "\\u2227 expected"; break;
- case 55: s = "|| expected"; break;
- case 56: s = "\\u2228 expected"; break;
- case 57: s = "== expected"; break;
- case 58: s = "<= expected"; break;
- case 59: s = ">= expected"; break;
- case 60: s = "!= expected"; break;
- case 61: s = "!! expected"; break;
- case 62: s = "!in expected"; break;
- case 63: s = "\\u2260 expected"; break;
- case 64: s = "\\u2264 expected"; break;
- case 65: s = "\\u2265 expected"; break;
- case 66: s = "+ expected"; break;
- case 67: s = "- expected"; break;
- case 68: s = "/ expected"; break;
- case 69: s = "% expected"; break;
- case 70: s = "! expected"; break;
- case 71: s = "\\u00ac expected"; break;
- case 72: s = "false expected"; break;
- case 73: s = "true expected"; break;
- case 74: s = "null expected"; break;
- case 75: s = "fresh expected"; break;
- case 76: s = "[ expected"; break;
- case 77: s = "] expected"; break;
- case 78: s = ". expected"; break;
- case 79: s = ".. expected"; break;
- case 80: s = "this expected"; break;
- case 81: s = "old expected"; break;
- case 82: s = "forall expected"; break;
- case 83: s = "\\u2200 expected"; break;
- case 84: s = "exists expected"; break;
- case 85: s = "\\u2203 expected"; break;
- case 86: s = ":: expected"; break;
- case 87: s = "\\u2022 expected"; break;
- case 88: s = "??? expected"; break;
- case 89: s = "invalid ClassMemberDecl"; break;
- case 90: s = "invalid FunctionDecl"; break;
- case 91: s = "invalid MethodDecl"; break;
- case 92: s = "invalid TypeAndToken"; break;
- case 93: s = "invalid MethodSpec"; break;
- case 94: s = "invalid MethodSpec"; break;
- case 95: s = "invalid ReferenceType"; break;
- case 96: s = "invalid FunctionSpec"; break;
- case 97: s = "invalid ExtendedExpr"; break;
- case 98: s = "invalid IfThenElseExpr"; break;
- case 99: s = "invalid Stmt"; break;
- case 100: s = "invalid OneStmt"; break;
- case 101: s = "invalid IfStmt"; break;
- case 102: s = "invalid ForeachStmt"; break;
- case 103: s = "invalid AssignRhs"; break;
- case 104: s = "invalid Guard"; break;
- case 105: s = "invalid CallStmtSubExpr"; break;
- case 106: s = "invalid EquivOp"; break;
- case 107: s = "invalid ImpliesOp"; break;
- case 108: s = "invalid AndOp"; break;
- case 109: s = "invalid OrOp"; break;
- case 110: s = "invalid RelOp"; break;
- case 111: s = "invalid AddOp"; break;
- case 112: s = "invalid UnaryExpression"; break;
- case 113: s = "invalid MulOp"; break;
- case 114: s = "invalid NegOp"; break;
- case 115: s = "invalid SelectExpression"; break;
- case 116: s = "invalid ConstAtomExpression"; break;
- case 117: s = "invalid ObjectExpression"; break;
- case 118: s = "invalid ObjectExpression"; break;
- case 119: s = "invalid SelectOrCallSuffix"; break;
- case 120: s = "invalid SelectOrCallSuffix"; break;
- case 121: s = "invalid QuantifierGuts"; break;
- case 122: s = "invalid Forall"; break;
- case 123: s = "invalid Exists"; break;
- case 124: s = "invalid QSep"; break;
- case 125: s = "invalid AttributeOrTrigger"; break;
- case 126: s = "invalid AttributeArg"; break;
+ case 33: s = "match expected"; break;
+ case 34: s = "case expected"; break;
+ case 35: s = "=> expected"; break;
+ case 36: s = "label expected"; break;
+ case 37: s = "break expected"; break;
+ case 38: s = "return expected"; break;
+ case 39: s = ":= expected"; break;
+ case 40: s = "new expected"; break;
+ case 41: s = "havoc expected"; break;
+ case 42: s = "while expected"; break;
+ case 43: s = "invariant expected"; break;
+ case 44: s = "decreases expected"; break;
+ case 45: s = "* expected"; break;
+ case 46: s = "call expected"; break;
+ case 47: s = "foreach expected"; break;
+ case 48: s = "in expected"; break;
+ case 49: s = "| expected"; break;
+ case 50: s = "assert expected"; break;
+ case 51: s = "assume expected"; break;
+ case 52: s = "<==> expected"; break;
+ case 53: s = "\\u21d4 expected"; break;
+ case 54: s = "==> expected"; break;
+ case 55: s = "\\u21d2 expected"; break;
+ case 56: s = "&& expected"; break;
+ case 57: s = "\\u2227 expected"; break;
+ case 58: s = "|| expected"; break;
+ case 59: s = "\\u2228 expected"; break;
+ case 60: s = "== expected"; break;
+ case 61: s = "<= expected"; break;
+ case 62: s = ">= expected"; break;
+ case 63: s = "!= expected"; break;
+ case 64: s = "!! expected"; break;
+ case 65: s = "!in expected"; break;
+ case 66: s = "\\u2260 expected"; break;
+ case 67: s = "\\u2264 expected"; break;
+ case 68: s = "\\u2265 expected"; break;
+ case 69: s = "+ expected"; break;
+ case 70: s = "- expected"; break;
+ case 71: s = "/ expected"; break;
+ case 72: s = "% expected"; break;
+ case 73: s = "! expected"; break;
+ case 74: s = "\\u00ac expected"; break;
+ case 75: s = "false expected"; break;
+ case 76: s = "true expected"; break;
+ case 77: s = "null expected"; break;
+ case 78: s = "# expected"; break;
+ case 79: s = ". expected"; break;
+ case 80: s = "fresh expected"; break;
+ case 81: s = "[ expected"; break;
+ case 82: s = "] expected"; break;
+ case 83: s = ".. expected"; break;
+ case 84: s = "this expected"; break;
+ case 85: s = "old expected"; break;
+ case 86: s = "forall expected"; break;
+ case 87: s = "\\u2200 expected"; break;
+ case 88: s = "exists expected"; break;
+ case 89: s = "\\u2203 expected"; break;
+ case 90: s = ":: expected"; break;
+ case 91: s = "\\u2022 expected"; break;
+ case 92: s = "??? expected"; break;
+ case 93: s = "invalid ClassMemberDecl"; break;
+ case 94: s = "invalid FunctionDecl"; break;
+ case 95: s = "invalid MethodDecl"; break;
+ case 96: s = "invalid TypeAndToken"; break;
+ case 97: s = "invalid MethodSpec"; break;
+ case 98: s = "invalid MethodSpec"; break;
+ case 99: s = "invalid ReferenceType"; break;
+ case 100: s = "invalid FunctionSpec"; break;
+ case 101: s = "invalid FunctionBody"; break;
+ case 102: s = "invalid IfThenElseExpr"; break;
+ case 103: s = "invalid MatchExpression"; break;
+ case 104: s = "invalid ExtendedExpr"; break;
+ case 105: s = "invalid Stmt"; break;
+ case 106: s = "invalid OneStmt"; break;
+ case 107: s = "invalid IfStmt"; break;
+ case 108: s = "invalid ForeachStmt"; break;
+ case 109: s = "invalid AssignRhs"; break;
+ case 110: s = "invalid Guard"; break;
+ case 111: s = "invalid CallStmtSubExpr"; break;
+ case 112: s = "invalid EquivOp"; break;
+ case 113: s = "invalid ImpliesOp"; break;
+ case 114: s = "invalid AndOp"; break;
+ case 115: s = "invalid OrOp"; break;
+ case 116: s = "invalid RelOp"; break;
+ case 117: s = "invalid AddOp"; break;
+ case 118: s = "invalid UnaryExpression"; break;
+ case 119: s = "invalid MulOp"; break;
+ case 120: s = "invalid NegOp"; break;
+ case 121: s = "invalid SelectExpression"; break;
+ case 122: s = "invalid ConstAtomExpression"; break;
+ case 123: s = "invalid ObjectExpression"; break;
+ case 124: s = "invalid ObjectExpression"; break;
+ case 125: s = "invalid SelectOrCallSuffix"; break;
+ case 126: s = "invalid SelectOrCallSuffix"; break;
+ case 127: s = "invalid QuantifierGuts"; break;
+ case 128: s = "invalid Forall"; break;
+ case 129: s = "invalid Exists"; break;
+ case 130: s = "invalid QSep"; break;
+ case 131: s = "invalid AttributeOrTrigger"; break;
+ case 132: s = "invalid AttributeArg"; break;
default: s = "error " + n; break;
}
@@ -1698,20 +1786,20 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
static bool[,]! set = {
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,T,x,T, x,T,T,T, x,x,T,T, x,x,x,T, T,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,T,x,T, x,T,T,T, x,x,T,T, x,x,x,T, T,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,x,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},
- {x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, T,T,x,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,T,x,T, x,x,x,x, T,T,T,x, x,T,T,x, x,x,T,T, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, T,T,x,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,T,x,T, x,x,x,x, T,T,T,x, x,T,T,x, x,x,T,T, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, T,T,x,x, T,T,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},
+ {x,x,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, T,T,x,x, T,T,x,x, x,x,x,x, x,x}
};
diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc index 24ccb44e..26a7b965 100644 --- a/Source/Dafny/Printer.ssc +++ b/Source/Dafny/Printer.ssc @@ -128,6 +128,8 @@ namespace Microsoft.Dafny { PrintType(f.ResultType);
if (f.Body == null) {
wr.WriteLine(";");
+ } else {
+ wr.WriteLine();
}
foreach (Expression r in f.Req) {
Indent(2 * IndentAmount);
@@ -374,7 +376,7 @@ namespace Microsoft.Dafny { } else if (stmt is ForeachStmt) {
ForeachStmt s = (ForeachStmt)stmt;
- wr.Write("foreach ({0} in ", s.BoundVar);
+ wr.Write("foreach ({0} in ", s.BoundVar.Name);
PrintExpression(s.Collection);
if (!LiteralExpr.IsTrue(s.Range)) {
wr.Write(" | ");
@@ -392,6 +394,7 @@ namespace Microsoft.Dafny { PrintStatement(s.BodyAssign, ind);
wr.WriteLine();
}
+ Indent(indent);
wr.Write("}");
} else {
@@ -435,6 +438,33 @@ namespace Microsoft.Dafny { els = ite.Els;
}
PrintExtendedExpr(els, ind);
+ } else if (expr is MatchExpr) {
+ MatchExpr me = (MatchExpr)expr;
+ wr.Write("match ");
+ PrintExpression(me.Source);
+ bool needsCurlies = exists{MatchCase mc in me.Cases; mc.Body is MatchExpr};
+ wr.WriteLine(needsCurlies ? " {" : "");
+ int caseInd = ind + (needsCurlies ? IndentAmount : 0);
+ foreach (MatchCase mc in me.Cases) {
+ 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.Name);
+ sep = ", ";
+ }
+ wr.Write(")");
+ }
+ wr.WriteLine(" =>");
+ Indent(caseInd + IndentAmount);
+ PrintExpression(mc.Body);
+ wr.WriteLine();
+ }
+ if (needsCurlies) {
+ Indent(ind);
+ wr.WriteLine("}");
+ }
} else {
PrintExpression(expr, ind);
wr.WriteLine();
@@ -476,6 +506,15 @@ namespace Microsoft.Dafny { } else if (expr is IdentifierExpr) {
wr.Write(((IdentifierExpr)expr).Name);
+ } else if (expr is DatatypeValue) {
+ DatatypeValue dtv = (DatatypeValue)expr;
+ wr.Write("#{0}.{1}", dtv.DatatypeName, dtv.MemberName);
+ if (dtv.Arguments.Count != 0) {
+ wr.Write("(");
+ PrintExpressionList(dtv.Arguments);
+ wr.Write(")");
+ }
+
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
wr.Write(e is SetDisplayExpr ? "{" : "[");
@@ -681,6 +720,8 @@ namespace Microsoft.Dafny { } else if (expr is ITEExpr) {
assert false; // ITE is an extended expression and should be printed only using PrintExtendedExpr
+ } else if (expr is MatchExpr) {
+ assert false; // MatchExpr is an extended expression and should be printed only using PrintExtendedExpr
} else {
assert false; // unexpected expression
}
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 367c81aa..c89e925a 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -1030,6 +1030,54 @@ namespace Microsoft.Dafny { } else {
expr.Type = e.Var.Type;
}
+
+ } else if (expr is DatatypeValue) {
+ DatatypeValue dtv = (DatatypeValue)expr;
+ TopLevelDecl d;
+ if (!classes.TryGetValue(dtv.DatatypeName, out d)) {
+ Error(expr.tok, "Undeclared datatype: {0}", dtv.DatatypeName);
+ } else if (!(d is DatatypeDecl)) {
+ Error(expr.tok, "Expected datatype, found class: {0}", dtv.DatatypeName);
+ } else {
+ // this resolution is a little special, in that the syntax shows only the base name, not its instantiation (which is inferred)
+ DatatypeDecl dt = (DatatypeDecl)d;
+ List<Type!> gt = new List<Type!>(dt.TypeArgs.Count);
+ Dictionary<TypeParameter!,Type!> subst = new Dictionary<TypeParameter!,Type!>();
+ for (int i = 0; i < dt.TypeArgs.Count; i++) {
+ Type t = new InferredTypeProxy();
+ gt.Add(t);
+ subst.Add(dt.TypeArgs[i], t);
+ }
+ expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt);
+ ResolveType(expr.Type);
+
+ DatatypeCtor ctor;
+ if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {
+ Error(expr.tok, "undeclared constructor {0} in datatype {1}", dtv.MemberName, dtv.DatatypeName);
+ } else {
+ assert ctor != null; // follows from postcondition of TryGetValue
+ dtv.Ctor = ctor;
+ if (ctor.Formals.Count != dtv.Arguments.Count) {
+ Error(expr.tok, "wrong number of arguments to datatype constructor {0} (found {1}, expected {2})", dtv.DatatypeName, dtv.Arguments.Count, ctor.Formals.Count);
+ }
+ // add the constructor's own type parameters to the substitution map
+ foreach (TypeParameter p in ctor.TypeArgs) {
+ subst.Add(p, new ParamTypeProxy(p));
+ }
+ }
+ int j = 0;
+ foreach (Expression arg in dtv.Arguments) {
+ ResolveExpression(arg, twoState);
+ assert arg.Type != null; // follows from postcondition of ResolveExpression
+ if (ctor != null && j < ctor.Formals.Count) {
+ Type st = SubstType(ctor.Formals[j].Type, subst);
+ if (!UnifyTypes(arg.Type, st)) {
+ Error(arg.tok, "incorrect type of datatype constructor argument (found {0}, expected {1})", arg.Type, st);
+ }
+ }
+ j++;
+ }
+ }
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
@@ -1355,6 +1403,91 @@ namespace Microsoft.Dafny { Error(expr, "the else branch of an if-then-else expression must be a boolean (instead got {0})", e.Els.Type);
}
expr.Type = Type.Bool;
+
+ } else if (expr is MatchExpr) {
+ MatchExpr me = (MatchExpr)expr;
+ assert !twoState; // currently, match expressions are allowed only at the outermost level of function bodies
+ ResolveExpression(me.Source, twoState);
+ assert me.Source.Type != null; // follows from postcondition of ResolveExpression
+ UserDefinedType sourceType = null;
+ DatatypeDecl dtd = null;
+ Dictionary<TypeParameter!,Type!> subst = new Dictionary<TypeParameter!,Type!>();
+ if (me.Source.Type.IsDatatype) {
+ sourceType = (UserDefinedType)me.Source.Type;
+ dtd = (DatatypeDecl!)sourceType.ResolvedClass;
+ }
+ Dictionary<string!,DatatypeCtor!> ctors;
+ if (dtd == null) {
+ Error(me.Source, "the type of the match source expression must be a datatype");
+ ctors = null;
+ } else {
+ assert sourceType != null; // dtd and sourceType are set together above
+ ctors = datatypeCtors[dtd];
+ 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");
+ }
+
+ // 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]);
+ }
+ }
+
+ Dictionary<string!,object> memberNamesUsed = new Dictionary<string!,object>(); // this is really a set
+ expr.Type = new InferredTypeProxy();
+ foreach (MatchCase mc in me.Cases) {
+ DatatypeCtor ctor = null;
+ if (ctors != null) {
+ 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 {
+ 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.Arguments.Count, ctor.Formals.Count);
+ }
+ if (memberNamesUsed.ContainsKey(mc.Id)) {
+ Error(mc.tok, "member {0} appears in more than one case", mc.Id);
+ } else {
+ memberNamesUsed.Add(mc.Id, null); // add mc.Id to the set of names used
+ }
+ }
+ }
+ scope.PushMarker();
+ if (ctor != null) {
+ // add the constructor's own type parameters to the substitution map
+ foreach (TypeParameter p in ctor.TypeArgs) {
+ subst.Add(p, new ParamTypeProxy(p));
+ }
+ }
+ 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.Type);
+ if (ctor != null && i < ctor.Formals.Count) {
+ Type st = SubstType(ctor.Formals[i].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++;
+ }
+ ResolveExpression(mc.Body, twoState);
+ 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) {
+ Error(expr, "match expression does not cover all constructors");
+ }
} else {
assert false; // unexpected expression
diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc index 9c5f0886..1e0e8e8f 100644 --- a/Source/Dafny/Scanner.ssc +++ b/Source/Dafny/Scanner.ssc @@ -30,20 +30,21 @@ public class Scanner { [Microsoft.Contracts.Verify(false)]
static Scanner() {
- start[0] = 52;
- start[33] = 31;
+ start[0] = 54;
+ start[33] = 32;
start[34] = 3;
- start[37] = 42;
- start[38] = 25;
+ start[35] = 45;
+ start[37] = 43;
+ start[38] = 26;
start[39] = 1;
start[40] = 12;
start[41] = 13;
- start[42] = 15;
- start[43] = 39;
+ start[42] = 17;
+ start[43] = 40;
start[44] = 8;
- start[45] = 40;
+ start[45] = 41;
start[46] = 46;
- start[47] = 41;
+ start[47] = 42;
start[48] = 2;
start[49] = 2;
start[50] = 2;
@@ -57,7 +58,7 @@ public class Scanner { start[58] = 9;
start[59] = 7;
start[60] = 10;
- start[61] = 21;
+ start[61] = 14;
start[62] = 11;
start[63] = 1;
start[65] = 1;
@@ -86,9 +87,9 @@ public class Scanner { start[88] = 1;
start[89] = 1;
start[90] = 1;
- start[91] = 44;
+ start[91] = 47;
start[92] = 1;
- start[93] = 45;
+ start[93] = 48;
start[95] = 1;
start[96] = 1;
start[97] = 1;
@@ -118,21 +119,21 @@ public class Scanner { start[121] = 1;
start[122] = 1;
start[123] = 5;
- start[124] = 16;
+ start[124] = 18;
start[125] = 6;
- start[172] = 43;
- start[8226] = 51;
- start[8658] = 24;
- start[8660] = 20;
- start[8704] = 48;
- start[8707] = 49;
- start[8743] = 27;
- start[8744] = 29;
- start[8800] = 36;
- start[8804] = 37;
- start[8805] = 38;
+ start[172] = 44;
+ start[8226] = 53;
+ start[8658] = 25;
+ start[8660] = 22;
+ start[8704] = 50;
+ start[8707] = 51;
+ start[8743] = 28;
+ start[8744] = 30;
+ start[8800] = 37;
+ start[8804] = 38;
+ start[8805] = 39;
}
- const int noSym = 88;
+ const int noSym = 92;
static short[] start = new short[16385];
@@ -294,27 +295,29 @@ public class Scanner { case "reads": t.kind = 30; break;
case "if": t.kind = 31; break;
case "else": t.kind = 32; break;
- case "label": t.kind = 33; break;
- case "break": t.kind = 34; break;
- case "return": t.kind = 35; break;
- case "new": t.kind = 37; break;
- case "havoc": t.kind = 38; break;
- case "while": t.kind = 39; break;
- case "invariant": t.kind = 40; break;
- case "decreases": t.kind = 41; break;
- case "call": t.kind = 43; break;
- case "foreach": t.kind = 44; break;
- case "in": t.kind = 45; break;
- case "assert": t.kind = 47; break;
- case "assume": t.kind = 48; break;
- case "false": t.kind = 72; break;
- case "true": t.kind = 73; break;
- case "null": t.kind = 74; break;
- case "fresh": t.kind = 75; break;
- case "this": t.kind = 80; break;
- case "old": t.kind = 81; break;
- case "forall": t.kind = 82; break;
- case "exists": t.kind = 84; break;
+ case "match": t.kind = 33; break;
+ case "case": t.kind = 34; break;
+ case "label": t.kind = 36; break;
+ case "break": t.kind = 37; break;
+ case "return": t.kind = 38; break;
+ case "new": t.kind = 40; break;
+ case "havoc": t.kind = 41; break;
+ case "while": t.kind = 42; break;
+ case "invariant": t.kind = 43; break;
+ case "decreases": t.kind = 44; break;
+ case "call": t.kind = 46; break;
+ case "foreach": t.kind = 47; break;
+ case "in": t.kind = 48; break;
+ case "assert": t.kind = 50; break;
+ case "assume": t.kind = 51; break;
+ case "false": t.kind = 75; break;
+ case "true": t.kind = 76; break;
+ case "null": t.kind = 77; break;
+ case "fresh": t.kind = 80; break;
+ case "this": t.kind = 84; break;
+ case "old": t.kind = 85; break;
+ case "forall": t.kind = 86; break;
+ case "exists": t.kind = 88; break;
default: break;
}
@@ -352,107 +355,112 @@ public class Scanner { case 8:
{t.kind = 10; goto done;}
case 9:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 14;}
- else if (ch == ':') {buf.Append(ch); NextCh(); goto case 50;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 16;}
+ else if (ch == ':') {buf.Append(ch); NextCh(); goto case 52;}
else {t.kind = 11; goto done;}
case 10:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 17;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 19;}
else {t.kind = 12; goto done;}
case 11:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 30;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 31;}
else {t.kind = 13; goto done;}
case 12:
{t.kind = 21; goto done;}
case 13:
{t.kind = 22; goto done;}
case 14:
- {t.kind = 36; goto done;}
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 15;}
+ else if (ch == '=') {buf.Append(ch); NextCh(); goto case 23;}
+ else {t.kind = noSym; goto done;}
case 15:
- {t.kind = 42; goto done;}
+ {t.kind = 35; goto done;}
case 16:
- if (ch == '|') {buf.Append(ch); NextCh(); goto case 28;}
- else {t.kind = 46; goto done;}
+ {t.kind = 39; goto done;}
case 17:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 18;}
- else {t.kind = 58; goto done;}
+ {t.kind = 45; goto done;}
case 18:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 19;}
- else {t.kind = noSym; goto done;}
+ if (ch == '|') {buf.Append(ch); NextCh(); goto case 29;}
+ else {t.kind = 49; goto done;}
case 19:
- {t.kind = 49; goto done;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}
+ else {t.kind = 61; goto done;}
case 20:
- {t.kind = 50; goto done;}
- case 21:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 22;}
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 21;}
else {t.kind = noSym; goto done;}
+ case 21:
+ {t.kind = 52; goto done;}
case 22:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 23;}
- else {t.kind = 57; goto done;}
+ {t.kind = 53; goto done;}
case 23:
- {t.kind = 51; goto done;}
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 24;}
+ else {t.kind = 60; goto done;}
case 24:
- {t.kind = 52; goto done;}
+ {t.kind = 54; goto done;}
case 25:
- if (ch == '&') {buf.Append(ch); NextCh(); goto case 26;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 55; goto done;}
case 26:
- {t.kind = 53; goto done;}
+ if (ch == '&') {buf.Append(ch); NextCh(); goto case 27;}
+ else {t.kind = noSym; goto done;}
case 27:
- {t.kind = 54; goto done;}
+ {t.kind = 56; goto done;}
case 28:
- {t.kind = 55; goto done;}
+ {t.kind = 57; goto done;}
case 29:
- {t.kind = 56; goto done;}
+ {t.kind = 58; goto done;}
case 30:
{t.kind = 59; goto done;}
case 31:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 32;}
- else if (ch == '!') {buf.Append(ch); NextCh(); goto case 33;}
- else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 34;}
- else {t.kind = 70; goto done;}
+ {t.kind = 62; goto done;}
case 32:
- {t.kind = 60; goto done;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 33;}
+ else if (ch == '!') {buf.Append(ch); NextCh(); goto case 34;}
+ else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 35;}
+ else {t.kind = 73; goto done;}
case 33:
- {t.kind = 61; goto done;}
+ {t.kind = 63; goto done;}
case 34:
- if (ch == 'n') {buf.Append(ch); NextCh(); goto case 35;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 64; goto done;}
case 35:
- {t.kind = 62; goto done;}
+ if (ch == 'n') {buf.Append(ch); NextCh(); goto case 36;}
+ else {t.kind = noSym; goto done;}
case 36:
- {t.kind = 63; goto done;}
+ {t.kind = 65; goto done;}
case 37:
- {t.kind = 64; goto done;}
+ {t.kind = 66; goto done;}
case 38:
- {t.kind = 65; goto done;}
+ {t.kind = 67; goto done;}
case 39:
- {t.kind = 66; goto done;}
+ {t.kind = 68; goto done;}
case 40:
- {t.kind = 67; goto done;}
+ {t.kind = 69; goto done;}
case 41:
- {t.kind = 68; goto done;}
+ {t.kind = 70; goto done;}
case 42:
- {t.kind = 69; goto done;}
- case 43:
{t.kind = 71; goto done;}
+ case 43:
+ {t.kind = 72; goto done;}
case 44:
- {t.kind = 76; goto done;}
+ {t.kind = 74; goto done;}
case 45:
- {t.kind = 77; goto done;}
+ {t.kind = 78; goto done;}
case 46:
- if (ch == '.') {buf.Append(ch); NextCh(); goto case 47;}
- else {t.kind = 78; goto done;}
+ if (ch == '.') {buf.Append(ch); NextCh(); goto case 49;}
+ else {t.kind = 79; goto done;}
case 47:
- {t.kind = 79; goto done;}
+ {t.kind = 81; goto done;}
case 48:
- {t.kind = 83; goto done;}
+ {t.kind = 82; goto done;}
case 49:
- {t.kind = 85; goto done;}
+ {t.kind = 83; goto done;}
case 50:
- {t.kind = 86; goto done;}
- case 51:
{t.kind = 87; goto done;}
- case 52: {t.kind = 0; goto done;}
+ case 51:
+ {t.kind = 89; goto done;}
+ case 52:
+ {t.kind = 90; goto done;}
+ case 53:
+ {t.kind = 91; goto done;}
+ case 54: {t.kind = 0; goto done;}
}
done:
t.val = buf.ToString();
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index 6d586bf3..6e9030c3 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -9,7 +9,6 @@ using Microsoft.Contracts; using Bpl = Microsoft.Boogie;
using System.Text;
-// TODO: wellformedness checks for function bodies
// TODO: totality checks for statements
// TODO: totality checks for pre/post conditions
@@ -110,6 +109,7 @@ namespace Microsoft.Dafny { public readonly Bpl.Constant! CevHeapName;
public readonly Bpl.Type! ClassNameType;
public readonly Bpl.Type! DatatypeType;
+ public readonly Bpl.Type! DtCtorId;
public readonly Bpl.Expr! Null;
private readonly Bpl.Constant! allocField;
public Bpl.IdentifierExpr! Alloc(Token! tok) {
@@ -118,7 +118,7 @@ namespace Microsoft.Dafny { public PredefinedDecls(Bpl.TypeCtorDecl! refType, Bpl.TypeCtorDecl! boxType, Bpl.TypeCtorDecl! cevTokenType, Bpl.TypeCtorDecl! cevVariableKind, Bpl.TypeCtorDecl! cevEventType,
Bpl.TypeSynonymDecl! setTypeCtor, Bpl.TypeCtorDecl! seqTypeCtor, Bpl.TypeCtorDecl! fieldNameType,
- Bpl.GlobalVariable! heap, Bpl.TypeCtorDecl! classNameType, Bpl.TypeCtorDecl! datatypeType,
+ Bpl.GlobalVariable! heap, Bpl.TypeCtorDecl! classNameType, Bpl.TypeCtorDecl! datatypeType, Bpl.TypeCtorDecl! dtCtorId,
Bpl.Constant! allocField, Bpl.Constant! cevHeapNameConst) {
Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());
this.RefType = refT;
@@ -134,6 +134,7 @@ namespace Microsoft.Dafny { this.CevHeapName = cevHeapNameConst;
this.ClassNameType = new Bpl.CtorType(Token.NoToken, classNameType, new Bpl.TypeSeq());
this.DatatypeType = new Bpl.CtorType(Token.NoToken, datatypeType, new Bpl.TypeSeq());
+ this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq());
this.allocField = allocField;
this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);
}
@@ -154,6 +155,7 @@ namespace Microsoft.Dafny { Bpl.TypeCtorDecl fieldNameType = null;
Bpl.TypeCtorDecl classNameType = null;
Bpl.TypeCtorDecl datatypeType = null;
+ Bpl.TypeCtorDecl dtCtorId = null;
Bpl.TypeCtorDecl boxType = null;
Bpl.GlobalVariable heap = null;
Bpl.Constant allocField = null;
@@ -169,6 +171,8 @@ namespace Microsoft.Dafny { classNameType = dt;
} else if (dt.Name == "DatatypeType") {
datatypeType = dt;
+ } else if (dt.Name == "DtCtorId") {
+ dtCtorId = dt;
} else if (dt.Name == "ref") {
refType = dt;
} else if (dt.Name == "BoxType") {
@@ -209,6 +213,8 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName");
} else if (datatypeType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType");
+ } else if (dtCtorId == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type DtCtorId");
} else if (refType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type ref");
} else if (boxType == null) {
@@ -227,7 +233,7 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of constant #loc.$Heap");
} else {
return new PredefinedDecls(refType, boxType, cevTokenType, cevVariableKind, cevEventType,
- setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType,
+ setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
allocField, cevHeapNameConst);
}
return null;
@@ -259,11 +265,10 @@ namespace Microsoft.Dafny { return new Bpl.Program();
}
foreach (TopLevelDecl d in program.Classes) {
- if (d is ClassDecl) {
- AddClassMembers((ClassDecl)d);
+ if (d is DatatypeDecl) {
+ AddDatatype((DatatypeDecl)d);
} else {
- DatatypeDecl dt = (DatatypeDecl)d;
- // TODO: handle DatatypeDecl
+ AddClassMembers((ClassDecl)d);
}
}
foreach (TopLevelDecl d in program.Classes) {
@@ -285,13 +290,80 @@ namespace Microsoft.Dafny { }
}
} else {
- DatatypeDecl dt = (DatatypeDecl)d;
- // TODO: handle DatatypeDecl
+ assert d is DatatypeDecl;
}
}
return sink;
}
+ void AddDatatype(DatatypeDecl! dt)
+ requires sink != null && predef != null;
+ {
+ foreach (DatatypeCtor ctor in dt.Ctors) {
+ // Add: function #dt.ctor(paramTypes) returns (DatatypeType);
+ Bpl.VariableSeq argTypes = new Bpl.VariableSeq();
+ foreach (Formal arg in ctor.Formals) {
+ Bpl.Variable a = new Bpl.Formal(arg.tok, new Bpl.TypedIdent(arg.tok, Bpl.TypedIdent.NoName, TrType(arg.Type)), true);
+ argTypes.Add(a);
+ }
+ Bpl.Variable resType = new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), false);
+ Bpl.Function fn = new Bpl.Function(ctor.tok, ctor.FullName, argTypes, resType);
+ sink.TopLevelDeclarations.Add(fn);
+ // Add: const unique ##dt.ctor: DtCtorId;
+ Bpl.Constant cid = new Bpl.Constant(ctor.tok, new Bpl.TypedIdent(ctor.tok, "#" + ctor.FullName, predef.DtCtorId), true);
+ sink.TopLevelDeclarations.Add(cid);
+ // Add: axiom (forall params :: DatatypeCtorId(#dt.ctor(params)) == ##dt.ctor);
+ Bpl.VariableSeq! bvs;
+ List<Bpl.Expr!>! args;
+ CreateBoundVariables(ctor.Formals, out bvs, out args);
+ Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
+ lhs = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, lhs);
+ Bpl.Expr q = Bpl.Expr.Eq(lhs, new Bpl.IdentifierExpr(ctor.tok, cid));
+ if (bvs.Length != 0) {
+ q = new Bpl.ForallExpr(ctor.tok, bvs, q);
+ }
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
+ // Add injectivity axioms:
+ int i = 0;
+ foreach (Formal arg in ctor.Formals) {
+ // function ##dt.ctor#i(DatatypeType) returns (Ti);
+ argTypes = new Bpl.VariableSeq();
+ argTypes.Add(new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), true));
+ resType = new Bpl.Formal(arg.tok, new Bpl.TypedIdent(arg.tok, Bpl.TypedIdent.NoName, TrType(arg.Type)), false);
+ fn = new Bpl.Function(ctor.tok, "#" + ctor.FullName + "#" + i, argTypes, resType);
+ sink.TopLevelDeclarations.Add(fn);
+ // axiom (forall params :: ##dt.ctor#i(#dt.ctor(params)) == params_i);
+ CreateBoundVariables(ctor.Formals, out bvs, out args);
+ lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
+ lhs = FunctionCall(ctor.tok, fn.Name, TrType(arg.Type), lhs);
+ q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Eq(lhs, args[i]));
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
+ if (arg.Type.IsDatatype) {
+ // axiom (forall params :: DtRank(params_i) < DtRank(#dt.ctor(params)));
+ CreateBoundVariables(ctor.Formals, out bvs, out args);
+ lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, args[i]);
+ Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
+ rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
+ q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Lt(lhs, rhs));
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
+ }
+ i++;
+ }
+ }
+ }
+
+ void CreateBoundVariables(List<Formal!>! formals, out Bpl.VariableSeq! bvs, out List<Bpl.Expr!>! args)
+ ensures bvs.Length == args.Count;
+ {
+ bvs = new Bpl.VariableSeq();
+ args = new List<Bpl.Expr!>();
+ foreach (Formal arg in formals) {
+ Bpl.Variable bv = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "a" + bvs.Length, TrType(arg.Type)));
+ bvs.Add(bv);
+ args.Add(new Bpl.IdentifierExpr(arg.tok, bv));
+ }
+ }
+
void AddClassMembers(ClassDecl! c)
requires sink != null && predef != null;
{
@@ -313,49 +385,18 @@ namespace Microsoft.Dafny { if (useFunc != null) {
sink.TopLevelDeclarations.Add(useFunc);
}
- if (f.Body != null) {
- ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
-
- // axiom (forall $Heap, formals :: f#use(formals) && this != null && $IsHeap($Heap) && Pre($Heap,formals) ==> f(formals) == body)
- // The antecedent f#use(formals) is included only if the function has been declared as 'use'.
- // Note, an antecedent $Heap[this,alloc] is intentionally left out: including it would only weaken
- // the axiom. Moreover, leaving it out does not introduce any soundness problem, because the Dafny
- // allocation statement changes only an allocation bit and then re-assumes $IsGoodHeap; so if it is
- // sound after that, then it would also have been sound just before the allocation.
- Bpl.VariableSeq formals = new Bpl.VariableSeq();
- Bpl.ExprSeq args = new Bpl.ExprSeq();
- Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
- formals.Add(bv);
- args.Add(new Bpl.IdentifierExpr(f.tok, bv));
- Bpl.BoundVariable bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
- formals.Add(bvThis);
- Bpl.Expr bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis);
- args.Add(bvThisIdExpr);
- foreach (Formal p in f.Formals) {
- bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
- formals.Add(bv);
- args.Add(new Bpl.IdentifierExpr(p.tok, bv));
- }
- Bpl.Expr ante = Bpl.Expr.And(
- Bpl.Expr.Neq(bvThisIdExpr, predef.Null),
- FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr));
- foreach (Expression req in f.Req) {
- ante = Bpl.Expr.And(ante, etran.TrExpr(req));
+ 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 (MatchCase mc in me.Cases) {
+ assert mc.Ctor != null; // the field is filled in by resolution
+ Bpl.Axiom ax = FunctionAxiom(f, mc.Body, formal, mc.Ctor, mc.Arguments);
+ sink.TopLevelDeclarations.Add(ax);
}
- Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
- Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);
- Bpl.Trigger tr;
- if (f.Use) {
- Bpl.FunctionCall useID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#use", TrType(f.ResultType)));
- Bpl.Expr useAppl = new Bpl.NAryExpr(f.tok, useID, args);
- ante = Bpl.Expr.And(useAppl, ante);
- tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(useAppl));
- } else {
- tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(funcAppl));
- }
- Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
- Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, Bpl.Expr.Eq(funcAppl, etran.TrExpr(f.Body))));
- sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
+
+ } else if (f.Body != null) {
+ Bpl.Axiom ax = FunctionAxiom(f, f.Body, null, null, null);
+ sink.TopLevelDeclarations.Add(ax);
}
} else if (member is Method) {
@@ -369,6 +410,92 @@ namespace Microsoft.Dafny { }
}
+ Bpl.Axiom! FunctionAxiom(Function! f, Expression! body, Formal specializationFormal,
+ DatatypeCtor ctor, List<BoundVar!> specializationReplacementFormals)
+ requires predef != null;
+ requires specializationFormal == null <==> ctor == null;
+ requires specializationFormal == null <==> specializationReplacementFormals == null;
+ {
+ ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
+
+ // axiom (forall $Heap, formals :: f#use(args) && this != null && $IsHeap($Heap) && Pre($Heap,args) ==> f(args) == body)
+ //
+ // 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".
+ // 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" are also replaced by
+ // that expression.
+ //
+ // The antecedent f#use(fff) is included only if the function has been declared as 'use'.
+ //
+ // Note, an antecedent $Heap[this,alloc] is intentionally left out: including it would only weaken
+ // the axiom. Moreover, leaving it out does not introduce any soundness problem, because the Dafny
+ // allocation statement changes only an allocation bit and then re-assumes $IsGoodHeap; so if it is
+ // sound after that, then it would also have been sound just before the allocation.
+ Bpl.VariableSeq formals = new Bpl.VariableSeq();
+ Bpl.ExprSeq args = new Bpl.ExprSeq();
+ Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
+ formals.Add(bv);
+ args.Add(new Bpl.IdentifierExpr(f.tok, bv));
+ Bpl.BoundVariable bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
+ formals.Add(bvThis);
+ Bpl.Expr bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis);
+ args.Add(bvThisIdExpr);
+ DatatypeValue r = null;
+ if (specializationReplacementFormals != null) {
+ assert ctor != null; // follows from if guard and the precondition
+ List<Expression!> rArgs = new List<Expression!>();
+ foreach (BoundVar p in specializationReplacementFormals) {
+ 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);
+ }
+ r = new DatatypeValue(f.tok, ((!)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) {
+ bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
+ formals.Add(bv);
+ args.Add(new Bpl.IdentifierExpr(p.tok, bv));
+ } else {
+ assert r != null; // it is set above
+ args.Add(etran.TrExpr(r));
+ }
+ }
+
+ Bpl.Expr ante = Bpl.Expr.And(
+ Bpl.Expr.Neq(bvThisIdExpr, predef.Null),
+ FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr));
+ foreach (Expression req in f.Req) {
+ ante = Bpl.Expr.And(ante, etran.TrExpr(req));
+ }
+ Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
+ Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);
+ Bpl.Trigger tr;
+ if (f.Use) {
+ Bpl.FunctionCall useID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#use", TrType(f.ResultType)));
+ Bpl.Expr useAppl = new Bpl.NAryExpr(f.tok, useID, args);
+ ante = Bpl.Expr.And(useAppl, ante);
+ tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(useAppl));
+ } else {
+ tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(funcAppl));
+ }
+ Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
+ if (specializationFormal != null) {
+ assert r != null;
+ Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
+ substMap.Add(specializationFormal, r);
+ body = Substitute(body, new ThisExpr(f.tok), substMap);
+ }
+ Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, Bpl.Expr.Eq(funcAppl, etran.TrExpr(body))));
+ return new Bpl.Axiom(f.tok, ax);
+ }
+
void AddAllocationAxiom(Field! f)
requires sink != null && predef != null;
{
@@ -676,16 +803,15 @@ namespace Microsoft.Dafny { req, new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());
sink.TopLevelDeclarations.Add(proc);
- Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
+ Bpl.VariableSeq locals = new Bpl.VariableSeq();
Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
-
- CheckWellformed(f.Body, f, Position.Positive, builder, etran);
+ CheckWellformed(f.Body, f, Position.Positive, locals, builder, etran);
Bpl.Implementation impl = new Bpl.Implementation(f.tok, proc.Name,
typeParams,
Bpl.Formal.StripWhereClauses(proc.InParams),
Bpl.Formal.StripWhereClauses(proc.OutParams),
- localVariables, builder.Collect(f.tok));
+ locals, builder.Collect(f.tok));
sink.TopLevelDeclarations.Add(impl);
}
@@ -736,6 +862,9 @@ namespace Microsoft.Dafny { }
// TODO: check reads permissions and check preconditions
return BplAnd(r, IsTotal(e.Args, etran));
+ } else if (expr is DatatypeValue) {
+ DatatypeValue dtv = (DatatypeValue)expr;
+ return IsTotal(dtv.Arguments, etran);
} else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
return new Bpl.OldExpr(expr.tok, IsTotal(e.E, etran));
@@ -827,7 +956,7 @@ namespace Microsoft.Dafny { }
}
- void CheckWellformed(Expression! expr, Function func, Position pos, Bpl.StmtListBuilder! builder, ExpressionTranslator! etran)
+ void CheckWellformed(Expression! expr, Function func, Position pos, Bpl.VariableSeq! locals, Bpl.StmtListBuilder! builder, ExpressionTranslator! etran)
requires predef != null;
{
if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr) {
@@ -835,102 +964,130 @@ namespace Microsoft.Dafny { } else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
foreach (Expression el in e.Elements) {
- CheckWellformed(el, func, Position.Neither, builder, etran);
+ CheckWellformed(el, func, Position.Neither, locals, builder, etran);
}
} else if (expr is FieldSelectExpr) {
FieldSelectExpr e = (FieldSelectExpr)expr;
- CheckWellformed(e.Obj, func, Position.Neither, builder, etran);
+ CheckWellformed(e.Obj, func, Position.Neither, locals, builder, etran);
CheckNonNull(expr.tok, e.Obj, builder, etran);
if (func != null) {
builder.Add(Assert(expr.tok, InRWClause(expr.tok, etran.TrExpr(e.Obj), func.Reads, etran), "insufficient reads clause to read field"));
}
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
- CheckWellformed(e.Seq, func, Position.Neither, builder, etran);
+ CheckWellformed(e.Seq, func, Position.Neither, locals, builder, etran);
Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr e0 = null;
if (e.E0 != null) {
e0 = etran.TrExpr(e.E0);
- CheckWellformed(e.E0, func, Position.Neither, builder, etran);
+ CheckWellformed(e.E0, func, Position.Neither, locals, builder, etran);
builder.Add(new Bpl.AssertCmd(expr.tok, InSeqRange(expr.tok, e0, seq, null, !e.SelectOne)));
}
if (e.E1 != null) {
- CheckWellformed(e.E1, func, Position.Neither, builder, etran);
+ CheckWellformed(e.E1, func, Position.Neither, locals, builder, etran);
builder.Add(new Bpl.AssertCmd(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, e0, true)));
}
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
- CheckWellformed(e.Seq, func, Position.Neither, builder, etran);
+ CheckWellformed(e.Seq, func, Position.Neither, locals, builder, etran);
Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr index = etran.TrExpr(e.Index);
- CheckWellformed(e.Index, func, Position.Neither, builder, etran);
+ CheckWellformed(e.Index, func, Position.Neither, locals, builder, etran);
builder.Add(new Bpl.AssertCmd(expr.tok, InSeqRange(expr.tok, index, seq, null, false)));
- CheckWellformed(e.Value, func, Position.Neither, builder, etran);
+ CheckWellformed(e.Value, func, Position.Neither, locals, builder, etran);
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
- CheckWellformed(e.Receiver, func, Position.Neither, builder, etran);
+ CheckWellformed(e.Receiver, func, Position.Neither, locals, builder, etran);
CheckNonNull(expr.tok, e.Receiver, builder, etran);
foreach (Expression arg in e.Args) {
- CheckWellformed(arg, func, Position.Neither, builder, etran);
+ CheckWellformed(arg, func, Position.Neither, locals, builder, etran);
}
// TODO: check wellformedness of call (call.reads is subset of reads, and either e.Function returns a boolean and is in a positive position, or e.Function returns something else and the subset is a proper subset)
// TODO: and check preconditions of call
+ } else if (expr is DatatypeValue) {
+ DatatypeValue dtv = (DatatypeValue)expr;
+ foreach (Expression arg in dtv.Arguments) {
+ CheckWellformed(arg, func, Position.Neither, locals, builder, etran);
+ }
} else if (expr is OldExpr || expr is FreshExpr) {
assert false; // unexpected expression in function body
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
- CheckWellformed(e.E, func, e.Op == UnaryExpr.Opcode.Not ? Negate(pos) : Position.Neither, builder, etran);
+ CheckWellformed(e.E, func, e.Op == UnaryExpr.Opcode.Not ? Negate(pos) : Position.Neither, locals, builder, etran);
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
- CheckWellformed(e.E0, func, e.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp ? Negate(pos) : pos, builder, etran);
+ CheckWellformed(e.E0, func, e.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp ? Negate(pos) : pos, locals, builder, etran);
switch (e.ResolvedOp) {
case BinaryExpr.ResolvedOpcode.And:
case BinaryExpr.ResolvedOpcode.Imp:
{
Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
- CheckWellformed(e.E1, func, pos, b, etran);
+ CheckWellformed(e.E1, func, pos, locals, b, etran);
builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.E0), b.Collect(expr.tok), null, null));
}
break;
case BinaryExpr.ResolvedOpcode.Or:
{
Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
- CheckWellformed(e.E1, func, pos, b, etran);
+ CheckWellformed(e.E1, func, pos, locals, b, etran);
builder.Add(new Bpl.IfCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0)), b.Collect(expr.tok), null, null));
}
break;
default:
- CheckWellformed(e.E1, func, pos, builder, etran);
+ CheckWellformed(e.E1, func, pos, locals, builder, etran);
break;
}
} else if (expr is QuantifierExpr) {
-#if TODO
QuantifierExpr e = (QuantifierExpr)expr;
- Bpl.Expr total = IsTotal(e.Body, etran);
- if (total != Bpl.Expr.True) {
- Bpl.VariableSeq bvars = new Bpl.VariableSeq();
- foreach (BoundVar bv in e.BoundVars) {
- // TODO: the following needs to take into account name clashes, for which the Boogie rules are different from the Dafny rules
- bvars.Add(new Bpl.BoundVariable(bv.tok, new Bpl.TypedIdent(bv.tok, bv.UniqueName, TrType(bv.Type))));
- }
- if (expr is ForallExpr) {
- total = new Bpl.ForallExpr(expr.tok, bvars, total);
- } else {
- total = new Bpl.ExistsExpr(expr.tok, bvars, total);
- }
- }
- return total;
-#endif
+ Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
+ foreach (BoundVar bv in e.BoundVars) {
+ VarDecl local = new VarDecl(bv.tok, bv.Name, bv.Type, null);
+ local.type = local.OptionalType; // resolve local here
+ IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);
+ ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here
+ substMap.Add(bv, ie);
+ locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
+ }
+ Expression body = Substitute(e.Body, new ThisExpr(expr.tok), substMap);
+ CheckWellformed(body, func, pos, locals, builder, etran);
+
} else if (expr is ITEExpr) {
-#if TODO
ITEExpr e = (ITEExpr)expr;
- Bpl.Expr total = IsTotal(e.Test, etran);
- total = BplAnd(total, IsTotal(e.Thn, etran));
- total = BplAnd(total, IsTotal(e.Els, etran));
- return total;
-#endif
+ CheckWellformed(e.Test, func, pos, locals, builder, etran);
+ Bpl.StmtListBuilder bThen = new Bpl.StmtListBuilder();
+ Bpl.StmtListBuilder bElse = new Bpl.StmtListBuilder();
+ CheckWellformed(e.Thn, func, pos, locals, bThen, etran);
+ CheckWellformed(e.Els, func, pos, locals, bElse, etran);
+ builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.Test), bThen.Collect(expr.tok), null, bElse.Collect(expr.tok)));
+
+ } else if (expr is MatchExpr) {
+ MatchExpr me = (MatchExpr)expr;
+ CheckWellformed(me.Source, func, pos, locals, builder, etran);
+ Bpl.Expr src = etran.TrExpr(me.Source);
+ foreach (MatchCase mc in me.Cases) {
+ assert mc.Ctor != null; // follows from the fact that mc has been successfully resolved
+ Bpl.ExprSeq args = new Bpl.ExprSeq();
+ for (int i = 0; i < mc.Arguments.Count; i++) {
+ BoundVar p = mc.Arguments[i];
+ Bpl.Variable local = new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
+ locals.Add(local);
+ IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);
+ ie.Var = p; ie.Type = ie.Var.Type; // resolve it here
+
+ Type t = mc.Ctor.Formals[i].Type;
+ args.Add(etran.CondApplyBox(expr.tok, new Bpl.IdentifierExpr(p.tok, local), (!)p.Type, t));
+ }
+ Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(mc.tok, mc.Ctor.FullName, predef.DatatypeType);
+ Bpl.Expr ct = new Bpl.NAryExpr(mc.tok, new Bpl.FunctionCall(id), args);
+
+ // generate: if (src == ctor(args)) { mc.Body is well-formed }
+ Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
+ CheckWellformed(mc.Body, func, pos, locals, b, etran);
+ builder.Add(new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), null, null));
+ }
+
} else {
assert false; // unexpected expression
}
@@ -1575,6 +1732,12 @@ namespace Microsoft.Dafny { Bpl.Expr e1 = FunctionCall(stmt.Tok, BuiltinFunction.SeqLength, null, bf);
eq = Bpl.Expr.Eq(e0, e1);
less = Bpl.Expr.Lt(e0, e1);
+ } else if (ty.IsDatatype) {
+ Bpl.Expr e0 = FunctionCall(stmt.Tok, BuiltinFunction.DtRank, null, d);
+ Bpl.Expr e1 = FunctionCall(stmt.Tok, BuiltinFunction.DtRank, null, bf);
+ eq = Bpl.Expr.Eq(e0, e1);
+ less = Bpl.Expr.Lt(e0, e1);
+
} else {
// reference type
Bpl.Expr e0 = Bpl.Expr.Neq(d, predef.Null);
@@ -1797,10 +1960,11 @@ namespace Microsoft.Dafny { Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, bRhs);
builder.Add(cmd);
} else {
- Bpl.NAryExpr bLhs = (Bpl.NAryExpr)etran.TrExpr(lhs); // TODO: is this cast always justified?
- assert bLhs.Args.Length == 3; // we're expecting h[o,f]
- Bpl.IdentifierExpr h = (Bpl.IdentifierExpr!)bLhs.Args[0]; // TODO: is this cast always justified?
- Bpl.Cmd cmd = Bpl.Cmd.MapAssign(tok, h, (!)bLhs.Args[1], (!)bLhs.Args[2], bRhs);
+ FieldSelectExpr fse = (FieldSelectExpr)lhs;
+ assert fse.Field != null;
+ Bpl.IdentifierExpr h = (Bpl.IdentifierExpr!)etran.HeapExpr; // TODO: is this cast always justified?
+ bRhs = etran.CondApplyBox(tok, bRhs, (!)((ExprRhs)rhs).Expr.Type, fse.Field.Type);
+ Bpl.Cmd cmd = Bpl.Cmd.MapAssign(tok, h, etran.TrExpr(fse.Obj), new Bpl.IdentifierExpr(tok, GetField(fse.Field)), bRhs);
builder.Add(cmd);
// assume $IsGoodHeap($Heap);
builder.Add(AssumeGoodHeap(tok, etran));
@@ -1885,7 +2049,7 @@ namespace Microsoft.Dafny { } else if (expr is IdentifierExpr) {
IdentifierExpr e = (IdentifierExpr)expr;
return TrVar(expr.tok, (!)e.Var);
-
+
} else if (expr is SetDisplayExpr) {
SetDisplayExpr e = (SetDisplayExpr)expr;
Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SetEmpty, predef.BoxType);
@@ -1908,7 +2072,8 @@ namespace Microsoft.Dafny { } else if (expr is FieldSelectExpr) {
FieldSelectExpr e = (FieldSelectExpr)expr;
- return Bpl.Expr.SelectTok(expr.tok, HeapExpr, TrExpr(e.Obj), new Bpl.IdentifierExpr(expr.tok, translator.GetField((!)e.Field)));
+ Bpl.Expr result = Bpl.Expr.SelectTok(expr.tok, HeapExpr, TrExpr(e.Obj), new Bpl.IdentifierExpr(expr.tok, translator.GetField((!)e.Field)));
+ return CondApplyUnbox(expr.tok, result, e.Field.Type, (!)expr.Type);
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
@@ -1957,6 +2122,18 @@ namespace Microsoft.Dafny { Bpl.Expr result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(id), args);
return CondApplyUnbox(expr.tok, result, e.Function.ResultType, expr.Type);
+ } else if (expr is DatatypeValue) {
+ DatatypeValue dtv = (DatatypeValue)expr;
+ assert dtv.Ctor != null; // since dtv has been successfully resolved
+ Bpl.ExprSeq args = new Bpl.ExprSeq();
+ for (int i = 0; i < dtv.Arguments.Count; i++) {
+ Expression arg = dtv.Arguments[i];
+ Type t = dtv.Ctor.Formals[i].Type;
+ args.Add(CondApplyBox(expr.tok, TrExpr(arg), (!)arg.Type, t));
+ }
+ Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(dtv.tok, dtv.Ctor.FullName, predef.DatatypeType);
+ return new Bpl.NAryExpr(dtv.tok, new Bpl.FunctionCall(id), args);
+
} else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
return new Bpl.OldExpr(expr.tok, TrExpr(e.E));
@@ -2377,6 +2554,9 @@ namespace Microsoft.Dafny { TypeTuple,
DeclType,
+ DatatypeCtorId,
+ DtRank,
+
// CEV
CevInit,
CevVarIntro,
@@ -2507,6 +2687,15 @@ namespace Microsoft.Dafny { assert typeInstantiation != null;
return FunctionCall(tok, "DeclType", predef.ClassNameType, args);
+ case BuiltinFunction.DatatypeCtorId:
+ assert args.Length == 1;
+ assert typeInstantiation == null;
+ return FunctionCall(tok, "DatatypeCtorId", predef.DtCtorId, args);
+ case BuiltinFunction.DtRank:
+ assert args.Length == 1;
+ assert typeInstantiation == null;
+ return FunctionCall(tok, "DtRank", Bpl.Type.Int, args);
+
case BuiltinFunction.CevInit:
assert args.Length == 1;
assert typeInstantiation == null;
@@ -2538,6 +2727,15 @@ namespace Microsoft.Dafny { return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, function, returnType)), new Bpl.ExprSeq(args));
}
+ Bpl.NAryExpr! FunctionCall(Token! tok, string! function, Bpl.Type! returnType, List<Bpl.Expr!>! args)
+ {
+ Bpl.ExprSeq aa = new Bpl.ExprSeq();
+ foreach (Bpl.Expr arg in args) {
+ aa.Add(arg);
+ }
+ return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, function, returnType)), aa);
+ }
+
public IEnumerable<Expression!>! SplitExpr(Expression! expr, bool expandFunctions)
requires expr.Type is BoolType;
{
@@ -2594,7 +2792,7 @@ namespace Microsoft.Dafny { } else if (expandFunctions && expr is FunctionCallExpr) {
FunctionCallExpr fexp = (FunctionCallExpr)expr;
assert fexp.Function != null; // filled in during resolution
- if (fexp.Function.Body != null) {
+ if (fexp.Function.Body != null && !(fexp.Function.Body is MatchExpr)) {
// inline this body
Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
assert fexp.Args.Count == fexp.Function.Formals.Count;
@@ -2691,6 +2889,15 @@ namespace Microsoft.Dafny { newExpr = newFce;
}
+ } else if (expr is DatatypeValue) {
+ DatatypeValue dtv = (DatatypeValue)expr;
+ List<Expression!> newArgs = SubstituteExprList(dtv.Arguments, receiverReplacement, substMap);
+ if (newArgs != dtv.Arguments) {
+ DatatypeValue newDtv = new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArgs);
+ newDtv.Ctor = dtv.Ctor; // resolve on the fly (and set newDtv.Type below, at end)
+ newExpr = newDtv;
+ }
+
} else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
Expression se = Substitute(e.E, receiverReplacement, substMap);
diff --git a/Source/DafnyDriver/DafnyDriver.ssc b/Source/DafnyDriver/DafnyDriver.ssc index 8817f761..f0935199 100644 --- a/Source/DafnyDriver/DafnyDriver.ssc +++ b/Source/DafnyDriver/DafnyDriver.ssc @@ -208,7 +208,7 @@ namespace Microsoft.Boogie string err = Dafny.Main.ParseCheck(fileNames, "synthetic program", out dafnyProgram);
if (err != null) {
ErrorWriteLine(err);
- } else if (dafnyProgram != null) {
+ } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {
Dafny.Translator translator = new Dafny.Translator();
Program boogieProgram = translator.Translate(dafnyProgram);
if (CommandLineOptions.Clo.PrintFile != null)
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 9c74a7ea..62457ec4 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -89,7 +89,7 @@ Dafny program verifier finished with 4 verified, 0 errors -------------------- Termination.dfy --------------------
-Dafny program verifier finished with 5 verified, 0 errors
+Dafny program verifier finished with 6 verified, 0 errors
-------------------- Use.dfy --------------------
Use.dfy(12,5): Error BP5001: This assertion might not hold.
@@ -125,4 +125,8 @@ TypeParameters.dfy(63,5): Error BP5001: This assertion might not hold. Execution trace:
(0,0): anon0
-Dafny program verifier finished with 7 verified, 2 errors
+Dafny program verifier finished with 9 verified, 2 errors
+
+-------------------- Datatypes.dfy --------------------
+
+Dafny program verifier finished with 6 verified, 0 errors
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index 4f247c79..61ae9cb6 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -7,25 +7,25 @@ class Node { var data: int;
var next: Node;
- function Repr(list: List<int>)
+ function Repr(list: List<int>): bool
reads this;
{ match list
case Nil =>
next == null
case Cons(d,cdr) =>
- data == d && next.Repr(cdr)
+ data == d && next != null && next.Repr(cdr)
}
method Init()
modifies this;
- ensures Repr(this, #List<int>.Nil);
+ ensures Repr(#List.Nil);
{
next := null;
}
method Add(d: int, L: List<int>) returns (r: Node)
requires Repr(L);
- ensures r.Repr(#List<int>.Cons(d, L));
+ ensures r.Repr(#List.Cons(d, L));
{
r := new Node;
r.data := d;
@@ -37,7 +37,7 @@ class AnotherNode { var data: int;
var next: AnotherNode;
- function Repr(n: AnotherNode, list: List<int>)
+ function Repr(n: AnotherNode, list: List<int>): bool
reads n;
{ match list
case Nil =>
@@ -47,14 +47,14 @@ class AnotherNode { }
method Create() returns (n: AnotherNode)
- ensures Repr(n, #List<int>.Nil);
+ ensures Repr(n, #List.Nil);
{
n := null;
}
method Add(n: AnotherNode, d: int, L: List<int>) returns (r: AnotherNode)
requires Repr(n, L);
- ensures Repr(r, #List<int>.Cons(d, L));
+ ensures Repr(r, #List.Cons(d, L));
{
r := new AnotherNode;
r.data := d;
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index ee9d9613..39361b7b 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -76,4 +76,22 @@ class Termination { }
}
}
+
+ method Q<T>(list: List<T>) {
+ var l := list;
+ while (l != #List.Nil)
+ decreases l;
+ {
+ call x, l := Traverse(l);
+ }
+ }
+
+ method Traverse<T>(a: List<T>) returns (val: T, b: List<T>);
+ requires a != #List.Nil;
+ ensures a == #List.Cons(val, b);
+}
+
+datatype List<T> {
+ Nil;
+ Cons(T, List<T>);
}
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index 794f2f95..680679d4 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -60,6 +60,39 @@ class SequenceTest { {
var s := [2, 5, 3];
call t := Add(s, 7);
- assert [2,5,7,3] == t || [2,5,3] == t;
+ assert [2,5,7,3] == t || [2,5,3] == t; // error
+ }
+}
+
+// -------------------------
+
+class CC<T> {
+ var x: T;
+ method M(c: CC<T>, z: T) returns (y: T)
+ requires c != null;
+ modifies this;
+ ensures y == c.x && x == z;
+ {
+ x := c.x;
+ x := z;
+ y := c.x;
+ }
+}
+
+class CClient {
+ method Main() {
+ var c := new CC<int>;
+ var k := c.x + 3;
+ if (c.x == c.x) {
+ k := k + 1;
+ }
+ var m := c.x;
+ if (m == c.x) {
+ k := k + 1;
+ }
+ c.x := 5;
+ c.x := c.x;
+ call z := c.M(c, 17);
+ assert z == c.x;
}
}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index a6cfa2c0..4fa6832e 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -20,7 +20,7 @@ for %%f in (BQueue.bpl) do ( for %%f in (SmallTests.dfy Queue.dfy ListCopy.dfy
BinaryTree.dfy ListReverse.dfy ListContents.dfy
SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy
- TypeParameters.dfy) do (
+ TypeParameters.dfy Datatypes.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% %* %%f
|