summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/Dafny/Cloner.cs11
-rw-r--r--Source/Dafny/Dafny.atg294
-rw-r--r--Source/Dafny/DafnyAst.cs145
-rw-r--r--Source/Dafny/Parser.cs1466
-rw-r--r--Source/Dafny/Printer.cs82
-rw-r--r--Source/Dafny/Resolver.cs502
-rw-r--r--Source/Dafny/Rewriter.cs6
-rw-r--r--Source/Dafny/Scanner.cs162
-rw-r--r--Source/Dafny/Translator.cs4
-rw-r--r--Test/dafny0/Backticks.dfy.expect2
-rw-r--r--Test/dafny0/CallStmtTests.dfy.expect2
-rw-r--r--Test/dafny0/CoPrefix.dfy.expect6
-rw-r--r--Test/dafny0/CoResolution.dfy.expect12
-rw-r--r--Test/dafny0/Coinductive.dfy.expect2
-rw-r--r--Test/dafny0/DatatypeUpdate.dfy7
-rw-r--r--Test/dafny0/DatatypeUpdate.dfy.expect2
-rw-r--r--Test/dafny0/Datatypes.dfy.expect4
-rw-r--r--Test/dafny0/EqualityTypes.dfy.expect6
-rw-r--r--Test/dafny0/FunctionSpecifications.dfy.expect2
-rw-r--r--Test/dafny0/Iterators.dfy.expect24
-rw-r--r--Test/dafny0/Modules0.dfy.expect12
-rw-r--r--Test/dafny0/Modules1.dfy.expect4
-rw-r--r--Test/dafny0/NatTypes.dfy.expect4
-rw-r--r--Test/dafny0/NewtypesResolution.dfy.expect12
-rw-r--r--Test/dafny0/OpaqueFunctions.dfy.expect30
-rw-r--r--Test/dafny0/Parallel.dfy.expect4
-rw-r--r--Test/dafny0/ParallelResolveErrors.dfy.expect8
-rw-r--r--Test/dafny0/RealCompare.dfy.expect4
-rw-r--r--Test/dafny0/ResolutionErrors.dfy4
-rw-r--r--Test/dafny0/ResolutionErrors.dfy.expect50
-rw-r--r--Test/dafny0/ReturnErrors.dfy.expect4
-rw-r--r--Test/dafny0/SmallTests.dfy.expect8
-rw-r--r--Test/dafny0/StatementExpressions.dfy.expect4
-rw-r--r--Test/dafny0/TailCalls.dfy.expect2
-rw-r--r--Test/dafny0/Termination.dfy.expect2
-rw-r--r--Test/dafny0/Trait/TraitExtend.dfy.expect4
-rw-r--r--Test/dafny0/TypeTests.dfy.expect14
-rw-r--r--Test/dafny0/snapshots/runtest.snapshot.expect26
-rw-r--r--Test/dafny2/SnapshotableTrees.dfy.expect2
-rw-r--r--Test/hofs/Field.dfy.expect8
-rw-r--r--Test/hofs/ResolveError.dfy.expect10
41 files changed, 1757 insertions, 1200 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 60e737b1..4e0ccdcf 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -293,9 +293,16 @@ namespace Microsoft.Dafny
pp.Add(new ExpressionPair(CloneExpr(p.A), CloneExpr(p.B)));
}
return new MapDisplayExpr(Tok(expr.tok), pp);
+
+ } else if (expr is NameSegment) {
+ var e = (NameSegment)expr;
+ return new NameSegment(Tok(e.tok), e.Name, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));
} else if (expr is ExprDotName) {
var e = (ExprDotName)expr;
- return new ExprDotName(Tok(e.tok), CloneExpr(e.Obj), e.SuffixName);
+ return new ExprDotName(Tok(e.tok), CloneExpr(e.Lhs), e.SuffixName);
+ } else if (expr is ApplySuffix) {
+ var e = (ApplySuffix)expr;
+ return new ApplySuffix(Tok(e.tok), CloneExpr(e.Lhs), e.Args.ConvertAll(CloneExpr));
} else if (expr is MemberSelectExpr) {
var e = (MemberSelectExpr)expr;
@@ -319,7 +326,7 @@ namespace Microsoft.Dafny
} else if (expr is ApplyExpr) {
var e = (ApplyExpr)expr;
- return new ApplyExpr(Tok(e.tok), Tok(e.OpenParen), CloneExpr(e.Function), e.Args.ConvertAll(CloneExpr));
+ return new ApplyExpr(Tok(e.tok), CloneExpr(e.Function), e.Args.ConvertAll(CloneExpr));
} else if (expr is OldExpr) {
var e = (OldExpr)expr;
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index b59c586a..29e33b35 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -107,11 +107,6 @@ bool IsLoopSpec() {
return la.kind == _invariant | la.kind == _decreases | la.kind == _modifies;
}
-bool IsLoopSpecOrAlternative() {
- Token x = scanner.Peek();
- return IsLoopSpec() || (la.kind == _lbrace && x.kind == _case);
-}
-
bool IsParenStar() {
scanner.ResetPeek();
Token x = scanner.Peek();
@@ -164,6 +159,10 @@ bool IsMapDisplay() {
return la.kind == _map && scanner.Peek().kind == _lbracket;
}
+bool IsSuffix() {
+ return la.kind == _dot || la.kind == _lbracket || la.kind == _openparen;
+}
+
string UnwildIdent(string x, bool allowWildcardId) {
if (x.StartsWith("_")) {
if (allowWildcardId && x.Length == 1) {
@@ -227,9 +226,7 @@ bool IsIdentColonOrBar() {
}
bool SemiFollowsCall(bool allowSemi, Expression e) {
- return allowSemi && la.kind == _semi &&
- (e is FunctionCallExpr || e is ApplyExpr ||
- (e is IdentifierSequence && ((IdentifierSequence)e).OpenParen != null));
+ return allowSemi && la.kind == _semi && e is ApplySuffix;
}
bool CloseOptionalBrace(bool usesOptionalBrace) {
@@ -304,6 +301,7 @@ TOKENS
verticalbar = '|'.
doublecolon = "::".
bullet = '\u2022'.
+ dot = '.'.
semi = ';'.
darrow = "=>".
arrow = "->".
@@ -396,8 +394,8 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
{ Attribute<ref attrs> }
NoUSIdent<out id>
- [ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, parent, attrs, false); .)
- "{" (. module.BodyStartTok = t; .)
+ [ "refines" QualifiedModuleName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, parent, attrs, false); .)
+ "{" (. module.BodyStartTok = t; .)
{ SubModuleDecl<module, out sm> (. module.TopLevelDecls.Add(sm); .)
| ClassDecl<module, out c> (. module.TopLevelDecls.Add(c); .)
| TraitDecl<module, out trait> (. module.TopLevelDecls.Add(trait); .)
@@ -413,9 +411,9 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
|
"import" ["opened" (.opened = true;.)]
NoUSIdent<out id>
- [ "=" QualifiedName<out idPath>
+ [ "=" QualifiedModuleName<out idPath>
(. submodule = new AliasModuleDecl(idPath, id, parent, opened); .)
- | "as" QualifiedName<out idPath> ["default" QualifiedName<out idAssignment> ]
+ | "as" QualifiedModuleName<out idPath> ["default" QualifiedModuleName<out idAssignment> ]
(. submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); .)
]
[ SYNC ";"
@@ -434,12 +432,11 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
)
.
-QualifiedName<.out List<IToken> ids.>
-= (. IToken id; IToken idPrime; ids = new List<IToken>(); .)
+/* This production is used to parse module names, where it is known that it is a module name that is expected. */
+QualifiedModuleName<.out List<IToken> ids.>
+= (. IToken id; ids = new List<IToken>(); .)
Ident<out id> (. ids.Add(id); .)
- { IdentOrDigitsSuffix<out id, out idPrime> (. ids.Add(id);
- if (idPrime != null) { ids.Add(idPrime); }
- .)
+ { "." Ident<out id> (. ids.Add(id); .)
}
.
@@ -1024,7 +1021,8 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
.)
| Ident<out tok> (. gt = new List<Type>();
path = new List<IToken>(); .)
- { (. path.Add(tok); .)
+ { IF(la.kind == _dot) /* greedily parse as many identifiers as possible (if the next identifier really denotes a constructor in a "new" RHS, then it will be adjusted for later */
+ (. path.Add(tok); .)
"." Ident<out tok>
}
[ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt, path); .)
@@ -1131,7 +1129,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
theBuiltIns.CreateArrowTypeDecl(formals.Count);
if (isCoPredicate) {
// also create an arrow type for the corresponding prefix predicate
- theBuiltIns.CreateArrowTypeDecl(formals.Count);
+ theBuiltIns.CreateArrowTypeDecl(formals.Count + 1);
}
.)
.
@@ -1157,21 +1155,6 @@ FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ r
)
.
-LambdaSpec<.out Expression req, List<FrameExpression> reads.>
-= (. Contract.Requires(reads != null);
- Expression e; req = null; FrameExpression fe; .)
- { ( "requires" Expression<out e, true, false>
- (. if (req == null) {
- req = e;
- } else {
- req = new BinaryExpr(req.tok, BinaryExpr.Opcode.And, req, e);
- }
- .)
- | "reads" PossiblyWildFrameExpression<out fe, true> (. reads.Add(fe); .)
- )
- }
- .
-
PossiblyWildExpression<out Expression e, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr; .)
@@ -1487,15 +1470,17 @@ AlternativeBlock<.out List<GuardedAlternative> alternatives, out IToken endTok.>
}
"}" (. endTok = t; .)
.
-WhileStmt<out Statement/*!*/ stmt>
-= (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
+WhileStmt<out Statement stmt>
+= (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken x;
Expression guard = null; IToken guardEllipsis = null;
- List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
- List<Expression/*!*/> decreases = new List<Expression/*!*/>();
+
+ List<MaybeFreeExpression> invariants = new List<MaybeFreeExpression>();
+ List<Expression> decreases = new List<Expression>();
Attributes decAttrs = null;
Attributes modAttrs = null;
- List<FrameExpression/*!*/> mod = null;
- BlockStmt/*!*/ body = null; IToken bodyEllipsis = null;
+ List<FrameExpression> mod = null;
+
+ BlockStmt body = null; IToken bodyEllipsis = null;
IToken bodyStart = null, bodyEnd = null, endTok = Token.NoToken;
List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
@@ -1503,15 +1488,15 @@ WhileStmt<out Statement/*!*/ stmt>
.)
"while" (. x = t; .)
(
- IF(IsLoopSpecOrAlternative())
- LoopSpec<out invariants, out decreases, out mod, ref decAttrs, ref modAttrs>
+ IF(IsLoopSpec() || IsAlternative())
+ { LoopSpec<invariants, decreases, ref mod, ref decAttrs, ref modAttrs> }
AlternativeBlock<out alternatives, out endTok>
(. stmt = new AlternativeLoopStmt(x, endTok, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives); .)
|
( Guard<out guard> (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
| "..." (. guardEllipsis = t; .)
)
- LoopSpec<out invariants, out decreases, out mod, ref decAttrs, ref modAttrs>
+ { LoopSpec<invariants, decreases, ref mod, ref decAttrs, ref modAttrs> }
( IF(la.kind == _lbrace) /* if there's an open brace, claim it as the beginning of the loop body (as opposed to a BlockStmt following the loop) */
BlockStmt<out body, out bodyStart, out bodyEnd> (. endTok = body.EndTok; isDirtyLoop = false; .)
| IF(la.kind == _ellipsis) /* if there's an ellipsis, claim it as standing for the loop body (as opposed to a "...;" statement following the loop) */
@@ -1538,38 +1523,31 @@ WhileStmt<out Statement/*!*/ stmt>
.)
)
.
-LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs.>
-= (. FrameExpression/*!*/ fe;
- invariants = new List<MaybeFreeExpression/*!*/>();
- MaybeFreeExpression invariant = null;
- decreases = new List<Expression/*!*/>();
- mod = null;
+LoopSpec<.List<MaybeFreeExpression> invariants, List<Expression> decreases, ref List<FrameExpression> mod, ref Attributes decAttrs, ref Attributes modAttrs.>
+= (. Expression e; FrameExpression fe;
+ bool isFree = false; Attributes attrs = null;
.)
- {
- Invariant<out invariant> OldSemi (. invariants.Add(invariant); .)
+ ( SYNC
+ [ "free" (. isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated"); .)
+ ]
+ "invariant"
+ { IF(IsAttribute()) Attribute<ref attrs> }
+ Expression<out e, false, true> (. invariants.Add(new MaybeFreeExpression(e, isFree, attrs)); .)
+ OldSemi
| SYNC "decreases"
{ IF(IsAttribute()) Attribute<ref decAttrs> }
- DecreasesList<decreases, true, true> OldSemi
- | SYNC "modifies"
- { IF(IsAttribute()) Attribute<ref modAttrs> } (. mod = mod ?? new List<FrameExpression>(); .)
- [ FrameExpression<out fe, false, true> (. mod.Add(fe); .)
- { "," FrameExpression<out fe, false, true> (. mod.Add(fe); .)
- }
- ] OldSemi
- }
- .
-Invariant<out MaybeFreeExpression/*!*/ invariant>
-= (. bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; .)
- SYNC
- ["free" (. isFree = true;
- errors.Warning(t, "the 'free' keyword is soon to be deprecated");
- .)
- ]
- "invariant" { IF(IsAttribute()) Attribute<ref attrs> }
- Expression<out e, false, true> (. invariant = new MaybeFreeExpression(e, isFree, attrs); .)
+ DecreasesList<decreases, true, true>
+ OldSemi
+ | SYNC "modifies" (. mod = mod ?? new List<FrameExpression>(); .)
+ { IF(IsAttribute()) Attribute<ref modAttrs> }
+ FrameExpression<out fe, false, true> (. mod.Add(fe); .)
+ { "," FrameExpression<out fe, false, true> (. mod.Add(fe); .)
+ }
+ OldSemi
+ )
.
-DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard, bool allowLambda.>
-= (. Expression/*!*/ e; .)
+DecreasesList<.List<Expression> decreases, bool allowWildcard, bool allowLambda.>
+= (. Expression e; .)
PossiblyWildExpression<out e, allowLambda> (. if (!allowWildcard && e is WildcardExpr) {
SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods");
} else {
@@ -1758,17 +1736,16 @@ ModifyStmt<out Statement s>
.)
.
-CalcStmt<out Statement/*!*/ s>
+CalcStmt<out Statement s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x;
- CalcStmt.CalcOp/*!*/ op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;
- var lines = new List<Expression/*!*/>();
- var hints = new List<BlockStmt/*!*/>();
+ CalcStmt.CalcOp op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;
+ var lines = new List<Expression>();
+ var hints = new List<BlockStmt>();
CalcStmt.CalcOp stepOp;
var stepOps = new List<CalcStmt.CalcOp>();
CalcStmt.CalcOp maybeOp;
- Expression/*!*/ e;
- BlockStmt/*!*/ h;
+ Expression e;
IToken opTok;
IToken danglingOperator = null;
.)
@@ -1781,7 +1758,7 @@ CalcStmt<out Statement/*!*/ s>
.)
]
"{"
- { Expression<out e, false, true> (. lines.Add(e); stepOp = calcOp; danglingOperator = null; .)
+ { Expression<out e, false, true> (. lines.Add(e); stepOp = calcOp; danglingOperator = null; .)
";"
[ CalcOp<out opTok, out op> (. maybeOp = resOp.ResultOp(op);
if (maybeOp == null) {
@@ -1792,10 +1769,25 @@ CalcStmt<out Statement/*!*/ s>
danglingOperator = opTok;
}
.)
- ] (. stepOps.Add(stepOp); .)
- Hint<out h> (. hints.Add(h);
- if (h.Body.Count != 0) { danglingOperator = null; }
- .)
+ ] (. stepOps.Add(stepOp); .)
+
+ /* now for the hint, which we build up as a possibly empty sequence of statements placed into one BlockStmt */
+ (. var subhints = new List<Statement>();
+ IToken hintStart = la; IToken hintEnd = hintStart;
+ IToken t0, t1;
+ BlockStmt subBlock; Statement subCalc;
+ .)
+ { IF(la.kind == _lbrace || la.kind == _calc) /* Grab as a hint if possible, not a next line in the calculation whose expression begins with an open brace
+ * or StmtExpr containing a calc. A user has to rewrite such a line to be enclosed in parentheses.
+ */
+ ( BlockStmt<out subBlock, out t0, out t1> (. hintEnd = subBlock.EndTok; subhints.Add(subBlock); .)
+ | CalcStmt<out subCalc> (. hintEnd = subCalc.EndTok; subhints.Add(subCalc); .)
+ )
+ }
+ (. var h = new BlockStmt(hintStart, hintEnd, subhints); // if the hint is empty, hintStart is the first token of the next line, but it doesn't matter because the block statement is just used as a container
+ hints.Add(h);
+ if (h.Body.Count != 0) { danglingOperator = null; }
+ .)
}
"}"
(.
@@ -1836,25 +1828,7 @@ CalcOp<out IToken x, out CalcStmt.CalcOp/*!*/ op>
}
.)
.
-Hint<out BlockStmt s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); // returns an empty block statement if the hint is empty
- var subhints = new List<Statement/*!*/>();
- IToken bodyStart, bodyEnd;
- BlockStmt/*!*/ block;
- Statement/*!*/ calc;
- Token x = la;
- IToken endTok = x;
- .)
- { IF(la.kind == _lbrace || la.kind == _calc) /* Grab as a hint if possible, not a next line in the calculation whose expression begins with an open brace
- * or StmtExpr containing a calc. A user has to rewrite such a line to be enclosed in parentheses.
- */
- ( BlockStmt<out block, out bodyStart, out bodyEnd> (. endTok = block.EndTok; subhints.Add(block); .)
- | CalcStmt<out calc> (. endTok = calc.EndTok; subhints.Add(calc); .)
- )
- }
- (. s = new BlockStmt(x, endTok, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container
- .)
- .
+
/*------------------------------------------------------------------------*/
/* Note. In order to avoid LL(1) warnings for expressions that "parse as far as possible", it is
* necessary to use Coco/R's IF construct. That means there are two ways to check for some of
@@ -2130,25 +2104,25 @@ UnaryExpression<out Expression e, bool allowSemi, bool allowLambda>
| IF(IsMapDisplay()) /* this alternative must be checked before going into EndlessExpression, where there is another "map" */
"map" (. x = t; .)
MapDisplayExpr<x, out e>
- { Suffix<ref e> }
+ { IF(IsSuffix()) Suffix<ref e> }
| IF(IsLambda(allowLambda))
LambdaExpression<out e, allowSemi> /* this is an endless expression */
| EndlessExpression<out e, allowSemi, allowLambda>
- | DottedIdentifiersAndFunction<out e>
- { Suffix<ref e> }
+ | NameSegment<out e>
+ { IF(IsSuffix()) Suffix<ref e> }
| DisplayExpr<out e>
- { Suffix<ref e> }
+ { IF(IsSuffix()) Suffix<ref e> }
| MultiSetExpr<out e>
- { Suffix<ref e> }
+ { IF(IsSuffix()) Suffix<ref e> }
| ConstAtomExpression<out e, allowSemi, allowLambda>
- { Suffix<ref e> }
+ { IF(IsSuffix()) Suffix<ref e> }
)
.
Lhs<out Expression e>
= (. e = dummyExpr; // the assignment is to please the compiler, the dummy value to satisfy contracts in the event of a parse error
.)
- ( DottedIdentifiersAndFunction<out e>
+ ( NameSegment<out e>
{ Suffix<ref e> }
| ConstAtomExpression<out e, false, false>
Suffix<ref e>
@@ -2156,10 +2130,7 @@ Lhs<out Expression e>
)
.
-/* 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.)
- */
+/* A ConstAtomExpression is never an l-value, and does not start with an identifier. */
ConstAtomExpression<out Expression e, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
IToken/*!*/ x; BigInteger n; Basetypes.BigDec d;
@@ -2202,10 +2173,11 @@ LambdaExpression<out Expression e, bool allowSemi>
= (. IToken x = Token.NoToken;
IToken id; BoundVar bv;
var bvs = new List<BoundVar>();
- Expression body = null;
+ FrameExpression fe; Expression ee;
+ var reads = new List<FrameExpression>();
Expression req = null;
bool oneShot;
- var reads = new List<FrameExpression>();
+ Expression body = null;
.)
( WildIdent<out id, true> (. x = t; bvs.Add(new BoundVar(id, id.val, new InferredTypeProxy())); .)
| "(" (. x = t; .)
@@ -2216,7 +2188,9 @@ LambdaExpression<out Expression e, bool allowSemi>
]
")"
)
- LambdaSpec<out req, reads>
+ { "reads" PossiblyWildFrameExpression<out fe, true> (. reads.Add(fe); .)
+ | "requires" Expression<out ee, true, false> (. req = req == null ? ee : new BinaryExpr(req.tok, BinaryExpr.Opcode.And, req, ee); .)
+ }
LambdaArrow<out oneShot>
Expression<out body, allowSemi, true>
(. e = new LambdaExpr(x, oneShot, bvs, req, reads, body);
@@ -2224,8 +2198,8 @@ LambdaExpression<out Expression e, bool allowSemi>
.)
.
ParensExpression<out Expression e, bool allowSemi, bool allowLambda>
-= (. IToken x; IToken openParen;
- List<Expression> args = new List<Expression>();
+= (. IToken x;
+ var args = new List<Expression>();
.)
"(" (. x = t; .)
[ Expressions<args> ]
@@ -2238,15 +2212,10 @@ ParensExpression<out Expression e, bool allowSemi, bool allowLambda>
e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args);
}
.)
- { "(" (. openParen = t; args = new List<Expression>(); .)
- [ Expressions<args> ]
- ")"
- (. e = new ApplyExpr(x, openParen, e, args); .)
- }
.
DisplayExpr<out Expression e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
+ IToken x; List<Expression> elements;
e = dummyExpr;
.)
( "{" (. x = t; elements = new List<Expression/*!*/>(); .)
@@ -2440,55 +2409,56 @@ CasePattern<out CasePattern pat>
.)
.
/*------------------------------------------------------------------------*/
-DottedIdentifiersAndFunction<out Expression e>
-= (. IToken id, idPrime; IToken openParen = null;
- List<Expression> args = null;
- List<IToken> idents = new List<IToken>();
- e = null;
- var applyArgLists = new List<List<Expression>>();
+NameSegment<out Expression e>
+= (. IToken id;
+ IToken openParen = null; List<Expression> args = null;
.)
- Ident<out id> (. idents.Add(id); .)
- { IdentOrDigitsSuffix<out id, out idPrime> (. idents.Add(id);
- if (idPrime != null) { idents.Add(idPrime); id = idPrime; }
- .)
- }
- [ (. args = new List<Expression>(); .)
- [ "#" (. id.val = id.val + "#"; Expression k; .)
- "[" Expression<out k, true, true> "]" (. args.Add(k); .)
- ]
- "(" (. openParen = t; .)
- [ Expressions<args> ]
- ")"
- ]
-
- (. e = new IdentifierSequence(idents, openParen, args);
- foreach (var args_ in applyArgLists) {
- e = new ApplyExpr(id, openParen, e, args_);
+ Ident<out id>
+ [ HashCall<id, out openParen, out args> ]
+ /* Note, since HashCall updates id.val, we make sure not to use id.val until after the possibility of calling HashCall. */
+ (. e = new NameSegment(id, id.val, null);
+ if (openParen != null) {
+ e = new ApplySuffix(openParen, e, args);
}
.)
.
+/* The HashCall production extends a given identifier with a hash sign followed by
+ * a list of argument expressions. That is, if what was just parsed was an identifier id,
+ * then the HashCall production will continue parsing into id#[arg](args).
+ * One could imagine parsing just the id# as an expression, but Dafny doesn't do that
+ * since the first argument to a prefix predicate/method is textually set apart; instead
+ * if a programmer wants to curry the arguments, one has to resort to using a lambda
+ * expression, just like for other function applications.
+ * Note: This grammar production mutates the id.val field to append the hash sign.
+ */
+HashCall<.IToken id, out IToken openParen, out List<Expression> args.>
+= (. Expression k; args = new List<Expression>(); .)
+ "#" (. id.val = id.val + "#"; .)
+ "[" Expression<out k, true, true> "]" (. args.Add(k); .)
+ "(" (. openParen = t; .)
+ [ Expressions<args> ]
+ ")"
+ .
Suffix<ref Expression e>
= (. Contract.Requires(e != null); Contract.Ensures(e!=null);
- IToken id, x; List<Expression> args;
+ IToken id, x;
Expression e0 = null; Expression e1 = null; Expression ee; bool anyDots = false;
List<Expression> multipleLengths = null; bool takeRest = false; // takeRest is relevant only if multipleLengths is non-null
List<Expression> multipleIndices = null;
- bool func = false;
.)
- ( IdentOrDigitsSuffix<out id, out x> (. if (x != null) {
+ ( DotSuffix<out id, out x> (. if (x != null) {
// process id as a Suffix in its own right
e = new ExprDotName(id, e, id.val);
id = x; // move to the next Suffix
}
+ IToken openParen = null; List<Expression> args = null;
.)
- [ (. args = new List<Expression/*!*/>(); func = true; .)
- [ "#" (. id.val = id.val + "#"; Expression k; .)
- "[" Expression<out k, true, true> "]" (. args.Add(k); .)
- ]
- "(" (. IToken openParen = t; .)
- [ Expressions<args> ]
- ")" (. e = new FunctionCallExpr(id, id.val, e, openParen, args); .)
- ] (. if (!func) { e = new ExprDotName(id, e, id.val); } .)
+ [ HashCall<id, out openParen, out args> ]
+ (. e = new ExprDotName(id, e, id.val);
+ if (openParen != null) {
+ e = new ApplySuffix(openParen, e, args);
+ }
+ .)
| "[" (. x = t; .)
( Expression<out ee, true, true> (. e0 = ee; .)
( ".." (. anyDots = true; .)
@@ -2517,7 +2487,7 @@ Suffix<ref Expression e>
}
)
| ".." (. anyDots = true; .)
- [ Expression<out ee, true, true> (. e1 = ee; .)
+ [ Expression<out ee, true, true> (. e1 = ee; .)
]
)
(. if (multipleIndices != null) {
@@ -2555,9 +2525,9 @@ Suffix<ref Expression e>
}
.)
"]"
- | "(" (. IToken openParen = t; args = new List<Expression>(); .)
+ | "(" (. IToken openParen = t; var args = new List<Expression>(); .)
[ Expressions<args> ]
- ")" (. e = new ApplyExpr(e.tok, openParen, e, args); .)
+ ")" (. e = new ApplySuffix(openParen, e, args); .)
)
.
@@ -2654,7 +2624,7 @@ Ident<out IToken/*!*/ x>
// In the third case, x and y return as the tokens for the first and second digits.
// This parser production solves a problem where the scanner might parse a real number instead
// of stopping at the decimal point.
-IdentOrDigitsSuffix<out IToken x, out IToken y>
+DotSuffix<out IToken x, out IToken y>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null);
x = Token.NoToken;
y = null;
@@ -2666,7 +2636,7 @@ IdentOrDigitsSuffix<out IToken x, out IToken y>
int exponent = x.val.IndexOf('e');
if (0 <= exponent) {
// this is not a legal field/destructor name
- SemErr(x, "invalid IdentOrDigitsSuffix");
+ SemErr(x, "invalid DotSuffix");
} else {
int dot = x.val.IndexOf('.');
if (0 <= dot) {
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 58666c6a..d0e6e6fb 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -311,17 +311,6 @@ namespace Microsoft.Dafny {
// Type arguments to the type
public List<Type> TypeArgs = new List<Type> { };
- /// <summary>
- /// Used in error situations in order to reduce further error messages.
- /// </summary>
- //[Pure(false)]
- public static Type Flexible {
- get {
- Contract.Ensures(Contract.Result<Type>() != null);
- return new InferredTypeProxy();
- }
- }
-
[Pure]
public abstract string TypeName(ModuleDefinition/*?*/ context);
[Pure]
@@ -5295,6 +5284,47 @@ namespace Microsoft.Dafny {
: base(tok, name) { }
}
+ /// <summary>
+ /// This class is used only inside the resolver itself. It gets hung in the AST in uncompleted name segments.
+ /// </summary>
+ class Resolver_IdentifierExpr : Expression
+ {
+ public readonly TopLevelDecl Decl;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Decl != null);
+ Contract.Invariant(Type == null || Type is ResolverType_Module || Type is ResolverType_Type);
+ }
+
+ public class ResolverType_Module : Type
+ {
+ [Pure]
+ public override string TypeName(ModuleDefinition context) {
+ return "#module";
+ }
+ public override bool Equals(Type that) {
+ return that is ResolverType_Module;
+ }
+ }
+ public class ResolverType_Type : Type {
+ [Pure]
+ public override string TypeName(ModuleDefinition context) {
+ return "#type";
+ }
+ public override bool Equals(Type that) {
+ return that is ResolverType_Type;
+ }
+ }
+
+ public Resolver_IdentifierExpr(IToken tok, TopLevelDecl decl)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(decl != null);
+ Decl = decl;
+ Type = decl is ModuleDecl ? (Type)new ResolverType_Module() : new ResolverType_Type();
+ }
+ }
+
public abstract class DisplayExpression : Expression {
public readonly List<Expression> Elements;
[ContractInvariantMethod]
@@ -5353,7 +5383,6 @@ namespace Microsoft.Dafny {
}
}
- // Former FieldSelectExpression
public class MemberSelectExpr : Expression {
public readonly Expression Obj;
public readonly string MemberName;
@@ -5525,7 +5554,6 @@ namespace Microsoft.Dafny {
// Make a FunctionCallExpr otherwise, to call a resolvable anonymous function.
public readonly Expression Function;
public readonly List<Expression> Args;
- public readonly IToken OpenParen;
public override IEnumerable<Expression> SubExpressions {
get {
@@ -5536,11 +5564,10 @@ namespace Microsoft.Dafny {
}
}
- public ApplyExpr(IToken tok, IToken openParen, Expression receiver, List<Expression> args)
+ public ApplyExpr(IToken tok, Expression fn, List<Expression> args)
: base(tok)
{
- OpenParen = openParen;
- Function = receiver;
+ Function = fn;
Args = args;
}
}
@@ -6820,29 +6847,103 @@ namespace Microsoft.Dafny {
}
/// <summary>
- /// An ExprDotName desugars into either a FieldSelectExpr or a FunctionCallExpr (with a parameterless predicate function).
+ /// The parsing and resolution/type checking of expressions of the forms
+ /// 0. ident &lt; Types &gt;
+ /// 1. Expr . ident &lt; Types &gt;
+ /// 2. Expr ( Exprs )
+ /// 3. Expr [ Exprs ]
+ /// 4. Expr [ Expr .. Expr ]
+ /// is done as follows. These forms are parsed into the following AST classes:
+ /// 0. NameSegment
+ /// 1. ExprDotName
+ /// 2. ApplySuffix
+ /// 3. SeqSelectExpr or MultiSelectExpr
+ /// 4. SeqSelectExpr
+ ///
+ /// The first three of these inherit from ConcreteSyntaxExpression. The resolver will resolve
+ /// these into:
+ /// 0. IdentifierExpr or MemberSelectExpr (with .Lhs set to ImplicitThisExpr or StaticReceiverExpr)
+ /// 1. IdentifierExpr or MemberSelectExpr
+ /// 2. FuncionCallExpr or ApplyExpr
+ ///
+ /// The IdentifierExpr's that forms 0 and 1 can turn into sometimes denote the name of a module or
+ /// type. The .Type field of the corresponding resolved expressions are then the special Type subclasses
+ /// ResolutionType_Module and ResolutionType_Type, respectively. These will not be seen by the
+ /// verifier or compiler, since, in a well-formed program, the verifier and compiler will use the
+ /// .ResolvedExpr field of whatever form-1 expression contains these.
+ ///
+ /// Notes:
+ /// * IdentifierExpr and FunctionCallExpr are resolved-only expressions (that is, they don't contain
+ /// all the syntactic components that were used to parse them).
+ /// * Rather than the current SeqSelectExpr/MultiSelectExpr split of forms 3 and 4, it would
+ /// seem more natural to refactor these into 3: IndexSuffixExpr and 4: RangeSuffixExpr.
/// </summary>
- public class ExprDotName : ConcreteSyntaxExpression
+ abstract public class SuffixExpr : ConcreteSyntaxExpression {
+ public readonly Expression Lhs;
+ public SuffixExpr(IToken tok, Expression lhs)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(lhs != null);
+ Lhs = lhs;
+ }
+ }
+
+ public class NameSegment : ConcreteSyntaxExpression
+ {
+ public readonly string Name;
+ public readonly List<Type> OptTypeArguments;
+ public NameSegment(IToken tok, string name, List<Type> optTypeArguments)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Name = name;
+ OptTypeArguments = optTypeArguments;
+ }
+ }
+
+ /// <summary>
+ /// An ExprDotName desugars into either an IdentifierExpr (if the Lhs is a static name) or a MemberSelectExpr (if the Lhs is a computed expression).
+ /// </summary>
+ public class ExprDotName : SuffixExpr
{
- public readonly Expression Obj;
public readonly string SuffixName;
+ public readonly List<Type> OptTypeArguments;
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Obj != null);
Contract.Invariant(SuffixName != null);
}
public ExprDotName(IToken tok, Expression obj, string suffixName)
- : base(tok) {
+ : base(tok, obj) {
Contract.Requires(tok != null);
Contract.Requires(obj != null);
Contract.Requires(suffixName != null);
- this.Obj = obj;
this.SuffixName = suffixName;
}
}
+ /// <summary>
+ /// An ApplySuffix desugars into either an ApplyExpr or a FunctionCallExpr
+ /// </summary>
+ public class ApplySuffix : SuffixExpr
+ {
+ public readonly List<Expression> Args;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Args != null);
+ }
+
+ public ApplySuffix(IToken tok, Expression lhs, List<Expression> args)
+ : base(tok, lhs) {
+ Contract.Requires(tok != null);
+ Contract.Requires(lhs != null);
+ Contract.Requires(cce.NonNullElements(args));
+ Args = args;
+ }
+ }
+
public class IdentifierSequence : ConcreteSyntaxExpression
{
public readonly List<IToken> Tokens;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index d30a3fd9..79ace7f7 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -26,27 +26,28 @@ public class Parser {
public const int _verticalbar = 10;
public const int _doublecolon = 11;
public const int _bullet = 12;
- public const int _semi = 13;
- public const int _darrow = 14;
- public const int _arrow = 15;
- public const int _assume = 16;
- public const int _calc = 17;
- public const int _case = 18;
- public const int _decreases = 19;
- public const int _invariant = 20;
- public const int _map = 21;
- public const int _modifies = 22;
- public const int _reads = 23;
- public const int _requires = 24;
- public const int _lbrace = 25;
- public const int _rbrace = 26;
- public const int _lbracket = 27;
- public const int _rbracket = 28;
- public const int _openparen = 29;
- public const int _closeparen = 30;
- public const int _star = 31;
- public const int _notIn = 32;
- public const int _ellipsis = 33;
+ public const int _dot = 13;
+ public const int _semi = 14;
+ public const int _darrow = 15;
+ public const int _arrow = 16;
+ public const int _assume = 17;
+ public const int _calc = 18;
+ public const int _case = 19;
+ public const int _decreases = 20;
+ public const int _invariant = 21;
+ public const int _map = 22;
+ public const int _modifies = 23;
+ public const int _reads = 24;
+ public const int _requires = 25;
+ public const int _lbrace = 26;
+ public const int _rbrace = 27;
+ public const int _lbracket = 28;
+ public const int _rbracket = 29;
+ public const int _openparen = 30;
+ public const int _closeparen = 31;
+ public const int _star = 32;
+ public const int _notIn = 33;
+ public const int _ellipsis = 34;
public const int maxT = 133;
const bool T = true;
@@ -153,11 +154,6 @@ bool IsLoopSpec() {
return la.kind == _invariant | la.kind == _decreases | la.kind == _modifies;
}
-bool IsLoopSpecOrAlternative() {
- Token x = scanner.Peek();
- return IsLoopSpec() || (la.kind == _lbrace && x.kind == _case);
-}
-
bool IsParenStar() {
scanner.ResetPeek();
Token x = scanner.Peek();
@@ -210,6 +206,10 @@ bool IsMapDisplay() {
return la.kind == _map && scanner.Peek().kind == _lbracket;
}
+bool IsSuffix() {
+ return la.kind == _dot || la.kind == _lbracket || la.kind == _openparen;
+}
+
string UnwildIdent(string x, bool allowWildcardId) {
if (x.StartsWith("_")) {
if (allowWildcardId && x.Length == 1) {
@@ -273,9 +273,7 @@ bool IsIdentColonOrBar() {
}
bool SemiFollowsCall(bool allowSemi, Expression e) {
- return allowSemi && la.kind == _semi &&
- (e is FunctionCallExpr || e is ApplyExpr ||
- (e is IdentifierSequence && ((IdentifierSequence)e).OpenParen != null));
+ return allowSemi && la.kind == _semi && e is ApplySuffix;
}
bool CloseOptionalBrace(bool usesOptionalBrace) {
@@ -367,7 +365,7 @@ bool IsNotEndOfCase() {
TraitDecl/*!*/ trait;
Contract.Assert(defaultModule != null);
- while (la.kind == 34) {
+ while (la.kind == 35) {
Get();
Expect(7);
{
@@ -387,42 +385,42 @@ bool IsNotEndOfCase() {
}
while (StartOf(1)) {
switch (la.kind) {
- case 35: case 36: case 38: {
+ case 36: case 37: case 39: {
SubModuleDecl(defaultModule, out submodule);
defaultModule.TopLevelDecls.Add(submodule);
break;
}
- case 43: {
+ case 44: {
ClassDecl(defaultModule, out c);
defaultModule.TopLevelDecls.Add(c);
break;
}
- case 48: case 49: {
+ case 49: case 50: {
DatatypeDecl(defaultModule, out dt);
defaultModule.TopLevelDecls.Add(dt);
break;
}
- case 51: {
+ case 52: {
NewtypeDecl(defaultModule, out td);
defaultModule.TopLevelDecls.Add(td);
break;
}
- case 52: {
+ case 53: {
OtherTypeDecl(defaultModule, out td);
defaultModule.TopLevelDecls.Add(td);
break;
}
- case 54: {
+ case 55: {
IteratorDecl(defaultModule, out iter);
defaultModule.TopLevelDecls.Add(iter);
break;
}
- case 45: {
+ case 46: {
TraitDecl(defaultModule, out trait);
defaultModule.TopLevelDecls.Add(trait);
break;
}
- case 46: case 47: case 50: case 59: case 60: case 61: case 62: case 63: case 78: case 79: case 80: {
+ case 47: case 48: case 51: case 60: case 61: case 62: case 63: case 64: case 78: case 79: case 80: {
ClassMemberDecl(membersDefaultClass, false);
break;
}
@@ -455,94 +453,94 @@ bool IsNotEndOfCase() {
bool isAbstract = false;
bool opened = false;
- if (la.kind == 35 || la.kind == 36) {
- if (la.kind == 35) {
+ if (la.kind == 36 || la.kind == 37) {
+ if (la.kind == 36) {
Get();
isAbstract = true;
}
- Expect(36);
- while (la.kind == 25) {
+ Expect(37);
+ while (la.kind == 26) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 37) {
+ if (la.kind == 38) {
Get();
- QualifiedName(out idRefined);
+ QualifiedModuleName(out idRefined);
}
module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, parent, attrs, false);
- Expect(25);
+ Expect(26);
module.BodyStartTok = t;
while (StartOf(1)) {
switch (la.kind) {
- case 35: case 36: case 38: {
+ case 36: case 37: case 39: {
SubModuleDecl(module, out sm);
module.TopLevelDecls.Add(sm);
break;
}
- case 43: {
+ case 44: {
ClassDecl(module, out c);
module.TopLevelDecls.Add(c);
break;
}
- case 45: {
+ case 46: {
TraitDecl(module, out trait);
module.TopLevelDecls.Add(trait);
break;
}
- case 48: case 49: {
+ case 49: case 50: {
DatatypeDecl(module, out dt);
module.TopLevelDecls.Add(dt);
break;
}
- case 51: {
+ case 52: {
NewtypeDecl(module, out td);
module.TopLevelDecls.Add(td);
break;
}
- case 52: {
+ case 53: {
OtherTypeDecl(module, out td);
module.TopLevelDecls.Add(td);
break;
}
- case 54: {
+ case 55: {
IteratorDecl(module, out iter);
module.TopLevelDecls.Add(iter);
break;
}
- case 46: case 47: case 50: case 59: case 60: case 61: case 62: case 63: case 78: case 79: case 80: {
+ case 47: case 48: case 51: case 60: case 61: case 62: case 63: case 64: case 78: case 79: case 80: {
ClassMemberDecl(namedModuleDefaultClassMembers, false);
break;
}
}
}
- Expect(26);
+ Expect(27);
module.BodyEndTok = t;
module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
submodule = new LiteralModuleDecl(module, parent);
- } else if (la.kind == 38) {
+ } else if (la.kind == 39) {
Get();
- if (la.kind == 39) {
+ if (la.kind == 40) {
Get();
opened = true;
}
NoUSIdent(out id);
- if (la.kind == 40 || la.kind == 41) {
- if (la.kind == 40) {
+ if (la.kind == 41 || la.kind == 42) {
+ if (la.kind == 41) {
Get();
- QualifiedName(out idPath);
+ QualifiedModuleName(out idPath);
submodule = new AliasModuleDecl(idPath, id, parent, opened);
} else {
Get();
- QualifiedName(out idPath);
- if (la.kind == 42) {
+ QualifiedModuleName(out idPath);
+ if (la.kind == 43) {
Get();
- QualifiedName(out idAssignment);
+ QualifiedModuleName(out idAssignment);
}
submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened);
}
}
- if (la.kind == 13) {
- while (!(la.kind == 0 || la.kind == 13)) {SynErr(134); Get();}
+ if (la.kind == 14) {
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(134); Get();}
Get();
}
if (submodule == null) {
@@ -564,25 +562,25 @@ bool IsNotEndOfCase() {
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 43)) {SynErr(136); Get();}
- Expect(43);
- while (la.kind == 25) {
+ while (!(la.kind == 0 || la.kind == 44)) {SynErr(136); Get();}
+ Expect(44);
+ while (la.kind == 26) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 57) {
+ if (la.kind == 58) {
GenericParameters(typeArgs);
}
- if (la.kind == 44) {
+ if (la.kind == 45) {
Get();
Type(out trait);
}
- Expect(25);
+ Expect(26);
bodyStart = t;
while (StartOf(2)) {
ClassMemberDecl(members, true);
}
- Expect(26);
+ Expect(27);
c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, trait);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
@@ -599,29 +597,29 @@ bool IsNotEndOfCase() {
IToken bodyStart = Token.NoToken; // dummy assignment
bool co = false;
- while (!(la.kind == 0 || la.kind == 48 || la.kind == 49)) {SynErr(137); Get();}
- if (la.kind == 48) {
+ while (!(la.kind == 0 || la.kind == 49 || la.kind == 50)) {SynErr(137); Get();}
+ if (la.kind == 49) {
Get();
- } else if (la.kind == 49) {
+ } else if (la.kind == 50) {
Get();
co = true;
} else SynErr(138);
- while (la.kind == 25) {
+ while (la.kind == 26) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 57) {
+ if (la.kind == 58) {
GenericParameters(typeArgs);
}
- Expect(40);
+ Expect(41);
bodyStart = t;
DatatypeMemberDecl(ctors);
while (la.kind == 10) {
Get();
DatatypeMemberDecl(ctors);
}
- if (la.kind == 13) {
- while (!(la.kind == 0 || la.kind == 13)) {SynErr(139); Get();}
+ if (la.kind == 14) {
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(139); Get();}
Get();
}
if (co) {
@@ -641,12 +639,12 @@ bool IsNotEndOfCase() {
Type baseType = null;
Expression wh;
- Expect(51);
- while (la.kind == 25) {
+ Expect(52);
+ while (la.kind == 26) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- Expect(40);
+ Expect(41);
if (IsIdentColonOrBar()) {
NoUSIdent(out bvId);
if (la.kind == 8) {
@@ -671,24 +669,24 @@ bool IsNotEndOfCase() {
td = null;
Type ty;
- Expect(52);
- while (la.kind == 25) {
+ Expect(53);
+ while (la.kind == 26) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 29) {
+ if (la.kind == 30) {
Get();
- Expect(53);
- Expect(30);
+ Expect(54);
+ Expect(31);
eqSupport = TypeParameter.EqualitySupportValue.Required;
- if (la.kind == 57) {
+ if (la.kind == 58) {
GenericParameters(typeArgs);
}
} else if (StartOf(4)) {
- if (la.kind == 57) {
+ if (la.kind == 58) {
GenericParameters(typeArgs);
}
- if (la.kind == 40) {
+ if (la.kind == 41) {
Get();
Type(out ty);
td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs);
@@ -698,8 +696,8 @@ bool IsNotEndOfCase() {
td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);
}
- if (la.kind == 13) {
- while (!(la.kind == 0 || la.kind == 13)) {SynErr(142); Get();}
+ if (la.kind == 14) {
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(142); Get();}
Get();
}
}
@@ -727,19 +725,19 @@ bool IsNotEndOfCase() {
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 54)) {SynErr(143); Get();}
- Expect(54);
- while (la.kind == 25) {
+ while (!(la.kind == 0 || la.kind == 55)) {SynErr(143); Get();}
+ Expect(55);
+ while (la.kind == 26) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 29 || la.kind == 57) {
- if (la.kind == 57) {
+ if (la.kind == 30 || la.kind == 58) {
+ if (la.kind == 58) {
GenericParameters(typeArgs);
}
Formals(true, true, ins);
- if (la.kind == 55 || la.kind == 56) {
- if (la.kind == 55) {
+ if (la.kind == 56 || la.kind == 57) {
+ if (la.kind == 56) {
Get();
} else {
Get();
@@ -747,14 +745,14 @@ bool IsNotEndOfCase() {
}
Formals(false, true, outs);
}
- } else if (la.kind == 33) {
+ } else if (la.kind == 34) {
Get();
signatureEllipsis = t;
} else SynErr(144);
while (StartOf(5)) {
IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs);
}
- if (la.kind == 25) {
+ if (la.kind == 26) {
BlockStmt(out body, out bodyStart, out bodyEnd);
}
iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,
@@ -777,21 +775,21 @@ bool IsNotEndOfCase() {
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 45)) {SynErr(145); Get();}
- Expect(45);
- while (la.kind == 25) {
+ while (!(la.kind == 0 || la.kind == 46)) {SynErr(145); Get();}
+ Expect(46);
+ while (la.kind == 26) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 57) {
+ if (la.kind == 58) {
GenericParameters(typeArgs);
}
- Expect(25);
+ Expect(26);
bodyStart = t;
while (StartOf(2)) {
ClassMemberDecl(members, true);
}
- Expect(26);
+ Expect(27);
trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs);
trait.BodyStartTok = bodyStart;
trait.BodyEndTok = t;
@@ -804,8 +802,8 @@ bool IsNotEndOfCase() {
Function/*!*/ f;
MemberModifiers mmod = new MemberModifiers();
- while (la.kind == 46 || la.kind == 47) {
- if (la.kind == 46) {
+ while (la.kind == 47 || la.kind == 48) {
+ if (la.kind == 47) {
Get();
mmod.IsGhost = true;
} else {
@@ -813,7 +811,7 @@ bool IsNotEndOfCase() {
mmod.IsStatic = true;
}
}
- if (la.kind == 50) {
+ if (la.kind == 51) {
FieldDecl(mmod, mm);
} else if (la.kind == 78 || la.kind == 79 || la.kind == 80) {
FunctionDecl(mmod, out f);
@@ -828,14 +826,14 @@ bool IsNotEndOfCase() {
string name;
var args = new List<Expression>();
- Expect(25);
+ Expect(26);
Expect(8);
Expect(1);
name = t.val;
if (StartOf(7)) {
Expressions(args);
}
- Expect(26);
+ Expect(27);
attrs = new Attributes(name, args, attrs);
}
@@ -849,15 +847,14 @@ bool IsNotEndOfCase() {
}
- void QualifiedName(out List<IToken> ids) {
- IToken id; IToken idPrime; ids = new List<IToken>();
+ void QualifiedModuleName(out List<IToken> ids) {
+ IToken id; ids = new List<IToken>();
Ident(out id);
ids.Add(id);
- while (la.kind == 77) {
- IdentOrDigitsSuffix(out id, out idPrime);
- ids.Add(id);
- if (idPrime != null) { ids.Add(idPrime); }
-
+ while (la.kind == 13) {
+ Get();
+ Ident(out id);
+ ids.Add(id);
}
}
@@ -867,60 +864,18 @@ bool IsNotEndOfCase() {
x = t;
}
- void IdentOrDigitsSuffix(out IToken x, out IToken y) {
- Contract.Ensures(Contract.ValueAtReturn(out x) != null);
- x = Token.NoToken;
- y = null;
-
- Expect(77);
- if (la.kind == 1) {
- Get();
- x = t;
- } else if (la.kind == 2) {
- Get();
- x = t;
- } else if (la.kind == 4) {
- Get();
- x = t;
- int exponent = x.val.IndexOf('e');
- if (0 <= exponent) {
- // this is not a legal field/destructor name
- SemErr(x, "invalid IdentOrDigitsSuffix");
- } else {
- int dot = x.val.IndexOf('.');
- if (0 <= dot) {
- y = new Token();
- y.pos = x.pos + dot + 1;
- y.val = x.val.Substring(dot + 1);
- x.val = x.val.Substring(0, dot);
- y.col = x.col + dot + 1;
- y.line = x.line;
- y.filename = x.filename;
- y.kind = x.kind;
- }
- }
-
- } else if (la.kind == 24) {
- Get();
- x = t;
- } else if (la.kind == 23) {
- Get();
- x = t;
- } else SynErr(147);
- }
-
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
Contract.Requires(cce.NonNullElements(typeArgs));
IToken/*!*/ id;
TypeParameter.EqualitySupportValue eqSupport;
- Expect(57);
+ Expect(58);
NoUSIdent(out id);
eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
- if (la.kind == 29) {
+ if (la.kind == 30) {
Get();
- Expect(53);
- Expect(30);
+ Expect(54);
+ Expect(31);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
@@ -928,15 +883,15 @@ bool IsNotEndOfCase() {
Get();
NoUSIdent(out id);
eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
- if (la.kind == 29) {
+ if (la.kind == 30) {
Get();
- Expect(53);
- Expect(30);
+ Expect(54);
+ Expect(31);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
}
- Expect(58);
+ Expect(59);
}
void Type(out Type ty) {
@@ -949,11 +904,11 @@ bool IsNotEndOfCase() {
Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
- while (!(la.kind == 0 || la.kind == 50)) {SynErr(148); Get();}
- Expect(50);
+ while (!(la.kind == 0 || la.kind == 51)) {SynErr(147); Get();}
+ Expect(51);
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
- while (la.kind == 25) {
+ while (la.kind == 26) {
Attribute(ref attrs);
}
FIdentType(out id, out ty);
@@ -987,46 +942,46 @@ bool IsNotEndOfCase() {
if (la.kind == 78) {
Get();
- if (la.kind == 59) {
+ if (la.kind == 60) {
Get();
isFunctionMethod = true;
}
if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
- while (la.kind == 25) {
+ while (la.kind == 26) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 29 || la.kind == 57) {
- if (la.kind == 57) {
+ if (la.kind == 30 || la.kind == 58) {
+ if (la.kind == 58) {
GenericParameters(typeArgs);
}
Formals(true, isFunctionMethod, formals);
Expect(8);
Type(out returnType);
- } else if (la.kind == 33) {
+ } else if (la.kind == 34) {
Get();
signatureEllipsis = t;
- } else SynErr(149);
+ } else SynErr(148);
} else if (la.kind == 79) {
Get();
isPredicate = true;
- if (la.kind == 59) {
+ if (la.kind == 60) {
Get();
isFunctionMethod = true;
}
if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); }
- while (la.kind == 25) {
+ while (la.kind == 26) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (StartOf(8)) {
- if (la.kind == 57) {
+ if (la.kind == 58) {
GenericParameters(typeArgs);
}
missingOpenParen = true;
- if (la.kind == 29) {
+ if (la.kind == 30) {
Formals(true, isFunctionMethod, formals);
missingOpenParen = false;
}
@@ -1035,25 +990,25 @@ bool IsNotEndOfCase() {
Get();
SemErr(t, "predicates do not have an explicitly declared return type; it is always bool");
}
- } else if (la.kind == 33) {
+ } else if (la.kind == 34) {
Get();
signatureEllipsis = t;
- } else SynErr(150);
+ } else SynErr(149);
} else if (la.kind == 80) {
Get();
isCoPredicate = true;
if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
- while (la.kind == 25) {
+ while (la.kind == 26) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (StartOf(8)) {
- if (la.kind == 57) {
+ if (la.kind == 58) {
GenericParameters(typeArgs);
}
missingOpenParen = true;
- if (la.kind == 29) {
+ if (la.kind == 30) {
Formals(true, isFunctionMethod, formals);
missingOpenParen = false;
}
@@ -1062,16 +1017,16 @@ bool IsNotEndOfCase() {
Get();
SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool");
}
- } else if (la.kind == 33) {
+ } else if (la.kind == 34) {
Get();
signatureEllipsis = t;
- } else SynErr(151);
- } else SynErr(152);
+ } else SynErr(150);
+ } else SynErr(151);
decreases = isCoPredicate ? null : new List<Expression/*!*/>();
while (StartOf(9)) {
FunctionSpec(reqs, reads, ens, decreases);
}
- if (la.kind == 25) {
+ if (la.kind == 26) {
FunctionBody(out body, out bodyStart, out bodyEnd);
}
if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported")) {
@@ -1094,7 +1049,7 @@ bool IsNotEndOfCase() {
theBuiltIns.CreateArrowTypeDecl(formals.Count);
if (isCoPredicate) {
// also create an arrow type for the corresponding prefix predicate
- theBuiltIns.CreateArrowTypeDecl(formals.Count);
+ theBuiltIns.CreateArrowTypeDecl(formals.Count + 1);
}
}
@@ -1121,21 +1076,21 @@ bool IsNotEndOfCase() {
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(StartOf(10))) {SynErr(153); Get();}
- if (la.kind == 59) {
+ while (!(StartOf(10))) {SynErr(152); Get();}
+ if (la.kind == 60) {
Get();
- } else if (la.kind == 60) {
+ } else if (la.kind == 61) {
Get();
isLemma = true;
- } else if (la.kind == 61) {
+ } else if (la.kind == 62) {
Get();
isCoLemma = true;
- } else if (la.kind == 62) {
+ } else if (la.kind == 63) {
Get();
isCoLemma = true;
errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'");
- } else if (la.kind == 63) {
+ } else if (la.kind == 64) {
Get();
if (allowConstructor) {
isConstructor = true;
@@ -1143,7 +1098,7 @@ bool IsNotEndOfCase() {
SemErr(t, "constructors are allowed only in classes");
}
- } else SynErr(154);
+ } else SynErr(153);
keywordToken = t;
if (isLemma) {
if (mmod.IsGhost) {
@@ -1162,7 +1117,7 @@ bool IsNotEndOfCase() {
}
}
- while (la.kind == 25) {
+ while (la.kind == 26) {
Attribute(ref attrs);
}
if (la.kind == 1) {
@@ -1176,24 +1131,24 @@ bool IsNotEndOfCase() {
}
}
- if (la.kind == 29 || la.kind == 57) {
- if (la.kind == 57) {
+ if (la.kind == 30 || la.kind == 58) {
+ if (la.kind == 58) {
GenericParameters(typeArgs);
}
Formals(true, !mmod.IsGhost, ins);
- if (la.kind == 56) {
+ if (la.kind == 57) {
Get();
if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); }
Formals(false, !mmod.IsGhost, outs);
}
- } else if (la.kind == 33) {
+ } else if (la.kind == 34) {
Get();
signatureEllipsis = t;
- } else SynErr(155);
+ } else SynErr(154);
while (StartOf(11)) {
MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
}
- if (la.kind == 25) {
+ if (la.kind == 26) {
BlockStmt(out body, out bodyStart, out bodyEnd);
}
if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) {
@@ -1225,11 +1180,11 @@ bool IsNotEndOfCase() {
IToken/*!*/ id;
List<Formal/*!*/> formals = new List<Formal/*!*/>();
- while (la.kind == 25) {
+ while (la.kind == 26) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 29) {
+ if (la.kind == 30) {
FormalsOptionalIds(formals);
}
ctors.Add(new DatatypeCtor(id, id.val, formals, attrs));
@@ -1237,7 +1192,7 @@ bool IsNotEndOfCase() {
void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
- Expect(29);
+ Expect(30);
if (StartOf(12)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
@@ -1247,7 +1202,7 @@ bool IsNotEndOfCase() {
formals.Add(new Formal(id, name, ty, true, isGhost));
}
}
- Expect(30);
+ Expect(31);
}
void FIdentType(out IToken/*!*/ id, out Type/*!*/ ty) {
@@ -1259,14 +1214,14 @@ bool IsNotEndOfCase() {
} else if (la.kind == 2) {
Get();
id = t;
- } else SynErr(156);
+ } else SynErr(155);
Expect(8);
Type(out ty);
}
void OldSemi() {
- if (la.kind == 13) {
- while (!(la.kind == 0 || la.kind == 13)) {SynErr(157); Get();}
+ if (la.kind == 14) {
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(156); Get();}
Get();
}
}
@@ -1275,7 +1230,7 @@ bool IsNotEndOfCase() {
Expression e0; IToken endTok;
EquivExpression(out e, allowSemi, allowLambda);
if (SemiFollowsCall(allowSemi, e)) {
- Expect(13);
+ Expect(14);
endTok = t;
Expression(out e0, allowSemi, allowLambda);
e = new StmtExpr(e.tok,
@@ -1289,7 +1244,7 @@ bool IsNotEndOfCase() {
Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
isGhost = false;
- if (la.kind == 46) {
+ if (la.kind == 47) {
Get();
if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); }
}
@@ -1341,7 +1296,7 @@ bool IsNotEndOfCase() {
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);
string name = null; id = Token.NoToken; ty = new BoolType()/*dummy*/; isGhost = false;
- if (la.kind == 46) {
+ if (la.kind == 47) {
Get();
isGhost = true;
}
@@ -1363,7 +1318,7 @@ bool IsNotEndOfCase() {
id = t; name = id.val;
Expect(8);
Type(out ty);
- } else SynErr(158);
+ } else SynErr(157);
if (name != null) {
identName = name;
} else {
@@ -1378,35 +1333,35 @@ bool IsNotEndOfCase() {
List<Type> gt = null;
switch (la.kind) {
- case 67: {
+ case 68: {
Get();
tok = t;
break;
}
- case 68: {
+ case 69: {
Get();
tok = t; ty = new CharType();
break;
}
- case 69: {
+ case 70: {
Get();
tok = t; ty = new NatType();
break;
}
- case 70: {
+ case 71: {
Get();
tok = t; ty = new IntType();
break;
}
- case 71: {
+ case 72: {
Get();
tok = t; ty = new RealType();
break;
}
- case 72: {
+ case 73: {
Get();
tok = t; gt = new List<Type/*!*/>();
- if (la.kind == 57) {
+ if (la.kind == 58) {
GenericInstantiation(gt);
}
if (gt.Count > 1) {
@@ -1416,10 +1371,10 @@ bool IsNotEndOfCase() {
break;
}
- case 73: {
+ case 74: {
Get();
tok = t; gt = new List<Type/*!*/>();
- if (la.kind == 57) {
+ if (la.kind == 58) {
GenericInstantiation(gt);
}
if (gt.Count > 1) {
@@ -1429,10 +1384,10 @@ bool IsNotEndOfCase() {
break;
}
- case 74: {
+ case 75: {
Get();
tok = t; gt = new List<Type/*!*/>();
- if (la.kind == 57) {
+ if (la.kind == 58) {
GenericInstantiation(gt);
}
if (gt.Count > 1) {
@@ -1442,15 +1397,15 @@ bool IsNotEndOfCase() {
break;
}
- case 75: {
+ case 76: {
Get();
tok = t; ty = new UserDefinedType(tok, tok.val, new List<Type>(), new List<IToken>());
break;
}
- case 21: {
+ case 22: {
Get();
tok = t; gt = new List<Type/*!*/>();
- if (la.kind == 57) {
+ if (la.kind == 58) {
GenericInstantiation(gt);
}
if (gt.Count == 0) {
@@ -1464,7 +1419,7 @@ bool IsNotEndOfCase() {
break;
}
- case 29: {
+ case 30: {
Get();
tok = t; gt = new List<Type>();
if (StartOf(3)) {
@@ -1476,7 +1431,7 @@ bool IsNotEndOfCase() {
gt.Add(ty);
}
}
- Expect(30);
+ Expect(31);
if (gt.Count == 1) {
// just return the type 'ty'
} else {
@@ -1488,13 +1443,13 @@ bool IsNotEndOfCase() {
break;
}
- case 1: case 5: case 76: {
+ case 1: case 5: case 77: {
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(159); break;
+ default: SynErr(158); break;
}
- if (la.kind == 15) {
+ if (la.kind == 16) {
Type t2;
Get();
tok = t;
@@ -1510,8 +1465,8 @@ bool IsNotEndOfCase() {
void Formals(bool incoming, bool allowGhostKeyword, List<Formal> formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken id; Type ty; bool isGhost;
- Expect(29);
- if (la.kind == 1 || la.kind == 46) {
+ Expect(30);
+ if (la.kind == 1 || la.kind == 47) {
GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
while (la.kind == 9) {
@@ -1520,7 +1475,7 @@ bool IsNotEndOfCase() {
formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
}
}
- Expect(30);
+ Expect(31);
}
void IteratorSpec(List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/*!*/ mod, List<Expression/*!*/> decreases,
@@ -1529,8 +1484,8 @@ List<MaybeFreeExpression/*!*/>/*!*/ yieldReq, List<MaybeFreeExpression/*!*/>/*!*
ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null;
- while (!(StartOf(13))) {SynErr(160); Get();}
- if (la.kind == 23) {
+ while (!(StartOf(13))) {SynErr(159); Get();}
+ if (la.kind == 24) {
Get();
while (IsAttribute()) {
Attribute(ref readsAttrs);
@@ -1543,7 +1498,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
reads.Add(fe);
}
OldSemi();
- } else if (la.kind == 22) {
+ } else if (la.kind == 23) {
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -1557,17 +1512,17 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
}
OldSemi();
} else if (StartOf(14)) {
- if (la.kind == 64) {
+ if (la.kind == 65) {
Get();
isFree = true;
errors.Warning(t, "the 'free' keyword is soon to be deprecated");
}
- if (la.kind == 66) {
+ if (la.kind == 67) {
Get();
isYield = true;
}
- if (la.kind == 24) {
+ if (la.kind == 25) {
Get();
Expression(out e, false, false);
OldSemi();
@@ -1577,7 +1532,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
req.Add(new MaybeFreeExpression(e, isFree));
}
- } else if (la.kind == 65) {
+ } else if (la.kind == 66) {
Get();
while (IsAttribute()) {
Attribute(ref ensAttrs);
@@ -1590,27 +1545,27 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
}
- } else SynErr(161);
- } else if (la.kind == 19) {
+ } else SynErr(160);
+ } else if (la.kind == 20) {
Get();
while (IsAttribute()) {
Attribute(ref decrAttrs);
}
DecreasesList(decreases, false, false);
OldSemi();
- } else SynErr(162);
+ } else SynErr(161);
}
void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
Contract.Ensures(Contract.ValueAtReturn(out block) != null);
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(25);
+ Expect(26);
bodyStart = t;
while (StartOf(15)) {
Stmt(body);
}
- Expect(26);
+ Expect(27);
bodyEnd = t;
block = new BlockStmt(bodyStart, bodyEnd, body);
}
@@ -1620,8 +1575,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null;
- while (!(StartOf(16))) {SynErr(163); Get();}
- if (la.kind == 22) {
+ while (!(StartOf(16))) {SynErr(162); Get();}
+ if (la.kind == 23) {
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -1634,19 +1589,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod.Add(fe);
}
OldSemi();
- } else if (la.kind == 24 || la.kind == 64 || la.kind == 65) {
- if (la.kind == 64) {
+ } else if (la.kind == 25 || la.kind == 65 || la.kind == 66) {
+ if (la.kind == 65) {
Get();
isFree = true;
errors.Warning(t, "the 'free' keyword is soon to be deprecated");
}
- if (la.kind == 24) {
+ if (la.kind == 25) {
Get();
Expression(out e, false, false);
OldSemi();
req.Add(new MaybeFreeExpression(e, isFree));
- } else if (la.kind == 65) {
+ } else if (la.kind == 66) {
Get();
while (IsAttribute()) {
Attribute(ref ensAttrs);
@@ -1654,15 +1609,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression(out e, false, false);
OldSemi();
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
- } else SynErr(164);
- } else if (la.kind == 19) {
+ } else SynErr(163);
+ } else if (la.kind == 20) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true, false);
OldSemi();
- } else SynErr(165);
+ } else SynErr(164);
}
void FrameExpression(out FrameExpression fe, bool allowSemi, bool allowLambda) {
@@ -1686,11 +1641,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Ident(out id);
fieldName = id.val;
fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName);
- } else SynErr(166);
+ } else SynErr(165);
}
- void DecreasesList(List<Expression/*!*/> decreases, bool allowWildcard, bool allowLambda) {
- Expression/*!*/ e;
+ void DecreasesList(List<Expression> decreases, bool allowWildcard, bool allowLambda) {
+ Expression e;
PossiblyWildExpression(out e, allowLambda);
if (!allowWildcard && e is WildcardExpr) {
SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods");
@@ -1712,7 +1667,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {
Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty;
- Expect(57);
+ Expect(58);
Type(out ty);
gt.Add(ty);
while (la.kind == 9) {
@@ -1720,7 +1675,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Type(out ty);
gt.Add(ty);
}
- Expect(58);
+ Expect(59);
}
void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {
@@ -1729,13 +1684,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Type> gt;
List<IToken> path;
- if (la.kind == 76) {
+ if (la.kind == 77) {
Get();
tok = t; ty = new ObjectType();
} else if (la.kind == 5) {
Get();
tok = t; gt = new List<Type>();
- if (la.kind == 57) {
+ if (la.kind == 58) {
GenericInstantiation(gt);
}
int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));
@@ -1745,16 +1700,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Ident(out tok);
gt = new List<Type>();
path = new List<IToken>();
- while (la.kind == 77) {
+ while (la.kind == _dot) {
path.Add(tok);
- Get();
+ Expect(13);
Ident(out tok);
}
- if (la.kind == 57) {
+ if (la.kind == 58) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt, path);
- } else SynErr(167);
+ } else SynErr(166);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {
@@ -1762,13 +1717,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Requires(cce.NonNullElements(reads));
Contract.Requires(decreases == null || cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
- while (!(StartOf(17))) {SynErr(168); Get();}
- if (la.kind == 24) {
+ while (!(StartOf(17))) {SynErr(167); Get();}
+ if (la.kind == 25) {
Get();
Expression(out e, false, false);
OldSemi();
reqs.Add(e);
- } else if (la.kind == 23) {
+ } else if (la.kind == 24) {
Get();
PossiblyWildFrameExpression(out fe, false);
reads.Add(fe);
@@ -1778,12 +1733,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
reads.Add(fe);
}
OldSemi();
- } else if (la.kind == 65) {
+ } else if (la.kind == 66) {
Get();
Expression(out e, false, false);
OldSemi();
ens.Add(e);
- } else if (la.kind == 19) {
+ } else if (la.kind == 20) {
Get();
if (decreases == null) {
SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");
@@ -1792,58 +1747,37 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
DecreasesList(decreases, false, false);
OldSemi();
- } else SynErr(169);
+ } else SynErr(168);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
- Expect(25);
+ Expect(26);
bodyStart = t;
Expression(out e, true, true);
- Expect(26);
+ Expect(27);
bodyEnd = t;
}
void PossiblyWildFrameExpression(out FrameExpression fe, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
- if (la.kind == 31) {
+ if (la.kind == 32) {
Get();
fe = new FrameExpression(t, new WildcardExpr(t), null);
} else if (StartOf(18)) {
FrameExpression(out fe, allowSemi, false);
- } else SynErr(170);
- }
-
- void LambdaSpec(out Expression req, List<FrameExpression> reads) {
- Contract.Requires(reads != null);
- Expression e; req = null; FrameExpression fe;
- while (la.kind == 23 || la.kind == 24) {
- if (la.kind == 24) {
- Get();
- Expression(out e, true, false);
- if (req == null) {
- req = e;
- } else {
- req = new BinaryExpr(req.tok, BinaryExpr.Opcode.And, req, e);
- }
-
- } else {
- Get();
- PossiblyWildFrameExpression(out fe, true);
- reads.Add(fe);
- }
- }
+ } else SynErr(169);
}
void PossiblyWildExpression(out Expression e, bool allowLambda) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
- if (la.kind == 31) {
+ if (la.kind == 32) {
Get();
e = new WildcardExpr(t);
} else if (StartOf(7)) {
Expression(out e, false, allowLambda);
- } else SynErr(171);
+ } else SynErr(170);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1860,9 +1794,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken bodyStart, bodyEnd;
int breakCount;
- while (!(StartOf(19))) {SynErr(172); Get();}
+ while (!(StartOf(19))) {SynErr(171); Get();}
switch (la.kind) {
- case 25: {
+ case 26: {
BlockStmt(out bs, out bodyStart, out bodyEnd);
s = bs;
break;
@@ -1871,7 +1805,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
AssertStmt(out s);
break;
}
- case 16: {
+ case 17: {
AssumeStmt(out s);
break;
}
@@ -1879,11 +1813,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
PrintStmt(out s);
break;
}
- case 1: case 2: case 3: case 4: case 6: case 7: case 10: case 29: case 70: case 71: case 125: case 126: case 127: case 128: case 129: case 130: {
+ case 1: case 2: case 3: case 4: case 6: case 7: case 10: case 30: case 71: case 72: case 125: case 126: case 127: case 128: case 129: case 130: {
UpdateStmt(out s);
break;
}
- case 46: case 50: {
+ case 47: case 51: {
VarDeclStatement(out s);
break;
}
@@ -1903,7 +1837,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ForallStmt(out s);
break;
}
- case 17: {
+ case 18: {
CalcStmt(out s);
break;
}
@@ -1926,26 +1860,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 1) {
NoUSIdent(out id);
label = id.val;
- } else if (la.kind == 13 || la.kind == 83) {
+ } else if (la.kind == 14 || la.kind == 83) {
while (la.kind == 83) {
Get();
breakCount++;
}
- } else SynErr(173);
- while (!(la.kind == 0 || la.kind == 13)) {SynErr(174); Get();}
- Expect(13);
+ } else SynErr(172);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(173); Get();}
+ Expect(14);
s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount);
break;
}
- case 66: case 86: {
+ case 67: case 86: {
ReturnStmt(out s);
break;
}
- case 33: {
+ case 34: {
SkeletonStmt(out s);
break;
}
- default: SynErr(175); break;
+ default: SynErr(174); break;
}
}
@@ -1961,11 +1895,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
if (StartOf(7)) {
Expression(out e, false, true);
- } else if (la.kind == 33) {
+ } else if (la.kind == 34) {
Get();
dotdotdot = t;
- } else SynErr(176);
- Expect(13);
+ } else SynErr(175);
+ Expect(14);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssertStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
} else {
@@ -1979,18 +1913,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression e = dummyExpr; Attributes attrs = null;
IToken dotdotdot = null;
- Expect(16);
+ Expect(17);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
}
if (StartOf(7)) {
Expression(out e, false, true);
- } else if (la.kind == 33) {
+ } else if (la.kind == 34) {
Get();
dotdotdot = t;
- } else SynErr(177);
- Expect(13);
+ } else SynErr(176);
+ Expect(14);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssumeStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
} else {
@@ -2013,7 +1947,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression(out e, false, true);
args.Add(e);
}
- Expect(13);
+ Expect(14);
s = new PrintStmt(x, t, args);
}
@@ -2029,11 +1963,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Lhs(out e);
x = e.tok;
- if (la.kind == 13 || la.kind == 25) {
- while (la.kind == 25) {
+ if (la.kind == 14 || la.kind == 26) {
+ while (la.kind == 26) {
Attribute(ref attrs);
}
- Expect(13);
+ Expect(14);
endTok = t; rhss.Add(new ExprRhs(e, attrs));
} else if (la.kind == 9 || la.kind == 85 || la.kind == 87) {
lhss.Add(e); lhs0 = e;
@@ -2056,17 +1990,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
x = t;
if (la.kind == _assume) {
- Expect(16);
+ Expect(17);
suchThatAssume = t;
}
Expression(out suchThat, false, true);
- } else SynErr(178);
- Expect(13);
+ } else SynErr(177);
+ Expect(14);
endTok = t;
} else if (la.kind == 8) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(179);
+ } else SynErr(178);
if (suchThat != null) {
s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume);
} else {
@@ -2090,20 +2024,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Attributes attrs = null;
IToken endTok;
- if (la.kind == 46) {
+ if (la.kind == 47) {
Get();
isGhost = true; x = t;
}
- Expect(50);
+ Expect(51);
if (!isGhost) { x = t; }
- while (la.kind == 25) {
+ while (la.kind == 26) {
Attribute(ref attrs);
}
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d); d.Attributes = attrs; attrs = null;
while (la.kind == 9) {
Get();
- while (la.kind == 25) {
+ while (la.kind == 26) {
Attribute(ref attrs);
}
LocalIdentTypeOptional(out d, isGhost);
@@ -2126,14 +2060,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
assignTok = t;
if (la.kind == _assume) {
- Expect(16);
+ Expect(17);
suchThatAssume = t;
}
Expression(out suchThat, false, true);
}
}
- while (!(la.kind == 0 || la.kind == 13)) {SynErr(180); Get();}
- Expect(13);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(179); Get();}
+ Expect(14);
endTok = t;
ConcreteUpdateStatement update;
if (suchThat != null) {
@@ -2185,10 +2119,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 89) {
IfStmt(out s);
els = s; endTok = s.EndTok;
- } else if (la.kind == 25) {
+ } else if (la.kind == 26) {
BlockStmt(out bs, out bodyStart, out bodyEnd);
els = bs; endTok = bs.EndTok;
- } else SynErr(181);
+ } else SynErr(180);
}
if (guardEllipsis != null) {
ifStmt = new SkeletonStatement(new IfStmt(x, endTok, guard, thn, els), guardEllipsis, null);
@@ -2196,18 +2130,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ifStmt = new IfStmt(x, endTok, guard, thn, els);
}
- } else SynErr(182);
+ } else SynErr(181);
}
- void WhileStmt(out Statement/*!*/ stmt) {
- Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
+ void WhileStmt(out Statement stmt) {
+ Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken x;
Expression guard = null; IToken guardEllipsis = null;
- List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
- List<Expression/*!*/> decreases = new List<Expression/*!*/>();
+
+ List<MaybeFreeExpression> invariants = new List<MaybeFreeExpression>();
+ List<Expression> decreases = new List<Expression>();
Attributes decAttrs = null;
Attributes modAttrs = null;
- List<FrameExpression/*!*/> mod = null;
- BlockStmt/*!*/ body = null; IToken bodyEllipsis = null;
+ List<FrameExpression> mod = null;
+
+ BlockStmt body = null; IToken bodyEllipsis = null;
IToken bodyStart = null, bodyEnd = null, endTok = Token.NoToken;
List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
@@ -2215,8 +2151,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(91);
x = t;
- if (IsLoopSpecOrAlternative()) {
- LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
+ if (IsLoopSpec() || IsAlternative()) {
+ while (StartOf(22)) {
+ LoopSpec(invariants, decreases, ref mod, ref decAttrs, ref modAttrs);
+ }
AlternativeBlock(out alternatives, out endTok);
stmt = new AlternativeLoopStmt(x, endTok, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives);
} else if (StartOf(20)) {
@@ -2227,15 +2165,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
guardEllipsis = t;
}
- LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
+ while (StartOf(22)) {
+ LoopSpec(invariants, decreases, ref mod, ref decAttrs, ref modAttrs);
+ }
if (la.kind == _lbrace) {
BlockStmt(out body, out bodyStart, out bodyEnd);
endTok = body.EndTok; isDirtyLoop = false;
} else if (la.kind == _ellipsis) {
- Expect(33);
+ Expect(34);
bodyEllipsis = t; endTok = t; isDirtyLoop = false;
- } else if (StartOf(22)) {
- } else SynErr(183);
+ } else if (StartOf(23)) {
+ } else SynErr(182);
if (guardEllipsis != null || bodyEllipsis != null) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -2253,7 +2193,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
}
- } else SynErr(184);
+ } else SynErr(183);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -2266,19 +2206,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t;
Expression(out e, true, true);
if (la.kind == _lbrace) {
- Expect(25);
+ Expect(26);
usesOptionalBrace = true;
- while (la.kind == 18) {
+ while (la.kind == 19) {
CaseStatement(out c);
cases.Add(c);
}
- Expect(26);
- } else if (StartOf(22)) {
+ Expect(27);
+ } else if (StartOf(23)) {
while (la.kind == _case) {
CaseStatement(out c);
cases.Add(c);
}
- } else SynErr(185);
+ } else SynErr(184);
s = new MatchStmt(x, t, e, cases, usesOptionalBrace);
}
@@ -2303,30 +2243,30 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t;
errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");
- } else SynErr(186);
+ } else SynErr(185);
if (la.kind == _openparen) {
- Expect(29);
+ Expect(30);
if (la.kind == 1) {
QuantifierDomain(out bvars, out attrs, out range);
}
- Expect(30);
- } else if (StartOf(23)) {
+ Expect(31);
+ } else if (StartOf(24)) {
if (la.kind == _ident) {
QuantifierDomain(out bvars, out attrs, out range);
}
- } else SynErr(187);
+ } else SynErr(186);
if (bvars == null) { bvars = new List<BoundVar>(); }
if (range == null) { range = new LiteralExpr(x, true); }
- while (la.kind == 64 || la.kind == 65) {
+ while (la.kind == 65 || la.kind == 66) {
isFree = false;
- if (la.kind == 64) {
+ if (la.kind == 65) {
Get();
isFree = true;
errors.Warning(t, "the 'free' keyword is soon to be deprecated");
}
- Expect(65);
+ Expect(66);
Expression(out e, false, true);
ens.Add(new MaybeFreeExpression(e, isFree));
OldSemi();
@@ -2346,23 +2286,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
- void CalcStmt(out Statement/*!*/ s) {
+ void CalcStmt(out Statement s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x;
- CalcStmt.CalcOp/*!*/ op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;
- var lines = new List<Expression/*!*/>();
- var hints = new List<BlockStmt/*!*/>();
+ CalcStmt.CalcOp op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;
+ var lines = new List<Expression>();
+ var hints = new List<BlockStmt>();
CalcStmt.CalcOp stepOp;
var stepOps = new List<CalcStmt.CalcOp>();
CalcStmt.CalcOp maybeOp;
- Expression/*!*/ e;
- BlockStmt/*!*/ h;
+ Expression e;
IToken opTok;
IToken danglingOperator = null;
- Expect(17);
+ Expect(18);
x = t;
- if (StartOf(24)) {
+ if (StartOf(25)) {
CalcOp(out opTok, out calcOp);
maybeOp = calcOp.ResultOp(calcOp); // guard against non-transitive calcOp (like !=)
if (maybeOp == null) {
@@ -2371,12 +2310,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
resOp = calcOp;
}
- Expect(25);
+ Expect(26);
while (StartOf(7)) {
Expression(out e, false, true);
lines.Add(e); stepOp = calcOp; danglingOperator = null;
- Expect(13);
- if (StartOf(24)) {
+ Expect(14);
+ if (StartOf(25)) {
CalcOp(out opTok, out op);
maybeOp = resOp.ResultOp(op);
if (maybeOp == null) {
@@ -2389,12 +2328,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
stepOps.Add(stepOp);
- Hint(out h);
+ var subhints = new List<Statement>();
+ IToken hintStart = la; IToken hintEnd = hintStart;
+ IToken t0, t1;
+ BlockStmt subBlock; Statement subCalc;
+
+ while (la.kind == _lbrace || la.kind == _calc) {
+ if (la.kind == 26) {
+ BlockStmt(out subBlock, out t0, out t1);
+ hintEnd = subBlock.EndTok; subhints.Add(subBlock);
+ } else if (la.kind == 18) {
+ CalcStmt(out subCalc);
+ hintEnd = subCalc.EndTok; subhints.Add(subCalc);
+ } else SynErr(187);
+ }
+ var h = new BlockStmt(hintStart, hintEnd, subhints); // if the hint is empty, hintStart is the first token of the next line, but it doesn't matter because the block statement is just used as a container
hints.Add(h);
if (h.Body.Count != 0) { danglingOperator = null; }
}
- Expect(26);
+ Expect(27);
if (danglingOperator != null) {
SemErr(danglingOperator, "a calculation cannot end with an operator");
}
@@ -2426,14 +2379,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
FrameExpression(out fe, false, true);
mod.Add(fe);
}
- } else if (la.kind == 33) {
+ } else if (la.kind == 34) {
Get();
ellipsisToken = t;
} else SynErr(188);
- if (la.kind == 25) {
+ if (la.kind == 26) {
BlockStmt(out body, out bodyStart, out endTok);
- } else if (la.kind == 13) {
- while (!(la.kind == 0 || la.kind == 13)) {SynErr(189); Get();}
+ } else if (la.kind == 14) {
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(189); Get();}
Get();
endTok = t;
} else SynErr(190);
@@ -2453,11 +2406,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 86) {
Get();
returnTok = t;
- } else if (la.kind == 66) {
+ } else if (la.kind == 67) {
Get();
returnTok = t; isYield = true;
} else SynErr(191);
- if (StartOf(25)) {
+ if (StartOf(26)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
while (la.kind == 9) {
@@ -2466,7 +2419,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
rhss.Add(r);
}
}
- Expect(13);
+ Expect(14);
if (isYield) {
s = new YieldStmt(returnTok, t, rhss);
} else {
@@ -2480,7 +2433,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Expression> exprs = null;
IToken tok, dotdotdot, whereTok;
Expression e;
- Expect(33);
+ Expect(34);
dotdotdot = t;
if (la.kind == 84) {
Get();
@@ -2506,7 +2459,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
}
- Expect(13);
+ Expect(14);
s = new SkeletonStatement(dotdotdot, t, names, exprs);
}
@@ -2523,25 +2476,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 27 || la.kind == 29 || la.kind == 77) {
- if (la.kind == 27) {
+ if (la.kind == 13 || la.kind == 28 || la.kind == 30) {
+ if (la.kind == 28) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(28);
+ Expect(29);
var tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
} else {
x = null; args = new List<Expression/*!*/>();
- if (la.kind == 77) {
+ if (la.kind == 13) {
Get();
Ident(out x);
}
- Expect(29);
+ Expect(30);
if (StartOf(7)) {
Expressions(args);
}
- Expect(30);
+ Expect(31);
}
}
if (ee != null) {
@@ -2552,14 +2505,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
r = new TypeRhs(newToken, ty);
}
- } else if (la.kind == 31) {
+ } else if (la.kind == 32) {
Get();
r = new HavocRhs(t);
} else if (StartOf(7)) {
Expression(out e, false, true);
r = new ExprRhs(e);
} else SynErr(192);
- while (la.kind == 25) {
+ while (la.kind == 26) {
Attribute(ref attrs);
}
r.Attributes = attrs;
@@ -2569,14 +2522,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = dummyExpr; // the assignment is to please the compiler, the dummy value to satisfy contracts in the event of a parse error
if (la.kind == 1) {
- DottedIdentifiersAndFunction(out e);
- while (la.kind == 27 || la.kind == 29 || la.kind == 77) {
+ NameSegment(out e);
+ while (la.kind == 13 || la.kind == 28 || la.kind == 30) {
Suffix(ref e);
}
- } else if (StartOf(26)) {
+ } else if (StartOf(27)) {
ConstAtomExpression(out e, false, false);
Suffix(ref e);
- while (la.kind == 27 || la.kind == 29 || la.kind == 77) {
+ while (la.kind == 13 || la.kind == 28 || la.kind == 30) {
Suffix(ref e);
}
} else SynErr(193);
@@ -2599,31 +2552,31 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression e;
List<Statement> body;
- Expect(25);
- while (la.kind == 18) {
+ Expect(26);
+ while (la.kind == 19) {
Get();
x = t;
Expression(out e, true, false);
- Expect(14);
+ Expect(15);
body = new List<Statement>();
while (StartOf(15)) {
Stmt(body);
}
alternatives.Add(new GuardedAlternative(x, e, body));
}
- Expect(26);
+ Expect(27);
endTok = t;
}
void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
- if (la.kind == 31) {
+ if (la.kind == 32) {
Get();
e = null;
} else if (IsParenStar()) {
- Expect(29);
- Expect(31);
Expect(30);
+ Expect(32);
+ Expect(31);
e = null;
} else if (StartOf(7)) {
Expression(out ee, true, true);
@@ -2631,62 +2584,47 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else SynErr(194);
}
- void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs) {
- FrameExpression/*!*/ fe;
- invariants = new List<MaybeFreeExpression/*!*/>();
- MaybeFreeExpression invariant = null;
- decreases = new List<Expression/*!*/>();
- mod = null;
+ void LoopSpec(List<MaybeFreeExpression> invariants, List<Expression> decreases, ref List<FrameExpression> mod, ref Attributes decAttrs, ref Attributes modAttrs) {
+ Expression e; FrameExpression fe;
+ bool isFree = false; Attributes attrs = null;
- while (StartOf(27)) {
- if (la.kind == 20 || la.kind == 64) {
- Invariant(out invariant);
- OldSemi();
- invariants.Add(invariant);
- } else if (la.kind == 19) {
- while (!(la.kind == 0 || la.kind == 19)) {SynErr(195); Get();}
+ if (la.kind == 21 || la.kind == 65) {
+ while (!(la.kind == 0 || la.kind == 21 || la.kind == 65)) {SynErr(195); Get();}
+ if (la.kind == 65) {
Get();
- while (IsAttribute()) {
- Attribute(ref decAttrs);
- }
- DecreasesList(decreases, true, true);
- OldSemi();
- } else {
- while (!(la.kind == 0 || la.kind == 22)) {SynErr(196); Get();}
- Get();
- while (IsAttribute()) {
- Attribute(ref modAttrs);
- }
- mod = mod ?? new List<FrameExpression>();
- if (StartOf(18)) {
- FrameExpression(out fe, false, true);
- mod.Add(fe);
- while (la.kind == 9) {
- Get();
- FrameExpression(out fe, false, true);
- mod.Add(fe);
- }
- }
- OldSemi();
+ isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated");
}
- }
- }
-
- void Invariant(out MaybeFreeExpression/*!*/ invariant) {
- bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null;
- while (!(la.kind == 0 || la.kind == 20 || la.kind == 64)) {SynErr(197); Get();}
- if (la.kind == 64) {
+ Expect(21);
+ while (IsAttribute()) {
+ Attribute(ref attrs);
+ }
+ Expression(out e, false, true);
+ invariants.Add(new MaybeFreeExpression(e, isFree, attrs));
+ OldSemi();
+ } else if (la.kind == 20) {
+ while (!(la.kind == 0 || la.kind == 20)) {SynErr(196); Get();}
Get();
- isFree = true;
- errors.Warning(t, "the 'free' keyword is soon to be deprecated");
-
- }
- Expect(20);
- while (IsAttribute()) {
- Attribute(ref attrs);
- }
- Expression(out e, false, true);
- invariant = new MaybeFreeExpression(e, isFree, attrs);
+ while (IsAttribute()) {
+ Attribute(ref decAttrs);
+ }
+ DecreasesList(decreases, true, true);
+ OldSemi();
+ } else if (la.kind == 23) {
+ while (!(la.kind == 0 || la.kind == 23)) {SynErr(197); Get();}
+ Get();
+ mod = mod ?? new List<FrameExpression>();
+ while (IsAttribute()) {
+ Attribute(ref modAttrs);
+ }
+ FrameExpression(out fe, false, true);
+ mod.Add(fe);
+ while (la.kind == 9) {
+ Get();
+ FrameExpression(out fe, false, true);
+ mod.Add(fe);
+ }
+ OldSemi();
+ } else SynErr(198);
}
void CaseStatement(out MatchCaseStmt/*!*/ c) {
@@ -2696,10 +2634,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
BoundVar/*!*/ bv;
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(18);
+ Expect(19);
x = t;
Ident(out id);
- if (la.kind == 29) {
+ if (la.kind == 30) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
@@ -2708,9 +2646,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IdentTypeOptional(out bv);
arguments.Add(bv);
}
- Expect(30);
+ Expect(31);
}
- Expect(14);
+ Expect(15);
while (IsNotEndOfCase()) {
Stmt(body);
}
@@ -2745,23 +2683,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = null;
switch (la.kind) {
- case 53: {
+ case 54: {
Get();
x = t; binOp = BinaryExpr.Opcode.Eq;
if (la.kind == 98) {
Get();
- Expect(27);
- Expression(out k, true, true);
Expect(28);
+ Expression(out k, true, true);
+ Expect(29);
}
break;
}
- case 57: {
+ case 58: {
Get();
x = t; binOp = BinaryExpr.Opcode.Lt;
break;
}
- case 58: {
+ case 59: {
Get();
x = t; binOp = BinaryExpr.Opcode.Gt;
break;
@@ -2811,7 +2749,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; binOp = BinaryExpr.Opcode.Exp;
break;
}
- default: SynErr(198); break;
+ default: SynErr(199); break;
}
if (k == null) {
op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
@@ -2821,28 +2759,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
- void Hint(out BlockStmt s) {
- Contract.Ensures(Contract.ValueAtReturn(out s) != null); // returns an empty block statement if the hint is empty
- var subhints = new List<Statement/*!*/>();
- IToken bodyStart, bodyEnd;
- BlockStmt/*!*/ block;
- Statement/*!*/ calc;
- Token x = la;
- IToken endTok = x;
-
- while (la.kind == _lbrace || la.kind == _calc) {
- if (la.kind == 25) {
- BlockStmt(out block, out bodyStart, out bodyEnd);
- endTok = block.EndTok; subhints.Add(block);
- } else if (la.kind == 17) {
- CalcStmt(out calc);
- endTok = calc.EndTok; subhints.Add(calc);
- } else SynErr(199);
- }
- s = new BlockStmt(x, endTok, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container
-
- }
-
void EquivOp() {
if (la.kind == 105) {
Get();
@@ -3109,23 +3025,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
k = null;
switch (la.kind) {
- case 53: {
+ case 54: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
if (la.kind == 98) {
Get();
- Expect(27);
- Expression(out k, true, true);
Expect(28);
+ Expression(out k, true, true);
+ Expect(29);
}
break;
}
- case 57: {
+ case 58: {
Get();
x = t; op = BinaryExpr.Opcode.Lt;
break;
}
- case 58: {
+ case 59: {
Get();
x = t; op = BinaryExpr.Opcode.Gt;
break;
@@ -3145,9 +3061,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.Neq;
if (la.kind == 98) {
Get();
- Expect(27);
- Expression(out k, true, true);
Expect(28);
+ Expression(out k, true, true);
+ Expect(29);
}
break;
}
@@ -3156,7 +3072,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 32: {
+ case 33: {
Get();
x = t; op = BinaryExpr.Opcode.NotIn;
break;
@@ -3232,10 +3148,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
UnaryExpression(out e, allowSemi, allowLambda);
e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Not, e);
} else if (IsMapDisplay()) {
- Expect(21);
+ Expect(22);
x = t;
MapDisplayExpr(x, out e);
- while (la.kind == 27 || la.kind == 29 || la.kind == 77) {
+ while (IsSuffix()) {
Suffix(ref e);
}
} else if (IsLambda(allowLambda)) {
@@ -3243,23 +3159,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(28)) {
EndlessExpression(out e, allowSemi, allowLambda);
} else if (la.kind == 1) {
- DottedIdentifiersAndFunction(out e);
- while (la.kind == 27 || la.kind == 29 || la.kind == 77) {
+ NameSegment(out e);
+ while (IsSuffix()) {
Suffix(ref e);
}
- } else if (la.kind == 25 || la.kind == 27) {
+ } else if (la.kind == 26 || la.kind == 28) {
DisplayExpr(out e);
- while (la.kind == 27 || la.kind == 29 || la.kind == 77) {
+ while (IsSuffix()) {
Suffix(ref e);
}
- } else if (la.kind == 73) {
+ } else if (la.kind == 74) {
MultiSetExpr(out e);
- while (la.kind == 27 || la.kind == 29 || la.kind == 77) {
+ while (IsSuffix()) {
Suffix(ref e);
}
- } else if (StartOf(26)) {
+ } else if (StartOf(27)) {
ConstAtomExpression(out e, allowSemi, allowLambda);
- while (la.kind == 27 || la.kind == 29 || la.kind == 77) {
+ while (IsSuffix()) {
Suffix(ref e);
}
} else SynErr(213);
@@ -3267,7 +3183,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void MulOp(out IToken x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 31) {
+ if (la.kind == 32) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
} else if (la.kind == 123) {
@@ -3284,50 +3200,39 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;
e = dummyExpr;
- Expect(27);
+ Expect(28);
if (StartOf(7)) {
MapLiteralExpressions(out elements);
}
e = new MapDisplayExpr(mapToken, elements);
- Expect(28);
+ Expect(29);
}
void Suffix(ref Expression e) {
Contract.Requires(e != null); Contract.Ensures(e!=null);
- IToken id, x; List<Expression> args;
+ IToken id, x;
Expression e0 = null; Expression e1 = null; Expression ee; bool anyDots = false;
List<Expression> multipleLengths = null; bool takeRest = false; // takeRest is relevant only if multipleLengths is non-null
List<Expression> multipleIndices = null;
- bool func = false;
- if (la.kind == 77) {
- IdentOrDigitsSuffix(out id, out x);
+ if (la.kind == 13) {
+ DotSuffix(out id, out x);
if (x != null) {
// process id as a Suffix in its own right
e = new ExprDotName(id, e, id.val);
id = x; // move to the next Suffix
}
+ IToken openParen = null; List<Expression> args = null;
- if (la.kind == 29 || la.kind == 98) {
- args = new List<Expression/*!*/>(); func = true;
- if (la.kind == 98) {
- Get();
- id.val = id.val + "#"; Expression k;
- Expect(27);
- Expression(out k, true, true);
- Expect(28);
- args.Add(k);
- }
- Expect(29);
- IToken openParen = t;
- if (StartOf(7)) {
- Expressions(args);
- }
- Expect(30);
- e = new FunctionCallExpr(id, id.val, e, openParen, args);
+ if (la.kind == 98) {
+ HashCall(id, out openParen, out args);
}
- if (!func) { e = new ExprDotName(id, e, id.val); }
- } else if (la.kind == 27) {
+ e = new ExprDotName(id, e, id.val);
+ if (openParen != null) {
+ e = new ApplySuffix(openParen, e, args);
+ }
+
+ } else if (la.kind == 28) {
Get();
x = t;
if (StartOf(7)) {
@@ -3363,7 +3268,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
takeRest = true;
}
}
- } else if (la.kind == 9 || la.kind == 28) {
+ } else if (la.kind == 9 || la.kind == 29) {
while (la.kind == 9) {
Get();
Expression(out ee, true, true);
@@ -3417,15 +3322,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
}
- Expect(28);
- } else if (la.kind == 29) {
+ Expect(29);
+ } else if (la.kind == 30) {
Get();
- IToken openParen = t; args = new List<Expression>();
+ IToken openParen = t; var args = new List<Expression>();
if (StartOf(7)) {
Expressions(args);
}
- Expect(30);
- e = new ApplyExpr(e.tok, openParen, e, args);
+ Expect(31);
+ e = new ApplySuffix(openParen, e, args);
} else SynErr(217);
}
@@ -3433,15 +3338,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken x = Token.NoToken;
IToken id; BoundVar bv;
var bvs = new List<BoundVar>();
- Expression body = null;
+ FrameExpression fe; Expression ee;
+ var reads = new List<FrameExpression>();
Expression req = null;
bool oneShot;
- var reads = new List<FrameExpression>();
+ Expression body = null;
if (la.kind == 1) {
WildIdent(out id, true);
x = t; bvs.Add(new BoundVar(id, id.val, new InferredTypeProxy()));
- } else if (la.kind == 29) {
+ } else if (la.kind == 30) {
Get();
x = t;
if (la.kind == 1) {
@@ -3453,9 +3359,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
bvs.Add(bv);
}
}
- Expect(30);
+ Expect(31);
} else SynErr(218);
- LambdaSpec(out req, reads);
+ while (la.kind == 24 || la.kind == 25) {
+ if (la.kind == 24) {
+ Get();
+ PossiblyWildFrameExpression(out fe, true);
+ reads.Add(fe);
+ } else {
+ Get();
+ Expression(out ee, true, false);
+ req = req == null ? ee : new BinaryExpr(req.tok, BinaryExpr.Opcode.And, req, ee);
+ }
+ }
LambdaArrow(out oneShot);
Expression(out body, allowSemi, true);
e = new LambdaExpr(x, oneShot, bvs, req, reads, body);
@@ -3489,21 +3405,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
QuantifierGuts(out e, allowSemi, allowLambda);
break;
}
- case 72: {
+ case 73: {
SetComprehensionExpr(out e, allowSemi, allowLambda);
break;
}
- case 16: case 17: case 93: {
+ case 17: case 18: case 93: {
StmtInExpr(out s);
Expression(out e, allowSemi, allowLambda);
e = new StmtExpr(s.Tok, s, e);
break;
}
- case 46: case 50: {
+ case 47: case 51: {
LetExpr(out e, allowSemi, allowLambda);
break;
}
- case 21: {
+ case 22: {
Get();
x = t;
MapComprehensionExpr(x, out e, allowSemi, allowLambda);
@@ -3517,66 +3433,42 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
}
- void DottedIdentifiersAndFunction(out Expression e) {
- IToken id, idPrime; IToken openParen = null;
- List<Expression> args = null;
- List<IToken> idents = new List<IToken>();
- e = null;
- var applyArgLists = new List<List<Expression>>();
+ void NameSegment(out Expression e) {
+ IToken id;
+ IToken openParen = null; List<Expression> args = null;
Ident(out id);
- idents.Add(id);
- while (la.kind == 77) {
- IdentOrDigitsSuffix(out id, out idPrime);
- idents.Add(id);
- if (idPrime != null) { idents.Add(idPrime); id = idPrime; }
-
+ if (la.kind == 98) {
+ HashCall(id, out openParen, out args);
}
- if (la.kind == 29 || la.kind == 98) {
- args = new List<Expression>();
- if (la.kind == 98) {
- Get();
- id.val = id.val + "#"; Expression k;
- Expect(27);
- Expression(out k, true, true);
- Expect(28);
- args.Add(k);
- }
- Expect(29);
- openParen = t;
- if (StartOf(7)) {
- Expressions(args);
- }
- Expect(30);
- }
- e = new IdentifierSequence(idents, openParen, args);
- foreach (var args_ in applyArgLists) {
- e = new ApplyExpr(id, openParen, e, args_);
+ e = new NameSegment(id, id.val, null);
+ if (openParen != null) {
+ e = new ApplySuffix(openParen, e, args);
}
}
void DisplayExpr(out Expression e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
+ IToken x; List<Expression> elements;
e = dummyExpr;
- if (la.kind == 25) {
+ if (la.kind == 26) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(7)) {
Expressions(elements);
}
e = new SetDisplayExpr(x, elements);
- Expect(26);
- } else if (la.kind == 27) {
+ Expect(27);
+ } else if (la.kind == 28) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(7)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(28);
+ Expect(29);
} else SynErr(220);
}
@@ -3585,22 +3477,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
- Expect(73);
+ Expect(74);
x = t;
- if (la.kind == 25) {
+ if (la.kind == 26) {
Get();
elements = new List<Expression/*!*/>();
if (StartOf(7)) {
Expressions(elements);
}
e = new MultiSetDisplayExpr(x, elements);
- Expect(26);
- } else if (la.kind == 29) {
+ Expect(27);
+ } else if (la.kind == 30) {
Get();
x = t; elements = new List<Expression/*!*/>();
Expression(out e, true, true);
e = new MultiSetFormingExpr(x, e);
- Expect(30);
+ Expect(31);
} else SynErr(221);
}
@@ -3656,18 +3548,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
case 129: {
Get();
x = t;
- Expect(29);
- Expression(out e, true, true);
Expect(30);
+ Expression(out e, true, true);
+ Expect(31);
e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Fresh, e);
break;
}
case 130: {
Get();
x = t;
- Expect(29);
- Expression(out e, true, true);
Expect(30);
+ Expression(out e, true, true);
+ Expect(31);
e = new OldExpr(x, e);
break;
}
@@ -3679,21 +3571,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(10);
break;
}
- case 70: case 71: {
- if (la.kind == 70) {
+ case 71: case 72: {
+ if (la.kind == 71) {
Get();
x = t; toType = new IntType();
} else {
Get();
x = t; toType = new RealType();
}
- Expect(29);
- Expression(out e, true, true);
Expect(30);
+ Expression(out e, true, true);
+ Expect(31);
e = new ConversionExpr(x, e, toType);
break;
}
- case 29: {
+ case 30: {
ParensExpression(out e, allowSemi, allowLambda);
break;
}
@@ -3743,15 +3635,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void ParensExpression(out Expression e, bool allowSemi, bool allowLambda) {
- IToken x; IToken openParen;
- List<Expression> args = new List<Expression>();
+ IToken x;
+ var args = new List<Expression>();
- Expect(29);
+ Expect(30);
x = t;
if (StartOf(7)) {
Expressions(args);
}
- Expect(30);
+ Expect(31);
if (args.Count == 1) {
e = new ParensExpression(x, args[0]);
} else {
@@ -3760,23 +3652,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args);
}
- while (la.kind == 29) {
- Get();
- openParen = t; args = new List<Expression>();
- if (StartOf(7)) {
- Expressions(args);
- }
- Expect(30);
- e = new ApplyExpr(x, openParen, e, args);
- }
}
void LambdaArrow(out bool oneShot) {
oneShot = true;
- if (la.kind == 14) {
+ if (la.kind == 15) {
Get();
oneShot = false;
- } else if (la.kind == 15) {
+ } else if (la.kind == 16) {
Get();
oneShot = true;
} else SynErr(224);
@@ -3826,13 +3709,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t;
Expression(out e, allowSemi, allowLambda);
if (la.kind == _lbrace) {
- Expect(25);
+ Expect(26);
usesOptionalBrace = true;
- while (la.kind == 18) {
+ while (la.kind == 19) {
CaseExpression(out c, true, true);
cases.Add(c);
}
- Expect(26);
+ Expect(27);
} else if (StartOf(29)) {
while (la.kind == _case) {
CaseExpression(out c, allowSemi, allowLambda);
@@ -3876,7 +3759,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression range;
Expression body = null;
- Expect(72);
+ Expect(73);
x = t;
IdentTypeOptional(out bv);
bvars.Add(bv);
@@ -3900,9 +3783,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
s = dummyStmt;
if (la.kind == 93) {
AssertStmt(out s);
- } else if (la.kind == 16) {
- AssumeStmt(out s);
} else if (la.kind == 17) {
+ AssumeStmt(out s);
+ } else if (la.kind == 18) {
CalcStmt(out s);
} else SynErr(227);
}
@@ -3916,11 +3799,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
bool exact = true;
e = dummyExpr;
- if (la.kind == 46) {
+ if (la.kind == 47) {
Get();
isGhost = true; x = t;
}
- Expect(50);
+ Expect(51);
if (!isGhost) { x = t; }
CasePattern(out pat);
if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); }
@@ -3952,7 +3835,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression(out e, false, true);
letRHSs.Add(e);
}
- Expect(13);
+ Expect(14);
Expression(out e, allowSemi, allowLambda);
e = new LetExpr(x, letLHSs, letRHSs, e, exact);
}
@@ -3978,7 +3861,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (IsIdentParen()) {
Ident(out id);
- Expect(29);
+ Expect(30);
arguments = new List<CasePattern>();
if (la.kind == 1) {
CasePattern(out pat);
@@ -3989,7 +3872,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
arguments.Add(pat);
}
}
- Expect(30);
+ Expect(31);
pat = new CasePattern(id, id.val, arguments);
} else if (la.kind == 1) {
IdentTypeOptional(out bv);
@@ -4008,10 +3891,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
BoundVar/*!*/ bv;
Expression/*!*/ body;
- Expect(18);
+ Expect(19);
x = t;
Ident(out id);
- if (la.kind == 29) {
+ if (la.kind == 30) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
@@ -4020,13 +3903,71 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IdentTypeOptional(out bv);
arguments.Add(bv);
}
- Expect(30);
+ Expect(31);
}
- Expect(14);
+ Expect(15);
Expression(out body, allowSemi, allowLambda);
c = new MatchCaseExpr(x, id.val, arguments, body);
}
+ void HashCall(IToken id, out IToken openParen, out List<Expression> args) {
+ Expression k; args = new List<Expression>();
+ Expect(98);
+ id.val = id.val + "#";
+ Expect(28);
+ Expression(out k, true, true);
+ Expect(29);
+ args.Add(k);
+ Expect(30);
+ openParen = t;
+ if (StartOf(7)) {
+ Expressions(args);
+ }
+ Expect(31);
+ }
+
+ void DotSuffix(out IToken x, out IToken y) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null);
+ x = Token.NoToken;
+ y = null;
+
+ Expect(13);
+ if (la.kind == 1) {
+ Get();
+ x = t;
+ } else if (la.kind == 2) {
+ Get();
+ x = t;
+ } else if (la.kind == 4) {
+ Get();
+ x = t;
+ int exponent = x.val.IndexOf('e');
+ if (0 <= exponent) {
+ // this is not a legal field/destructor name
+ SemErr(x, "invalid DotSuffix");
+ } else {
+ int dot = x.val.IndexOf('.');
+ if (0 <= dot) {
+ y = new Token();
+ y.pos = x.pos + dot + 1;
+ y.val = x.val.Substring(dot + 1);
+ x.val = x.val.Substring(0, dot);
+ y.col = x.col + dot + 1;
+ y.line = x.line;
+ y.filename = x.filename;
+ y.kind = x.kind;
+ }
+ }
+
+ } else if (la.kind == 25) {
+ Get();
+ x = t;
+ } else if (la.kind == 24) {
+ Get();
+ x = t;
+ } else SynErr(230);
+ }
+
public void Parse() {
@@ -4040,36 +3981,36 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
static readonly bool[,]/*!*/ set = {
- {T,T,T,T, T,x,T,T, x,x,T,x, x,T,x,x, T,T,x,T, T,x,T,T, T,T,x,x, x,T,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,T,T,x, T,T,T,x, x,x,T,x, x,x,x,T, T,T,T,T, T,T,T,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,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,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,T, T,x,T,x, x,x,x,T, x,T,T,T, T,T,T,T, T,x,T,x, x,x,x,T, T,T,T,T, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,T, T,T,T,T, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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},
- {T,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, T,x,T,x, T,x,x,T, x,T,T,T, T,T,T,T, T,x,T,x, x,T,x,T, T,T,T,T, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, T,T,x,x, x,T,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, T,T,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,T,x, x,T,T,T, T,T,T,x, x,x,x},
- {T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,T,T,x, x,T,x,x, x,x,x,T, T,x,T,x, x,x,x,T, x,T,T,T, T,T,T,T, T,x,T,x, x,T,x,T, T,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,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,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,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, 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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,T,x,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, 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},
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {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, 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,T, T,x,T,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,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,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,T, x,x,T,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, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T, T,x,T,T, x,x,T,x, x,x,x,x, T,T,x,x, x,T,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,T,x,x, T,T,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,T,x, x,T,T,T, T,T,T,x, x,x,x},
- {T,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,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,T,T,T, T,T,T,x, x,x,x},
- {x,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, T,T,x,x, x,T,x,x, x,T,x,T, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,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,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, T,T,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,T,x, x,T,T,T, T,T,T,x, x,x,x},
- {x,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, T,T,x,x, x,T,x,x, x,T,x,T, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, T,T,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,T,x, x,T,T,T, T,T,T,x, x,x,x},
- {x,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,T,T,x, x,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,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,T,T,T, T,T,T,x, x,x,x},
- {x,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,T,T,x, x,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,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,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,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, T,T,x,x, x,T,x,x, x,T,x,T, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,x,x, x,x,x,x, x,x,T,x, x,x,x,x, T,T,x,x, T,T,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,T,x, x,T,T,T, T,T,T,x, x,x,x},
- {x,x,T,T, T,x,T,T, x,x,T,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,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,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,T, T,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, 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, T,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,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,T,x, x,x,x,x, x,T,x,x, T,T,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,x,x,x, x,x,x},
- {T,T,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,T,T, T,T,T,x, T,T,T,T, T,T,x,T, T,x,T,x, x,x,x,T, x,T,T,T, T,T,T,T, T,T,T,x, x,T,T,T, T,T,T,T, T,T,T,x, x,x,T,T, x,x,x,x, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,T, T,T,T,T, T,T,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x}
+ {T,T,T,T, T,x,T,T, x,x,T,x, x,x,T,x, x,T,T,x, T,T,x,T, T,T,T,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,T,T, x,T,T,T, x,x,x,T, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,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,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, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,T, T,T,x,T, x,x,x,x, T,T,T,T, T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, T,T,T,T, T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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},
+ {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,x,T, x,x,x,x, x,x,x,x, T,T,x,T, x,T,x,x, T,x,T,T, T,T,T,T, T,T,x,T, x,x,T,x, T,T,T,T, T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, x,T,T,x, x,x,T,x, x,x,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, T,T,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,T,x, x,T,T,T, T,T,T,x, x,x,x},
+ {T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,T,x, x,x,x,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,T, T,T,x,T, x,x,T,x, T,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, 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,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},
+ {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, 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, T,x,x,T, 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,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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,x, 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,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},
+ {T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,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,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,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,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,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, T,x,x,T, 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,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},
+ {T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,x},
+ {x,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, x,T,T,x, x,x,T,x, x,x,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,x, x,x,x,x, x,T,T,x, x,x,x,x, x,T,x,x, T,T,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,T,x, x,T,T,T, T,T,T,x, x,x,x},
+ {T,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,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,T,T,T, T,T,T,x, x,x,x},
+ {x,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, x,T,T,x, x,x,T,x, x,x,T,x, T,x,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, T,T,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,T,x, x,T,T,T, T,T,T,x, x,x,x},
+ {x,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, x,T,T,x, x,x,T,x, x,x,T,x, T,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, T,T,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,T,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, T,T,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,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,T, T,x,T,T, x,x,T,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,T, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,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,T,T,T, T,T,T,x, x,x,x},
+ {x,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,T, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,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,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,T,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,T, T,x,T,T, x,x,T,x, x,x,x,x, x,T,T,x, x,x,T,x, x,x,T,x, T,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,x, x,x,x,x, x,x,T,x, x,x,x,x, T,T,x,x, T,T,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,T,x, x,T,T,T, T,T,T,x, x,x,x},
+ {x,x,T,T, T,x,T,T, 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,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,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, 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,T,x, x,x,x,x, x,T,x,x, T,T,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,x,x,x, x,x,x},
+ {T,T,T,T, T,x,T,T, T,T,T,T, T,x,T,T, T,T,T,T, T,T,x,T, T,T,T,T, x,T,T,T, T,T,T,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,T,T, T,T,T,T, x,x,x,T, T,x,x,x, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,T, T,T,T,T, T,T,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x}
};
} // end Parser
@@ -4107,71 +4048,71 @@ public class Errors {
case 10: s = "verticalbar expected"; break;
case 11: s = "doublecolon expected"; break;
case 12: s = "bullet expected"; break;
- case 13: s = "semi expected"; break;
- case 14: s = "darrow expected"; break;
- case 15: s = "arrow expected"; break;
- case 16: s = "assume expected"; break;
- case 17: s = "calc expected"; break;
- case 18: s = "case expected"; break;
- case 19: s = "decreases expected"; break;
- case 20: s = "invariant expected"; break;
- case 21: s = "map expected"; break;
- case 22: s = "modifies expected"; break;
- case 23: s = "reads expected"; break;
- case 24: s = "requires expected"; break;
- case 25: s = "lbrace expected"; break;
- case 26: s = "rbrace expected"; break;
- case 27: s = "lbracket expected"; break;
- case 28: s = "rbracket expected"; break;
- case 29: s = "openparen expected"; break;
- case 30: s = "closeparen expected"; break;
- case 31: s = "star expected"; break;
- case 32: s = "notIn expected"; break;
- case 33: s = "ellipsis expected"; break;
- case 34: s = "\"include\" expected"; break;
- case 35: s = "\"abstract\" expected"; break;
- case 36: s = "\"module\" expected"; break;
- case 37: s = "\"refines\" expected"; break;
- case 38: s = "\"import\" expected"; break;
- case 39: s = "\"opened\" expected"; break;
- case 40: s = "\"=\" expected"; break;
- case 41: s = "\"as\" expected"; break;
- case 42: s = "\"default\" expected"; break;
- case 43: s = "\"class\" expected"; break;
- case 44: s = "\"extends\" expected"; break;
- case 45: s = "\"trait\" expected"; break;
- case 46: s = "\"ghost\" expected"; break;
- case 47: s = "\"static\" expected"; break;
- case 48: s = "\"datatype\" expected"; break;
- case 49: s = "\"codatatype\" expected"; break;
- case 50: s = "\"var\" expected"; break;
- case 51: s = "\"newtype\" expected"; break;
- case 52: s = "\"type\" expected"; break;
- case 53: s = "\"==\" expected"; break;
- case 54: s = "\"iterator\" expected"; break;
- case 55: s = "\"yields\" expected"; break;
- case 56: s = "\"returns\" expected"; break;
- case 57: s = "\"<\" expected"; break;
- case 58: s = "\">\" expected"; break;
- case 59: s = "\"method\" expected"; break;
- case 60: s = "\"lemma\" expected"; break;
- case 61: s = "\"colemma\" expected"; break;
- case 62: s = "\"comethod\" expected"; break;
- case 63: s = "\"constructor\" expected"; break;
- case 64: s = "\"free\" expected"; break;
- case 65: s = "\"ensures\" expected"; break;
- case 66: s = "\"yield\" expected"; break;
- case 67: s = "\"bool\" expected"; break;
- case 68: s = "\"char\" expected"; break;
- case 69: s = "\"nat\" expected"; break;
- case 70: s = "\"int\" expected"; break;
- case 71: s = "\"real\" expected"; break;
- case 72: s = "\"set\" expected"; break;
- case 73: s = "\"multiset\" expected"; break;
- case 74: s = "\"seq\" expected"; break;
- case 75: s = "\"string\" expected"; break;
- case 76: s = "\"object\" expected"; break;
- case 77: s = "\".\" expected"; break;
+ case 13: s = "dot expected"; break;
+ case 14: s = "semi expected"; break;
+ case 15: s = "darrow expected"; break;
+ case 16: s = "arrow expected"; break;
+ case 17: s = "assume expected"; break;
+ case 18: s = "calc expected"; break;
+ case 19: s = "case expected"; break;
+ case 20: s = "decreases expected"; break;
+ case 21: s = "invariant expected"; break;
+ case 22: s = "map expected"; break;
+ case 23: s = "modifies expected"; break;
+ case 24: s = "reads expected"; break;
+ case 25: s = "requires expected"; break;
+ case 26: s = "lbrace expected"; break;
+ case 27: s = "rbrace expected"; break;
+ case 28: s = "lbracket expected"; break;
+ case 29: s = "rbracket expected"; break;
+ case 30: s = "openparen expected"; break;
+ case 31: s = "closeparen expected"; break;
+ case 32: s = "star expected"; break;
+ case 33: s = "notIn expected"; break;
+ case 34: s = "ellipsis expected"; break;
+ case 35: s = "\"include\" expected"; break;
+ case 36: s = "\"abstract\" expected"; break;
+ case 37: s = "\"module\" expected"; break;
+ case 38: s = "\"refines\" expected"; break;
+ case 39: s = "\"import\" expected"; break;
+ case 40: s = "\"opened\" expected"; break;
+ case 41: s = "\"=\" expected"; break;
+ case 42: s = "\"as\" expected"; break;
+ case 43: s = "\"default\" expected"; break;
+ case 44: s = "\"class\" expected"; break;
+ case 45: s = "\"extends\" expected"; break;
+ case 46: s = "\"trait\" expected"; break;
+ case 47: s = "\"ghost\" expected"; break;
+ case 48: s = "\"static\" expected"; break;
+ case 49: s = "\"datatype\" expected"; break;
+ case 50: s = "\"codatatype\" expected"; break;
+ case 51: s = "\"var\" expected"; break;
+ case 52: s = "\"newtype\" expected"; break;
+ case 53: s = "\"type\" expected"; break;
+ case 54: s = "\"==\" expected"; break;
+ case 55: s = "\"iterator\" expected"; break;
+ case 56: s = "\"yields\" expected"; break;
+ case 57: s = "\"returns\" expected"; break;
+ case 58: s = "\"<\" expected"; break;
+ case 59: s = "\">\" expected"; break;
+ case 60: s = "\"method\" expected"; break;
+ case 61: s = "\"lemma\" expected"; break;
+ case 62: s = "\"colemma\" expected"; break;
+ case 63: s = "\"comethod\" expected"; break;
+ case 64: s = "\"constructor\" expected"; break;
+ case 65: s = "\"free\" expected"; break;
+ case 66: s = "\"ensures\" expected"; break;
+ case 67: s = "\"yield\" expected"; break;
+ case 68: s = "\"bool\" expected"; break;
+ case 69: s = "\"char\" expected"; break;
+ case 70: s = "\"nat\" expected"; break;
+ case 71: s = "\"int\" expected"; break;
+ case 72: s = "\"real\" expected"; break;
+ case 73: s = "\"set\" expected"; break;
+ case 74: s = "\"multiset\" expected"; break;
+ case 75: s = "\"seq\" expected"; break;
+ case 76: s = "\"string\" expected"; break;
+ case 77: s = "\"object\" expected"; break;
case 78: s = "\"function\" expected"; break;
case 79: s = "\"predicate\" expected"; break;
case 80: s = "\"copredicate\" expected"; break;
@@ -4241,47 +4182,47 @@ public class Errors {
case 144: s = "invalid IteratorDecl"; break;
case 145: s = "this symbol not expected in TraitDecl"; break;
case 146: s = "invalid ClassMemberDecl"; break;
- case 147: s = "invalid IdentOrDigitsSuffix"; break;
- case 148: s = "this symbol not expected in FieldDecl"; break;
+ case 147: s = "this symbol not expected in FieldDecl"; break;
+ case 148: s = "invalid FunctionDecl"; break;
case 149: s = "invalid FunctionDecl"; break;
case 150: s = "invalid FunctionDecl"; break;
case 151: s = "invalid FunctionDecl"; break;
- case 152: s = "invalid FunctionDecl"; break;
- case 153: s = "this symbol not expected in MethodDecl"; break;
+ case 152: s = "this symbol not expected in MethodDecl"; break;
+ case 153: s = "invalid MethodDecl"; break;
case 154: s = "invalid MethodDecl"; break;
- case 155: s = "invalid MethodDecl"; break;
- case 156: s = "invalid FIdentType"; break;
- case 157: s = "this symbol not expected in OldSemi"; break;
- case 158: s = "invalid TypeIdentOptional"; break;
- case 159: s = "invalid TypeAndToken"; break;
- case 160: s = "this symbol not expected in IteratorSpec"; break;
+ case 155: s = "invalid FIdentType"; break;
+ case 156: s = "this symbol not expected in OldSemi"; break;
+ case 157: s = "invalid TypeIdentOptional"; break;
+ case 158: s = "invalid TypeAndToken"; break;
+ case 159: s = "this symbol not expected in IteratorSpec"; break;
+ case 160: s = "invalid IteratorSpec"; break;
case 161: s = "invalid IteratorSpec"; break;
- case 162: s = "invalid IteratorSpec"; break;
- case 163: s = "this symbol not expected in MethodSpec"; break;
+ case 162: s = "this symbol not expected in MethodSpec"; break;
+ case 163: s = "invalid MethodSpec"; break;
case 164: s = "invalid MethodSpec"; break;
- case 165: s = "invalid MethodSpec"; break;
- case 166: s = "invalid FrameExpression"; break;
- case 167: s = "invalid ReferenceType"; break;
- case 168: s = "this symbol not expected in FunctionSpec"; break;
- case 169: s = "invalid FunctionSpec"; break;
- case 170: s = "invalid PossiblyWildFrameExpression"; break;
- case 171: s = "invalid PossiblyWildExpression"; break;
- case 172: s = "this symbol not expected in OneStmt"; break;
- case 173: s = "invalid OneStmt"; break;
- case 174: s = "this symbol not expected in OneStmt"; break;
- case 175: s = "invalid OneStmt"; break;
- case 176: s = "invalid AssertStmt"; break;
- case 177: s = "invalid AssumeStmt"; break;
+ case 165: s = "invalid FrameExpression"; break;
+ case 166: s = "invalid ReferenceType"; break;
+ case 167: s = "this symbol not expected in FunctionSpec"; break;
+ case 168: s = "invalid FunctionSpec"; break;
+ case 169: s = "invalid PossiblyWildFrameExpression"; break;
+ case 170: s = "invalid PossiblyWildExpression"; break;
+ case 171: s = "this symbol not expected in OneStmt"; break;
+ case 172: s = "invalid OneStmt"; break;
+ case 173: s = "this symbol not expected in OneStmt"; break;
+ case 174: s = "invalid OneStmt"; break;
+ case 175: s = "invalid AssertStmt"; break;
+ case 176: s = "invalid AssumeStmt"; break;
+ case 177: s = "invalid UpdateStmt"; break;
case 178: s = "invalid UpdateStmt"; break;
- case 179: s = "invalid UpdateStmt"; break;
- case 180: s = "this symbol not expected in VarDeclStatement"; break;
+ case 179: s = "this symbol not expected in VarDeclStatement"; break;
+ case 180: s = "invalid IfStmt"; break;
case 181: s = "invalid IfStmt"; break;
- case 182: s = "invalid IfStmt"; break;
+ case 182: s = "invalid WhileStmt"; break;
case 183: s = "invalid WhileStmt"; break;
- case 184: s = "invalid WhileStmt"; break;
- case 185: s = "invalid MatchStmt"; break;
+ case 184: s = "invalid MatchStmt"; break;
+ case 185: s = "invalid ForallStmt"; break;
case 186: s = "invalid ForallStmt"; break;
- case 187: s = "invalid ForallStmt"; break;
+ case 187: s = "invalid CalcStmt"; break;
case 188: s = "invalid ModifyStmt"; break;
case 189: s = "this symbol not expected in ModifyStmt"; break;
case 190: s = "invalid ModifyStmt"; break;
@@ -4291,9 +4232,9 @@ public class Errors {
case 194: s = "invalid Guard"; break;
case 195: s = "this symbol not expected in LoopSpec"; break;
case 196: s = "this symbol not expected in LoopSpec"; break;
- case 197: s = "this symbol not expected in Invariant"; break;
- case 198: s = "invalid CalcOp"; break;
- case 199: s = "invalid Hint"; break;
+ case 197: s = "this symbol not expected in LoopSpec"; break;
+ case 198: s = "invalid LoopSpec"; break;
+ case 199: s = "invalid CalcOp"; break;
case 200: s = "invalid EquivOp"; break;
case 201: s = "invalid ImpliesOp"; break;
case 202: s = "invalid ExpliesOp"; break;
@@ -4324,6 +4265,7 @@ public class Errors {
case 227: s = "invalid StmtInExpr"; break;
case 228: s = "invalid LetExpr"; break;
case 229: s = "invalid CasePattern"; break;
+ case 230: s = "invalid DotSuffix"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 36eeb554..856c6085 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -133,10 +133,30 @@ namespace Microsoft.Dafny {
wr.WriteLine("*/");
}
wr.WriteLine();
+ PrintCallGraph(prog.DefaultModuleDef, 0);
PrintTopLevelDecls(prog.DefaultModuleDef.TopLevelDecls, 0, Path.GetFullPath(prog.Name));
wr.Flush();
}
+ public void PrintCallGraph(ModuleDefinition module, int indent) {
+ Contract.Requires(module != null);
+ Contract.Requires(0 <= indent);
+ if (DafnyOptions.O.DafnyPrintResolvedFile != null) {
+ // print call graph
+ Indent(indent); wr.WriteLine("/* CALL GRAPH for module {0}:", module.Name);
+ var SCCs = module.CallGraph.TopologicallySortedComponents();
+ SCCs.Reverse();
+ foreach (var clbl in SCCs) {
+ Indent(indent); wr.WriteLine(" * SCC at height {0}:", module.CallGraph.GetSCCRepresentativeId(clbl));
+ var r = module.CallGraph.GetSCC(clbl);
+ foreach (var m in r) {
+ Indent(indent); wr.WriteLine(" * {0}", m.NameRelativeToModule);
+ }
+ }
+ Indent(indent); wr.WriteLine(" */");
+ }
+ }
+
public void PrintTopLevelDecls(List<TopLevelDecl> decls, int indent, string fileBeingPrinted) {
Contract.Requires(decls!= null);
int i = 0;
@@ -247,6 +267,7 @@ namespace Microsoft.Dafny {
wr.WriteLine("{ }");
} else {
wr.WriteLine("{");
+ PrintCallGraph(module, indent + IndentAmount);
PrintTopLevelDecls(module.TopLevelDecls, indent + IndentAmount, fileBeingPrinted);
Indent(indent);
wr.WriteLine("}");
@@ -1207,6 +1228,25 @@ namespace Microsoft.Dafny {
Indent(indent);
wr.WriteLine("}");
}
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ Indent(indent);
+ wr.Write("var ");
+ string sep = "";
+ foreach (var lhs in e.LHSs) {
+ wr.Write(sep);
+ PrintCasePattern(lhs);
+ sep = ", ";
+ }
+ if (e.Exact) {
+ wr.Write(" := ");
+ } else {
+ wr.Write(" :| ");
+ }
+ PrintExpressionList(e.RHSs, true);
+ wr.WriteLine(";");
+ PrintExtendedExpr(e.Body, indent, isRightmost, endWithCloseParen);
+
} else if (expr is ParensExpression) {
PrintExtendedExpr(((ParensExpression)expr).E, indent, isRightmost, endWithCloseParen);
} else {
@@ -1320,21 +1360,46 @@ namespace Microsoft.Dafny {
wr.Write("[");
PrintExpressionPairList(e.Elements);
wr.Write("]");
+
+ } else if (expr is NameSegment) {
+ var e = (NameSegment)expr;
+ wr.Write(e.Name);
+
} else if (expr is ExprDotName) {
var e = (ExprDotName)expr;
// determine if parens are needed
int opBindingStrength = 0x70;
- bool parensNeeded = !(e.Obj is ImplicitThisExpr) &&
+ bool parensNeeded = !(e.Lhs is ImplicitThisExpr) &&
opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
if (parensNeeded) { wr.Write("("); }
- if (!(e.Obj is ImplicitThisExpr)) {
- PrintExpr(e.Obj, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
+ if (!(e.Lhs is ImplicitThisExpr)) {
+ PrintExpr(e.Lhs, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
wr.Write(".");
}
wr.Write(e.SuffixName);
if (parensNeeded) { wr.Write(")"); }
+ } else if (expr is ApplySuffix) {
+ var e = (ApplySuffix)expr;
+ // determine if parens are needed
+ int opBindingStrength = 0x70;
+ bool parensNeeded = !(e.Lhs is ImplicitThisExpr) &&
+ opBindingStrength < contextBindingStrength ||
+ (fragileContext && opBindingStrength == contextBindingStrength);
+
+ if (parensNeeded) { wr.Write("("); }
+ if (ParensMayMatter(e.Lhs)) {
+ wr.Write("(");
+ PrintExpression(e.Lhs, false);
+ wr.Write(")");
+ } else {
+ PrintExpr(e.Lhs, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
+ }
+ wr.Write("(");
+ PrintExpressionList(e.Args, false);
+ wr.Write(")");
+ if (parensNeeded) { wr.Write(")"); }
} else if (expr is MemberSelectExpr) {
MemberSelectExpr e = (MemberSelectExpr)expr;
@@ -1840,6 +1905,17 @@ namespace Microsoft.Dafny {
}
}
+ bool ParensMayMatter(Expression expr) {
+ Contract.Requires(expr != null);
+ int parenPairs = 0;
+ for (; expr is ParensExpression; parenPairs++) {
+ expr = ((ParensExpression)expr).E;
+ }
+ // If the program were resolved, we could be more precise than the following (in particular, looking
+ // to see if expr denotes a MemberSelectExpr of a member that is a Function.
+ return parenPairs != 0 && (expr is NameSegment || expr is ExprDotName);
+ }
+
void PrintCasePattern(CasePattern pat) {
Contract.Requires(pat != null);
var v = pat.Var;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 167b56c2..47cf17b5 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -509,7 +509,7 @@ namespace Microsoft.Dafny
return
new SetComprehension(e.tok, bvars,
new BinaryExpr(e.tok, BinaryExpr.Opcode.In, obj,
- new ApplyExpr(e.tok, e.tok, e, bexprs)
+ new ApplyExpr(e.tok, e, bexprs)
{
Type = new SetType(new ObjectType())
})
@@ -5191,6 +5191,7 @@ namespace Microsoft.Dafny
callRhs = callRhs ?? (CallRhs)rhs;
} else {
var er = (ExprRhs)rhs;
+#if OLD_STUFF
if (er.Expr is IdentifierSequence) {
var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, new ResolveOpts(codeContext, true), true);
isEffectful = cRhs != null;
@@ -5199,6 +5200,13 @@ namespace Microsoft.Dafny
var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, new ResolveOpts(codeContext, true), true);
isEffectful = cRhs != null;
callRhs = callRhs ?? cRhs;
+#else
+ if (er.Expr is ApplySuffix) {
+ var a = (ApplySuffix)er.Expr;
+ var cRhs = ResolveApplySuffix(a, new ResolveOpts(codeContext, true), true);
+ isEffectful = cRhs != null;
+ callRhs = callRhs ?? cRhs;
+#endif
} else {
ResolveExpression(er.Expr, new ResolveOpts(codeContext, true));
isEffectful = false;
@@ -6002,9 +6010,9 @@ namespace Microsoft.Dafny
}
/// <summary>
- /// Returns a resolved FieldSelectExpr.
+ /// Returns a resolved MemberSelectExpr.
/// </summary>
- public static MemberSelectExpr NewFieldSelectExpr(IToken tok, Expression obj, Field field, Dictionary<TypeParameter, Type> typeSubstMap) {
+ public static MemberSelectExpr NewMemberSelectExpr(IToken tok, Expression obj, Field field, Dictionary<TypeParameter, Type> typeSubstMap) {
Contract.Requires(tok != null);
Contract.Requires(obj != null);
Contract.Requires(field != null);
@@ -6342,15 +6350,24 @@ namespace Microsoft.Dafny
}
}
expr.Type = new MapType(domainType, rangeType);
+ } else if (expr is NameSegment) {
+ var e = (NameSegment)expr;
+ ResolveNameSegment(e, true, null, opts, false);
+ if (e.Type is Resolver_IdentifierExpr.ResolverType_Module) {
+ Error(e.tok, "name of module ({0}) is used as a variable", e.Name);
+ } else if (e.Type is Resolver_IdentifierExpr.ResolverType_Type) {
+ Error(e.tok, "name of type ({0}) is used as a variable", e.Name);
+ }
+
} else if (expr is ExprDotName) {
var e = (ExprDotName)expr;
-
+#if OLD_WAY
// The following call to ResolveExpression is just preliminary. If it succeeds, it is redone below on the resolved expression. Thus,
// it's okay to be more lenient here and use coLevel (instead of trying to use CoLevel_Dec(coLevel), which is needed when .Name denotes a
// destructor for a co-datatype).
- ResolveExpression(e.Obj, opts);
- Contract.Assert(e.Obj.Type != null); // follows from postcondition of ResolveExpression
- Expression resolved = ResolveMemberSelect(expr.tok, e.Obj, e.SuffixName);
+ ResolveExpression(e.Lhs, opts);
+ Contract.Assert(e.Lhs.Type != null); // follows from postcondition of ResolveExpression
+ Expression resolved = ResolveMemberSelect(expr.tok, e.Lhs, e.SuffixName);
if (resolved == null) {
// error has already been reported by ResolvePredicateOrField
@@ -6360,6 +6377,18 @@ namespace Microsoft.Dafny
ResolveExpression(e.ResolvedExpression, opts);
e.Type = e.ResolvedExpression.Type;
}
+#else
+ ResolveDotSuffix(e, true, null, opts, false);
+ if (e.Type is Resolver_IdentifierExpr.ResolverType_Module) {
+ Error(e.tok, "name of module ({0}) is used as a variable", e.SuffixName);
+ } else if (e.Type is Resolver_IdentifierExpr.ResolverType_Type) {
+ Error(e.tok, "name of type ({0}) is used as a variable", e.SuffixName);
+ }
+#endif
+
+ } else if (expr is ApplySuffix) {
+ var e = (ApplySuffix)expr;
+ ResolveApplySuffix(e, opts, false);
} else if (expr is MemberSelectExpr) {
var e = (MemberSelectExpr)expr;
@@ -6477,22 +6506,17 @@ namespace Microsoft.Dafny
} else if (e.Seq.Type.IsDatatype) {
var dt = e.Seq.Type.AsDatatype;
- if (!(e.Index is IdentifierSequence || (e.Index is LiteralExpr && ((LiteralExpr)e.Index).Value is BigInteger))) {
+ if (!(e.Index is NameSegment|| (e.Index is LiteralExpr && ((LiteralExpr)e.Index).Value is BigInteger))) {
Error(expr, "datatype updates must be to datatype destructors");
} else {
string destructor_str = null;
- if (e.Index is IdentifierSequence) {
- IdentifierSequence iseq = (IdentifierSequence)e.Index;
-
- if (iseq.Tokens.Count() != 1) {
- Error(expr, "datatype updates must name a single datatype destructor");
- } else {
- destructor_str = iseq.Tokens.First().val;
- }
+ if (e.Index is NameSegment) {
+ var seg = (NameSegment)e.Index;
+ destructor_str = seg.Name;
} else {
Contract.Assert(e.Index is LiteralExpr && ((LiteralExpr)e.Index).Value is BigInteger);
- destructor_str = ((LiteralExpr)e.Index).tok.val;
+ destructor_str = ((LiteralExpr)e.Index).tok.val; // note, take the string of digits, not the parsed integer
}
if (destructor_str != null) {
@@ -6549,9 +6573,9 @@ namespace Microsoft.Dafny
}
var fnType = e.Function.Type.AsArrowType;
if (fnType == null) {
- Error(e.OpenParen, "apply expression requires a function (got {0})", e.Function.Type);
+ Error(e.tok, "non-function expression (of type {0}) is called with parameters", e.Function.Type);
} else if (fnType.Arity != e.Args.Count) {
- Error(e.OpenParen, "wrong number of arguments to function application (function type '{0}' expects {1}, got {2})", fnType, fnType.Arity, e.Args.Count);
+ Error(e.tok, "wrong number of arguments to function application (function type '{0}' expects {1}, got {2})", fnType, fnType.Arity, e.Args.Count);
} else {
for (var i = 0; i < fnType.Arity; i++) {
if (!UnifyTypes(fnType.Args[i], e.Args[i].Type)) {
@@ -7162,7 +7186,7 @@ namespace Microsoft.Dafny
if (expr.Type == null) {
// some resolution error occurred
- expr.Type = Type.Flexible;
+ expr.Type = new InferredTypeProxy();
}
}
@@ -7226,6 +7250,438 @@ namespace Microsoft.Dafny
}
}
+ /// <summary>
+ /// Look up expr.Name in the following order:
+ /// 0. Local variable, parameter, or bound variable.
+ /// (Language design note: If this clashes with something of interest, one can always rename the local variable locally.)
+ /// 1. Member of enclosing class (an implicit "this" is inserted, if needed)
+ /// 2. If isLastNameSegment:
+ /// Unambiguous constructor name of a datatype in the enclosing module (if two constructors have the same name, an error message is produced here)
+ /// (Language design note: If the constructor name is ambiguous or if one of the steps above takes priority, one can qualify the constructor name with the name of the datatype)
+ /// 3. Member of the enclosing module (type name or the name of a module)
+ /// 4. Static function or method in the enclosing module or its imports
+ ///
+ /// </summary>
+ /// <param name="expr"></param>
+ /// <param name="isLastNameSegment">Indicates that the NameSegment is not directly enclosed in another NameSegment or ExprDotName expression.</param>
+ /// <param name="args">If the NameSegment is enclosed in an ApplySuffix, then these are the arguments. The method returns null to indicate
+ /// that these arguments, if any, were not used. If args is non-null and the method does use them, the method returns the resolved expression
+ /// that incorporates these arguments.</param>
+ /// <param name="opts"></param>
+ /// <param name="allowMethodCall">If false, generates an error if the name denotes a method. If true and the name denotes a method, returns
+ /// a MemberSelectExpr whose .Member is a Method.</param>
+ Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<Expression> args, ResolveOpts opts, bool allowMethodCall) {
+ Contract.Requires(expr != null);
+ Contract.Requires(!expr.WasResolved());
+ Contract.Requires(opts != null);
+ Contract.Ensures(Contract.Result<Expression>() == null || args != null);
+
+ if (expr.OptTypeArguments != null) {
+ foreach (var ty in expr.OptTypeArguments) {
+ ResolveType(expr.tok, ty, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
+ }
+ }
+
+ Expression r = null; // the resolved expression, if successful
+ Expression rWithArgs = null; // the resolved expression after incorporating "args"
+
+ // For 0:
+ var v = scope.Find(expr.Name);
+ // For 1:
+ Dictionary<string, MemberDecl> members;
+ // For 1 and 4:
+ MemberDecl member = null;
+ Expression receiver = null; // non-null implies that member is non-null, too; and it means that r should be constructed from receiver.member
+ // For 2:
+ Tuple<DatatypeCtor, bool> pair;
+ // For 3:
+ TopLevelDecl decl;
+
+ if (v != null) {
+ // ----- 0. local variable, parameter, or bound variable
+ var rr = new IdentifierExpr(expr.tok, expr.Name);
+ rr.Var = v; rr.Type = v.Type;
+ r = rr;
+ } else if (currentClass != null && classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(expr.Name, out member)) {
+ // ----- 1. member of the enclosing class
+ if (member.IsStatic) {
+ receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);
+ } else {
+ if (!scope.AllowInstance) {
+ Error(expr.tok, "'this' is not allowed in a 'static' context");
+ // nevertheless, set "receiver" to a value so we can continue resolution
+ }
+ receiver = new ImplicitThisExpr(expr.tok);
+ receiver.Type = GetThisType(expr.tok, (ClassDecl)member.EnclosingClass); // resolve here
+ }
+ // "receiver" and "member" have been set; "r" will be filled in below
+ } else if (isLastNameSegment && moduleInfo.Ctors.TryGetValue(expr.Name, out pair)) {
+ // ----- 2. datatype constructor
+ if (pair.Item2) {
+ // there is more than one constructor with this name
+ Error(expr.tok, "the name '{0}' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, '{1}.{0}')", expr.Name, pair.Item1.EnclosingDatatype.Name);
+ } else {
+ var rr = new DatatypeValue(expr.tok, pair.Item1.EnclosingDatatype.Name, expr.Name, args ?? new List<Expression>());
+ ResolveDatatypeValue(opts, rr, pair.Item1.EnclosingDatatype);
+ if (args == null) {
+ r = rr;
+ } else {
+ r = rr; // this doesn't really matter, since we're returning an "rWithArgs" (but if would have been proper to have returned the ctor as a lambda)
+ rWithArgs = rr;
+ }
+ }
+ } else if (moduleInfo.TopLevels.TryGetValue(expr.Name, out decl)) {
+ // ----- 3. Member of the enclosing module
+ if (decl is AmbiguousTopLevelDecl) {
+ Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", expr.Name, ((AmbiguousTopLevelDecl)decl).ModuleNames());
+ } else {
+ // We have found a module name or a type name, neither of which is an expression. However, the NameSegment we're
+ // looking at may be followed by a further suffix that makes this into an expresion. We postpone the rest of the
+ // resolution to any such suffix. For now, we create a temporary expression that will never be seen by the compiler
+ // or verifier, just to have a placeholder where we can recorded what we have found.
+ r = new Resolver_IdentifierExpr(expr.tok, decl);
+ }
+
+ } else if (moduleInfo.StaticMembers.TryGetValue(expr.Name, out member)) {
+ // ----- 4. static member of the enclosing module
+ Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default
+ if (member is AmbiguousMemberDecl) {
+ Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1}", expr.Name, ((AmbiguousMemberDecl)member).ModuleNames());
+ } else {
+ receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);
+ }
+ // "receiver" and "member" have been set; "r" will be filled in below
+
+ } else {
+ // ----- None of the above
+ Error(expr.tok, "unresolved identifier: {0}", expr.Name);
+ }
+
+ // Now, continue processing cases 1 and 4:
+ if (receiver != null) {
+ Contract.Assert(member != null);
+ Contract.Assert(receiver.WasResolved());
+ r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);
+ }
+
+ if (r == null) {
+ // an error has been reported above; we won't fill in .ResolvedExpression, but we still must fill in .Type
+ expr.Type = new InferredTypeProxy();
+ } else {
+ expr.ResolvedExpression = r;
+ expr.Type = r.Type;
+ }
+ return rWithArgs;
+ }
+
+ /// <summary>
+ /// To resolve "id" in expression "E . id", do:
+ /// * If E denotes a module name M:
+ /// 0. If isLastNameSegment:
+ /// Unambiguous constructor name of a datatype in module M (if two constructors have the same name, an error message is produced here)
+ /// (Language design note: If the constructor name is ambiguous or if one of the steps above takes priority, one can qualify the constructor name with the name of the datatype)
+ /// 0. Member of module M: sub-module (including submodules of imports), class, datatype, etc.
+ /// (if two imported types have the same name, an error message is produced here)
+ /// 1. Static function or method of M._default
+ /// (Note that in contrast to ResolveNameSegment, imported modules, etc. are ignored)
+ /// * If E denotes a type:
+ /// 2. Look up id as a member of that type
+ /// * If E denotes an expression:
+ /// 3. Let T be the type of E. Look up id in T.
+ /// </summary>
+ /// <param name="expr"></param>
+ /// <param name="isLastNameSegment">Indicates that the ExprDotName is not directly enclosed in another ExprDotName expression.</param>
+ /// <param name="args">If the ExprDotName is enclosed in an ApplySuffix, then these are the arguments. The method returns null to indicate
+ /// that these arguments, if any, were not used. If args is non-null and the method does use them, the method returns the resolved expression
+ /// that incorporates these arguments.</param>
+ /// <param name="opts"></param>
+ /// <param name="allowMethodCall">If false, generates an error if the name denotes a method. If true and the name denotes a method, returns
+ /// a Resolver_MethodCall.</param>
+ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List<Expression> args, ResolveOpts opts, bool allowMethodCall) {
+ Contract.Requires(expr != null);
+ Contract.Requires(!expr.WasResolved());
+ Contract.Requires(opts != null);
+ Contract.Ensures(Contract.Result<Expression>() == null || args != null);
+
+ if (expr.Lhs is NameSegment) {
+ ResolveNameSegment((NameSegment)expr.Lhs, false, null, opts, false);
+ } else if (expr.Lhs is ExprDotName) {
+ ResolveDotSuffix((ExprDotName)expr.Lhs, false, null, opts, false);
+ } else {
+ ResolveExpression(expr.Lhs, opts);
+ }
+
+ if (expr.OptTypeArguments != null) {
+ foreach (var ty in expr.OptTypeArguments) {
+ ResolveType(expr.tok, ty, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
+ }
+ }
+
+ Expression r = null; // the resolved expression, if successful
+ Expression rWithArgs = null; // the resolved expression after incorporating "args"
+
+ MemberDecl member = null;
+ Expression receiver = null; // non-null implies that member is non-null, too; and it means that r should be constructed from receiver.member
+
+ var lhs = expr.Lhs.Resolved;
+ if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Module) {
+ var ri = (Resolver_IdentifierExpr)lhs;
+ var sig = ((ModuleDecl)ri.Decl).Signature;
+ sig = GetSignature(sig);
+ // For 1:
+ TopLevelDecl decl;
+ Tuple<DatatypeCtor, bool> pair;
+
+ if (isLastNameSegment && moduleInfo.Ctors.TryGetValue(expr.SuffixName, out pair)) {
+ // ----- 0. datatype constructor
+ if (pair.Item2) {
+ // there is more than one constructor with this name
+ Error(expr.tok, "the name '{0}' denotes a datatype constructor in module {2}, but does not do so uniquely; add an explicit qualification (for example, '{1}.{0}')", expr.SuffixName, pair.Item1.EnclosingDatatype.Name, ((ModuleDecl)ri.Decl).Name);
+ } else {
+ var rr = new DatatypeValue(expr.tok, pair.Item1.EnclosingDatatype.Name, expr.SuffixName, args ?? new List<Expression>());
+ ResolveExpression(rr, opts);
+ if (args == null) {
+ r = rr;
+ } else {
+ r = rr; // this doesn't really matter, since we're returning an "rWithArgs" (but if would have been proper to have returned the ctor as a lambda)
+ rWithArgs = rr;
+ }
+ }
+ } else if (sig.TopLevels.TryGetValue(expr.SuffixName, out decl)) {
+ // ----- 1. Member of the specified module
+ if (decl is AmbiguousTopLevelDecl) {
+ Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", expr.SuffixName, ((AmbiguousTopLevelDecl)decl).ModuleNames());
+ } else {
+ // We have found a module name or a type name, neither of which is an expression. However, the ExprDotName we're
+ // looking at may be followed by a further suffix that makes this into an expresion. We postpone the rest of the
+ // resolution to any such suffix. For now, we create a temporary expression that will never be seen by the compiler
+ // or verifier, just to have a placeholder where we can recorded what we have found.
+ r = new Resolver_IdentifierExpr(expr.tok, decl);
+ }
+ } else if (sig.StaticMembers.TryGetValue(expr.SuffixName, out member)) {
+ // ----- 2. static member of the specified module
+ Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default
+ if (member is AmbiguousMemberDecl) {
+ Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1}", expr.SuffixName, ((AmbiguousMemberDecl)member).ModuleNames());
+ } else {
+ receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);
+ }
+ // "receiver" and "member" have been set; "r" will be filled in below
+ // TODO (can be done in else branch above)
+ } else {
+ Error(expr.tok, "unresolved identifier: {0}", expr.SuffixName);
+ }
+
+ } else if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) {
+ var ri = (Resolver_IdentifierExpr)lhs;
+ var decl = ri.Decl;
+ // ----- 3. Look up name in type
+ // expand any synonyms
+ var tpArgs = decl.TypeArgs.ConvertAll(_ => (Type)new InferredTypeProxy());
+ var ty = new UserDefinedType(expr.tok, decl.Name, decl, tpArgs).NormalizeExpand();
+ if (ty.IsRefType) {
+ // ----- LHS is a class
+ var cd = (ClassDecl)((UserDefinedType)ty).ResolvedClass;
+ Dictionary<string, MemberDecl> members;
+ if (classMembers.TryGetValue(cd, out members) && members.TryGetValue(expr.SuffixName, out member)) {
+ if (!member.IsStatic) {
+ Error(expr.tok, "accessing member '{0}' requires an instance expression", expr.SuffixName);
+ // nevertheless, continue creating an expression that approximates a correct one
+ }
+ receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);
+ }
+ } else if (ty.IsDatatype) {
+ // ----- LHS is a datatype
+ var dt = ty.AsDatatype;
+ Dictionary<string, DatatypeCtor> members;
+ DatatypeCtor ctor;
+ if (datatypeCtors.TryGetValue(dt, out members) && members.TryGetValue(expr.SuffixName, out ctor)) {
+ var rr = new DatatypeValue(expr.tok, ctor.EnclosingDatatype.Name, expr.SuffixName, args ?? new List<Expression>());
+ ResolveDatatypeValue(opts, rr, ctor.EnclosingDatatype);
+ if (args == null) {
+ r = rr;
+ } else {
+ r = rr; // this doesn't really matter, since we're returning an "rWithArgs" (but if would have been proper to have returned the ctor as a lambda)
+ rWithArgs = rr;
+ }
+ }
+ }
+ if (receiver == null && r == null) {
+ Error(expr.tok, "member '{0}' does not exist in type '{1}'", expr.SuffixName, ri.Decl.Name);
+ }
+ } else if (lhs != null) {
+ // ----- 4. Look up name in the type of the Lhs
+ NonProxyType nptype;
+ member = ResolveMember(expr.tok, expr.Lhs.Type, expr.SuffixName, out nptype);
+ if (member != null) {
+ receiver = expr.Lhs;
+ }
+ }
+
+ if (receiver != null) {
+ Contract.Assert(member != null);
+ Contract.Assert(receiver.WasResolved());
+ r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);
+ }
+
+ if (r == null) {
+ // an error has been reported above; we won't fill in .ResolvedExpression, but we still must fill in .Type
+ expr.Type = new InferredTypeProxy();
+ } else {
+ expr.ResolvedExpression = r;
+ expr.Type = r.Type;
+ }
+ return rWithArgs;
+ }
+
+ Expression ResolveExprDotCall(IToken tok, Expression receiver, MemberDecl member, List<Type> optTypeArguments, ICodeContext caller, bool allowMethodCall) {
+ Contract.Requires(tok != null);
+ Contract.Requires(receiver != null);
+ Contract.Requires(receiver.WasResolved());
+ Contract.Requires(member != null);
+ Contract.Requires(caller != null);
+
+ var rr = new MemberSelectExpr(tok, receiver, member.Name);
+ rr.Member = member;
+
+ // Now, fill in rr.Type. This requires taking into consideration the type parameters passed to the receiver's type as well as any type
+ // parameters used in this NameSegment.
+ // Add to "subst" the type parameters given to the member's class/datatype
+ Dictionary<TypeParameter, Type> subst;
+ var udt = receiver.Type.NormalizeExpand() as UserDefinedType;
+ if (udt != null && udt.ResolvedClass != null) {
+ subst = TypeSubstitutionMap(udt.ResolvedClass.TypeArgs, udt.TypeArgs);
+ } else {
+ subst = new Dictionary<TypeParameter, Type>();
+ }
+
+ if (member is Field) {
+ if (optTypeArguments != null) {
+ Error(tok, "a field ({0}) does not take any type arguments (got {1})", member.Name, optTypeArguments.Count);
+ }
+ rr.Type = SubstType(((Field)member).Type, subst);
+ } else if (member is Function) {
+ var fn = (Function)member;
+ int suppliedTypeArguments = optTypeArguments == null ? 0 : optTypeArguments.Count;
+ if (optTypeArguments != null && suppliedTypeArguments != fn.TypeArgs.Count) {
+ Error(tok, "function {0} expects {1} type arguments (got {2})", member.Name, fn.TypeArgs.Count, suppliedTypeArguments);
+ }
+ rr.TypeApplication = new List<Type>();
+ for (int i = 0; i < fn.TypeArgs.Count; i++) {
+ var ta = i < suppliedTypeArguments ? optTypeArguments[i] : new InferredTypeProxy();
+ rr.TypeApplication.Add(ta);
+ subst.Add(fn.TypeArgs[i], ta);
+ }
+ rr.Type = new ArrowType(fn.tok, fn.Formals.ConvertAll(f => SubstType(f.Type, subst)), SubstType(fn.ResultType, subst), builtIns.SystemModule);
+ AddCallGraphEdge(rr, caller, fn);
+ } else {
+ // the member is a method
+ Contract.Assert(member is Method);
+ if (!allowMethodCall) {
+ // it's a method and method calls are not allowed in the given context
+ Error(tok, "expression is not allowed to invoke a method ({0})", member.Name);
+ }
+ rr.Type = new InferredTypeProxy(); // fill in this field, in order to make "rr" resolved
+ }
+ return rr;
+ }
+
+
+ CallRhs ResolveApplySuffix(ApplySuffix e, ResolveOpts opts, bool allowMethodCall) {
+ Contract.Requires(e != null);
+ Contract.Requires(opts != null);
+ Contract.Ensures(Contract.Result<CallRhs>() == null || allowMethodCall);
+ Expression r = null; // upon success, the expression to which the ApplySuffix resolves
+ var errorCount = ErrorCount;
+ if (e.Lhs is NameSegment) {
+ r = ResolveNameSegment((NameSegment)e.Lhs, true, e.Args, opts, allowMethodCall);
+ // note, if r is non-null, then e.Args have been resolved and r is a resolved expression that incorporates e.Args
+ } else if (e.Lhs is ExprDotName) {
+ r = ResolveDotSuffix((ExprDotName)e.Lhs, true, e.Args, opts, allowMethodCall);
+ // note, if r is non-null, then e.Args have been resolved and r is a resolved expression that incorporates e.Args
+ } else {
+ ResolveExpression(e.Lhs, opts);
+ }
+ if (r == null) {
+ foreach (var arg in e.Args) {
+ ResolveExpression(arg, opts);
+ }
+ var fnType = e.Lhs.Type.AsArrowType;
+ if (fnType == null) {
+ var lhs = e.Lhs.Resolved;
+ if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Module) {
+ Error(e.tok, "name of module ({0}) is used as a function", ((Resolver_IdentifierExpr)lhs).Decl.Name);
+ } else if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) {
+ // It may be a conversion expression
+ var decl = ((Resolver_IdentifierExpr)lhs).Decl;
+ var tpArgs = decl.TypeArgs.ConvertAll(_ => (Type)new InferredTypeProxy());
+ var ty = new UserDefinedType(e.tok, decl.Name, decl, tpArgs);
+ if (ty.AsNewtype != null) {
+ if (e.Args.Count != 1) {
+ Error(e.tok, "conversion operation to {0} got wrong number of arguments (expected 1, got {1})", decl.Name, e.Args.Count);
+ }
+ var conversionArg = 1 <= e.Args.Count ? e.Args[0] :
+ ty.IsNumericBased(Type.NumericPersuation.Int) ? LiteralExpr.CreateIntLiteral(e.tok, 0) :
+ LiteralExpr.CreateRealLiteral(e.tok, Basetypes.BigDec.ZERO);
+ r = new ConversionExpr(e.tok, conversionArg, ty);
+ ResolveExpression(r, opts);
+ // resolve the rest of the arguments, if any
+ for (int i = 1; i < e.Args.Count; i++) {
+ ResolveExpression(e.Args[i], opts);
+ }
+ } else {
+ Error(e.tok, "name of type ({0}) is used as a function", decl.Name);
+ }
+ } else {
+ if (lhs is MemberSelectExpr && ((MemberSelectExpr)lhs).Member is Method) {
+ var mse = (MemberSelectExpr)lhs;
+ var method = (Method)mse.Member;
+ if (allowMethodCall) {
+ var cRhs = new CallRhs(e.tok, mse.Obj, method.Name, e.Args);
+ cRhs.Method = method;
+ return cRhs;
+ } else {
+ Error(e.tok, "method call is not allowed to be used in an expression context ({0})", method.Name);
+ }
+ } else if (lhs != null) { // if e.Lhs.Resolved is null, then e.Lhs was not successfully resolved and an error has already been reported
+ Error(e.tok, "non-function expression (of type {0}) is called with parameters", e.Lhs.Type);
+ }
+ }
+ } else {
+ var mse = e.Lhs is NameSegment || e.Lhs is ExprDotName ? e.Lhs.Resolved as MemberSelectExpr : null;
+ var callee = mse == null ? null : mse.Member as Function;
+ if (fnType.Arity != e.Args.Count) {
+ var what = callee != null ? string.Format("function '{0}'", callee.Name) : string.Format("function type '{0}'", fnType);
+ Error(e.tok, "wrong number of arguments to function application ({0} expects {1}, got {2})", what, fnType.Arity, e.Args.Count);
+ } else {
+ for (var i = 0; i < fnType.Arity; i++) {
+ if (!UnifyTypes(fnType.Args[i], e.Args[i].Type)) {
+ Error(e.Args[i].tok, "type mismatch for argument {0} (function expects {1}, got {2})", i, fnType.Args[i], e.Args[i].Type);
+ }
+ }
+ if (errorCount != ErrorCount) {
+ // no nothing else; error has been reported
+ } else if (callee != null) {
+ // produce a FunctionCallExpr instead of an ApplyExpr(MemberSelectExpr)
+ r = new FunctionCallExpr(e.Lhs.tok, callee.Name, mse.Obj, e.tok, e.Args);
+ ResolveExpression(r, opts);
+ } else {
+ r = new ApplyExpr(e.Lhs.tok, e.Lhs, e.Args);
+ r.Type = fnType.Result;
+ }
+ }
+ }
+ }
+ if (r == null) {
+ // an error has been reported above; we won't fill in .ResolvedExpression, but we still must fill in .Type
+ e.Type = new InferredTypeProxy();
+ } else {
+ e.ResolvedExpression = r;
+ e.Type = r.Type;
+ }
+ return null;
+ }
+
private void ResolveDatatypeValue(ResolveOpts opts, DatatypeValue dtv, DatatypeDecl dt) {
// this resolution is a little special, in that the syntax shows only the base name, not its instantiation (which is inferred)
List<Type> gt = new List<Type>(dt.TypeArgs.Count);
@@ -7246,7 +7702,7 @@ namespace Microsoft.Dafny
Contract.Assert(ctor != null); // follows from postcondition of TryGetValue
dtv.Ctor = ctor;
if (ctor.Formals.Count != dtv.Arguments.Count) {
- Error(dtv.tok, "wrong number of arguments to datatype constructor {0} (found {1}, expected {2})", dtv.DatatypeName, dtv.Arguments.Count, ctor.Formals.Count);
+ Error(dtv.tok, "wrong number of arguments to datatype constructor {0} (found {1}, expected {2})", ctor.Name, dtv.Arguments.Count, ctor.Formals.Count);
}
}
int j = 0;
@@ -7485,7 +7941,7 @@ namespace Microsoft.Dafny
var field = member as Field;
if (field != null) {
if (field.Type.IsArrowType || field.Type.IsTypeParameter) {
- return new ApplyExpr(tok, openParen, new ExprDotName(tok, receiver, fn), args);
+ return new ApplyExpr(openParen, new ExprDotName(tok, receiver, fn), args);
}
}
return new FunctionCallExpr(tok, fn, receiver, openParen, args);
@@ -7903,7 +8359,7 @@ namespace Microsoft.Dafny
} else if (e.Arguments != null) {
Contract.Assert(p == e.Tokens.Count);
if (r.Type.IsArrowType || r.Type.IsTypeParameter) {
- r = new ApplyExpr(e.tok, e.OpenParen, r, e.Arguments);
+ r = new ApplyExpr(e.OpenParen, r, e.Arguments);
ResolveExpression(r, opts);
} else {
Error(e.OpenParen, "non-function expression is called with parameters");
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 6034e207..31ba1a3d 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -217,7 +217,7 @@ namespace Microsoft.Dafny
// the field has been inherited from a refined module, so don't include it here
continue;
}
- var F = Resolver.NewFieldSelectExpr(tok, implicitSelf, ff.Item1, null);
+ var F = Resolver.NewMemberSelectExpr(tok, implicitSelf, ff.Item1, null);
var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NeqCommon, F, cNull);
var c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, F, Repr);
if (ff.Item2 == null) {
@@ -296,7 +296,7 @@ namespace Microsoft.Dafny
// TODO: these assignments should be included on every return path
foreach (var ff in subobjects) {
- var F = Resolver.NewFieldSelectExpr(tok, implicitSelf, ff.Item1, null); // create a resolved FieldSelectExpr
+ var F = Resolver.NewMemberSelectExpr(tok, implicitSelf, ff.Item1, null); // create a resolved MemberSelectExpr
Expression e = new SetDisplayExpr(tok, new List<Expression>() { F });
e.Type = new SetType(new ObjectType()); // resolve here
var rhs = new BinaryExpr(tok, BinaryExpr.Opcode.Add, Repr, e);
@@ -306,7 +306,7 @@ namespace Microsoft.Dafny
// Repr := Repr + {F} (so, nothing else to do)
} else {
// Repr := Repr + {F} + F.Repr
- var FRepr = Resolver.NewFieldSelectExpr(tok, F, ff.Item2, null); // create resolved FieldSelectExpr
+ var FRepr = Resolver.NewMemberSelectExpr(tok, F, ff.Item2, null); // create resolved MemberSelectExpr
rhs = new BinaryExpr(tok, BinaryExpr.Opcode.Add, rhs, FRepr);
rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union; // resolve here
rhs.Type = Repr.Type; // resolve here
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index f54acb78..fb257ead 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -263,9 +263,10 @@ public class Scanner {
start[44] = 29;
start[124] = 90;
start[8226] = 31;
+ start[46] = 91;
start[59] = 32;
- start[61] = 91;
- start[45] = 92;
+ start[61] = 92;
+ start[45] = 93;
start[123] = 35;
start[125] = 36;
start[91] = 37;
@@ -273,8 +274,7 @@ public class Scanner {
start[40] = 39;
start[41] = 40;
start[42] = 41;
- start[33] = 93;
- start[46] = 94;
+ start[33] = 94;
start[60] = 95;
start[62] = 96;
start[96] = 64;
@@ -495,54 +495,54 @@ public class Scanner {
void CheckLiteral() {
switch (t.val) {
- case "assume": t.kind = 16; break;
- case "calc": t.kind = 17; break;
- case "case": t.kind = 18; break;
- case "decreases": t.kind = 19; break;
- case "invariant": t.kind = 20; break;
- case "map": t.kind = 21; break;
- case "modifies": t.kind = 22; break;
- case "reads": t.kind = 23; break;
- case "requires": t.kind = 24; break;
- case "include": t.kind = 34; break;
- case "abstract": t.kind = 35; break;
- case "module": t.kind = 36; break;
- case "refines": t.kind = 37; break;
- case "import": t.kind = 38; break;
- case "opened": t.kind = 39; break;
- case "as": t.kind = 41; break;
- case "default": t.kind = 42; break;
- case "class": t.kind = 43; break;
- case "extends": t.kind = 44; break;
- case "trait": t.kind = 45; break;
- case "ghost": t.kind = 46; break;
- case "static": t.kind = 47; break;
- case "datatype": t.kind = 48; break;
- case "codatatype": t.kind = 49; break;
- case "var": t.kind = 50; break;
- case "newtype": t.kind = 51; break;
- case "type": t.kind = 52; break;
- case "iterator": t.kind = 54; break;
- case "yields": t.kind = 55; break;
- case "returns": t.kind = 56; break;
- case "method": t.kind = 59; break;
- case "lemma": t.kind = 60; break;
- case "colemma": t.kind = 61; break;
- case "comethod": t.kind = 62; break;
- case "constructor": t.kind = 63; break;
- case "free": t.kind = 64; break;
- case "ensures": t.kind = 65; break;
- case "yield": t.kind = 66; break;
- case "bool": t.kind = 67; break;
- case "char": t.kind = 68; break;
- case "nat": t.kind = 69; break;
- case "int": t.kind = 70; break;
- case "real": t.kind = 71; break;
- case "set": t.kind = 72; break;
- case "multiset": t.kind = 73; break;
- case "seq": t.kind = 74; break;
- case "string": t.kind = 75; break;
- case "object": t.kind = 76; break;
+ case "assume": t.kind = 17; break;
+ case "calc": t.kind = 18; break;
+ case "case": t.kind = 19; break;
+ case "decreases": t.kind = 20; break;
+ case "invariant": t.kind = 21; break;
+ case "map": t.kind = 22; break;
+ case "modifies": t.kind = 23; break;
+ case "reads": t.kind = 24; break;
+ case "requires": t.kind = 25; break;
+ case "include": t.kind = 35; break;
+ case "abstract": t.kind = 36; break;
+ case "module": t.kind = 37; break;
+ case "refines": t.kind = 38; break;
+ case "import": t.kind = 39; break;
+ case "opened": t.kind = 40; break;
+ case "as": t.kind = 42; break;
+ case "default": t.kind = 43; break;
+ case "class": t.kind = 44; break;
+ case "extends": t.kind = 45; break;
+ case "trait": t.kind = 46; break;
+ case "ghost": t.kind = 47; break;
+ case "static": t.kind = 48; break;
+ case "datatype": t.kind = 49; break;
+ case "codatatype": t.kind = 50; break;
+ case "var": t.kind = 51; break;
+ case "newtype": t.kind = 52; break;
+ case "type": t.kind = 53; break;
+ case "iterator": t.kind = 55; break;
+ case "yields": t.kind = 56; break;
+ case "returns": t.kind = 57; break;
+ case "method": t.kind = 60; break;
+ case "lemma": t.kind = 61; break;
+ case "colemma": t.kind = 62; break;
+ case "comethod": t.kind = 63; break;
+ case "constructor": t.kind = 64; break;
+ case "free": t.kind = 65; break;
+ case "ensures": t.kind = 66; break;
+ case "yield": t.kind = 67; break;
+ case "bool": t.kind = 68; break;
+ case "char": t.kind = 69; break;
+ case "nat": t.kind = 70; break;
+ case "int": t.kind = 71; break;
+ case "real": t.kind = 72; break;
+ case "set": t.kind = 73; break;
+ case "multiset": t.kind = 74; break;
+ case "seq": t.kind = 75; break;
+ case "string": t.kind = 76; break;
+ case "object": t.kind = 77; break;
case "function": t.kind = 78; break;
case "predicate": t.kind = 79; break;
case "copredicate": t.kind = 80; break;
@@ -705,25 +705,25 @@ public class Scanner {
case 31:
{t.kind = 12; break;}
case 32:
- {t.kind = 13; break;}
- case 33:
{t.kind = 14; break;}
- case 34:
+ case 33:
{t.kind = 15; break;}
+ case 34:
+ {t.kind = 16; break;}
case 35:
- {t.kind = 25; break;}
- case 36:
{t.kind = 26; break;}
- case 37:
+ case 36:
{t.kind = 27; break;}
- case 38:
+ case 37:
{t.kind = 28; break;}
- case 39:
+ case 38:
{t.kind = 29; break;}
- case 40:
+ case 39:
{t.kind = 30; break;}
- case 41:
+ case 40:
{t.kind = 31; break;}
+ case 41:
+ {t.kind = 32; break;}
case 42:
if (ch == 'n') {AddCh(); goto case 43;}
else {goto case 0;}
@@ -734,9 +734,9 @@ public class Scanner {
{
tlen -= apx;
SetScannerBehindT();
- t.kind = 32; break;}
+ t.kind = 33; break;}
case 45:
- {t.kind = 33; break;}
+ {t.kind = 34; break;}
case 46:
recEnd = pos; recKind = 2;
if (ch >= '0' && ch <= '9') {AddCh(); goto case 46;}
@@ -886,39 +886,39 @@ public class Scanner {
if (ch == '|') {AddCh(); goto case 81;}
else {t.kind = 10; break;}
case 91:
- recEnd = pos; recKind = 40;
- if (ch == '>') {AddCh(); goto case 33;}
- else if (ch == '=') {AddCh(); goto case 97;}
- else {t.kind = 40; break;}
+ recEnd = pos; recKind = 13;
+ if (ch == '.') {AddCh(); goto case 97;}
+ else {t.kind = 13; break;}
case 92:
+ recEnd = pos; recKind = 41;
+ if (ch == '>') {AddCh(); goto case 33;}
+ else if (ch == '=') {AddCh(); goto case 98;}
+ else {t.kind = 41; break;}
+ case 93:
recEnd = pos; recKind = 122;
if (ch == '>') {AddCh(); goto case 34;}
else {t.kind = 122; break;}
- case 93:
+ case 94:
recEnd = pos; recKind = 115;
if (ch == 'i') {AddCh(); goto case 42;}
else if (ch == '=') {AddCh(); goto case 69;}
else {t.kind = 115; break;}
- case 94:
- recEnd = pos; recKind = 77;
- if (ch == '.') {AddCh(); goto case 98;}
- else {t.kind = 77; break;}
case 95:
- recEnd = pos; recKind = 57;
+ recEnd = pos; recKind = 58;
if (ch == '=') {AddCh(); goto case 99;}
- else {t.kind = 57; break;}
+ else {t.kind = 58; break;}
case 96:
- recEnd = pos; recKind = 58;
+ recEnd = pos; recKind = 59;
if (ch == '=') {AddCh(); goto case 68;}
- else {t.kind = 58; break;}
+ else {t.kind = 59; break;}
case 97:
- recEnd = pos; recKind = 53;
- if (ch == '>') {AddCh(); goto case 75;}
- else {t.kind = 53; break;}
- case 98:
recEnd = pos; recKind = 132;
if (ch == '.') {AddCh(); goto case 45;}
else {t.kind = 132; break;}
+ case 98:
+ recEnd = pos; recKind = 54;
+ if (ch == '>') {AddCh(); goto case 75;}
+ else {t.kind = 54; break;}
case 99:
recEnd = pos; recKind = 99;
if (ch == '=') {AddCh(); goto case 100;}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3ce7dad5..f19fa0da 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -10476,7 +10476,7 @@ namespace Microsoft.Dafny {
var mem = recv as MemberSelectExpr;
var fn = mem == null ? null : mem.Member as Function;
if (fn != null) {
- return TrExpr(new FunctionCallExpr(e.tok, fn.Name, mem.Obj, e.OpenParen, e.Args) {
+ return TrExpr(new FunctionCallExpr(e.tok, fn.Name, mem.Obj, e.tok, e.Args) {
Function = fn,
Type = e.Type,
TypeArgumentSubstitutions = Util.Dict(GetTypeParams(fn), mem.TypeApplication)
@@ -13066,7 +13066,7 @@ namespace Microsoft.Dafny {
ApplyExpr e = (ApplyExpr)expr;
Expression fn = Substitute(e.Function);
List<Expression> args = SubstituteExprList(e.Args);
- newExpr = new ApplyExpr(e.tok, e.OpenParen, fn, args);
+ newExpr = new ApplyExpr(e.tok, fn, args);
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
diff --git a/Test/dafny0/Backticks.dfy.expect b/Test/dafny0/Backticks.dfy.expect
index 82fc2933..ab2bbc52 100644
--- a/Test/dafny0/Backticks.dfy.expect
+++ b/Test/dafny0/Backticks.dfy.expect
@@ -3,7 +3,7 @@ Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Backticks.dfy(77,7): Error: call may violate context's modifies clause
+Backticks.dfy(77,8): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
diff --git a/Test/dafny0/CallStmtTests.dfy.expect b/Test/dafny0/CallStmtTests.dfy.expect
index 57a33c62..8a334754 100644
--- a/Test/dafny0/CallStmtTests.dfy.expect
+++ b/Test/dafny0/CallStmtTests.dfy.expect
@@ -1,3 +1,3 @@
CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable
-CallStmtTests.dfy(17,8): Error: actual out-parameter 0 is required to be a ghost variable
+CallStmtTests.dfy(17,10): Error: actual out-parameter 0 is required to be a ghost variable
2 resolution/type errors detected in CallStmtTests.dfy
diff --git a/Test/dafny0/CoPrefix.dfy.expect b/Test/dafny0/CoPrefix.dfy.expect
index c2453a09..c92a09c1 100644
--- a/Test/dafny0/CoPrefix.dfy.expect
+++ b/Test/dafny0/CoPrefix.dfy.expect
@@ -8,17 +8,17 @@ CoPrefix.dfy(168,15): Related location: This is the postcondition that might not
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-CoPrefix.dfy(176,5): Error: cannot prove termination; try supplying a decreases clause
+CoPrefix.dfy(176,11): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoPrefix.dfy(63,7): Error: failure to decrease termination measure
+CoPrefix.dfy(63,57): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon7_Then
(0,0): anon8_Else
(0,0): anon9_Then
-CoPrefix.dfy(76,7): Error: cannot prove termination; try supplying a decreases clause
+CoPrefix.dfy(76,56): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon7_Then
diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect
index 9acb5a58..45d1e598 100644
--- a/Test/dafny0/CoResolution.dfy.expect
+++ b/Test/dafny0/CoResolution.dfy.expect
@@ -7,19 +7,19 @@ CoResolution.dfy(67,10): Error: a copredicate is not allowed to declare any read
CoResolution.dfy(73,31): Error: a copredicate is not allowed to declare any ensures clause
CoResolution.dfy(82,20): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(86,20): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(95,4): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(95,5): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(109,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(110,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(115,17): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(121,17): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(115,24): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(121,28): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(129,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(130,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(135,17): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(141,17): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(135,26): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(141,30): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(202,12): Error: type variable '_T0' in the function call to 'A' could not be determined
-CoResolution.dfy(202,12): Error: the type of this expression is underspecified
+CoResolution.dfy(202,13): Error: the type of this expression is underspecified
CoResolution.dfy(202,19): Error: type variable '_T0' in the function call to 'S' could not be determined
24 resolution/type errors detected in CoResolution.dfy
diff --git a/Test/dafny0/Coinductive.dfy.expect b/Test/dafny0/Coinductive.dfy.expect
index ce3e3a8d..26fec211 100644
--- a/Test/dafny0/Coinductive.dfy.expect
+++ b/Test/dafny0/Coinductive.dfy.expect
@@ -13,5 +13,5 @@ Coinductive.dfy(106,17): Error: a copredicate can be called recursively only in
Coinductive.dfy(116,24): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
Coinductive.dfy(122,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
Coinductive.dfy(123,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
-Coinductive.dfy(148,5): Error: a recursive call from a copredicate can go only to other copredicates
+Coinductive.dfy(148,21): Error: a recursive call from a copredicate can go only to other copredicates
16 resolution/type errors detected in Coinductive.dfy
diff --git a/Test/dafny0/DatatypeUpdate.dfy b/Test/dafny0/DatatypeUpdate.dfy
index 7869fba3..f39aa4ce 100644
--- a/Test/dafny0/DatatypeUpdate.dfy
+++ b/Test/dafny0/DatatypeUpdate.dfy
@@ -28,3 +28,10 @@ function F(d: Dt): Dt
{
d[x := 5]
}
+
+datatype NumericNames = NumNam(010: int)
+
+method UpdateNumNam(nn: NumericNames, y: int) returns (pp: NumericNames)
+{
+ pp := nn[010 := y]; // not to be confused with a field name 10
+}
diff --git a/Test/dafny0/DatatypeUpdate.dfy.expect b/Test/dafny0/DatatypeUpdate.dfy.expect
index 52595bf9..790f6509 100644
--- a/Test/dafny0/DatatypeUpdate.dfy.expect
+++ b/Test/dafny0/DatatypeUpdate.dfy.expect
@@ -1,2 +1,2 @@
-Dafny program verifier finished with 3 verified, 0 errors
+Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/dafny0/Datatypes.dfy.expect b/Test/dafny0/Datatypes.dfy.expect
index f6b51252..874df45e 100644
--- a/Test/dafny0/Datatypes.dfy.expect
+++ b/Test/dafny0/Datatypes.dfy.expect
@@ -47,11 +47,11 @@ Execution trace:
(0,0): anon23_Then
(0,0): anon24_Else
(0,0): anon25_Then
-Datatypes.dfy(170,14): Error: assertion violation
+Datatypes.dfy(170,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
-Datatypes.dfy(172,14): Error: assertion violation
+Datatypes.dfy(172,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else
diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect
index f296ed4b..9f277582 100644
--- a/Test/dafny0/EqualityTypes.dfy.expect
+++ b/Test/dafny0/EqualityTypes.dfy.expect
@@ -5,7 +5,7 @@ EqualityTypes.dfy(41,8): Error: opaque type 'Y' is not allowed to be replaced by
EqualityTypes.dfy(45,11): Error: type 'X' is used to refine an opaque type with equality support, but 'X' does not support equality
EqualityTypes.dfy(46,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality
EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)
-EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0) (perhaps try declaring type parameter '_T0' on line 81 as '_T0(==)', which says it can only be instantiated with a type that supports equality)
+EqualityTypes.dfy(85,9): Error: type parameter 0 (T) passed to method M must support equality (got _T0) (perhaps try declaring type parameter '_T0' on line 81 as '_T0(==)', which says it can only be instantiated with a type that supports equality)
EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D)
EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D)
EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D)
@@ -26,10 +26,10 @@ EqualityTypes.dfy(210,8): Error: set argument type must support equality (got Co
EqualityTypes.dfy(211,20): Error: set argument type must support equality (got Co)
EqualityTypes.dfy(211,29): Error: set argument type must support equality (got Co)
EqualityTypes.dfy(212,17): Error: set argument type must support equality (got Co)
-EqualityTypes.dfy(233,4): Error: type parameter 0 (A) passed to method Explicit must support equality (got Co)
+EqualityTypes.dfy(233,12): Error: type parameter 0 (A) passed to method Explicit must support equality (got Co)
EqualityTypes.dfy(233,13): Error: set argument type must support equality (got Co)
EqualityTypes.dfy(234,19): Error: set argument type must support equality (got Co)
-EqualityTypes.dfy(236,4): Error: type parameter 0 (A) passed to method InferEqualitySupportIsRequired must support equality (got Co)
+EqualityTypes.dfy(236,34): Error: type parameter 0 (A) passed to method InferEqualitySupportIsRequired must support equality (got Co)
EqualityTypes.dfy(236,35): Error: set argument type must support equality (got Co)
EqualityTypes.dfy(238,24): Error: set argument type must support equality (got Co)
EqualityTypes.dfy(239,21): Error: multiset argument type must support equality (got Co)
diff --git a/Test/dafny0/FunctionSpecifications.dfy.expect b/Test/dafny0/FunctionSpecifications.dfy.expect
index e7df68f7..4b9aa202 100644
--- a/Test/dafny0/FunctionSpecifications.dfy.expect
+++ b/Test/dafny0/FunctionSpecifications.dfy.expect
@@ -41,7 +41,7 @@ FunctionSpecifications.dfy(158,3): Error: cannot prove termination; try supplyin
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-FunctionSpecifications.dfy(167,3): Error: cannot prove termination; try supplying a decreases clause
+FunctionSpecifications.dfy(167,11): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon3_Else
diff --git a/Test/dafny0/Iterators.dfy.expect b/Test/dafny0/Iterators.dfy.expect
index 0087691b..f0c6e400 100644
--- a/Test/dafny0/Iterators.dfy.expect
+++ b/Test/dafny0/Iterators.dfy.expect
@@ -1,38 +1,38 @@
-Iterators.dfy(251,9): Error: failure to decrease termination measure
+Iterators.dfy(251,10): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(274,9): Error: failure to decrease termination measure
+Iterators.dfy(274,10): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(284,24): Error: failure to decrease termination measure
+Iterators.dfy(284,32): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
-Iterators.dfy(296,9): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(296,10): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(317,9): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(317,10): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(326,24): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(326,32): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
-Iterators.dfy(343,9): Error: failure to decrease termination measure
+Iterators.dfy(343,10): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(353,24): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(353,32): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
-Iterators.dfy(370,9): Error: failure to decrease termination measure
+Iterators.dfy(370,10): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
@@ -65,7 +65,7 @@ Execution trace:
Iterators.dfy(197,3): anon17_Else
Iterators.dfy(197,3): anon19_Else
(0,0): anon21_Then
-Iterators.dfy(40,14): Error BP5002: A precondition for this call might not hold.
+Iterators.dfy(40,22): Error BP5002: A precondition for this call might not hold.
Iterators.dfy(4,10): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
@@ -85,13 +85,13 @@ Iterators.dfy(150,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Iterators.dfy(155,16): Error BP5002: A precondition for this call might not hold.
+Iterators.dfy(155,24): Error BP5002: A precondition for this call might not hold.
Iterators.dfy(125,10): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Iterators.dfy(234,14): Error: assertion violation
+Iterators.dfy(234,21): Error: assertion violation
Execution trace:
(0,0): anon0
Iterators.dfy(225,3): anon14_LoopHead
diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect
index e50dc797..90436ed8 100644
--- a/Test/dafny0/Modules0.dfy.expect
+++ b/Test/dafny0/Modules0.dfy.expect
@@ -8,11 +8,11 @@ Modules0.dfy(56,21): Error: Undeclared top-level type or type parameter: MyClass
Modules0.dfy(57,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
Modules0.dfy(68,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
Modules0.dfy(76,9): Error: type MyClass1 does not have a member Down
-Modules0.dfy(76,6): Error: expected method call, found expression
+Modules0.dfy(76,13): Error: expected method call, found expression
Modules0.dfy(79,9): Error: type MyClass0 does not have a member Down
-Modules0.dfy(79,6): Error: expected method call, found expression
+Modules0.dfy(79,13): Error: expected method call, found expression
Modules0.dfy(84,8): Error: type MyClassY does not have a member M
-Modules0.dfy(84,6): Error: expected method call, found expression
+Modules0.dfy(84,9): Error: expected method call, found expression
Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)
Modules0.dfy(224,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
Modules0.dfy(224,8): Error: new can be applied only to reference types (got X)
@@ -23,12 +23,12 @@ Modules0.dfy(283,19): Error: Undeclared top-level type or type parameter: D (did
Modules0.dfy(283,12): Error: new can be applied only to reference types (got D)
Modules0.dfy(286,25): Error: type of the receiver is not fully determined at this program point
Modules0.dfy(287,16): Error: type of the receiver is not fully determined at this program point
-Modules0.dfy(287,6): Error: expected method call, found expression
+Modules0.dfy(287,17): Error: expected method call, found expression
Modules0.dfy(288,16): Error: type of the receiver is not fully determined at this program point
-Modules0.dfy(288,6): Error: expected method call, found expression
+Modules0.dfy(288,17): Error: expected method call, found expression
Modules0.dfy(310,24): Error: module Q_Imp does not exist
Modules0.dfy(102,6): Error: type MyClassY does not have a member M
-Modules0.dfy(102,4): Error: expected method call, found expression
+Modules0.dfy(102,7): Error: expected method call, found expression
Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts
Modules0.dfy(141,11): Error: old expressions are allowed only in specification and ghost contexts
Modules0.dfy(142,11): Error: fresh expressions are allowed only in specification and ghost contexts
diff --git a/Test/dafny0/Modules1.dfy.expect b/Test/dafny0/Modules1.dfy.expect
index b269e3b2..342b5808 100644
--- a/Test/dafny0/Modules1.dfy.expect
+++ b/Test/dafny0/Modules1.dfy.expect
@@ -10,11 +10,11 @@ Modules1.dfy(94,18): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-Modules1.dfy(56,3): Error: decreases expression must be bounded below by 0
+Modules1.dfy(56,9): Error: decreases expression must be bounded below by 0
Modules1.dfy(54,13): Related location
Execution trace:
(0,0): anon0
-Modules1.dfy(62,3): Error: failure to decrease termination measure
+Modules1.dfy(62,9): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/NatTypes.dfy.expect b/Test/dafny0/NatTypes.dfy.expect
index b0613150..7bee017c 100644
--- a/Test/dafny0/NatTypes.dfy.expect
+++ b/Test/dafny0/NatTypes.dfy.expect
@@ -25,7 +25,7 @@ Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
-NatTypes.dfy(92,19): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(92,22): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
@@ -35,7 +35,7 @@ Execution trace:
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
-NatTypes.dfy(130,21): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(130,35): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
diff --git a/Test/dafny0/NewtypesResolution.dfy.expect b/Test/dafny0/NewtypesResolution.dfy.expect
index bb1624f9..28b745c5 100644
--- a/Test/dafny0/NewtypesResolution.dfy.expect
+++ b/Test/dafny0/NewtypesResolution.dfy.expect
@@ -14,14 +14,14 @@ NewtypesResolution.dfy(91,31): Error: old expressions are not allowed in this co
NewtypesResolution.dfy(101,24): Error: Wrong number of type arguments (1 instead of 0) passed to newtype: N
NewtypesResolution.dfy(105,10): Error: recursive dependency involving a newtype: _default.BadLemma -> Cycle
NewtypesResolution.dfy(114,10): Error: recursive dependency involving a newtype: SelfCycle -> SelfCycle
-NewtypesResolution.dfy(120,21): Error: name of type ('N9') is used as a variable
+NewtypesResolution.dfy(120,21): Error: name of type (N9) is used as a variable
NewtypesResolution.dfy(139,6): Error: RHS (of type int) not assignable to LHS (of type Int)
NewtypesResolution.dfy(140,6): Error: RHS (of type AnotherInt) not assignable to LHS (of type Int)
-NewtypesResolution.dfy(156,9): Error: name of type ('B') is used as a variable
-NewtypesResolution.dfy(157,11): Error: name of type ('Syn') is used as a variable
-NewtypesResolution.dfy(162,8): Error: member U does not exist in class Klass
-NewtypesResolution.dfy(162,4): Error: expected method call, found expression
-NewtypesResolution.dfy(188,39): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)
+NewtypesResolution.dfy(156,9): Error: name of type (B) is used as a variable
+NewtypesResolution.dfy(157,11): Error: name of type (Syn) is used as a variable
+NewtypesResolution.dfy(162,8): Error: member 'U' does not exist in type 'Y'
+NewtypesResolution.dfy(162,9): Error: expected method call, found expression
+NewtypesResolution.dfy(188,60): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)
NewtypesResolution.dfy(219,11): Error: new must use an integer-based expression for the array size (got real for index 2)
NewtypesResolution.dfy(221,13): Error: arguments to < must have the same type (got Even and nat)
NewtypesResolution.dfy(223,13): Error: arguments to < must have the same type (got Even and int)
diff --git a/Test/dafny0/OpaqueFunctions.dfy.expect b/Test/dafny0/OpaqueFunctions.dfy.expect
index df076f60..3aa09714 100644
--- a/Test/dafny0/OpaqueFunctions.dfy.expect
+++ b/Test/dafny0/OpaqueFunctions.dfy.expect
@@ -1,30 +1,30 @@
OpaqueFunctions.dfy(27,16): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(52,7): Error BP5002: A precondition for this call might not hold.
+OpaqueFunctions.dfy(52,8): Error BP5002: A precondition for this call might not hold.
OpaqueFunctions.dfy(24,16): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
OpaqueFunctions.dfy(58,20): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(60,14): Error: assertion violation
+OpaqueFunctions.dfy(60,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
-OpaqueFunctions.dfy(63,14): Error: assertion violation
+OpaqueFunctions.dfy(63,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-OpaqueFunctions.dfy(66,14): Error: assertion violation
+OpaqueFunctions.dfy(66,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-OpaqueFunctions.dfy(77,14): Error: assertion violation
+OpaqueFunctions.dfy(77,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-OpaqueFunctions.dfy(79,9): Error BP5002: A precondition for this call might not hold.
+OpaqueFunctions.dfy(79,10): Error BP5002: A precondition for this call might not hold.
OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
@@ -32,23 +32,23 @@ Execution trace:
OpaqueFunctions.dfy(86,20): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(88,14): Error: assertion violation
+OpaqueFunctions.dfy(88,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
-OpaqueFunctions.dfy(91,14): Error: assertion violation
+OpaqueFunctions.dfy(91,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-OpaqueFunctions.dfy(94,14): Error: assertion violation
+OpaqueFunctions.dfy(94,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-OpaqueFunctions.dfy(105,14): Error: assertion violation
+OpaqueFunctions.dfy(105,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-OpaqueFunctions.dfy(107,9): Error BP5002: A precondition for this call might not hold.
+OpaqueFunctions.dfy(107,10): Error BP5002: A precondition for this call might not hold.
OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
@@ -56,19 +56,19 @@ Execution trace:
OpaqueFunctions.dfy(114,20): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(116,14): Error: assertion violation
+OpaqueFunctions.dfy(116,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
-OpaqueFunctions.dfy(119,14): Error: assertion violation
+OpaqueFunctions.dfy(119,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-OpaqueFunctions.dfy(122,14): Error: assertion violation
+OpaqueFunctions.dfy(122,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-OpaqueFunctions.dfy(138,12): Error: assertion violation
+OpaqueFunctions.dfy(138,13): Error: assertion violation
Execution trace:
(0,0): anon0
OpaqueFunctions.dfy(202,12): Error: assertion violation
diff --git a/Test/dafny0/Parallel.dfy.expect b/Test/dafny0/Parallel.dfy.expect
index c994cd39..6b726cd5 100644
--- a/Test/dafny0/Parallel.dfy.expect
+++ b/Test/dafny0/Parallel.dfy.expect
@@ -1,4 +1,4 @@
-Parallel.dfy(34,5): Error BP5002: A precondition for this call might not hold.
+Parallel.dfy(34,10): Error BP5002: A precondition for this call might not hold.
Parallel.dfy(60,14): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
@@ -60,7 +60,7 @@ Execution trace:
(0,0): anon19_Then
(0,0): anon20_Then
(0,0): anon5
-Parallel.dfy(296,10): Error: assertion violation
+Parallel.dfy(296,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else
diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect
index 78a43ed9..7305bfce 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy.expect
+++ b/Test/dafny0/ParallelResolveErrors.dfy.expect
@@ -7,8 +7,8 @@ ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost con
ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(63,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(64,13): Error: new allocation not allowed in ghost context
-ParallelResolveErrors.dfy(65,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
-ParallelResolveErrors.dfy(66,6): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods
+ParallelResolveErrors.dfy(65,22): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(66,20): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods
ParallelResolveErrors.dfy(73,19): Error: trying to break out of more loop levels than there are enclosing loops
ParallelResolveErrors.dfy(77,18): Error: return statement is not allowed inside a forall statement
ParallelResolveErrors.dfy(84,21): Error: trying to break out of more loop levels than there are enclosing loops
@@ -17,6 +17,6 @@ ParallelResolveErrors.dfy(86,20): Error: break label is undefined or not in scop
ParallelResolveErrors.dfy(95,24): Error: trying to break out of more loop levels than there are enclosing loops
ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scope: OutsideLoop
ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations
-ParallelResolveErrors.dfy(115,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
-ParallelResolveErrors.dfy(120,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(115,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(120,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
21 resolution/type errors detected in ParallelResolveErrors.dfy
diff --git a/Test/dafny0/RealCompare.dfy.expect b/Test/dafny0/RealCompare.dfy.expect
index e0f70fc0..5b25fa25 100644
--- a/Test/dafny0/RealCompare.dfy.expect
+++ b/Test/dafny0/RealCompare.dfy.expect
@@ -1,8 +1,8 @@
-RealCompare.dfy(35,5): Error: failure to decrease termination measure
+RealCompare.dfy(35,6): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-RealCompare.dfy(50,3): Error: decreases expression must be bounded below by 0.0
+RealCompare.dfy(50,4): Error: decreases expression must be bounded below by 0.0
RealCompare.dfy(48,13): Related location
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index bb51b01f..2f340557 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -95,8 +95,8 @@ method TestNameResolution1() {
// parameters match the signature of only one of those constructors)
var d3 := Abc.David(20, 40); // error: wrong number of parameters
var d4 := Rst.David(20, 40);
- var e := Eleanor;
- assert Tuv(e, this.Eleanor) == 10;
+ var e := Eleanor; // this resolves to the field, not the Abc datatype constructor
+ assert Tuv(Abc.Eleanor, e) == 10;
}
// --------------- ghost tests -------------------------------------
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 7789c6f8..9ba6a1b3 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -16,27 +16,27 @@ ResolutionErrors.dfy(608,15): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(608,15): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(619,20): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(621,8): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(619,29): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(621,17): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(639,21): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(676,8): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(686,8): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(676,18): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(686,22): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(689,20): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(700,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(700,16): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(701,21): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(702,8): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(702,18): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(705,19): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(724,8): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(724,22): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(727,20): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(732,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(732,16): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(733,21): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(734,8): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(734,9): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(737,19): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(762,4): Error: calls to methods with side-effects are not allowed inside a statement expression
-ResolutionErrors.dfy(763,4): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(764,4): Error: wrong number of method result arguments (got 0, expected 1)
+ResolutionErrors.dfy(762,17): Error: calls to methods with side-effects are not allowed inside a statement expression
+ResolutionErrors.dfy(763,18): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(764,18): Error: wrong number of method result arguments (got 0, expected 1)
ResolutionErrors.dfy(775,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(785,4): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(796,36): Error: ghost variables are allowed only in specification contexts
@@ -92,13 +92,13 @@ ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(112,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(116,11): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(117,9): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(117,10): Error: actual out-parameter 0 is required to be a ghost variable
ResolutionErrors.dfy(124,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(128,23): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(135,4): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(139,21): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(140,35): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(149,9): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(149,10): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(155,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(196,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
ResolutionErrors.dfy(219,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
@@ -124,32 +124,31 @@ ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)
ResolutionErrors.dfy(26,11): Error: array selection requires an array4 (got array<T>)
-ResolutionErrors.dfy(56,14): Error: a field must be selected via an object, not just a class name
+ResolutionErrors.dfy(56,14): Error: accessing member 'X' requires an instance expression
ResolutionErrors.dfy(57,7): Error: unresolved identifier: F
-ResolutionErrors.dfy(58,14): Error: an instance function must be selected via an object, not just a class name
-ResolutionErrors.dfy(58,7): Error: call to instance function requires an instance
+ResolutionErrors.dfy(58,14): Error: accessing member 'F' requires an instance expression
ResolutionErrors.dfy(59,7): Error: unresolved identifier: G
ResolutionErrors.dfy(61,7): Error: unresolved identifier: M
-ResolutionErrors.dfy(62,7): Error: call to instance method requires an instance
+ResolutionErrors.dfy(62,14): Error: accessing member 'M' requires an instance expression
ResolutionErrors.dfy(63,7): Error: unresolved identifier: N
-ResolutionErrors.dfy(66,8): Error: non-function expression is called with parameters
-ResolutionErrors.dfy(67,14): Error: member z does not exist in class Global
+ResolutionErrors.dfy(66,8): Error: non-function expression (of type int) is called with parameters
+ResolutionErrors.dfy(67,14): Error: member 'z' does not exist in type 'Global'
ResolutionErrors.dfy(86,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
ResolutionErrors.dfy(91,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(94,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(96,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
+ResolutionErrors.dfy(96,16): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
ResolutionErrors.dfy(258,4): Error: label shadows an enclosing label
ResolutionErrors.dfy(263,2): Error: duplicate label
ResolutionErrors.dfy(289,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
ResolutionErrors.dfy(290,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(292,4): Error: a constructor is allowed to be called only when an object is being allocated
+ResolutionErrors.dfy(292,9): Error: a constructor is allowed to be called only when an object is being allocated
ResolutionErrors.dfy(306,16): Error: arguments must have the same type (got int and DTD_List)
ResolutionErrors.dfy(307,16): Error: arguments must have the same type (got DTD_List and int)
ResolutionErrors.dfy(308,25): Error: arguments must have the same type (got bool and int)
ResolutionErrors.dfy(311,18): Error: ghost fields are allowed only in specification contexts
ResolutionErrors.dfy(320,15): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(345,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
+ResolutionErrors.dfy(345,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(357,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
ResolutionErrors.dfy(365,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
ResolutionErrors.dfy(370,6): Error: all lines in a calculation must have the same type (got int after bool)
@@ -160,7 +159,7 @@ ResolutionErrors.dfy(374,10): Error: second argument to ==> must be of type bool
ResolutionErrors.dfy(379,10): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(379,10): Error: second argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(384,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ResolutionErrors.dfy(406,6): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(406,9): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(408,12): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(410,8): Error: a hint is not allowed to update a variable declared outside the hint
ResolutionErrors.dfy(467,7): Error: ghost variables are allowed only in specification contexts
@@ -174,14 +173,13 @@ ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies cla
ResolutionErrors.dfy(913,9): Error: unresolved identifier: s
ResolutionErrors.dfy(924,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
ResolutionErrors.dfy(925,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
-ResolutionErrors.dfy(931,9): Error: condition is expected to be of type bool, but is int
+ResolutionErrors.dfy(931,16): Error: condition is expected to be of type bool, but is int
ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3
ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2
-ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int))
ResolutionErrors.dfy(955,15): Error: arguments to / must have the same type (got real and int)
ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (instead got real)
ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)
-ResolutionErrors.dfy(1129,2): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(1129,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
ResolutionErrors.dfy(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-186 resolution/type errors detected in ResolutionErrors.dfy
+184 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/ReturnErrors.dfy.expect b/Test/dafny0/ReturnErrors.dfy.expect
index a2b9d86d..3f43c226 100644
--- a/Test/dafny0/ReturnErrors.dfy.expect
+++ b/Test/dafny0/ReturnErrors.dfy.expect
@@ -1,4 +1,4 @@
-ReturnErrors.dfy(32,10): Error: cannot have method call in return statement.
-ReturnErrors.dfy(38,10): Error: cannot have effectful parameter in multi-return statement.
+ReturnErrors.dfy(32,11): Error: cannot have method call in return statement.
+ReturnErrors.dfy(38,11): Error: cannot have effectful parameter in multi-return statement.
ReturnErrors.dfy(43,10): Error: can only have initialization methods which modify at most 'this'.
3 resolution/type errors detected in ReturnErrors.dfy
diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index 824ad991..1983d2ac 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -24,16 +24,16 @@ Execution trace:
SmallTests.dfy(84,5): anon8_LoopHead
(0,0): anon8_LoopBody
(0,0): anon9_Then
-SmallTests.dfy(119,5): Error: call may violate context's modifies clause
+SmallTests.dfy(119,6): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
(0,0): anon3
-SmallTests.dfy(132,9): Error: call may violate context's modifies clause
+SmallTests.dfy(132,10): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-SmallTests.dfy(134,9): Error: call may violate context's modifies clause
+SmallTests.dfy(134,10): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Else
@@ -174,7 +174,7 @@ Execution trace:
SmallTests.dfy(621,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
-SmallTests.dfy(644,10): Error: assertion violation
+SmallTests.dfy(644,23): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon8_Then
diff --git a/Test/dafny0/StatementExpressions.dfy.expect b/Test/dafny0/StatementExpressions.dfy.expect
index 3f50d6d9..313c8884 100644
--- a/Test/dafny0/StatementExpressions.dfy.expect
+++ b/Test/dafny0/StatementExpressions.dfy.expect
@@ -1,4 +1,4 @@
-StatementExpressions.dfy(55,11): Error: cannot prove termination; try supplying a decreases clause
+StatementExpressions.dfy(55,12): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon6_Then
@@ -16,7 +16,7 @@ StatementExpressions.dfy(88,5): Error: value assigned to a nat must be non-negat
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-StatementExpressions.dfy(98,11): Error: cannot prove termination; try supplying a decreases clause
+StatementExpressions.dfy(98,18): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon6_Then
diff --git a/Test/dafny0/TailCalls.dfy.expect b/Test/dafny0/TailCalls.dfy.expect
index dc1eec5b..5c63112a 100644
--- a/Test/dafny0/TailCalls.dfy.expect
+++ b/Test/dafny0/TailCalls.dfy.expect
@@ -1,4 +1,4 @@
-TailCalls.dfy(21,15): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code
+TailCalls.dfy(21,16): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code
TailCalls.dfy(38,24): Error: sorry, tail-call optimizations are not supported for mutually recursive methods
TailCalls.dfy(43,24): Error: sorry, tail-call optimizations are not supported for mutually recursive methods
3 resolution/type errors detected in TailCalls.dfy
diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect
index ef8ee72e..fd86c8cb 100644
--- a/Test/dafny0/Termination.dfy.expect
+++ b/Test/dafny0/Termination.dfy.expect
@@ -1,4 +1,4 @@
-Termination.dfy[TerminationRefinement1](440,5): Error: failure to decrease termination measure
+Termination.dfy[TerminationRefinement1](440,6): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
Termination.dfy(360,47): Error: failure to decrease termination measure
diff --git a/Test/dafny0/Trait/TraitExtend.dfy.expect b/Test/dafny0/Trait/TraitExtend.dfy.expect
index 73a24ad8..2051fd81 100644
--- a/Test/dafny0/Trait/TraitExtend.dfy.expect
+++ b/Test/dafny0/Trait/TraitExtend.dfy.expect
@@ -1,3 +1,3 @@
-TraitExtend.dfy(40,20): Error: wrong number of function arguments (got 2, expected 3)
-TraitExtend.dfy(41,20): Error: wrong number of function arguments (got 3, expected 2)
+TraitExtend.dfy(40,24): Error: wrong number of arguments to function application (function 'Mul' expects 3, got 2)
+TraitExtend.dfy(41,24): Error: wrong number of arguments to function application (function 'Plus' expects 2, got 3)
2 resolution/type errors detected in TraitExtend.dfy
diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect
index 55fc916c..0a15ad67 100644
--- a/Test/dafny0/TypeTests.dfy.expect
+++ b/Test/dafny0/TypeTests.dfy.expect
@@ -1,13 +1,13 @@
TypeTests.dfy(156,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
TypeTests.dfy(162,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
TypeTests.dfy(169,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
-TypeTests.dfy(7,13): Error: incorrect type of function argument 0 (expected C, got D)
-TypeTests.dfy(7,13): Error: incorrect type of function argument 1 (expected D, got C)
-TypeTests.dfy(8,13): Error: incorrect type of function argument 0 (expected C, got int)
-TypeTests.dfy(8,13): Error: incorrect type of function argument 1 (expected D, got int)
-TypeTests.dfy(14,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
-TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
-TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
+TypeTests.dfy(7,17): Error: type mismatch for argument 0 (function expects C, got D)
+TypeTests.dfy(7,20): Error: type mismatch for argument 1 (function expects D, got C)
+TypeTests.dfy(8,15): Error: type mismatch for argument 0 (function expects C, got int)
+TypeTests.dfy(8,18): Error: type mismatch for argument 1 (function expects D, got int)
+TypeTests.dfy(14,16): Error: incorrect type of method in-parameter 0 (expected int, got bool)
+TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 0 (expected int, got C)
+TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 1 (expected C, got int)
TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
TypeTests.dfy(56,6): Error: Duplicate local-variable name: z
TypeTests.dfy(58,6): Error: Duplicate local-variable name: x
diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
index eedfce29..b37633ae 100644
--- a/Test/dafny0/snapshots/runtest.snapshot.expect
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -1,14 +1,14 @@
-------------------- Snapshots0.dfy --------------------
-Processing command (at Snapshots0.v0.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
Dafny program verifier finished with 3 verified, 0 errors
-Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,3)):
+Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,6)):
>>> added after: a##post##0 := a##post##0 && true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call1old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call1old#AT#$Heap, $o, $f)) && $HeapSucc(call1old#AT#$Heap, $Heap);
-Processing command (at Snapshots0.v1.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at <unknown location>) a##post##0 := a##post##0 && true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call1old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call1old#AT#$Heap, $o, $f)) && $HeapSucc(call1old#AT#$Heap, $Heap);
>>> AssumeNegationOfAssumptionVariable
@@ -21,7 +21,7 @@ Execution trace:
Dafny program verifier finished with 2 verified, 1 error
-------------------- Snapshots1.dfy --------------------
-Processing command (at Snapshots1.v0.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
@@ -29,11 +29,11 @@ Processing command (at Snapshots1.v0.dfy(12,3)) assert true;
>>> DoNothingToAssert
Dafny program verifier finished with 4 verified, 0 errors
-Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,3)):
+Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,4)):
>>> added after: a##post##0 := a##post##0 && false;
Processing command (at Snapshots1.v1.dfy(12,3)) assert true;
>>> MarkAsFullyVerified
-Processing command (at Snapshots1.v1.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
@@ -44,7 +44,7 @@ Execution trace:
Dafny program verifier finished with 3 verified, 1 error
-------------------- Snapshots2.dfy --------------------
-Processing command (at Snapshots2.v0.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
@@ -60,11 +60,11 @@ Processing command (at Snapshots2.v0.dfy(18,3)) assert true;
>>> DoNothingToAssert
Dafny program verifier finished with 6 verified, 0 errors
-Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots2.v1.dfy(3,3)):
+Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots2.v1.dfy(3,4)):
>>> added after: a##post##0 := a##post##0 && false;
Processing command (at Snapshots2.v1.dfy(18,3)) assert true;
>>> MarkAsFullyVerified
-Processing command (at Snapshots2.v1.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
@@ -125,11 +125,11 @@ Execution trace:
Dafny program verifier finished with 1 verified, 2 errors
-------------------- Snapshots5.dfy --------------------
-Processing command (at Snapshots5.v0.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
>>> DoNothingToAssert
-Processing command (at Snapshots5.v0.dfy(12,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots5.v0.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;
>>> DoNothingToAssert
@@ -137,11 +137,11 @@ Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: tru
>>> DoNothingToAssert
Dafny program verifier finished with 3 verified, 0 errors
-Processing command (at Snapshots5.v1.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
>>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(12,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots5.v1.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;
>>> MarkAsFullyVerified
diff --git a/Test/dafny2/SnapshotableTrees.dfy.expect b/Test/dafny2/SnapshotableTrees.dfy.expect
index d84bdc45..849b9e38 100644
--- a/Test/dafny2/SnapshotableTrees.dfy.expect
+++ b/Test/dafny2/SnapshotableTrees.dfy.expect
@@ -1,4 +1,4 @@
-SnapshotableTrees.dfy(68,16): Error BP5002: A precondition for this call might not hold.
+SnapshotableTrees.dfy(68,24): Error BP5002: A precondition for this call might not hold.
SnapshotableTrees.dfy(648,16): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
diff --git a/Test/hofs/Field.dfy.expect b/Test/hofs/Field.dfy.expect
index 927d8b06..9f6998f5 100644
--- a/Test/hofs/Field.dfy.expect
+++ b/Test/hofs/Field.dfy.expect
@@ -1,14 +1,14 @@
-Field.dfy(12,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
Field.dfy(12,12): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Field.dfy(21,10): Error: assertion violation
+Field.dfy(12,15): Error: assertion violation
Execution trace:
(0,0): anon0
Field.dfy(21,12): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
+Field.dfy(21,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
Dafny program verifier finished with 2 verified, 4 errors
diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect
index 2cf19369..c3e0c242 100644
--- a/Test/hofs/ResolveError.dfy.expect
+++ b/Test/hofs/ResolveError.dfy.expect
@@ -1,5 +1,5 @@
ResolveError.dfy(86,6): Error: RHS (of type ((int,bool)) -> real) not assignable to LHS (of type (int,bool) -> real)
-ResolveError.dfy(91,14): Error: incorrect type of method in-parameter 0 (expected ? -> ?, got (int,bool) -> real)
+ResolveError.dfy(91,15): Error: incorrect type of method in-parameter 0 (expected ? -> ?, got (int,bool) -> real)
ResolveError.dfy(101,6): Error: RHS (of type (()) -> real) not assignable to LHS (of type () -> real)
ResolveError.dfy(102,6): Error: RHS (of type () -> real) not assignable to LHS (of type (()) -> real)
ResolveError.dfy(7,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment
@@ -8,12 +8,12 @@ ResolveError.dfy(21,6): Error: LHS of assignment must denote a mutable field
ResolveError.dfy(31,16): Error: arguments must have the same type (got int and bool)
ResolveError.dfy(32,12): Error: wrong number of arguments to function application (function type 'int -> int' expects 1, got 2)
ResolveError.dfy(33,13): Error: type mismatch for argument 0 (function expects int, got bool)
-ResolveError.dfy(34,13): Error: incorrect type of function argument 0 (expected int, got bool)
+ResolveError.dfy(34,22): Error: type mismatch for argument 0 (function expects int, got bool)
ResolveError.dfy(35,25): Error: arguments must have the same type (got bool and int)
-ResolveError.dfy(36,13): Error: wrong number of function arguments (got 2, expected 1)
-ResolveError.dfy(37,13): Error: incorrect type of function argument 0 (expected int, got bool)
+ResolveError.dfy(36,21): Error: wrong number of arguments to function application (function 'requires' expects 1, got 2)
+ResolveError.dfy(37,19): Error: type mismatch for argument 0 (function expects int, got bool)
ResolveError.dfy(38,22): Error: arguments must have the same type (got set<object> and int)
-ResolveError.dfy(39,13): Error: wrong number of function arguments (got 2, expected 1)
+ResolveError.dfy(39,18): Error: wrong number of arguments to function application (function 'reads' expects 1, got 2)
ResolveError.dfy(46,15): Error: a reads-clause expression must denote an object or a collection of objects (instead got int)
ResolveError.dfy(47,7): Error: Precondition must be boolean (got int)
ResolveError.dfy(56,9): Error: condition is expected to be of type bool, but is () -> bool