summaryrefslogtreecommitdiff
path: root/Source/Dafny
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-05-21 18:15:17 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2011-05-21 18:15:17 -0700
commit9dbf2a6ce1e130f634c27da7bc300001e28aedaf (patch)
tree929593e6a181ba2cfb4fe94d5157f73f3667fae2 /Source/Dafny
parent1aa1ca45fc066c9f8d94eeff1a2dc140c49db393 (diff)
Dafny:
* started rewriting parsing of qualified identifiers in expressions * annoyingly, had to introduce AST nodes for concrete syntax * previous syntax for invoking datatype constructors: #List.Cons(h, t) new syntax: List.Cons(h, t) or, if only one datatype has a constructor named Cons: Cons(h, t) * Removed type parameters for datatype constructors from the grammar * Helped Test/VSI-Benchmarks/b4.dfy along with a couple of assertions (previously, its proving performance was highly varied)
Diffstat (limited to 'Source/Dafny')
-rw-r--r--Source/Dafny/Compiler.cs13
-rw-r--r--Source/Dafny/Dafny.atg63
-rw-r--r--Source/Dafny/DafnyAst.cs70
-rw-r--r--Source/Dafny/Parser.cs336
-rw-r--r--Source/Dafny/Printer.cs20
-rw-r--r--Source/Dafny/Resolver.cs184
-rw-r--r--Source/Dafny/Scanner.cs67
-rw-r--r--Source/Dafny/Translator.cs31
8 files changed, 535 insertions, 249 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) {
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 22:28:07 +0000