diff options
| -rw-r--r-- | Source/Dafny/Compiler.cs | 13 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 63 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 70 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 336 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 20 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 184 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 67 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 31 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 5 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/ControlStructures.dfy | 14 | ||||
| -rw-r--r-- | Test/dafny0/DTypes.dfy | 10 | ||||
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 10 | ||||
| -rw-r--r-- | Test/dafny0/NatTypes.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/Simple.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 8 | ||||
| -rw-r--r-- | Test/dafny0/Termination.dfy | 12 | ||||
| -rw-r--r-- | Test/dafny0/TypeAntecedents.dfy | 20 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny1/Induction.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny1/Rippling.dfy | 208 | ||||
| -rw-r--r-- | Test/dafny1/SchorrWaite.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny1/Substitution.dfy | 10 | ||||
| -rw-r--r-- | Test/dafny1/TreeDatatype.dfy | 16 |
24 files changed, 703 insertions, 414 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 6dabace1..80e597e5 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -186,15 +186,10 @@ namespace Microsoft.Dafny { // }
Indent(indent);
wr.Write("public class {0}", DtCtorName(ctor));
- if (dt.TypeArgs.Count != 0 || ctor.TypeArgs.Count != 0) {
+ if (dt.TypeArgs.Count != 0) {
wr.Write("<");
- string sep = "";
if (dt.TypeArgs.Count != 0) {
wr.Write("{0}", TypeParameters(dt.TypeArgs));
- sep = ",";
- }
- if (ctor.TypeArgs.Count != 0) {
- wr.Write("{0}{1}", sep, TypeParameters(ctor.TypeArgs));
}
wr.Write(">");
}
@@ -1444,7 +1439,11 @@ namespace Microsoft.Dafny { wr.Write(") : (");
TrExpr(e.Els);
wr.Write(")");
-
+
+ } else if (expr is ConcreteSyntaxExpression) {
+ var e = (ConcreteSyntaxExpression)expr;
+ TrExpr(e.ResolvedExpression);
+
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 388ae8cd..d25000ee 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -304,16 +304,14 @@ DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.> = (. Contract.Requires(cce.NonNullElements(ctors));
Attributes attrs = null;
IToken/*!*/ id;
- List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
List<Formal/*!*/> formals = new List<Formal/*!*/>();
.)
{ Attribute<ref attrs> }
Ident<out id>
- [ GenericParameters<typeArgs> ]
(. parseVarScope.PushMarker(); .)
[ FormalsOptionalIds<formals> ]
(. parseVarScope.PopMarker();
- ctors.Add(new DatatypeCtor(id, id.val, typeArgs, formals, attrs));
+ ctors.Add(new DatatypeCtor(id, id.val, formals, attrs));
.)
.
@@ -1238,15 +1236,23 @@ UnaryExpression<out Expression/*!*/ e> UnaryExpression<out e> (. e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); .)
| NegOp (. x = t; .)
UnaryExpression<out e> (. e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); .)
- | SelectExpression<out e>
+ | EndlessExpression<out e> /* these have no further suffix */
+ | DottedIdentifiersAndFunction<out e>
+ { Suffix<ref e> }
| ConstAtomExpression<out e>
+ { Suffix<ref e> }
)
.
NegOp = "!" | '\u00ac'.
-ConstAtomExpression<out Expression/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x, dtName, id; BigInteger n; List<Expression/*!*/>/*!*/ elements;
+/* A ConstAtomExpression is never an l-value. Also, a ConstAtomExpression is never followed by
+ * an open paren (but could very well have a suffix that starts with a period or a square bracket).
+ * (The "Also..." part may change if expressions in Dafny could yield functions.)
+ */
+ConstAtomExpression<out Expression/*!*/ e>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ IToken/*!*/ x, dtName, id; BigInteger n; List<Expression/*!*/>/*!*/ elements;
Expression e0, e1;
e = dummyExpr;
.)
@@ -1254,17 +1260,13 @@ ConstAtomExpression<out Expression/*!*/ e> | "true" (. e = new LiteralExpr(t, true); .)
| "null" (. e = new LiteralExpr(t); .)
| Nat<out n> (. e = new LiteralExpr(t, n); .)
- | "#" (. x = t; .)
- Ident<out dtName>
- "."
- Ident<out id> (. elements = new List<Expression/*!*/>(); .)
- [ "("
- [ Expressions<elements> ]
- ")" ] (. e = new DatatypeValue(t, dtName.val, id.val, elements); .)
+ | "this" (. e = new ThisExpr(t); .)
| "fresh" (. x = t; .)
"(" Expression<out e> ")" (. e = new FreshExpr(x, e); .)
| "allocated" (. x = t; .)
"(" Expression<out e> ")" (. e = new AllocatedExpr(x, e); .)
+ | "old" (. x = t; .)
+ "(" Expression<out e> ")" (. e = new OldExpr(x, e); .)
| "|" (. x = t; .)
Expression<out e> (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)
"|"
@@ -1274,7 +1276,19 @@ ConstAtomExpression<out Expression/*!*/ e> | "[" (. x = t; elements = new List<Expression/*!*/>(); .)
[ Expressions<elements> ] (. e = new SeqDisplayExpr(x, elements); .)
"]"
- | "if" (. x = t; .)
+ | "(" (. x = t; .)
+ Expression<out e> (. e = new ParensExpression(x, e); .)
+ ")"
+ )
+ .
+
+EndlessExpression<out Expression e>
+= (. IToken/*!*/ x, dtName, id; BigInteger n;
+ List<Expression/*!*/>/*!*/ elements;
+ Expression e0, e1;
+ e = dummyExpr;
+ .)
+ ( "if" (. x = t; .)
Expression<out e>
"then" Expression<out e0>
"else" Expression<out e1> (. e = new ITEExpr(x, e, e0, e1); .)
@@ -1283,6 +1297,7 @@ ConstAtomExpression<out Expression/*!*/ e> )
.
+
/*------------------------------------------------------------------------*/
/* returns one of:
@@ -1307,6 +1322,22 @@ SelectExpression<out Expression/*!*/ e> { SelectOrCallSuffix<ref e> }
.
+DottedIdentifiersAndFunction<out Expression e>
+= (. IToken id; IToken openParen = null;
+ List<Expression> args = null;
+ List<IToken> idents = new List<IToken>();
+ .)
+ Ident<out id> (. idents.Add(id); .)
+ { "."
+ Ident<out id> (. idents.Add(id); .)
+ }
+ [ "(" (. openParen = t; args = new List<Expression>(); .)
+ [ Expressions<args> ]
+ ")"
+ ]
+ (. e = new IdentifierSequence(idents, openParen, args); .)
+ .
+
IdentOrFuncExpression<out Expression/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id; e = dummyExpr; List<Expression/*!*/>/*!*/ args; .)
Ident<out id>
@@ -1323,6 +1354,10 @@ IdentOrFuncExpression<out Expression/*!*/ e> .)
.
+Suffix<ref Expression/*!*/ e>
+= SelectOrCallSuffix<ref e>
+ .
+
SelectOrCallSuffix<ref Expression/*!*/ e>
= (. Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x; List<Expression/*!*/>/*!*/ args;
Expression e0 = null; Expression e1 = null; Expression/*!*/ ee; bool anyDots = false;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index f0a58293..df49e8c7 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -725,28 +725,21 @@ namespace Microsoft.Dafny { }
public class DatatypeCtor : Declaration, TypeParameter.ParentType {
- public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;
public readonly List<Formal/*!*/>/*!*/ Formals;
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(TypeArgs));
Contract.Invariant(cce.NonNullElements(Formals));
}
// TODO: One could imagine having a precondition on datatype constructors
public DatatypeDecl EnclosingDatatype; // filled in during resolution
- public DatatypeCtor(IToken/*!*/ tok, string/*!*/ name, [Captured] List<TypeParameter/*!*/>/*!*/ typeArgs,
- [Captured] List<Formal/*!*/>/*!*/ formals,
- Attributes attributes)
+ public DatatypeCtor(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Formal/*!*/>/*!*/ formals, Attributes attributes)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
- Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(formals));
- this.TypeArgs = typeArgs;
this.Formals = formals;
-
}
public string FullName {
@@ -1235,6 +1228,8 @@ namespace Microsoft.Dafny { if (expr is OldExpr) {
expr = ((OldExpr)expr).E;
+ } else if (expr is ConcreteSyntaxExpression) {
+ expr = ((ConcreteSyntaxExpression)expr).ResolvedExpression;
} else {
break;
}
@@ -1795,6 +1790,20 @@ namespace Microsoft.Dafny { Contract.Invariant(tok != null);
}
+ public Expression Resolved {
+ get {
+ Contract.Requires(type != null); // should be called only on resolved expressions; this approximates that precondition
+ Expression r = this;
+ while (true) {
+ var rr = r as ConcreteSyntaxExpression;
+ if (rr == null) { break; }
+ r = rr.ResolvedExpression;
+ Contract.Assert(r != null); // this is true if the expression is indeed resolved
+ }
+ return r;
+ }
+ }
+
protected Type type;
public Type Type { // filled in during resolution
[Verify(false)] // TODO: how do we allow Type.get to modify type and still be [Pure]?
@@ -1899,7 +1908,6 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullElements(InferredTypeArgs));
}
-
public DatatypeValue(IToken tok, string datatypeName, string memberName, [Captured] List<Expression/*!*/>/*!*/ arguments)
: base(tok) {
Contract.Requires(cce.NonNullElements(arguments));
@@ -2707,7 +2715,6 @@ namespace Microsoft.Dafny { public readonly string FieldName;
public Field Field; // filled in during resolution (but is null if FieldName is)
-
public FrameExpression(Expression e, string fieldName) {
Contract.Requires(e != null);
Contract.Requires(!(e is WildcardExpr) || fieldName == null);
@@ -2716,4 +2723,45 @@ namespace Microsoft.Dafny { FieldName = fieldName;
}
}
-}
\ No newline at end of file +
+ /// <summary>
+ /// This class represents a piece of concrete syntax in the parse tree. During resolution,
+ /// it gets "replaced" by the expression in "ResolvedExpression".
+ /// </summary>
+ public abstract class ConcreteSyntaxExpression : Expression
+ {
+ public Expression ResolvedExpression; // filled in during resolution; after resolution, manipulation of "this" should proceed as with manipulating "this.ResolvedExpression"
+ public ConcreteSyntaxExpression(IToken tok)
+ : base(tok) {
+ }
+ public override IEnumerable<Expression> SubExpressions {
+ get { yield return ResolvedExpression; }
+ }
+ }
+
+ public class ParensExpression : ConcreteSyntaxExpression
+ {
+ public readonly Expression E;
+ public ParensExpression(IToken tok, Expression e)
+ : base(tok) {
+ E = e;
+ }
+ }
+
+ public class IdentifierSequence : ConcreteSyntaxExpression
+ {
+ public readonly List<IToken> Tokens;
+ public readonly IToken OpenParen;
+ public readonly List<Expression> Arguments;
+ public IdentifierSequence(List<IToken> tokens, IToken openParen, List<Expression> args)
+ : base(tokens[0]) {
+ Contract.Requires(tokens != null && 1 <= tokens.Count);
+ /* "args" is null to indicate the absence of a parenthesized suffix */
+ Contract.Requires(args == null || openParen != null);
+
+ Tokens = tokens;
+ OpenParen = openParen;
+ Arguments = args;
+ }
+ }
+}
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index aa02c796..c2af1f2f 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -20,7 +20,7 @@ public class Parser { public const int _digits = 2;
public const int _arrayToken = 3;
public const int _string = 4;
- public const int maxT = 107;
+ public const int maxT = 106;
const bool T = true;
const bool x = false;
@@ -379,7 +379,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! DatatypeMemberDecl(ctors);
}
Expect(15);
- } else SynErr(108);
+ } else SynErr(107);
dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
dt.BodyStartTok = bodyStart;
dt.BodyEndTok = t;
@@ -414,7 +414,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! mm.Add(m);
} else if (la.kind == 20) {
CouplingInvDecl(mmod, mm);
- } else SynErr(109);
+ } else SynErr(108);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -498,7 +498,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
FunctionBody(out bb, out bodyStart, out bodyEnd);
body = bb;
- } else SynErr(110);
+ } else SynErr(109);
parseVarScope.PopMarker();
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
f.BodyStartTok = bodyStart;
@@ -527,7 +527,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! } else if (la.kind == 10) {
Get();
isRefinement = true;
- } else SynErr(111);
+ } else SynErr(110);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
while (la.kind == 7) {
@@ -554,7 +554,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
BlockStmt(out bb, out bodyStart, out bodyEnd);
body = (BlockStmt)bb;
- } else SynErr(112);
+ } else SynErr(111);
parseVarScope.PopMarker();
if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
@@ -600,22 +600,18 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Contract.Requires(cce.NonNullElements(ctors));
Attributes attrs = null;
IToken/*!*/ id;
- List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
List<Formal/*!*/> formals = new List<Formal/*!*/>();
while (la.kind == 7) {
Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 23) {
- GenericParameters(typeArgs);
- }
parseVarScope.PushMarker();
if (la.kind == 32) {
FormalsOptionalIds(formals);
}
parseVarScope.PopMarker();
- ctors.Add(new DatatypeCtor(id, id.val, typeArgs, formals, attrs));
+ ctors.Add(new DatatypeCtor(id, id.val, formals, attrs));
}
@@ -748,7 +744,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! ReferenceType(out tok, out ty);
break;
}
- default: SynErr(113); break;
+ default: SynErr(112); break;
}
}
@@ -799,12 +795,12 @@ List<Expression/*!*/>/*!*/ decreases) { Expression(out e);
Expect(15);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else SynErr(114);
+ } else SynErr(113);
} else if (la.kind == 31) {
Get();
Expressions(decreases);
Expect(15);
- } else SynErr(115);
+ } else SynErr(114);
}
void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -886,7 +882,7 @@ List<Expression/*!*/>/*!*/ decreases) { GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else SynErr(116);
+ } else SynErr(115);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
@@ -918,7 +914,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
Expressions(decreases);
Expect(15);
- } else SynErr(117);
+ } else SynErr(116);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -929,7 +925,7 @@ List<Expression/*!*/>/*!*/ decreases) { MatchExpression(out e);
} else if (StartOf(8)) {
Expression(out e);
- } else SynErr(118);
+ } else SynErr(117);
Expect(8);
bodyEnd = t;
}
@@ -941,7 +937,7 @@ List<Expression/*!*/>/*!*/ decreases) { fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(8)) {
FrameExpression(out fe);
- } else SynErr(119);
+ } else SynErr(118);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -952,7 +948,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new WildcardExpr(t);
} else if (StartOf(8)) {
Expression(out e);
- } else SynErr(120);
+ } else SynErr(119);
}
void MatchExpression(out Expression/*!*/ e) {
@@ -1006,7 +1002,7 @@ List<Expression/*!*/>/*!*/ decreases) { MatchExpression(out e);
} else if (StartOf(8)) {
Expression(out e);
- } else SynErr(121);
+ } else SynErr(120);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1022,7 +1018,7 @@ List<Expression/*!*/>/*!*/ decreases) { ss.Add(s);
} else if (la.kind == 11 || la.kind == 18) {
VarDeclStmts(ss);
- } else SynErr(122);
+ } else SynErr(121);
}
void OneStmt(out Statement/*!*/ s) {
@@ -1046,7 +1042,7 @@ List<Expression/*!*/>/*!*/ decreases) { PrintStmt(out s);
break;
}
- case 1: case 32: case 99: case 100: {
+ case 1: case 32: case 94: case 97: {
AssignStmt(out s, true);
break;
}
@@ -1100,7 +1096,7 @@ List<Expression/*!*/>/*!*/ decreases) { s = new ReturnStmt(x);
break;
}
- default: SynErr(123); break;
+ default: SynErr(122); break;
}
}
@@ -1283,13 +1279,13 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(124);
+ } else SynErr(123);
}
ifStmt = new IfStmt(x, guard, thn, els);
} else if (la.kind == 7) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(125);
+ } else SynErr(124);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1314,7 +1310,7 @@ List<Expression/*!*/>/*!*/ decreases) { LoopSpec(out invariants, out decreases);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives);
- } else SynErr(126);
+ } else SynErr(125);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -1380,7 +1376,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 56) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else SynErr(127);
+ } else SynErr(126);
Expect(8);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1436,7 +1432,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(8)) {
Expression(out e);
ee = new List<Expression>() { e };
- } else SynErr(128);
+ } else SynErr(127);
if (ee == null && ty == null) { ee = new List<Expression>() { dummyExpr}; }
}
@@ -1444,9 +1440,9 @@ List<Expression/*!*/>/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
if (la.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (la.kind == 32 || la.kind == 99 || la.kind == 100) {
+ } else if (la.kind == 32 || la.kind == 94 || la.kind == 97) {
ObjectExpression(out e);
- } else SynErr(129);
+ } else SynErr(128);
while (la.kind == 52 || la.kind == 54) {
SelectOrCallSuffix(ref e);
}
@@ -1493,7 +1489,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(130);
+ } else SynErr(129);
Expect(33);
}
@@ -1586,10 +1582,10 @@ List<Expression/*!*/>/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
if (la.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (la.kind == 32 || la.kind == 99 || la.kind == 100) {
+ } else if (la.kind == 32 || la.kind == 94 || la.kind == 97) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else SynErr(131);
+ } else SynErr(130);
while (la.kind == 52 || la.kind == 54) {
SelectOrCallSuffix(ref e);
}
@@ -1603,7 +1599,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(8)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else SynErr(132);
+ } else SynErr(131);
}
void EquivExpression(out Expression/*!*/ e0) {
@@ -1633,7 +1629,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 69) {
Get();
- } else SynErr(133);
+ } else SynErr(132);
}
void LogicalExpression(out Expression/*!*/ e0) {
@@ -1671,7 +1667,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 71) {
Get();
- } else SynErr(134);
+ } else SynErr(133);
}
void RelationalExpression(out Expression/*!*/ e0) {
@@ -1689,7 +1685,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 73) {
Get();
- } else SynErr(135);
+ } else SynErr(134);
}
void OrOp() {
@@ -1697,7 +1693,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 75) {
Get();
- } else SynErr(136);
+ } else SynErr(135);
}
void Term(out Expression/*!*/ e0) {
@@ -1773,7 +1769,7 @@ List<Expression/*!*/>/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(137); break;
+ default: SynErr(136); break;
}
}
@@ -1795,7 +1791,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 86) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(138);
+ } else SynErr(137);
}
void UnaryExpression(out Expression/*!*/ e) {
@@ -1810,11 +1806,19 @@ List<Expression/*!*/>/*!*/ decreases) { x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
- } else if (StartOf(13)) {
- SelectExpression(out e);
} else if (StartOf(16)) {
+ EndlessExpression(out e);
+ } else if (la.kind == 1) {
+ DottedIdentifiersAndFunction(out e);
+ while (la.kind == 52 || la.kind == 54) {
+ Suffix(ref e);
+ }
+ } else if (StartOf(17)) {
ConstAtomExpression(out e);
- } else SynErr(139);
+ while (la.kind == 52 || la.kind == 54) {
+ Suffix(ref e);
+ }
+ } else SynErr(138);
}
void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
@@ -1828,7 +1832,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 88) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(140);
+ } else SynErr(139);
}
void NegOp() {
@@ -1836,11 +1840,61 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 90) {
Get();
+ } else SynErr(140);
+ }
+
+ void EndlessExpression(out Expression e) {
+ IToken/*!*/ x, dtName, id; BigInteger n;
+ List<Expression/*!*/>/*!*/ elements;
+ Expression e0, e1;
+ e = dummyExpr;
+
+ if (la.kind == 57) {
+ Get();
+ x = t;
+ Expression(out e);
+ Expect(98);
+ Expression(out e0);
+ Expect(58);
+ Expression(out e1);
+ e = new ITEExpr(x, e, e0, e1);
+ } else if (StartOf(18)) {
+ QuantifierGuts(out e);
+ } else if (la.kind == 37) {
+ ComprehensionExpr(out e);
} else SynErr(141);
}
+ void DottedIdentifiersAndFunction(out Expression e) {
+ IToken id; IToken openParen = null;
+ List<Expression> args = null;
+ List<IToken> idents = new List<IToken>();
+
+ Ident(out id);
+ idents.Add(id);
+ while (la.kind == 54) {
+ Get();
+ Ident(out id);
+ idents.Add(id);
+ }
+ if (la.kind == 32) {
+ Get();
+ openParen = t; args = new List<Expression>();
+ if (StartOf(8)) {
+ Expressions(args);
+ }
+ Expect(33);
+ }
+ e = new IdentifierSequence(idents, openParen, args);
+ }
+
+ void Suffix(ref Expression/*!*/ e) {
+ SelectOrCallSuffix(ref e);
+ }
+
void ConstAtomExpression(out Expression/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x, dtName, id; BigInteger n; List<Expression/*!*/>/*!*/ elements;
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ IToken/*!*/ x, dtName, id; BigInteger n; List<Expression/*!*/>/*!*/ elements;
Expression e0, e1;
e = dummyExpr;
@@ -1867,19 +1921,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
case 94: {
Get();
- x = t;
- Ident(out dtName);
- Expect(54);
- Ident(out id);
- elements = new List<Expression/*!*/>();
- if (la.kind == 32) {
- Get();
- if (StartOf(8)) {
- Expressions(elements);
- }
- Expect(33);
- }
- e = new DatatypeValue(t, dtName.val, id.val, elements);
+ e = new ThisExpr(t);
break;
}
case 95: {
@@ -1900,6 +1942,15 @@ List<Expression/*!*/>/*!*/ decreases) { e = new AllocatedExpr(x, e);
break;
}
+ case 97: {
+ Get();
+ x = t;
+ Expect(32);
+ Expression(out e);
+ Expect(33);
+ e = new OldExpr(x, e);
+ break;
+ }
case 17: {
Get();
x = t;
@@ -1928,23 +1979,12 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(53);
break;
}
- case 57: {
+ case 32: {
Get();
x = t;
Expression(out e);
- Expect(97);
- Expression(out e0);
- Expect(58);
- Expression(out e1);
- e = new ITEExpr(x, e, e0, e1);
- break;
- }
- case 101: case 102: case 103: case 104: {
- QuantifierGuts(out e);
- break;
- }
- case 37: {
- ComprehensionExpr(out e);
+ e = new ParensExpression(x, e);
+ Expect(33);
break;
}
default: SynErr(142); break;
@@ -1972,10 +2012,10 @@ List<Expression/*!*/>/*!*/ decreases) { Expression range = null;
Expression/*!*/ body;
- if (la.kind == 101 || la.kind == 102) {
+ if (la.kind == 100 || la.kind == 101) {
Forall();
x = t; univ = true;
- } else if (la.kind == 103 || la.kind == 104) {
+ } else if (la.kind == 102 || la.kind == 103) {
Exists();
x = t;
} else SynErr(143);
@@ -2025,7 +2065,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
Expect(17);
Expression(out range);
- if (la.kind == 105 || la.kind == 106) {
+ if (la.kind == 104 || la.kind == 105) {
QSep();
Expression(out body);
}
@@ -2059,10 +2099,10 @@ List<Expression/*!*/>/*!*/ decreases) { void ObjectExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
- if (la.kind == 99) {
+ if (la.kind == 94) {
Get();
e = new ThisExpr(t);
- } else if (la.kind == 100) {
+ } else if (la.kind == 97) {
Get();
x = t;
Expect(32);
@@ -2101,7 +2141,7 @@ List<Expression/*!*/>/*!*/ decreases) { if (StartOf(8)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 98) {
+ if (la.kind == 99) {
Get();
anyDots = true;
if (StartOf(8)) {
@@ -2124,7 +2164,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
} else SynErr(145);
- } else if (la.kind == 98) {
+ } else if (la.kind == 99) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
@@ -2156,17 +2196,17 @@ List<Expression/*!*/>/*!*/ decreases) { }
void Forall() {
- if (la.kind == 101) {
+ if (la.kind == 100) {
Get();
- } else if (la.kind == 102) {
+ } else if (la.kind == 101) {
Get();
} else SynErr(148);
}
void Exists() {
- if (la.kind == 103) {
+ if (la.kind == 102) {
Get();
- } else if (la.kind == 104) {
+ } else if (la.kind == 103) {
Get();
} else SynErr(149);
}
@@ -2186,9 +2226,9 @@ List<Expression/*!*/>/*!*/ decreases) { }
void QSep() {
- if (la.kind == 105) {
+ if (la.kind == 104) {
Get();
- } else if (la.kind == 106) {
+ } else if (la.kind == 105) {
Get();
} else SynErr(151);
}
@@ -2201,7 +2241,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(22);
Expect(1);
aName = t.val;
- if (StartOf(17)) {
+ if (StartOf(19)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 19) {
@@ -2225,24 +2265,26 @@ List<Expression/*!*/>/*!*/ decreases) { }
static readonly 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,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,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,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,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,x, x,x,x,x, x},
- {x,x,x,x, x,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, 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,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, 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,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,T, 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,T,x,T, 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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,x,x,x, x},
- {x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,T,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,x,x,T, T,T,x,x, x,x,x,x, T,T,x,T, x,T,T,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,T, T,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,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,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,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, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, x,x,x,x, T,T,x,T, x,T,T,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,T, 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, 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, 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,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, 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,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, 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,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,T, x,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,T, 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, T,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,T, T,T,T,T, T,x,x,x, x,T,T,T, T,x,x,x, x},
- {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,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,x, x,x,x,x},
+ {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,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,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,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,x, x,x,x,x},
+ {x,x,x,x, x,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, 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,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, 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, 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,T, 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,T,x,T, 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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T,x, x,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
+ {x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,T,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,x,x,T, T,T,x,x, x,x,x,x, T,T,x,T, x,T,T,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,T,x, x,T,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,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,T,x, x,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, 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, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, x,x,x,x, T,T,x,T, x,T,T,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,T,x, x,T,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, x,x,x,x, 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,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,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,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,T, x,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,x, x,x,x,x, x,x,x,x, x,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, T,T,T,T, x,x,x,x},
+ {x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,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,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x, T,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T,x, x,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x}
};
} // end Parser
@@ -2361,54 +2403,54 @@ public class Errors { case 91: s = "\"false\" expected"; break;
case 92: s = "\"true\" expected"; break;
case 93: s = "\"null\" expected"; break;
- case 94: s = "\"#\" expected"; break;
+ case 94: s = "\"this\" expected"; break;
case 95: s = "\"fresh\" expected"; break;
case 96: s = "\"allocated\" expected"; break;
- case 97: s = "\"then\" expected"; break;
- case 98: s = "\"..\" expected"; break;
- case 99: s = "\"this\" expected"; break;
- case 100: s = "\"old\" expected"; break;
- case 101: s = "\"forall\" expected"; break;
- case 102: s = "\"\\u2200\" expected"; break;
- case 103: s = "\"exists\" expected"; break;
- case 104: s = "\"\\u2203\" expected"; break;
- case 105: s = "\"::\" expected"; break;
- case 106: s = "\"\\u2022\" expected"; break;
- case 107: s = "??? expected"; break;
- case 108: s = "invalid DatatypeDecl"; break;
- case 109: s = "invalid ClassMemberDecl"; break;
- case 110: s = "invalid FunctionDecl"; break;
+ case 97: s = "\"old\" expected"; break;
+ case 98: s = "\"then\" expected"; break;
+ case 99: s = "\"..\" expected"; break;
+ case 100: s = "\"forall\" expected"; break;
+ case 101: s = "\"\\u2200\" expected"; break;
+ case 102: s = "\"exists\" expected"; break;
+ case 103: s = "\"\\u2203\" expected"; break;
+ case 104: s = "\"::\" expected"; break;
+ case 105: s = "\"\\u2022\" expected"; break;
+ case 106: s = "??? expected"; break;
+ case 107: s = "invalid DatatypeDecl"; break;
+ case 108: s = "invalid ClassMemberDecl"; break;
+ case 109: s = "invalid FunctionDecl"; break;
+ case 110: s = "invalid MethodDecl"; break;
case 111: s = "invalid MethodDecl"; break;
- case 112: s = "invalid MethodDecl"; break;
- case 113: s = "invalid TypeAndToken"; break;
+ case 112: s = "invalid TypeAndToken"; break;
+ case 113: s = "invalid MethodSpec"; break;
case 114: s = "invalid MethodSpec"; break;
- case 115: s = "invalid MethodSpec"; break;
- case 116: s = "invalid ReferenceType"; break;
- case 117: s = "invalid FunctionSpec"; break;
- case 118: s = "invalid FunctionBody"; break;
- case 119: s = "invalid PossiblyWildFrameExpression"; break;
- case 120: s = "invalid PossiblyWildExpression"; break;
- case 121: s = "invalid MatchOrExpr"; break;
- case 122: s = "invalid Stmt"; break;
- case 123: s = "invalid OneStmt"; break;
+ case 115: s = "invalid ReferenceType"; break;
+ case 116: s = "invalid FunctionSpec"; break;
+ case 117: s = "invalid FunctionBody"; break;
+ case 118: s = "invalid PossiblyWildFrameExpression"; break;
+ case 119: s = "invalid PossiblyWildExpression"; break;
+ case 120: s = "invalid MatchOrExpr"; break;
+ case 121: s = "invalid Stmt"; break;
+ case 122: s = "invalid OneStmt"; break;
+ case 123: s = "invalid IfStmt"; break;
case 124: s = "invalid IfStmt"; break;
- case 125: s = "invalid IfStmt"; break;
- case 126: s = "invalid WhileStmt"; break;
- case 127: s = "invalid ForeachStmt"; break;
- case 128: s = "invalid AssignRhs"; break;
- case 129: s = "invalid SelectExpression"; break;
- case 130: s = "invalid Guard"; break;
- case 131: s = "invalid CallStmtSubExpr"; break;
- case 132: s = "invalid AttributeArg"; break;
- case 133: s = "invalid EquivOp"; break;
- case 134: s = "invalid ImpliesOp"; break;
- case 135: s = "invalid AndOp"; break;
- case 136: s = "invalid OrOp"; break;
- case 137: s = "invalid RelOp"; break;
- case 138: s = "invalid AddOp"; break;
- case 139: s = "invalid UnaryExpression"; break;
- case 140: s = "invalid MulOp"; break;
- case 141: s = "invalid NegOp"; break;
+ case 125: s = "invalid WhileStmt"; break;
+ case 126: s = "invalid ForeachStmt"; break;
+ case 127: s = "invalid AssignRhs"; break;
+ case 128: s = "invalid SelectExpression"; break;
+ case 129: s = "invalid Guard"; break;
+ case 130: s = "invalid CallStmtSubExpr"; break;
+ case 131: s = "invalid AttributeArg"; break;
+ case 132: s = "invalid EquivOp"; break;
+ case 133: s = "invalid ImpliesOp"; break;
+ case 134: s = "invalid AndOp"; break;
+ case 135: s = "invalid OrOp"; break;
+ case 136: s = "invalid RelOp"; break;
+ case 137: s = "invalid AddOp"; break;
+ case 138: s = "invalid UnaryExpression"; break;
+ case 139: s = "invalid MulOp"; break;
+ case 140: s = "invalid NegOp"; break;
+ case 141: s = "invalid EndlessExpression"; break;
case 142: s = "invalid ConstAtomExpression"; break;
case 143: s = "invalid QuantifierGuts"; break;
case 144: s = "invalid ObjectExpression"; break;
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 2dd2724f..6a6cf8a8 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -248,7 +248,7 @@ namespace Microsoft.Dafny { public void PrintCtor(DatatypeCtor ctor, int indent) {
Contract.Requires(ctor != null);
Indent(indent);
- PrintClassMethodHelper("", ctor.Attributes, ctor.Name, ctor.TypeArgs);
+ PrintClassMethodHelper("", ctor.Attributes, ctor.Name, new List<TypeParameter>());
if (ctor.Formals.Count != 0) {
PrintFormals(ctor.Formals);
}
@@ -1016,6 +1016,24 @@ namespace Microsoft.Dafny { PrintExpression(ite.Els);
if (parensNeeded) { wr.Write(")"); }
+ } else if (expr is ParensExpression) {
+ var e = (ParensExpression)expr;
+ // printing of parentheses is done optimally, not according to the parentheses in the given program
+ PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, indent);
+
+ } else if (expr is IdentifierSequence) {
+ var e = (IdentifierSequence)expr;
+ string sep = "";
+ foreach (var id in e.Tokens) {
+ wr.Write("{0}{1}", sep, id.val);
+ sep = ".";
+ }
+ if (e.Arguments != null) {
+ wr.Write("(");
+ PrintExpressionList(e.Arguments);
+ wr.Write(")");
+ }
+
} else if (expr is MatchExpr) {
Contract.Assert(false); throw new cce.UnreachableException(); // MatchExpr is an extended expression and should be printed only using PrintExtendedExpr
} else {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 3549d0db..b01ca509 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -48,6 +48,7 @@ namespace Microsoft.Dafny { readonly Dictionary<string/*!*/,TopLevelDecl/*!*/>/*!*/ classes = new Dictionary<string/*!*/,TopLevelDecl/*!*/>();
readonly Dictionary<ClassDecl/*!*/,Dictionary<string/*!*/,MemberDecl/*!*/>/*!*/>/*!*/ classMembers = new Dictionary<ClassDecl/*!*/,Dictionary<string/*!*/,MemberDecl/*!*/>/*!*/>();
readonly Dictionary<DatatypeDecl/*!*/,Dictionary<string/*!*/,DatatypeCtor/*!*/>/*!*/>/*!*/ datatypeCtors = new Dictionary<DatatypeDecl/*!*/,Dictionary<string/*!*/,DatatypeCtor/*!*/>/*!*/>();
+ readonly Dictionary<string/*!*/, Tuple<DatatypeCtor, bool>> allDatatypeCtors = new Dictionary<string, Tuple<DatatypeCtor, bool>>();
readonly Graph<ModuleDecl/*!*/>/*!*/ importGraph = new Graph<ModuleDecl/*!*/>();
public Resolver(Program prog) {
@@ -205,6 +206,15 @@ namespace Microsoft.Dafny { Error(ctor, "Duplicate datatype constructor name: {0}", ctor.Name);
} else {
ctors.Add(ctor.Name, ctor);
+ // also register the constructor name globally
+ Tuple<DatatypeCtor, bool> pair;
+ if (allDatatypeCtors.TryGetValue(ctor.Name, out pair)) {
+ // mark it as a duplicate
+ allDatatypeCtors[ctor.Name] = new Tuple<DatatypeCtor, bool>(pair.Item1, true);
+ } else {
+ // add new
+ allDatatypeCtors.Add(ctor.Name, new Tuple<DatatypeCtor, bool>(ctor, false));
+ }
}
}
}
@@ -433,7 +443,6 @@ namespace Microsoft.Dafny { ctor.EnclosingDatatype = dt;
allTypeParameters.PushMarker();
- ResolveTypeParameters(ctor.TypeArgs, true, ctor);
ResolveCtorSignature(ctor);
allTypeParameters.PopMarker();
@@ -1432,7 +1441,7 @@ namespace Microsoft.Dafny { }
Dictionary<string,DatatypeCtor> ctors;
if (dtd == null) {
- Error(s.Source, "the type of the match source expression must be a datatype");
+ Error(s.Source, "the type of the match source expression must be a datatype (instead found {0})", s.Source.Type);
ctors = null;
} else {
Contract.Assert(sourceType != null); // dtd and sourceType are set together above
@@ -1467,12 +1476,6 @@ namespace Microsoft.Dafny { }
}
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)) {
@@ -1838,8 +1841,96 @@ namespace Microsoft.Dafny { // and it cannot be determined what the type of expr is, then it is fine to leave expr.Type as null. In that case, the end
// of this method will assign proxy type to the expression, which reduces the number of error messages that are produced
// while type checking the rest of the program.
-
- if (expr is LiteralExpr) {
+
+ if (expr is ParensExpression) {
+ var e = (ParensExpression)expr;
+ ResolveExpression(e.E, twoState, specContext);
+ e.ResolvedExpression = e.E;
+ e.Type = e.E.Type;
+
+ } else if (expr is IdentifierSequence) {
+ var e = (IdentifierSequence)expr;
+ // Look up "id" as follows:
+ // - local variable, parameter, or bound variable (if this clashes with something of interest, one can always rename the local variable locally)
+ // - type name (class or datatype)
+ // - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here)
+ // - field name (with implicit receiver) (if the field is ocluded by anything above, one can use an explicit "this.")
+ // Note, at present, modules do not give rise to new namespaces, which is something that should
+ // be changed in the language when modules are given more attention.
+ Expression r = null; // resolved version of e
+
+ TopLevelDecl decl;
+ Tuple<DatatypeCtor, bool> pair;
+ Dictionary<string, MemberDecl> members;
+ MemberDecl member;
+ var id = e.Tokens[0];
+ if (scope.Find(id.val) != null) {
+ // ----- root is a local variable, parameter, or bound variable
+ r = new IdentifierExpr(id, id.val);
+ ResolveExpression(r, twoState, specContext);
+ r = ResolveSuffix(r, e, 1, twoState, specContext);
+
+ } else if (classes.TryGetValue(id.val, out decl)) {
+ if (decl is ClassDecl) {
+ // ----- root is a class
+ var cd = (ClassDecl)decl;
+ Contract.Assert(false); // TODO
+
+ } else {
+ // ----- root is a datatype
+ var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl
+ if (e.Tokens.Count == 1 && e.Arguments == null) {
+ Error(id, "name of datatype ('{0}') is used as a variable", id.val);
+ } else if (e.Tokens.Count == 1 && e.Arguments != null) {
+ Error(id, "name of dataypte ('{0}') is used as a function", id.val);
+ // resolve the arguments nonetheless
+ foreach (var arg in e.Arguments) {
+ ResolveExpression(arg, twoState, specContext);
+ }
+ } else {
+ var args = (e.Tokens.Count == 2 ? e.Arguments : null) ?? new List<Expression>();
+ r = new DatatypeValue(id, id.val, e.Tokens[1].val, args);
+ ResolveExpression(r, twoState, specContext);
+ if (e.Tokens.Count != 2) {
+ r = ResolveSuffix(r, e, 2, twoState, specContext);
+ }
+ }
+ }
+
+ } else if (allDatatypeCtors.TryGetValue(id.val, out pair)) {
+ // ----- root is a datatype constructor
+ if (pair.Item2) {
+ // there is more than one constructor with this name
+ Error(id, "the name '{0}' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, '{1}.{0}')", id.val, pair.Item1.EnclosingDatatype.Name);
+ } else {
+ var args = (e.Tokens.Count == 1 ? e.Arguments : null) ?? new List<Expression>();
+ r = new DatatypeValue(id, pair.Item1.EnclosingDatatype.Name, id.val, args);
+ ResolveExpression(r, twoState, specContext);
+ if (e.Tokens.Count != 1) {
+ r = ResolveSuffix(r, e, 1, twoState, specContext);
+ }
+ }
+
+ } else if (classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member)) {
+ // ----- field, function, or method
+ r = ResolveSuffix(new ImplicitThisExpr(id), e, 0, twoState, specContext);
+
+ } else {
+ Error(id, "unresolved identifier: {0}", id.val);
+ // resolve arguments, if any
+ if (e.Arguments != null) {
+ foreach (var arg in e.Arguments) {
+ ResolveExpression(arg, twoState, specContext);
+ }
+ }
+ }
+
+ if (r != null) {
+ e.ResolvedExpression = r;
+ e.Type = r.Type;
+ }
+
+ } else if (expr is LiteralExpr) {
LiteralExpr e = (LiteralExpr)expr;
if (e.Value == null) {
e.Type = new ObjectTypeProxy();
@@ -1899,12 +1990,6 @@ namespace Microsoft.Dafny { 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) {
- Type t = new ParamTypeProxy(p);
- dtv.InferredTypeArgs.Add(t);
- subst.Add(p, t);
- }
}
int j = 0;
foreach (Expression arg in dtv.Arguments) {
@@ -2370,14 +2455,14 @@ namespace Microsoft.Dafny { Dictionary<string,DatatypeCtor> ctors;
IVariable goodMatchVariable = null;
if (dtd == null) {
- Error(me.Source, "the type of the match source expression must be a datatype");
+ Error(me.Source, "the type of the match source expression must be a datatype (instead found {0})", me.Source.Type);
ctors = null;
} else {
Contract.Assert(sourceType != null); // dtd and sourceType are set together above
ctors = datatypeCtors[dtd];
Contract.Assert(ctors != null); // dtd should have been inserted into datatypeCtors during a previous resolution stage
- IdentifierExpr ie = me.Source as IdentifierExpr;
+ IdentifierExpr ie = me.Source.Resolved as IdentifierExpr;
if (ie == null || !(ie.Var is Formal || ie.Var is BoundVar)) {
Error(me.Source.tok, "match source expression must be a formal parameter of the enclosing function or an enclosing match expression");
} else if (!matchVarContext.Contains(ie.Var)) {
@@ -2414,12 +2499,6 @@ namespace Microsoft.Dafny { }
}
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)) {
@@ -2472,6 +2551,39 @@ namespace Microsoft.Dafny { }
/// <summary>
+ /// Given resolved expression "r" and unresolved expressions e.Tokens[p..] and e.Arguments.
+ /// Returns a resolved version of the expression:
+ /// r . e.Tokens[p] . e.Tokens[p+1] ... . e.Tokens[e.Tokens.Count-1] ( e.Arguments )
+ /// </summary>
+ Expression ResolveSuffix(Expression r, IdentifierSequence e, int p, bool twoState, bool specContext) {
+ Contract.Requires(r != null);
+ Contract.Requires(e != null);
+ Contract.Requires(0 <= p && p <= e.Tokens.Count);
+ Contract.Ensures(Contract.Result<Expression>() != null);
+
+ int nonCallArguments = e.Arguments == null ? e.Tokens.Count : e.Tokens.Count - 1;
+ for (; p < nonCallArguments; p++) {
+ r = new FieldSelectExpr(e.Tokens[p], r, e.Tokens[p].val);
+ ResolveExpression(r, twoState, specContext);
+ }
+
+ if (p < e.Tokens.Count) {
+ Contract.Assert(e.Arguments != null);
+ // TODO: treat differently if what is being called is a method
+ r = new FunctionCallExpr(e.Tokens[p], e.Tokens[p].val, r, e.Arguments);
+ ResolveExpression(r, twoState, specContext);
+ } else if (e.Arguments != null) {
+ Contract.Assert(p == e.Tokens.Count);
+ Error(e.OpenParen, "non-function expression is called with parameters");
+ // resolve the arguments nonetheless
+ foreach (var arg in e.Arguments) {
+ ResolveExpression(arg, twoState, specContext);
+ }
+ }
+ return r;
+ }
+
+ /// <summary>
/// Tries to find a bounded pool for each of the bound variables "bvars" of "expr". If this process
/// fails, then "null" is returned and:
/// if "errorMessage" is non-null, then appropriate error messages are reported and "null" is returned;
@@ -2569,6 +2681,7 @@ namespace Microsoft.Dafny { /// The new "e0 op e1" is equivalent to the old "e0 op e1".
/// One of "e0" and "e1" is the identifier "boundVars[bvi]"; the return value is either 0 or 1, and indicates which.
/// The other of "e0" and "e1" is an expression whose free variables are not among "boundVars[bvi..]".
+ /// Ensures that the resulting "e0" and "e1" are not ConcreteSyntaxExpression's.
/// </summary>
int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1)
{
@@ -2577,8 +2690,12 @@ namespace Microsoft.Dafny { Contract.Requires(boundVars != null);
Contract.Requires(0 <= bvi && bvi < boundVars.Count);
Contract.Ensures(Contract.Result<int>() < 2);
+ Contract.Ensures(!(Contract.ValueAtReturn(out e0) is ConcreteSyntaxExpression));
+ Contract.Ensures(!(Contract.ValueAtReturn(out e1) is ConcreteSyntaxExpression));
var bv = boundVars[bvi];
+ e0 = e0.Resolved;
+ e1 = e1.Resolved;
// make an initial assessment of where bv is; to continue, we need bv to appear in exactly one operand
var fv0 = FreeVariables(e0);
@@ -2616,10 +2733,10 @@ namespace Microsoft.Dafny { } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add) {
// Change "A+B op C" into either "A op C-B" or "B op C-A", depending on where we find bv among A and B.
if (!FreeVariables(bin.E1).Contains(bv)) {
- thisSide = bin.E0;
+ thisSide = bin.E0.Resolved;
thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, thatSide, bin.E1);
} else {
- thisSide = bin.E1;
+ thisSide = bin.E1.Resolved;
thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, thatSide, bin.E0);
}
((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
@@ -2629,14 +2746,14 @@ namespace Microsoft.Dafny { // Change "A-B op C" in a similar way.
if (!FreeVariables(bin.E1).Contains(bv)) {
// change to "A op C+B"
- thisSide = bin.E0;
+ thisSide = bin.E0.Resolved;
thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Add, thatSide, bin.E1);
((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Add;
} else {
// In principle, change to "-B op C-A" and then to "B dualOp A-C". But since we don't want
// to change "op", we instead end with "A-C op B" and switch the mapping of thisSide/thatSide
// to e0/e1 (by inverting "whereIsBv").
- thisSide = bin.E1;
+ thisSide = bin.E1.Resolved;
thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, bin.E0, thatSide);
((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
whereIsBv = 1 - whereIsBv;
@@ -2689,6 +2806,7 @@ namespace Microsoft.Dafny { /// inequality is never returned and the comparisons > and >= are never returned; the negation of
/// a common equality or disequality is rewritten analogously.
/// Requires "expr" to be successfully resolved.
+ /// Ensures that what is returned is not a ConcreteSyntaxExpression.
/// </summary>
IEnumerable<Expression> NormalizedConjuncts(Expression expr, bool polarity) {
// We consider 5 cases. To describe them, define P(e)=Conjuncts(e,true) and N(e)=Conjuncts(e,false).
@@ -2700,6 +2818,7 @@ namespace Microsoft.Dafny { // So for ==>, we have:
// * X ==> Y P(_) = P(!X || Y) = (!X || Y) = (X ==> Y)
// N(_) = N(!X || Y) = N(!X),N(Y) = P(X),N(Y)
+ expr = expr.Resolved;
// Binary expressions
var b = expr as BinaryExpr;
@@ -3075,6 +3194,9 @@ namespace Microsoft.Dafny { return true;
}
return Contract.Exists( me.Cases,mc=> UsesSpecFeatures(mc.Body));
+ } else if (expr is ConcreteSyntaxExpression) {
+ var e = (ConcreteSyntaxExpression)expr;
+ return UsesSpecFeatures(e.ResolvedExpression);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
@@ -3087,8 +3209,8 @@ namespace Microsoft.Dafny { [ContractInvariantMethod]
void ObjectInvariant()
{
- Contract.Invariant(names != null);
- Contract.Invariant(things != null);
+ Contract.Invariant(names != null);
+ Contract.Invariant(things != null);
Contract.Invariant(names.Count == things.Count);
Contract.Invariant(-1 <= scopeSizeWhereInstancesWereDisallowed && scopeSizeWhereInstancesWereDisallowed <= names.Count);
}
@@ -3123,7 +3245,7 @@ namespace Microsoft.Dafny { }
}
- // Pushes name-->var association and returns "true", if name has not already been pushed since the last marker.
+ // Pushes name-->thing association and returns "true", if name has not already been pushed since the last marker.
// If name already has been pushed since the last marker, does nothing and returns "false".
public bool Push(string name, Thing thing) {
Contract.Requires(name != null);
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 817df6cd..940c249f 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer { public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 107;
- const int noSym = 107;
+ const int maxT = 106;
+ const int noSym = 106;
[ContractInvariantMethod]
@@ -260,25 +260,25 @@ public class Scanner { start[123] = 17;
start[125] = 18;
start[59] = 19;
- start[61] = 58;
- start[124] = 59;
+ start[61] = 57;
+ start[124] = 58;
start[44] = 20;
- start[58] = 60;
- start[60] = 61;
- start[62] = 62;
+ start[58] = 59;
+ start[60] = 60;
+ start[62] = 61;
start[40] = 21;
start[41] = 22;
start[42] = 23;
start[96] = 24;
start[91] = 27;
start[93] = 28;
- start[46] = 63;
+ start[46] = 62;
start[8660] = 31;
start[8658] = 33;
start[38] = 34;
start[8743] = 36;
start[8744] = 38;
- start[33] = 64;
+ start[33] = 63;
start[8800] = 44;
start[8804] = 45;
start[8805] = 46;
@@ -287,10 +287,9 @@ public class Scanner { start[47] = 49;
start[37] = 50;
start[172] = 51;
- start[35] = 52;
- start[8704] = 54;
- start[8707] = 55;
- start[8226] = 57;
+ start[8704] = 53;
+ start[8707] = 54;
+ start[8226] = 56;
start[Buffer.EOF] = -1;
}
@@ -536,13 +535,13 @@ public class Scanner { case "false": t.kind = 91; break;
case "true": t.kind = 92; break;
case "null": t.kind = 93; break;
+ case "this": t.kind = 94; break;
case "fresh": t.kind = 95; break;
case "allocated": t.kind = 96; break;
- case "then": t.kind = 97; break;
- case "this": t.kind = 99; break;
- case "old": t.kind = 100; break;
- case "forall": t.kind = 101; break;
- case "exists": t.kind = 103; break;
+ case "old": t.kind = 97; break;
+ case "then": t.kind = 98; break;
+ case "forall": t.kind = 100; break;
+ case "exists": t.kind = 102; break;
default: break;
}
}
@@ -717,54 +716,52 @@ public class Scanner { case 51:
{t.kind = 90; break;}
case 52:
- {t.kind = 94; break;}
+ {t.kind = 99; break;}
case 53:
- {t.kind = 98; break;}
+ {t.kind = 101; break;}
case 54:
- {t.kind = 102; break;}
+ {t.kind = 103; break;}
case 55:
{t.kind = 104; break;}
case 56:
{t.kind = 105; break;}
case 57:
- {t.kind = 106; break;}
- case 58:
recEnd = pos; recKind = 16;
if (ch == '>') {AddCh(); goto case 25;}
- else if (ch == '=') {AddCh(); goto case 65;}
+ else if (ch == '=') {AddCh(); goto case 64;}
else {t.kind = 16; break;}
- case 59:
+ case 58:
recEnd = pos; recKind = 17;
if (ch == '|') {AddCh(); goto case 37;}
else {t.kind = 17; break;}
- case 60:
+ case 59:
recEnd = pos; recKind = 22;
if (ch == '=') {AddCh(); goto case 26;}
- else if (ch == ':') {AddCh(); goto case 56;}
+ else if (ch == ':') {AddCh(); goto case 55;}
else {t.kind = 22; break;}
- case 61:
+ case 60:
recEnd = pos; recKind = 23;
- if (ch == '=') {AddCh(); goto case 66;}
+ if (ch == '=') {AddCh(); goto case 65;}
else {t.kind = 23; break;}
- case 62:
+ case 61:
recEnd = pos; recKind = 24;
if (ch == '=') {AddCh(); goto case 39;}
else {t.kind = 24; break;}
- case 63:
+ case 62:
recEnd = pos; recKind = 54;
- if (ch == '.') {AddCh(); goto case 53;}
+ if (ch == '.') {AddCh(); goto case 52;}
else {t.kind = 54; break;}
- case 64:
+ case 63:
recEnd = pos; recKind = 89;
if (ch == '=') {AddCh(); goto case 40;}
else if (ch == '!') {AddCh(); goto case 41;}
else if (ch == 'i') {AddCh(); goto case 42;}
else {t.kind = 89; break;}
- case 65:
+ case 64:
recEnd = pos; recKind = 76;
if (ch == '>') {AddCh(); goto case 32;}
else {t.kind = 76; break;}
- case 66:
+ case 65:
recEnd = pos; recKind = 77;
if (ch == '=') {AddCh(); goto case 29;}
else {t.kind = 77; break;}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index e338c0ca..0c750d8b 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -506,7 +506,7 @@ namespace Microsoft.Dafny { Contract.Requires(me != null);
Contract.Requires(layerOffset == 0 || layerOffset == 1);
- IVariable formal = ((IdentifierExpr)me.Source).Var; // correctness of casts follows from what resolution checks
+ IVariable formal = ((IdentifierExpr)me.Source.Resolved).Var; // correctness of casts follows from what resolution checks
foreach (MatchCaseExpr mc in me.Cases) {
Contract.Assert(mc.Ctor != null); // the field is filled in by resolution
Specialization s = new Specialization(formal, mc, prev);
@@ -1546,6 +1546,9 @@ namespace Microsoft.Dafny { total = BplAnd(total, Bpl.Expr.Imp(test, IsTotal(e.Thn, etran)));
total = BplAnd(total, Bpl.Expr.Imp(Bpl.Expr.Not(test), IsTotal(e.Els, etran)));
return total;
+ } else if (expr is ConcreteSyntaxExpression) {
+ var e = (ConcreteSyntaxExpression)expr;
+ return IsTotal(e.ResolvedExpression, etran);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
@@ -1676,6 +1679,9 @@ namespace Microsoft.Dafny { total = BplAnd(total, Bpl.Expr.Imp(test, CanCallAssumption(e.Thn, etran)));
total = BplAnd(total, Bpl.Expr.Imp(Bpl.Expr.Not(test), CanCallAssumption(e.Els, etran)));
return total;
+ } else if (expr is ConcreteSyntaxExpression) {
+ var e = (ConcreteSyntaxExpression)expr;
+ return CanCallAssumption(e.ResolvedExpression, etran);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
@@ -2083,7 +2089,11 @@ namespace Microsoft.Dafny { }
builder.Add(ifCmd);
result = null;
-
+
+ } else if (expr is ConcreteSyntaxExpression) {
+ var e = (ConcreteSyntaxExpression)expr;
+ CheckWellformedWithResult(e.ResolvedExpression, options, result, resultType, locals, builder, etran);
+
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
@@ -4635,7 +4645,11 @@ namespace Microsoft.Dafny { Bpl.Expr thn = TrExpr(e.Thn);
Bpl.Expr els = TrExpr(e.Els);
return new NAryExpr(expr.tok, new IfThenElse(expr.tok), new ExprSeq(g, thn, els));
-
+
+ } else if (expr is ConcreteSyntaxExpression) {
+ var e = (ConcreteSyntaxExpression)expr;
+ return TrExpr(e.ResolvedExpression);
+
} else if (expr is BoxingCastExpr) {
BoxingCastExpr e = (BoxingCastExpr)expr;
return CondApplyBox(e.tok, TrExpr(e.E), e.FromType, e.ToType);
@@ -5300,6 +5314,10 @@ namespace Microsoft.Dafny { return true;
}
+ } else if (expr is ConcreteSyntaxExpression) {
+ var e = (ConcreteSyntaxExpression)expr;
+ return TrSplitExpr(e.ResolvedExpression, splits, expandFunctions, etran);
+
} else if (expr is BinaryExpr) {
var bin = (BinaryExpr)expr;
if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {
@@ -5664,6 +5682,9 @@ namespace Microsoft.Dafny { return VarOccursInArgumentToRecursiveFunction(e.Test, n, null) || // test is not "elevated"
VarOccursInArgumentToRecursiveFunction(e.Thn, n, p) || // but the two branches are
VarOccursInArgumentToRecursiveFunction(e.Els, n, p);
+ } else if (expr is ConcreteSyntaxExpression) {
+ var e = (ConcreteSyntaxExpression)expr;
+ return VarOccursInArgumentToRecursiveFunction(e.ResolvedExpression, n, p);
} else if (expr is BoxingCastExpr) {
var e = (BoxingCastExpr)expr;
return VarOccursInArgumentToRecursiveFunction(e.E, n, p);
@@ -5857,6 +5878,10 @@ namespace Microsoft.Dafny { if (test != e.Test || thn != e.Thn || els != e.Els) {
newExpr = new ITEExpr(expr.tok, test, thn, els);
}
+
+ } else if (expr is ConcreteSyntaxExpression) {
+ var e = (ConcreteSyntaxExpression)expr;
+ return Substitute(e.ResolvedExpression, receiverReplacement, substMap);
}
if (newExpr == null) {
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index ebaeab84..9f7e272e 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -88,7 +88,7 @@ class Map<Key,Value> { }
}
- method Remove(key: Key)
+ method Remove(key: Key)// returns (ghost h: int)
requires Valid();
modifies Repr;
ensures Valid() && fresh(Repr - old(Repr));
@@ -111,6 +111,9 @@ class Map<Key,Value> { if (p != null) {
Keys := Keys[..n] + Keys[n+1..];
Values := Values[..n] + Values[n+1..];
+ assert Keys[n..] == old(Keys)[n+1..];
+ assert Values[n..] == old(Values)[n+1..];
+
nodes := nodes[..n] + nodes[n+1..];
if (prev == null) {
head := head.next;
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index e0874a66..d9d3a572 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -53,7 +53,7 @@ datatype List<T> { datatype WildData {
Something;
- JustAboutAnything<G, H>(G, myName: set<H>, int, WildData);
+ JustAboutAnything(bool, myName: set<int>, int, WildData);
More(List<int>);
}
@@ -620,7 +620,7 @@ Execution trace: (0,0): anon5
Termination.dfy(119,3): anon12_Else
(0,0): anon7
-Termination.dfy(248,36): Error: cannot prove termination; try supplying a decreases clause
+Termination.dfy(248,35): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon6_Else
(0,0): anon7_Else
@@ -694,7 +694,7 @@ DTypes.dfy(134,6): Related location: Related location DTypes.dfy(93,3): Related location: Related location
Execution trace:
(0,0): anon0
-DTypes.dfy(160,13): Error: assertion violation
+DTypes.dfy(160,12): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy index 35d939d3..2c9b3a35 100644 --- a/Test/dafny0/ControlStructures.dfy +++ b/Test/dafny0/ControlStructures.dfy @@ -9,7 +9,7 @@ method M0(d: D) }
method M1(d: D)
- requires d != #D.Blue;
+ requires d != D.Blue;
{
match (d) { // error: missing case: Purple
case Green =>
@@ -18,7 +18,7 @@ method M1(d: D) }
method M2(d: D)
- requires d != #D.Blue && d != #D.Purple;
+ requires d != D.Blue && d != D.Purple;
{
match (d) {
case Green =>
@@ -27,9 +27,9 @@ method M2(d: D) }
method M3(d: D)
- requires d == #D.Green;
+ requires d == D.Green;
{
- if (d != #D.Green) {
+ if (d != D.Green) {
match (d) {
// nothing here
}
@@ -37,9 +37,9 @@ method M3(d: D) }
method M4(d: D)
- requires d == #D.Green || d == #D.Red;
+ requires d == D.Green || d == D.Red;
{
- if (d != #D.Green) {
+ if (d != D.Green) {
match (d) { // error: missing case Red
// nothing here
}
@@ -56,7 +56,7 @@ function F0(d: D): int function F1(d: D, x: int): int
requires x < 100;
- requires d == #D.Red ==> x == 200; // (an impossibility, given the first precondition, so d != Red)
+ requires d == D.Red ==> x == 200; // (an impossibility, given the first precondition, so d != Red)
{
match (d)
case Purple => 80
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy index 2f59db73..b402c335 100644 --- a/Test/dafny0/DTypes.dfy +++ b/Test/dafny0/DTypes.dfy @@ -80,7 +80,7 @@ datatype Data { }
function G(d: Data): int
- requires d != #Data.Lemon;
+ requires d != Data.Lemon;
{
match d
case Lemon => G(d)
@@ -144,19 +144,19 @@ class DatatypeInduction<T> { method IntegerInduction_Succeeds(a: array<int>)
requires a != null;
requires a.Length == 0 || a[0] == 0;
- requires (forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1);
+ requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;
{
// The following assertion can be proved by induction:
- assert (forall n {:induction} :: 0 <= n && n < a.Length ==> a[n] == n*n);
+ assert forall n {:induction} :: 0 <= n && n < a.Length ==> a[n] == n*n;
}
method IntegerInduction_Fails(a: array<int>)
requires a != null;
requires a.Length == 0 || a[0] == 0;
- requires (forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1);
+ requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;
{
// ...but the induction heuristics don't recognize the situation as one where
// applying induction would be profitable:
- assert (forall n :: 0 <= n && n < a.Length ==> a[n] == n*n); // error reported
+ assert forall n :: 0 <= n && n < a.Length ==> a[n] == n*n; // error reported
}
}
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index 998b20bc..9a16a91a 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -19,14 +19,14 @@ class Node { method Init()
modifies this;
- ensures Repr(#List.Nil);
+ ensures Repr(Nil);
{
next := null;
}
method Add(d: int, L: List<int>) returns (r: Node)
requires Repr(L);
- ensures r != null && r.Repr(#List.Cons(d, L));
+ ensures r != null && r.Repr(Cons(d, L));
{
r := new Node;
r.data := d;
@@ -49,14 +49,14 @@ class AnotherNode { }
method Create() returns (n: AnotherNode)
- ensures Repr(n, #List.Nil);
+ ensures Repr(n, Nil);
{
n := null;
}
method Add(n: AnotherNode, d: int, L: List<int>) returns (r: AnotherNode)
requires Repr(n, L);
- ensures Repr(r, #List.Cons(d, L));
+ ensures Repr(r, Cons(d, L));
{
r := new AnotherNode;
r.data := d;
@@ -117,7 +117,7 @@ class NestedMatchExpr { method TestNesting0()
{
var x := 5;
- var list := #List.Cons(3, #List.Cons(6, #List.Nil));
+ var list := Cons(3, Cons(6, Nil));
assert Cadr(list, x) == 6;
match (list) {
case Nil => assert false;
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index 6b7ce9b9..161ac22f 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -47,7 +47,7 @@ function method FenEric<T>(t0: T, t1: T): T; datatype Pair<T> { Pr(T, T); }
method K(n: nat, i: int) {
- match (#Pair.Pr(n, i)) {
+ match (Pair.Pr(n, i)) {
case Pr(k, l) =>
assert k == n; // fine: although the type of k is int, we know it's equal to n
assert 0 <= k;
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy index d8c8d91d..930c4253 100644 --- a/Test/dafny0/Simple.dfy +++ b/Test/dafny0/Simple.dfy @@ -46,7 +46,7 @@ datatype List<T> { datatype WildData {
Something();
- JustAboutAnything<G,H>(G, myName: set<H>, int, WildData);
+ JustAboutAnything(bool, myName: set<int>, int, WildData);
More(List<int>);
}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index a5f02dc6..3359cff1 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -211,19 +211,19 @@ class AllocatedTests { assert allocated(6);
assert allocated(6);
assert allocated(null);
- assert allocated(#Lindgren.HerrNilsson);
+ assert allocated(Lindgren.HerrNilsson);
match (d) {
case Pippi(n) => assert allocated(n);
case Longstocking(q, dd) => assert allocated(q); assert allocated(dd);
case HerrNilsson => assert old(allocated(d));
}
- var ls := #Lindgren.Longstocking([], d);
+ var ls := Lindgren.Longstocking([], d);
assert allocated(ls);
assert old(allocated(ls));
- assert old(allocated(#Lindgren.Longstocking([r], d)));
- assert old(allocated(#Lindgren.Longstocking([n], d))); // error, because n was not allocated initially
+ assert old(allocated(Lindgren.Longstocking([r], d)));
+ assert old(allocated(Lindgren.Longstocking([n], d))); // error, because n was not allocated initially
}
}
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 226eadbe..5d411eb3 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -79,7 +79,7 @@ class Termination { method Q<T>(list: List<T>) {
var l := list;
- while (l != #List.Nil)
+ while (l != List.Nil)
decreases l;
{
call x, l := Traverse(l);
@@ -87,8 +87,8 @@ class Termination { }
method Traverse<T>(a: List<T>) returns (val: T, b: List<T>);
- requires a != #List.Nil;
- ensures a == #List.Cons(val, b);
+ requires a != List.Nil;
+ ensures a == List.Cons(val, b);
}
datatype List<T> {
@@ -245,7 +245,7 @@ function Zipper0<T>(a: List<T>, b: List<T>): List<T> {
match a
case Nil => b
- case Cons(x, c) => #List.Cons(x, Zipper0(b, c)) // error: cannot prove termination
+ case Cons(x, c) => List.Cons(x, Zipper0(b, c)) // error: cannot prove termination
}
function Zipper1<T>(a: List<T>, b: List<T>, k: bool): List<T>
@@ -253,7 +253,7 @@ function Zipper1<T>(a: List<T>, b: List<T>, k: bool): List<T> {
match a
case Nil => b
- case Cons(x, c) => #List.Cons(x, Zipper1(b, c, !k))
+ case Cons(x, c) => List.Cons(x, Zipper1(b, c, !k))
}
function Zipper2<T>(a: List<T>, b: List<T>): List<T>
@@ -262,7 +262,7 @@ function Zipper2<T>(a: List<T>, b: List<T>): List<T> {
match a
case Nil => b
- case Cons(x, c) => #List.Cons(x, Zipper2(b, c))
+ case Cons(x, c) => List.Cons(x, Zipper2(b, c))
}
// -------------------------- test translation of while (*) -----------------
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy index 6fe86493..a932eccf 100644 --- a/Test/dafny0/TypeAntecedents.dfy +++ b/Test/dafny0/TypeAntecedents.dfy @@ -7,14 +7,14 @@ datatype Unit { It; } datatype Color { Yellow; Blue; }
function F(a: Wrapper<Unit>): bool
- ensures a == #Wrapper.Wrap(#Unit.It);
+ ensures a == Wrapper.Wrap(Unit.It);
{
match a
case Wrap(u) => G(u)
}
function G(u: Unit): bool
- ensures u == #Unit.It;
+ ensures u == Unit.It;
{
match u
case It => true
@@ -23,19 +23,19 @@ function G(u: Unit): bool method BadLemma(c0: Color, c1: Color)
ensures c0 == c1;
{
- var w0 := #Wrapper.Wrap(c0);
- var w1 := #Wrapper.Wrap(c1);
+ var w0 := Wrapper.Wrap(c0);
+ var w1 := Wrapper.Wrap(c1);
// Manually, add the following assertions in Boogie. (These would
// be ill-typed in Dafny.)
- // assert _default.F($Heap, this, w0#6);
- // assert _default.F($Heap, this, w1#7);
+ // assert _default.F($Heap, this, w#06);
+ // assert _default.F($Heap, this, w#17);
assert w0 == w1; // this would be bad news (it should be reported as an error)
}
method Main() {
- call BadLemma(#Color.Yellow, #Color.Blue);
+ call BadLemma(Color.Yellow, Color.Blue);
assert false; // this shows how things can really go wrong if BadLemma verified successfully
}
@@ -82,9 +82,9 @@ method M(list: List, S: set<MyClass>) returns (ret: int) // note, the definedness problem in the next line sits inside an unreachable branch
assert (forall t: MyClass :: t != null ==> (if t.H() == 5 then true else 10 / 0 == 3));
- assert TakesADatatype(#List.Nil) == 12;
- assert TakesADatatype(#List.Cons(null, #List.Nil)) == 12;
- assert AlsoTakesADatatype(#GenData.Pair(false, true)) == 17;
+ assert TakesADatatype(List.Nil) == 12;
+ assert TakesADatatype(List.Cons(null, List.Nil)) == 12;
+ assert AlsoTakesADatatype(GenData.Pair(false, true)) == 17;
}
method N() returns (k: MyClass)
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 792c8fac..7deeb0a1 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -1,9 +1,9 @@ class C {
function F(c: C, d: D): bool { true }
method M(x: int) returns (y: int, c: C)
- requires F(#D.A, this); // 2 errors
+ requires F(D.A, this); // 2 errors
requires F(4, 5); // 2 errors
- requires F(this, #D.A); // good
+ requires F(this, D.A); // good
{ }
method Caller()
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index d785eead..0e4c58e0 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -169,7 +169,7 @@ function FooD(n: nat, d: D): int {
match d
case Nothing =>
- if n == 0 then 10 else FooD(n-1, #D.Something(d))
+ if n == 0 then 10 else FooD(n-1, D.Something(d))
case Something(next) =>
if n < 100 then n + 12 else FooD(n-13, next)
}
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index d5b3862b..3a455077 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -17,13 +17,13 @@ datatype Tree { Leaf; Node(Tree, Nat, Tree); } function not(b: Bool): Bool
{
match b
- case False => #Bool.True
- case True => #Bool.False
+ case False => True
+ case True => False
}
function and(a: Bool, b: Bool): Bool
{
- if a == #Bool.True && b == #Bool.True then #Bool.True else #Bool.False
+ if a == True && b == True then True else False
}
// Natural number functions
@@ -32,13 +32,13 @@ function add(x: Nat, y: Nat): Nat {
match x
case Zero => y
- case Suc(w) => #Nat.Suc(add(w, y))
+ case Suc(w) => Suc(add(w, y))
}
function minus(x: Nat, y: Nat): Nat
{
match x
- case Zero => #Nat.Zero
+ case Zero => Zero
case Suc(a) => match y
case Zero => x
case Suc(b) => minus(a, b)
@@ -48,38 +48,38 @@ function eq(x: Nat, y: Nat): Bool {
match x
case Zero => (match y
- case Zero => #Bool.True
- case Suc(b) => #Bool.False)
+ case Zero => True
+ case Suc(b) => False)
case Suc(a) => (match y
- case Zero => #Bool.False
+ case Zero => False
case Suc(b) => eq(a, b))
}
function leq(x: Nat, y: Nat): Bool
{
match x
- case Zero => #Bool.True
+ case Zero => True
case Suc(a) => match y
- case Zero => #Bool.False
+ case Zero => False
case Suc(b) => leq(a, b)
}
function less(x: Nat, y: Nat): Bool
{
match y
- case Zero => #Bool.False
+ case Zero => False
case Suc(b) => match x
- case Zero => #Bool.True
+ case Zero => True
case Suc(a) => less(a, b)
}
function min(x: Nat, y: Nat): Nat
{
match x
- case Zero => #Nat.Zero
+ case Zero => Zero
case Suc(a) => match y
- case Zero => #Nat.Zero
- case Suc(b) => #Nat.Suc(min(a, b))
+ case Zero => Zero
+ case Suc(b) => Suc(min(a, b))
}
function max(x: Nat, y: Nat): Nat
@@ -88,7 +88,7 @@ function max(x: Nat, y: Nat): Nat case Zero => y
case Suc(a) => match y
case Zero => x
- case Suc(b) => #Nat.Suc(max(a, b))
+ case Suc(b) => Suc(max(a, b))
}
// List functions
@@ -97,22 +97,22 @@ function concat(xs: List, ys: List): List {
match xs
case Nil => ys
- case Cons(x,tail) => #List.Cons(x, concat(tail, ys))
+ case Cons(x,tail) => Cons(x, concat(tail, ys))
}
function mem(x: Nat, xs: List): Bool
{
match xs
- case Nil => #Bool.False
- case Cons(y, ys) => if x == y then #Bool.True else mem(x, ys)
+ case Nil => False
+ case Cons(y, ys) => if x == y then True else mem(x, ys)
}
function delete(n: Nat, xs: List): List
{
match xs
- case Nil => #List.Nil
+ case Nil => Nil
case Cons(y, ys) =>
- if y == n then delete(n, ys) else #List.Cons(y, delete(n, ys))
+ if y == n then delete(n, ys) else Cons(y, delete(n, ys))
}
function drop(n: Nat, xs: List): List
@@ -120,38 +120,38 @@ function drop(n: Nat, xs: List): List match n
case Zero => xs
case Suc(m) => match xs
- case Nil => #List.Nil
+ case Nil => Nil
case Cons(x, tail) => drop(m, tail)
}
function take(n: Nat, xs: List): List
{
match n
- case Zero => #List.Nil
+ case Zero => Nil
case Suc(m) => match xs
- case Nil => #List.Nil
- case Cons(x, tail) => #List.Cons(x, take(m, tail))
+ case Nil => Nil
+ case Cons(x, tail) => Cons(x, take(m, tail))
}
function len(xs: List): Nat
{
match xs
- case Nil => #Nat.Zero
- case Cons(y, ys) => #Nat.Suc(len(ys))
+ case Nil => Zero
+ case Cons(y, ys) => Suc(len(ys))
}
function count(x: Nat, xs: List): Nat
{
match xs
- case Nil => #Nat.Zero
+ case Nil => Zero
case Cons(y, ys) =>
- if x == y then #Nat.Suc(count(x, ys)) else count(x, ys)
+ if x == y then Suc(count(x, ys)) else count(x, ys)
}
function last(xs: List): Nat
{
match xs
- case Nil => #Nat.Zero
+ case Nil => Zero
case Cons(y, ys) => match ys
case Nil => y
case Cons(z, zs) => last(ys)
@@ -160,39 +160,39 @@ function last(xs: List): Nat function mapF(xs: List): List
{
match xs
- case Nil => #List.Nil
- case Cons(y, ys) => #List.Cons(HardcodedUninterpretedFunction(y), mapF(ys))
+ case Nil => Nil
+ case Cons(y, ys) => Cons(HardcodedUninterpretedFunction(y), mapF(ys))
}
function HardcodedUninterpretedFunction(n: Nat): Nat;
function takeWhileAlways(hardcodedResultOfP: Bool, xs: List): List
{
match xs
- case Nil => #List.Nil
+ case Nil => Nil
case Cons(y, ys) =>
- if whilePredicate(hardcodedResultOfP, y) == #Bool.True
- then #List.Cons(y, takeWhileAlways(hardcodedResultOfP, ys))
- else #List.Nil
+ if whilePredicate(hardcodedResultOfP, y) == True
+ then Cons(y, takeWhileAlways(hardcodedResultOfP, ys))
+ else Nil
}
function whilePredicate(result: Bool, arg: Nat): Bool { result }
function dropWhileAlways(hardcodedResultOfP: Bool, xs: List): List
{
match xs
- case Nil => #List.Nil
+ case Nil => Nil
case Cons(y, ys) =>
- if whilePredicate(hardcodedResultOfP, y) == #Bool.True
+ if whilePredicate(hardcodedResultOfP, y) == True
then dropWhileAlways(hardcodedResultOfP, ys)
- else #List.Cons(y, ys)
+ else Cons(y, ys)
}
function filterP(xs: List): List
{
match xs
- case Nil => #List.Nil
+ case Nil => Nil
case Cons(y, ys) =>
- if HardcodedUninterpretedPredicate(y) == #Bool.True
- then #List.Cons(y, filterP(ys))
+ if HardcodedUninterpretedPredicate(y) == True
+ then Cons(y, filterP(ys))
else filterP(ys)
}
function HardcodedUninterpretedPredicate(n: Nat): Bool;
@@ -200,37 +200,37 @@ function HardcodedUninterpretedPredicate(n: Nat): Bool; function insort(n: Nat, xs: List): List
{
match xs
- case Nil => #List.Cons(n, #List.Nil)
+ case Nil => Cons(n, Nil)
case Cons(y, ys) =>
- if leq(n, y) == #Bool.True
- then #List.Cons(n, #List.Cons(y, ys))
- else #List.Cons(y, ins(n, ys))
+ if leq(n, y) == True
+ then Cons(n, Cons(y, ys))
+ else Cons(y, ins(n, ys))
}
function ins(n: Nat, xs: List): List
{
match xs
- case Nil => #List.Cons(n, #List.Nil)
+ case Nil => Cons(n, Nil)
case Cons(y, ys) =>
- if less(n, y) == #Bool.True
- then #List.Cons(n, #List.Cons(y, ys))
- else #List.Cons(y, ins(n, ys))
+ if less(n, y) == True
+ then Cons(n, Cons(y, ys))
+ else Cons(y, ins(n, ys))
}
function ins1(n: Nat, xs: List): List
{
match xs
- case Nil => #List.Cons(n, #List.Nil)
+ case Nil => Cons(n, Nil)
case Cons(y, ys) =>
if n == y
- then #List.Cons(y, ys)
- else #List.Cons(y, ins1(n, ys))
+ then Cons(y, ys)
+ else Cons(y, ins1(n, ys))
}
function sort(xs: List): List
{
match xs
- case Nil => #List.Nil
+ case Nil => Nil
case Cons(y, ys) => insort(y, sort(ys))
}
@@ -239,17 +239,17 @@ function sort(xs: List): List function zip(a: List, b: List): PList
{
match a
- case Nil => #PList.PNil
+ case Nil => PNil
case Cons(x, xs) => match b
- case Nil => #PList.PNil
- case Cons(y, ys) => #PList.PCons(#Pair.Pair(x, y), zip(xs, ys))
+ case Nil => PNil
+ case Cons(y, ys) => PCons(Pair.Pair(x, y), zip(xs, ys))
}
function zipConcat(x: Nat, xs: List, more: List): PList
{
match more
- case Nil => #PList.PNil
- case Cons(y, ys) => #PList.PCons(#Pair.Pair(x, y), zip(xs, ys))
+ case Nil => PNil
+ case Cons(y, ys) => PCons(Pair.Pair(x, y), zip(xs, ys))
}
// Binary tree functions
@@ -257,15 +257,15 @@ function zipConcat(x: Nat, xs: List, more: List): PList function height(t: Tree): Nat
{
match t
- case Leaf => #Nat.Zero
- case Node(l, x, r) => #Nat.Suc(max(height(l), height(r)))
+ case Leaf => Zero
+ case Node(l, x, r) => Suc(max(height(l), height(r)))
}
function mirror(t: Tree): Tree
{
match t
- case Leaf => #Tree.Leaf
- case Node(l, x, r) => #Tree.Node(mirror(r), x, mirror(l))
+ case Leaf => Leaf
+ case Node(l, x, r) => Node(mirror(r), x, mirror(l))
}
// The theorems to be proved
@@ -281,24 +281,24 @@ ghost method P2() }
ghost method P3()
- ensures (forall n, xs, ys :: leq(count(n, xs), count(n, concat(xs, ys))) == #Bool.True);
+ ensures (forall n, xs, ys :: leq(count(n, xs), count(n, concat(xs, ys))) == True);
{
}
ghost method P4()
- ensures (forall n, xs :: add(#Nat.Suc(#Nat.Zero), count(n, xs)) == count(n, #List.Cons(n, xs)));
+ ensures (forall n, xs :: add(Suc(Zero), count(n, xs)) == count(n, Cons(n, xs)));
{
}
ghost method P5()
ensures (forall n, xs, x ::
- add(#Nat.Suc(#Nat.Zero), count(n, xs)) == count(n, #List.Cons(x, xs))
+ add(Suc(Zero), count(n, xs)) == count(n, Cons(x, xs))
==> n == x);
{
}
ghost method P6()
- ensures (forall m, n :: minus(n, add(n, m)) == #Nat.Zero);
+ ensures (forall m, n :: minus(n, add(n, m)) == Zero);
{
}
@@ -318,12 +318,12 @@ ghost method P9() }
ghost method P10()
- ensures (forall m :: minus(m, m) == #Nat.Zero);
+ ensures (forall m :: minus(m, m) == Zero);
{
}
ghost method P11()
- ensures (forall xs :: drop(#Nat.Zero, xs) == xs);
+ ensures (forall xs :: drop(Zero, xs) == xs);
{
}
@@ -333,7 +333,7 @@ ghost method P12() }
ghost method P13()
- ensures (forall n, x, xs :: drop(#Nat.Suc(n), #List.Cons(x, xs)) == drop(n, xs));
+ ensures (forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs));
{
}
@@ -343,22 +343,22 @@ ghost method P14() }
ghost method P15()
- ensures (forall x, xs :: len(ins(x, xs)) == #Nat.Suc(len(xs)));
+ ensures (forall x, xs :: len(ins(x, xs)) == Suc(len(xs)));
{
}
ghost method P16()
- ensures (forall x, xs :: xs == #List.Nil ==> last(#List.Cons(x, xs)) == x);
+ ensures (forall x, xs :: xs == Nil ==> last(Cons(x, xs)) == x);
{
}
ghost method P17()
- ensures (forall n :: leq(n, #Nat.Zero) == #Bool.True <==> n == #Nat.Zero);
+ ensures (forall n :: leq(n, Zero) == True <==> n == Zero);
{
}
ghost method P18()
- ensures (forall i, m :: less(i, #Nat.Suc(add(i, m))) == #Bool.True);
+ ensures (forall i, m :: less(i, Suc(add(i, m))) == True);
{
}
@@ -371,15 +371,15 @@ ghost method P20() ensures (forall xs :: len(sort(xs)) == len(xs));
{
// proving this theorem requires an additional lemma:
- assert (forall k, ks :: len(ins(k, ks)) == len(#List.Cons(k, ks)));
+ assert (forall k, ks :: len(ins(k, ks)) == len(Cons(k, ks)));
// ...and one manually introduced case study:
assert (forall ys ::
- sort(ys) == #List.Nil ||
- (exists z, zs :: sort(ys) == #List.Cons(z, zs)));
+ sort(ys) == Nil ||
+ (exists z, zs :: sort(ys) == Cons(z, zs)));
}
ghost method P21()
- ensures (forall n, m :: leq(n, add(n, m)) == #Bool.True);
+ ensures (forall n, m :: leq(n, add(n, m)) == True);
{
}
@@ -394,37 +394,37 @@ ghost method P23() }
ghost method P24()
- ensures (forall a, b :: max(a, b) == a <==> leq(b, a) == #Bool.True);
+ ensures (forall a, b :: max(a, b) == a <==> leq(b, a) == True);
{
}
ghost method P25()
- ensures (forall a, b :: max(a, b) == b <==> leq(a, b) == #Bool.True);
+ ensures (forall a, b :: max(a, b) == b <==> leq(a, b) == True);
{
}
ghost method P26()
- ensures (forall x, xs, ys :: mem(x, xs) == #Bool.True ==> mem(x, concat(xs, ys)) == #Bool.True);
+ ensures (forall x, xs, ys :: mem(x, xs) == True ==> mem(x, concat(xs, ys)) == True);
{
}
ghost method P27()
- ensures (forall x, xs, ys :: mem(x, ys) == #Bool.True ==> mem(x, concat(xs, ys)) == #Bool.True);
+ ensures (forall x, xs, ys :: mem(x, ys) == True ==> mem(x, concat(xs, ys)) == True);
{
}
ghost method P28()
- ensures (forall x, xs :: mem(x, concat(xs, #List.Cons(x, #List.Nil))) == #Bool.True);
+ ensures (forall x, xs :: mem(x, concat(xs, Cons(x, Nil))) == True);
{
}
ghost method P29()
- ensures (forall x, xs :: mem(x, ins1(x, xs)) == #Bool.True);
+ ensures (forall x, xs :: mem(x, ins1(x, xs)) == True);
{
}
ghost method P30()
- ensures (forall x, xs :: mem(x, ins(x, xs)) == #Bool.True);
+ ensures (forall x, xs :: mem(x, ins(x, xs)) == True);
{
}
@@ -439,43 +439,43 @@ ghost method P32() }
ghost method P33()
- ensures (forall a, b :: min(a, b) == a <==> leq(a, b) == #Bool.True);
+ ensures (forall a, b :: min(a, b) == a <==> leq(a, b) == True);
{
}
ghost method P34()
- ensures (forall a, b :: min(a, b) == b <==> leq(b, a) == #Bool.True);
+ ensures (forall a, b :: min(a, b) == b <==> leq(b, a) == True);
{
}
ghost method P35()
- ensures (forall xs :: dropWhileAlways(#Bool.False, xs) == xs);
+ ensures (forall xs :: dropWhileAlways(False, xs) == xs);
{
}
ghost method P36()
- ensures (forall xs :: takeWhileAlways(#Bool.True, xs) == xs);
+ ensures (forall xs :: takeWhileAlways(True, xs) == xs);
{
}
ghost method P37()
- ensures (forall x, xs :: not(mem(x, delete(x, xs))) == #Bool.True);
+ ensures (forall x, xs :: not(mem(x, delete(x, xs))) == True);
{
}
ghost method P38()
- ensures (forall n, xs :: count(n, concat(xs, #List.Cons(n, #List.Nil))) == #Nat.Suc(count(n, xs)));
+ ensures (forall n, xs :: count(n, concat(xs, Cons(n, Nil))) == Suc(count(n, xs)));
{
}
ghost method P39()
ensures (forall n, x, xs ::
- add(count(n, #List.Cons(x, #List.Nil)), count(n, xs)) == count(n, #List.Cons(x, xs)));
+ add(count(n, Cons(x, Nil)), count(n, xs)) == count(n, Cons(x, xs)));
{
}
ghost method P40()
- ensures (forall xs :: take(#Nat.Zero, xs) == #List.Nil);
+ ensures (forall xs :: take(Zero, xs) == Nil);
{
}
@@ -485,7 +485,7 @@ ghost method P41() }
ghost method P42()
- ensures (forall n, x, xs :: take(#Nat.Suc(n), #List.Cons(x, xs)) == #List.Cons(x, take(n, xs)));
+ ensures (forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs)));
{
}
@@ -496,19 +496,19 @@ ghost method P43(p: Bool) }
ghost method P44()
- ensures (forall x, xs, ys :: zip(#List.Cons(x, xs), ys) == zipConcat(x, xs, ys));
+ ensures (forall x, xs, ys :: zip(Cons(x, xs), ys) == zipConcat(x, xs, ys));
{
}
ghost method P45()
ensures (forall x, xs, y, ys ::
- zip(#List.Cons(x, xs), #List.Cons(y, ys)) ==
- #PList.PCons(#Pair.Pair(x, y), zip(xs, ys)));
+ zip(Cons(x, xs), Cons(y, ys)) ==
+ PCons(Pair.Pair(x, y), zip(xs, ys)));
{
}
ghost method P46()
- ensures (forall ys :: zip(#List.Nil, ys) == #PList.PNil);
+ ensures (forall ys :: zip(Nil, ys) == PNil);
{
}
@@ -530,27 +530,27 @@ ghost method P54() }
ghost method P65()
- ensures (forall i, m :: less(i, #Nat.Suc(add(m, i))) == #Bool.True);
+ ensures (forall i, m :: less(i, Suc(add(m, i))) == True);
{
if (*) {
// the proof of this theorem follows from two lemmas:
- assert (forall i, m :: less(i, #Nat.Suc(add(i, m))) == #Bool.True);
+ assert (forall i, m :: less(i, Suc(add(i, m))) == True);
assert (forall m, n :: add(m, n) == add(n, m));
} else {
// a different way to prove it uses the following lemma:
- assert (forall x,y :: add(x, #Nat.Suc(y)) == #Nat.Suc(add(x,y)));
+ assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));
}
}
ghost method P67()
- ensures (forall m, n :: leq(n, add(m, n)) == #Bool.True);
+ ensures (forall m, n :: leq(n, add(m, n)) == True);
{
if (*) {
// the proof of this theorem follows from two lemmas:
- assert (forall m, n :: leq(n, add(n, m)) == #Bool.True);
+ assert (forall m, n :: leq(n, add(n, m)) == True);
assert (forall m, n :: add(m, n) == add(n, m));
} else {
// a different way to prove it uses the following lemma:
- assert (forall x,y :: add(x, #Nat.Suc(y)) == #Nat.Suc(add(x,y)));
+ assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));
}
}
diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy index 0d69b1b8..33442219 100644 --- a/Test/dafny1/SchorrWaite.dfy +++ b/Test/dafny1/SchorrWaite.dfy @@ -182,7 +182,7 @@ class Main { {
var t := root;
var p: Node := null; // parent of t in original graph
- ghost var path := #Path.Empty;
+ ghost var path := Path.Empty;
t.marked := true;
t.pathFromRoot := path;
ghost var stackNodes := [];
@@ -256,7 +256,7 @@ class Main { t.children := t.children[..t.childrenVisited] + [p] + t.children[t.childrenVisited + 1..];
p := t;
stackNodes := stackNodes + [t];
- path := #Path.Extend(path, t);
+ path := Path.Extend(path, t);
t := newT;
t.marked := true;
t.pathFromRoot := path;
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index 8d51bdd1..5cee5f6a 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -13,15 +13,15 @@ static function Subst(e: Expr, v: int, val: int): Expr {
match e
case Const(c) => e
- case Var(x) => if x == v then #Expr.Const(val) else e
- case Nary(op, args) => #Expr.Nary(op, SubstList(args, v, val))
+ case Var(x) => if x == v then Expr.Const(val) else e
+ case Nary(op, args) => Expr.Nary(op, SubstList(args, v, val))
}
static function SubstList(l: List, v: int, val: int): List
{
match l
case Nil => l
- case Cons(e, tail) => #List.Cons(Subst(e, v, val), SubstList(tail, v, val))
+ case Cons(e, tail) => Cons(Subst(e, v, val), SubstList(tail, v, val))
}
static ghost method Theorem(e: Expr, v: int, val: int)
@@ -59,8 +59,8 @@ static function Substitute(e: Expression, v: int, val: int): Expression {
match e
case Const(c) => e
- case Var(x) => if x == v then #Expression.Const(val) else e
- case Nary(op, args) => #Expression.Nary(op, SubstSeq(e, args, v, val))
+ case Var(x) => if x == v then Expression.Const(val) else e
+ case Nary(op, args) => Expression.Nary(op, SubstSeq(e, args, v, val))
}
static function SubstSeq(/*ghost*/ parent: Expression,
diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy index f576850e..f363a023 100644 --- a/Test/dafny1/TreeDatatype.dfy +++ b/Test/dafny1/TreeDatatype.dfy @@ -12,14 +12,14 @@ datatype Tree { static function Inc(t: Tree): Tree
{
match t
- case Node(n, children) => #Tree.Node(n+1, ForestInc(children))
+ case Node(n, children) => Tree.Node(n+1, ForestInc(children))
}
static function ForestInc(forest: List<Tree>): List<Tree>
{
match forest
case Nil => forest
- case Cons(tree, tail) => #List.Cons(Inc(tree), ForestInc(tail))
+ case Cons(tree, tail) => List.Cons(Inc(tree), ForestInc(tail))
}
// ------------------ generic list, generic tree (but GInc defined only for GTree<int>
@@ -31,14 +31,14 @@ datatype GTree<T> { static function GInc(t: GTree<int>): GTree<int>
{
match t
- case Node(n, children) => #GTree.Node(n+1, GForestInc(children))
+ case Node(n, children) => GTree.Node(n+1, GForestInc(children))
}
static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
{
match forest
case Nil => forest
- case Cons(tree, tail) => #List.Cons(GInc(tree), GForestInc(tail))
+ case Cons(tree, tail) => List.Cons(GInc(tree), GForestInc(tail))
}
// ------------------ non-generic structures
@@ -55,14 +55,14 @@ datatype OneTree { static function XInc(t: OneTree): OneTree
{
match t
- case Node(n, children) => #OneTree.Node(n+1, XForestInc(children))
+ case Node(n, children) => OneTree.Node(n+1, XForestInc(children))
}
static function XForestInc(forest: TreeList): TreeList
{
match forest
case Nil => forest
- case Cons(tree, tail) => #TreeList.Cons(XInc(tree), XForestInc(tail))
+ case Cons(tree, tail) => TreeList.Cons(XInc(tree), XForestInc(tail))
}
// ------------------ fun with recursive functions
@@ -77,7 +77,7 @@ function len<T>(l: List<T>): int function SingletonList<T>(h: T): List<T>
ensures len(SingletonList(h)) == 1;
{
- #List.Cons(h, #List.Nil)
+ List.Cons(h, List.Nil)
}
function Append<T>(a: List<T>, b: List<T>): List<T>
@@ -85,7 +85,7 @@ function Append<T>(a: List<T>, b: List<T>): List<T> {
match a
case Nil => b
- case Cons(h,t) => #List.Cons(h, Append(t, b))
+ case Cons(h,t) => List.Cons(h, Append(t, b))
}
function Rotate<T>(n: int, l: List<T>): List<T>
|