diff options
| -rw-r--r-- | Source/Dafny/Dafny.atg | 37 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 31 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 744 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 15 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 135 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 131 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 527 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/Coinductive.dfy | 41 | ||||
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 3 | ||||
| -rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 50 | ||||
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs | 1 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 2 | ||||
| -rw-r--r-- | Util/vim/syntax/dafny.vim | 2 |
16 files changed, 1209 insertions, 520 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index bfce5122..3280e96a 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -576,9 +576,9 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f> List<Expression/*!*/> reqs = new List<Expression/*!*/>();
List<Expression/*!*/> ens = new List<Expression/*!*/>();
List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();
- List<Expression/*!*/> decreases = new List<Expression/*!*/>();
+ List<Expression/*!*/> decreases;
Expression body = null;
- bool isPredicate = false;
+ bool isPredicate = false; bool isCoPredicate = false;
bool isFunctionMethod = false;
IToken openParen = null;
IToken bodyStart = Token.NoToken;
@@ -619,14 +619,34 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f> | "..." (. signatureOmitted = true;
openParen = Token.NoToken; .)
)
+
+ /* ----- copredicate ----- */
+ | "copredicate" (. isCoPredicate = true; .)
+ (. if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
+ .)
+ { Attribute<ref attrs> }
+ NoUSIdent<out id>
+ (
+ [ GenericParameters<typeArgs> ]
+ [ Formals<true, isFunctionMethod, formals, out openParen>
+ [ ":" (. SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); .)
+ ]
+ ]
+ | "..." (. signatureOmitted = true;
+ openParen = Token.NoToken; .)
+ )
)
+ (. decreases = isCoPredicate ? null : new List<Expression/*!*/>(); .)
{ FunctionSpec<reqs, reads, ens, decreases> }
[ FunctionBody<out body, out bodyStart, out bodyEnd>
]
(. if (isPredicate) {
f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,
reqs, reads, ens, new Specification<Expression>(decreases, null), body, false, attrs, signatureOmitted);
+ } else if (isCoPredicate) {
+ f = new CoPredicate(id, id.val, mmod.IsStatic, typeArgs, openParen, formals,
+ reqs, reads, ens, body, attrs, signatureOmitted);
} else {
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,
reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureOmitted);
@@ -635,8 +655,10 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f> f.BodyEndTok = bodyEnd;
.)
.
-FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases.>
-= (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
+FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases.>
+= (. Contract.Requires(cce.NonNullElements(reqs));
+ Contract.Requires(cce.NonNullElements(reads));
+ Contract.Requires(decreases == null || cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; .)
(
SYNC
@@ -646,7 +668,12 @@ FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ r }
] SYNC ";"
| "ensures" Expression<out e> SYNC ";" (. ens.Add(e); .)
- | "decreases" DecreasesList<decreases, false> SYNC ";"
+ | "decreases" (. if (decreases == null) {
+ SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");
+ decreases = new List<Expression/*!*/>();
+ }
+ .)
+ DecreasesList<decreases, false> SYNC ";"
)
.
PossiblyWildExpression<out Expression/*!*/ e>
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index ee4592ce..df6fc2a6 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -899,6 +899,20 @@ namespace Microsoft.Dafny { return compileName;
}
}
+
+ public static IEnumerable<Function> AllFunctions(List<TopLevelDecl> declarations) {
+ foreach (var d in declarations) {
+ var cl = d as ClassDecl;
+ if (cl != null) {
+ foreach (var member in cl.Members) {
+ var fn = member as Function;
+ if (fn != null) {
+ yield return fn;
+ }
+ }
+ }
+ }
+ }
}
public class DefaultModuleDecl : ModuleDefinition {
@@ -1479,6 +1493,19 @@ namespace Microsoft.Dafny { }
}
+ public class CoPredicate : Function
+ {
+ public readonly List<FunctionCallExpr> Uses = new List<FunctionCallExpr>(); // filled in during resolution, used by verifier
+
+ public CoPredicate(IToken tok, string name, bool isStatic,
+ List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals,
+ List<Expression> req, List<FrameExpression> reads, List<Expression> ens,
+ Expression body, Attributes attributes, bool signatureOmitted)
+ : base(tok, name, isStatic, true, typeArgs, openParen, formals, new BoolType(),
+ req, reads, ens, new Specification<Expression>(new List<Expression>(), null), body, attributes, signatureOmitted) {
+ }
+ }
+
public class Method : MemberDecl, TypeParameter.ParentType
{
public readonly bool SignatureIsOmitted;
@@ -2948,7 +2975,7 @@ namespace Microsoft.Dafny { public readonly Expression/*!*/ Receiver;
public readonly IToken OpenParen; // can be null if Args.Count == 0
public readonly List<Expression/*!*/>/*!*/ Args;
- public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions; // create, initialized, and used by resolution (could be deleted once all of resolution is done)
+ public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions; // created, initialized, and used by resolution (could be deleted once all of resolution is done)
public enum CoCallResolution { No, Yes, NoBecauseFunctionHasSideEffects, NoBecauseRecursiveCallsAreNotAllowedInThisContext, NoBecauseIsNotGuarded }
public CoCallResolution CoCall = CoCallResolution.No; // indicates whether or not the call is a co-recursive call; filled in by resolution
@@ -3885,7 +3912,7 @@ namespace Microsoft.Dafny { public class Specification<T> where T : class
{
- public List<T> Expressions;
+ public readonly List<T> Expressions;
[ContractInvariantMethod]
private void ObjectInvariant()
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 9ad05d3b..0435fcb2 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -21,7 +21,7 @@ public class Parser { public const int _colon = 5;
public const int _lbrace = 6;
public const int _rbrace = 7;
- public const int maxT = 107;
+ public const int maxT = 108;
const bool T = true;
const bool x = false;
@@ -212,7 +212,7 @@ bool IsAttribute() { defaultModule.TopLevelDecls.Add(at);
} else if (StartOf(2)) {
ClassMemberDecl(membersDefaultClass, isGhost, false);
- } else SynErr(108);
+ } else SynErr(109);
}
DefaultClassDecl defaultClass = null;
foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
@@ -275,7 +275,7 @@ bool IsAttribute() { module.TopLevelDecls.Add(at);
} else if (StartOf(2)) {
ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false);
- } else SynErr(109);
+ } else SynErr(110);
}
Expect(7);
module.BodyEndTok = t;
@@ -291,7 +291,7 @@ bool IsAttribute() { QualifiedName(out idPath);
Expect(12);
submodule = new AbstractModuleDecl(idPath, id, parent);
- } else SynErr(110);
+ } else SynErr(111);
}
void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {
@@ -303,7 +303,7 @@ bool IsAttribute() { List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 15)) {SynErr(111); Get();}
+ while (!(la.kind == 0 || la.kind == 15)) {SynErr(112); Get();}
Expect(15);
while (la.kind == 6) {
Attribute(ref attrs);
@@ -334,13 +334,13 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; // dummy assignment
bool co = false;
- while (!(la.kind == 0 || la.kind == 17 || la.kind == 18)) {SynErr(112); Get();}
+ while (!(la.kind == 0 || la.kind == 17 || la.kind == 18)) {SynErr(113); Get();}
if (la.kind == 17) {
Get();
} else if (la.kind == 18) {
Get();
co = true;
- } else SynErr(113);
+ } else SynErr(114);
while (la.kind == 6) {
Attribute(ref attrs);
}
@@ -355,7 +355,7 @@ bool IsAttribute() { Get();
DatatypeMemberDecl(ctors);
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(114); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(115); Get();}
Expect(12);
if (co) {
dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
@@ -384,7 +384,7 @@ bool IsAttribute() { eqSupport = TypeParameter.EqualitySupportValue.Required;
}
at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(115); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(116); Get();}
Expect(12);
}
@@ -406,13 +406,13 @@ bool IsAttribute() { }
if (la.kind == 20) {
FieldDecl(mmod, mm);
- } else if (la.kind == 45 || la.kind == 46) {
+ } else if (la.kind == 45 || la.kind == 46 || la.kind == 47) {
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (la.kind == 28 || la.kind == 29) {
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
- } else SynErr(116);
+ } else SynErr(117);
}
void Attribute(ref Attributes attrs) {
@@ -483,7 +483,7 @@ bool IsAttribute() { Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
- while (!(la.kind == 0 || la.kind == 20)) {SynErr(117); Get();}
+ while (!(la.kind == 0 || la.kind == 20)) {SynErr(118); Get();}
Expect(20);
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
@@ -497,7 +497,7 @@ bool IsAttribute() { IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(118); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(119); Get();}
Expect(12);
}
@@ -511,9 +511,9 @@ bool IsAttribute() { List<Expression/*!*/> reqs = new List<Expression/*!*/>();
List<Expression/*!*/> ens = new List<Expression/*!*/>();
List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();
- List<Expression/*!*/> decreases = new List<Expression/*!*/>();
+ List<Expression/*!*/> decreases;
Expression body = null;
- bool isPredicate = false;
+ bool isPredicate = false; bool isCoPredicate = false;
bool isFunctionMethod = false;
IToken openParen = null;
IToken bodyStart = Token.NoToken;
@@ -543,7 +543,7 @@ bool IsAttribute() { Get();
signatureOmitted = true;
openParen = Token.NoToken;
- } else SynErr(119);
+ } else SynErr(120);
} else if (la.kind == 46) {
Get();
isPredicate = true;
@@ -572,8 +572,34 @@ bool IsAttribute() { Get();
signatureOmitted = true;
openParen = Token.NoToken;
- } else SynErr(120);
- } else SynErr(121);
+ } else SynErr(121);
+ } else if (la.kind == 47) {
+ Get();
+ isCoPredicate = true;
+ if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
+
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ NoUSIdent(out id);
+ if (StartOf(3)) {
+ if (la.kind == 26) {
+ GenericParameters(typeArgs);
+ }
+ if (la.kind == 23) {
+ Formals(true, isFunctionMethod, formals, out openParen);
+ if (la.kind == 5) {
+ Get();
+ SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool");
+ }
+ }
+ } else if (la.kind == 31) {
+ Get();
+ signatureOmitted = true;
+ openParen = Token.NoToken;
+ } else SynErr(122);
+ } else SynErr(123);
+ decreases = isCoPredicate ? null : new List<Expression/*!*/>();
while (StartOf(4)) {
FunctionSpec(reqs, reads, ens, decreases);
}
@@ -583,6 +609,9 @@ bool IsAttribute() { if (isPredicate) {
f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,
reqs, reads, ens, new Specification<Expression>(decreases, null), body, false, attrs, signatureOmitted);
+ } else if (isCoPredicate) {
+ f = new CoPredicate(id, id.val, mmod.IsStatic, typeArgs, openParen, formals,
+ reqs, reads, ens, body, attrs, signatureOmitted);
} else {
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,
reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureOmitted);
@@ -612,7 +641,7 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 28 || la.kind == 29)) {SynErr(122); Get();}
+ while (!(la.kind == 0 || la.kind == 28 || la.kind == 29)) {SynErr(124); Get();}
if (la.kind == 28) {
Get();
} else if (la.kind == 29) {
@@ -623,7 +652,7 @@ bool IsAttribute() { SemErr(t, "constructors are only allowed in classes");
}
- } else SynErr(123);
+ } else SynErr(125);
if (isConstructor) {
if (mmod.IsGhost) {
SemErr(t, "constructors cannot be declared 'ghost'");
@@ -650,7 +679,7 @@ bool IsAttribute() { } else if (la.kind == 31) {
Get();
signatureOmitted = true; openParen = Token.NoToken;
- } else SynErr(124);
+ } else SynErr(126);
while (StartOf(5)) {
MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
}
@@ -844,7 +873,7 @@ bool IsAttribute() { ReferenceType(out tok, out ty);
break;
}
- default: SynErr(125); break;
+ default: SynErr(127); break;
}
}
@@ -869,7 +898,7 @@ 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(7))) {SynErr(126); Get();}
+ while (!(StartOf(7))) {SynErr(128); Get();}
if (la.kind == 32) {
Get();
while (IsAttribute()) {
@@ -884,7 +913,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(127); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(129); Get();}
Expect(12);
} else if (la.kind == 33 || la.kind == 34 || la.kind == 35) {
if (la.kind == 33) {
@@ -894,7 +923,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 34) {
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(128); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(130); Get();}
Expect(12);
req.Add(new MaybeFreeExpression(e, isFree));
} else if (la.kind == 35) {
@@ -903,19 +932,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Attribute(ref ensAttrs);
}
Expression(out e);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(129); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(131); Get();}
Expect(12);
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
- } else SynErr(130);
+ } else SynErr(132);
} else if (la.kind == 36) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(131); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(133); Get();}
Expect(12);
- } else SynErr(132);
+ } else SynErr(134);
}
void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -935,7 +964,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void FrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null;
Expression(out e);
- if (la.kind == 49) {
+ if (la.kind == 50) {
Get();
Ident(out id);
fieldName = id.val;
@@ -1015,20 +1044,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt, moduleName);
- } else SynErr(133);
+ } else SynErr(135);
}
- void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
- Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
+ void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {
+ Contract.Requires(cce.NonNullElements(reqs));
+ Contract.Requires(cce.NonNullElements(reads));
+ Contract.Requires(decreases == null || cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
if (la.kind == 34) {
- while (!(la.kind == 0 || la.kind == 34)) {SynErr(134); Get();}
+ while (!(la.kind == 0 || la.kind == 34)) {SynErr(136); Get();}
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(135); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(137); Get();}
Expect(12);
reqs.Add(e);
- } else if (la.kind == 47) {
+ } else if (la.kind == 48) {
Get();
if (StartOf(10)) {
PossiblyWildFrameExpression(out fe);
@@ -1039,20 +1070,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(136); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(138); Get();}
Expect(12);
} else if (la.kind == 35) {
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(137); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(139); Get();}
Expect(12);
ens.Add(e);
} else if (la.kind == 36) {
Get();
+ if (decreases == null) {
+ SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");
+ decreases = new List<Expression/*!*/>();
+ }
+
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(138); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(140); Get();}
Expect(12);
- } else SynErr(139);
+ } else SynErr(141);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -1066,23 +1102,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
- if (la.kind == 48) {
+ if (la.kind == 49) {
Get();
fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(8)) {
FrameExpression(out fe);
- } else SynErr(140);
+ } else SynErr(142);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
- if (la.kind == 48) {
+ if (la.kind == 49) {
Get();
e = new WildcardExpr(t);
} else if (StartOf(8)) {
Expression(out e);
- } else SynErr(141);
+ } else SynErr(143);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1099,26 +1135,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd;
int breakCount;
- while (!(StartOf(11))) {SynErr(142); Get();}
+ while (!(StartOf(11))) {SynErr(144); Get();}
switch (la.kind) {
case 6: {
BlockStmt(out bs, out bodyStart, out bodyEnd);
s = bs;
break;
}
- case 67: {
+ case 68: {
AssertStmt(out s);
break;
}
- case 55: {
+ case 56: {
AssumeStmt(out s);
break;
}
- case 68: {
+ case 69: {
PrintStmt(out s);
break;
}
- case 1: case 2: case 19: case 23: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
+ case 1: case 2: case 19: case 23: case 93: case 94: case 95: case 96: case 97: case 98: case 99: {
UpdateStmt(out s);
break;
}
@@ -1126,23 +1162,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo VarDeclStatement(out s);
break;
}
- case 60: {
+ case 61: {
IfStmt(out s);
break;
}
- case 64: {
+ case 65: {
WhileStmt(out s);
break;
}
- case 66: {
+ case 67: {
MatchStmt(out s);
break;
}
- case 69: {
+ case 70: {
ParallelStmt(out s);
break;
}
- case 50: {
+ case 51: {
Get();
x = t;
NoUSIdent(out id);
@@ -1151,24 +1187,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LList<Label>(new Label(x, id.val), s.Labels);
break;
}
- case 51: {
+ case 52: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
NoUSIdent(out id);
label = id.val;
- } else if (la.kind == 12 || la.kind == 51) {
- while (la.kind == 51) {
+ } else if (la.kind == 12 || la.kind == 52) {
+ while (la.kind == 52) {
Get();
breakCount++;
}
- } else SynErr(143);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(144); Get();}
+ } else SynErr(145);
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(146); Get();}
Expect(12);
s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
}
- case 52: {
+ case 53: {
ReturnStmt(out s);
break;
}
@@ -1178,7 +1214,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(12);
break;
}
- default: SynErr(145); break;
+ default: SynErr(147); break;
}
}
@@ -1186,7 +1222,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
Expression e = null; Attributes attrs = null;
- Expect(67);
+ Expect(68);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
@@ -1195,7 +1231,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e);
} else if (la.kind == 31) {
Get();
- } else SynErr(146);
+ } else SynErr(148);
Expect(12);
if (e == null) {
s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false);
@@ -1209,7 +1245,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
Expression e = null; Attributes attrs = null;
- Expect(55);
+ Expect(56);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
@@ -1218,7 +1254,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e);
} else if (la.kind == 31) {
Get();
- } else SynErr(147);
+ } else SynErr(149);
if (e == null) {
s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
} else {
@@ -1232,7 +1268,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
- Expect(68);
+ Expect(69);
x = t;
AttributeArg(out arg);
args.Add(arg);
@@ -1263,14 +1299,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(12);
rhss.Add(new ExprRhs(e, attrs));
- } else if (la.kind == 21 || la.kind == 53 || la.kind == 54) {
+ } else if (la.kind == 21 || la.kind == 54 || la.kind == 55) {
lhss.Add(e); lhs0 = e;
while (la.kind == 21) {
Get();
Lhs(out e);
lhss.Add(e);
}
- if (la.kind == 53) {
+ if (la.kind == 54) {
Get();
x = t;
Rhs(out r, lhs0);
@@ -1280,20 +1316,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Rhs(out r, lhs0);
rhss.Add(r);
}
- } else if (la.kind == 54) {
+ } else if (la.kind == 55) {
Get();
x = t;
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
suchThatAssume = t;
}
Expression(out suchThat);
- } else SynErr(148);
+ } else SynErr(150);
Expect(12);
} else if (la.kind == 5) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(149);
+ } else SynErr(151);
if (suchThat != null) {
s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
} else {
@@ -1324,8 +1360,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d);
}
- if (la.kind == 53 || la.kind == 54) {
- if (la.kind == 53) {
+ if (la.kind == 54 || la.kind == 55) {
+ if (la.kind == 54) {
Get();
assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
@@ -1341,7 +1377,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else {
Get();
assignTok = t;
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
suchThatAssume = t;
}
@@ -1380,7 +1416,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(60);
+ Expect(61);
x = t;
if (la.kind == 23 || la.kind == 31) {
if (la.kind == 23) {
@@ -1390,15 +1426,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo guardOmitted = true;
}
BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 61) {
+ if (la.kind == 62) {
Get();
- if (la.kind == 60) {
+ if (la.kind == 61) {
IfStmt(out s);
els = s;
} else if (la.kind == 6) {
BlockStmt(out bs, out bodyStart, out bodyEnd);
els = bs;
- } else SynErr(150);
+ } else SynErr(152);
}
if (guardOmitted) {
ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);
@@ -1409,7 +1445,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 6) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(151);
+ } else SynErr(153);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1425,7 +1461,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(64);
+ Expect(65);
x = t;
if (la.kind == 23 || la.kind == 31) {
if (la.kind == 23) {
@@ -1441,7 +1477,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 31) {
Get();
bodyOmitted = true;
- } else SynErr(152);
+ } else SynErr(154);
if (guardOmitted || bodyOmitted) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -1459,18 +1495,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives);
- } else SynErr(153);
+ } else SynErr(155);
}
void MatchStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
- Expect(66);
+ Expect(67);
x = t;
Expression(out e);
Expect(6);
- while (la.kind == 62) {
+ while (la.kind == 63) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1490,7 +1526,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BlockStmt/*!*/ block;
IToken bodyStart, bodyEnd;
- Expect(69);
+ Expect(70);
x = t;
Expect(23);
if (la.kind == 1) {
@@ -1523,7 +1559,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<AssignmentRhs> rhss = null;
AssignmentRhs r;
- Expect(52);
+ Expect(53);
returnTok = t;
if (StartOf(13)) {
Rhs(out r, null);
@@ -1547,16 +1583,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = null; // to please compiler
Attributes attrs = null;
- if (la.kind == 56) {
+ if (la.kind == 57) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 14 || la.kind == 23 || la.kind == 57) {
- if (la.kind == 57) {
+ if (la.kind == 14 || la.kind == 23 || la.kind == 58) {
+ if (la.kind == 58) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(58);
+ Expect(59);
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
} else if (la.kind == 14) {
@@ -1598,18 +1634,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = new TypeRhs(newToken, ty, initCall);
}
- } else if (la.kind == 59) {
+ } else if (la.kind == 60) {
Get();
x = t;
Expression(out e);
r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e));
- } else if (la.kind == 48) {
+ } else if (la.kind == 49) {
Get();
r = new HavocRhs(t);
} else if (StartOf(8)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(154);
+ } else SynErr(156);
while (la.kind == 6) {
Attribute(ref attrs);
}
@@ -1621,16 +1657,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 14 || la.kind == 57) {
+ while (la.kind == 14 || la.kind == 58) {
Suffix(ref e);
}
} else if (StartOf(14)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 14 || la.kind == 57) {
+ while (la.kind == 14 || la.kind == 58) {
Suffix(ref e);
}
- } else SynErr(155);
+ } else SynErr(157);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -1647,13 +1683,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
Expect(23);
- if (la.kind == 48) {
+ if (la.kind == 49) {
Get();
e = null;
} else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(156);
+ } else SynErr(158);
Expect(25);
}
@@ -1664,11 +1700,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Statement> body;
Expect(6);
- while (la.kind == 62) {
+ while (la.kind == 63) {
Get();
x = t;
Expression(out e);
- Expect(63);
+ Expect(64);
body = new List<Statement>();
while (StartOf(9)) {
Stmt(body);
@@ -1686,22 +1722,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod = null;
while (StartOf(15)) {
- if (la.kind == 33 || la.kind == 65) {
+ if (la.kind == 33 || la.kind == 66) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(157); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(159); Get();}
Expect(12);
invariants.Add(invariant);
} else if (la.kind == 36) {
- while (!(la.kind == 0 || la.kind == 36)) {SynErr(158); Get();}
+ while (!(la.kind == 0 || la.kind == 36)) {SynErr(160); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(159); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(161); Get();}
Expect(12);
} else {
- while (!(la.kind == 0 || la.kind == 32)) {SynErr(160); Get();}
+ while (!(la.kind == 0 || la.kind == 32)) {SynErr(162); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -1716,7 +1752,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(161); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(163); Get();}
Expect(12);
}
}
@@ -1724,12 +1760,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo 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 == 33 || la.kind == 65)) {SynErr(162); Get();}
+ while (!(la.kind == 0 || la.kind == 33 || la.kind == 66)) {SynErr(164); Get();}
if (la.kind == 33) {
Get();
isFree = true;
}
- Expect(65);
+ Expect(66);
while (IsAttribute()) {
Attribute(ref attrs);
}
@@ -1744,7 +1780,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(62);
+ Expect(63);
x = t;
Ident(out id);
if (la.kind == 23) {
@@ -1758,7 +1794,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(25);
}
- Expect(63);
+ Expect(64);
while (StartOf(9)) {
Stmt(body);
}
@@ -1773,7 +1809,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(8)) {
Expression(out e);
arg = new Attributes.Argument(t, e);
- } else SynErr(163);
+ } else SynErr(165);
}
void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -1801,7 +1837,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 70 || la.kind == 71) {
+ while (la.kind == 71 || la.kind == 72) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -1812,7 +1848,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ImpliesExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0);
- if (la.kind == 72 || la.kind == 73) {
+ if (la.kind == 73 || la.kind == 74) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -1821,23 +1857,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void EquivOp() {
- if (la.kind == 70) {
+ if (la.kind == 71) {
Get();
- } else if (la.kind == 71) {
+ } else if (la.kind == 72) {
Get();
- } else SynErr(164);
+ } else SynErr(166);
}
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(16)) {
- if (la.kind == 74 || la.kind == 75) {
+ if (la.kind == 75 || la.kind == 76) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 74 || la.kind == 75) {
+ while (la.kind == 75 || la.kind == 76) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1848,7 +1884,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 76 || la.kind == 77) {
+ while (la.kind == 77 || la.kind == 78) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1859,11 +1895,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void ImpliesOp() {
- if (la.kind == 72) {
+ if (la.kind == 73) {
Get();
- } else if (la.kind == 73) {
+ } else if (la.kind == 74) {
Get();
- } else SynErr(165);
+ } else SynErr(167);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -1957,25 +1993,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void AndOp() {
- if (la.kind == 74) {
+ if (la.kind == 75) {
Get();
- } else if (la.kind == 75) {
+ } else if (la.kind == 76) {
Get();
- } else SynErr(166);
+ } else SynErr(168);
}
void OrOp() {
- if (la.kind == 76) {
+ if (la.kind == 77) {
Get();
- } else if (la.kind == 77) {
+ } else if (la.kind == 78) {
Get();
- } else SynErr(167);
+ } else SynErr(169);
}
void Term(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (la.kind == 87 || la.kind == 88) {
+ while (la.kind == 88 || la.kind == 89) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2003,35 +2039,35 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 78: {
+ case 79: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 79: {
+ case 80: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 80: {
+ case 81: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 81: {
+ case 82: {
Get();
x = t; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 82: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 83: {
+ case 84: {
Get();
x = t; y = Token.NoToken;
- if (la.kind == 82) {
+ if (la.kind == 83) {
Get();
y = t;
}
@@ -2046,29 +2082,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break;
}
- case 84: {
+ case 85: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 85: {
+ case 86: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 86: {
+ case 87: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(168); break;
+ default: SynErr(170); break;
}
}
void Factor(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 48 || la.kind == 89 || la.kind == 90) {
+ while (la.kind == 49 || la.kind == 90 || la.kind == 91) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2077,44 +2113,44 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void AddOp(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 == 87) {
+ if (la.kind == 88) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 88) {
+ } else if (la.kind == 89) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(169);
+ } else SynErr(171);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 88: {
+ case 89: {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
break;
}
- case 83: case 91: {
+ case 84: case 92: {
NegOp();
x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 20: case 40: case 55: case 60: case 66: case 67: case 101: case 102: case 103: case 104: {
+ case 20: case 40: case 56: case 61: case 67: case 68: case 102: case 103: case 104: case 105: {
EndlessExpression(out e);
break;
}
case 1: {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 14 || la.kind == 57) {
+ while (la.kind == 14 || la.kind == 58) {
Suffix(ref e);
}
break;
}
- case 6: case 57: {
+ case 6: case 58: {
DisplayExpr(out e);
break;
}
@@ -2126,37 +2162,37 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo MapExpr(out e);
break;
}
- case 2: case 19: case 23: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
+ case 2: case 19: case 23: case 93: case 94: case 95: case 96: case 97: case 98: case 99: {
ConstAtomExpression(out e);
- while (la.kind == 14 || la.kind == 57) {
+ while (la.kind == 14 || la.kind == 58) {
Suffix(ref e);
}
break;
}
- default: SynErr(170); break;
+ default: SynErr(172); break;
}
}
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 == 48) {
+ if (la.kind == 49) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 89) {
+ } else if (la.kind == 90) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 90) {
+ } else if (la.kind == 91) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(171);
+ } else SynErr(173);
}
void NegOp() {
- if (la.kind == 83) {
+ if (la.kind == 84) {
Get();
- } else if (la.kind == 91) {
+ } else if (la.kind == 92) {
Get();
- } else SynErr(172);
+ } else SynErr(174);
}
void EndlessExpression(out Expression e) {
@@ -2167,22 +2203,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<BoundVar> letVars; List<Expression> letRHSs;
switch (la.kind) {
- case 60: {
+ case 61: {
Get();
x = t;
Expression(out e);
- Expect(99);
+ Expect(100);
Expression(out e0);
- Expect(61);
+ Expect(62);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
break;
}
- case 66: {
+ case 67: {
MatchExpression(out e);
break;
}
- case 101: case 102: case 103: case 104: {
+ case 102: case 103: case 104: case 105: {
QuantifierGuts(out e);
break;
}
@@ -2190,7 +2226,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ComprehensionExpr(out e);
break;
}
- case 67: {
+ case 68: {
Get();
x = t;
Expression(out e0);
@@ -2199,7 +2235,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new AssertExpr(x, e0, e1);
break;
}
- case 55: {
+ case 56: {
Get();
x = t;
Expression(out e0);
@@ -2220,7 +2256,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out d);
letVars.Add(d);
}
- Expect(53);
+ Expect(54);
Expression(out e);
letRHSs.Add(e);
while (la.kind == 21) {
@@ -2233,7 +2269,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new LetExpr(x, letVars, letRHSs, e);
break;
}
- default: SynErr(173); break;
+ default: SynErr(175); break;
}
}
@@ -2279,24 +2315,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new FunctionCallExpr(id, id.val, e, openParen, args);
}
if (!func) { e = new ExprDotName(id, e, id.val); }
- } else if (la.kind == 57) {
+ } else if (la.kind == 58) {
Get();
x = t;
if (StartOf(8)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 100) {
+ if (la.kind == 101) {
Get();
anyDots = true;
if (StartOf(8)) {
Expression(out ee);
e1 = ee;
}
- } else if (la.kind == 53) {
+ } else if (la.kind == 54) {
Get();
Expression(out ee);
e1 = ee;
- } else if (la.kind == 21 || la.kind == 58) {
+ } else if (la.kind == 21 || la.kind == 59) {
while (la.kind == 21) {
Get();
Expression(out ee);
@@ -2307,15 +2343,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee);
}
- } else SynErr(174);
- } else if (la.kind == 100) {
+ } else SynErr(176);
+ } else if (la.kind == 101) {
Get();
anyDots = true;
if (StartOf(8)) {
Expression(out ee);
e1 = ee;
}
- } else SynErr(175);
+ } else SynErr(177);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -2338,8 +2374,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- Expect(58);
- } else SynErr(176);
+ Expect(59);
+ } else SynErr(178);
}
void DisplayExpr(out Expression e) {
@@ -2355,15 +2391,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
e = new SetDisplayExpr(x, elements);
Expect(7);
- } else if (la.kind == 57) {
+ } else if (la.kind == 58) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(8)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(58);
- } else SynErr(177);
+ Expect(59);
+ } else SynErr(179);
}
void MultiSetExpr(out Expression e) {
@@ -2389,7 +2425,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(25);
} else if (StartOf(18)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(178);
+ } else SynErr(180);
}
void MapExpr(out Expression e) {
@@ -2400,14 +2436,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(43);
x = t;
- if (la.kind == 57) {
+ if (la.kind == 58) {
Get();
elements = new List<ExpressionPair/*!*/>();
if (StartOf(8)) {
MapLiteralExpressions(out elements);
}
e = new MapDisplayExpr(x, elements);
- Expect(58);
+ Expect(59);
} else if (la.kind == 1) {
BoundVar/*!*/ bv;
List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
@@ -2423,7 +2459,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new MapComprehension(x, bvars, range, body);
} else if (StartOf(18)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(179);
+ } else SynErr(181);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2432,17 +2468,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr;
switch (la.kind) {
- case 92: {
+ case 93: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 93: {
+ case 94: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 94: {
+ case 95: {
Get();
e = new LiteralExpr(t);
break;
@@ -2452,12 +2488,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new LiteralExpr(t, n);
break;
}
- case 95: {
+ case 96: {
Get();
e = new ThisExpr(t);
break;
}
- case 96: {
+ case 97: {
Get();
x = t;
Expect(23);
@@ -2466,7 +2502,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new FreshExpr(x, e);
break;
}
- case 97: {
+ case 98: {
Get();
x = t;
Expect(23);
@@ -2475,7 +2511,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new AllocatedExpr(x, e);
break;
}
- case 98: {
+ case 99: {
Get();
x = t;
Expect(23);
@@ -2500,7 +2536,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(25);
break;
}
- default: SynErr(180); break;
+ default: SynErr(182); break;
}
}
@@ -2519,34 +2555,34 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ d, r;
elements = new List<ExpressionPair/*!*/>();
Expression(out d);
- Expect(53);
+ Expect(54);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
while (la.kind == 21) {
Get();
Expression(out d);
- Expect(53);
+ Expect(54);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
}
}
void QSep() {
- if (la.kind == 105) {
+ if (la.kind == 106) {
Get();
- } else if (la.kind == 106) {
+ } else if (la.kind == 107) {
Get();
- } else SynErr(181);
+ } else SynErr(183);
}
void MatchExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
- Expect(66);
+ Expect(67);
x = t;
Expression(out e);
- while (la.kind == 62) {
+ while (la.kind == 63) {
CaseExpression(out c);
cases.Add(c);
}
@@ -2561,13 +2597,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression range;
Expression/*!*/ body;
- if (la.kind == 101 || la.kind == 102) {
+ if (la.kind == 102 || la.kind == 103) {
Forall();
x = t; univ = true;
- } else if (la.kind == 103 || la.kind == 104) {
+ } else if (la.kind == 104 || la.kind == 105) {
Exists();
x = t;
- } else SynErr(182);
+ } else SynErr(184);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body);
@@ -2598,7 +2634,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(19);
Expression(out range);
- if (la.kind == 105 || la.kind == 106) {
+ if (la.kind == 106 || la.kind == 107) {
QSep();
Expression(out body);
}
@@ -2613,7 +2649,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
Expression/*!*/ body;
- Expect(62);
+ Expect(63);
x = t;
Ident(out id);
if (la.kind == 23) {
@@ -2627,25 +2663,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(25);
}
- Expect(63);
+ Expect(64);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
}
void Forall() {
- if (la.kind == 101) {
+ if (la.kind == 102) {
Get();
- } else if (la.kind == 102) {
+ } else if (la.kind == 103) {
Get();
- } else SynErr(183);
+ } else SynErr(185);
}
void Exists() {
- if (la.kind == 103) {
+ if (la.kind == 104) {
Get();
- } else if (la.kind == 104) {
+ } else if (la.kind == 105) {
Get();
- } else SynErr(184);
+ } else SynErr(186);
}
void AttributeBody(ref Attributes attrs) {
@@ -2681,26 +2717,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
static readonly bool[,]/*!*/ set = {
- {T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, T,x,x,T, x,x,x,x, T,T,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,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, 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, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,x, x,x,x,x, T,T,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,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {T,x,x,x, x,x,T,T, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,T, x,x,T,x, T,T,x,x, x,x,T,T, T,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,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,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,T,x, x,x,T,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,T,x,T, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
- {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,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,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,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,T, T,x,x,T, 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,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
- {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,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,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,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,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,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,T,T,x, x,x,T,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,T,x,T, x,x,x,x, T,x,x,x, x,x,x,T, T,T,x,T, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,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,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, 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, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,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,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,T,x, x,T,T,T, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
- {x,T,T,x, T,x,T,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,T,x,T, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}
+ {T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, T,x,x,T, x,x,x,x, T,T,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, T,x,x,x, x,T,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,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, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,x, x,x,x,x, T,T,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, T,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,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},
+ {T,x,x,x, x,x,T,T, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,T, x,x,T,x, T,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,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,T,x, x,x,T,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,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,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,T, T,T,x,x, T,x,x,x, x,T,x,x, x,T,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, 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,T, T,x,x,T, 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,T,x,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,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,T, T,T,x,x, T,x,x,x, x,T,x,x, x,T,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,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,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,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,T,T,x, x,x,T,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,T,x,T, x,x,x,x, x,T,x,x, x,x,x,x, T,T,T,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,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,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,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, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,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,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,T,x, x,x,x,T, x,x,T,T, T,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x},
+ {x,T,T,x, T,x,T,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,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}
};
} // end Parser
@@ -2772,144 +2808,146 @@ public class Errors { case 44: s = "\"object\" expected"; break;
case 45: s = "\"function\" expected"; break;
case 46: s = "\"predicate\" expected"; break;
- case 47: s = "\"reads\" expected"; break;
- case 48: s = "\"*\" expected"; break;
- case 49: s = "\"`\" expected"; break;
- case 50: s = "\"label\" expected"; break;
- case 51: s = "\"break\" expected"; break;
- case 52: s = "\"return\" expected"; break;
- case 53: s = "\":=\" expected"; break;
- case 54: s = "\":|\" expected"; break;
- case 55: s = "\"assume\" expected"; break;
- case 56: s = "\"new\" expected"; break;
- case 57: s = "\"[\" expected"; break;
- case 58: s = "\"]\" expected"; break;
- case 59: s = "\"choose\" expected"; break;
- case 60: s = "\"if\" expected"; break;
- case 61: s = "\"else\" expected"; break;
- case 62: s = "\"case\" expected"; break;
- case 63: s = "\"=>\" expected"; break;
- case 64: s = "\"while\" expected"; break;
- case 65: s = "\"invariant\" expected"; break;
- case 66: s = "\"match\" expected"; break;
- case 67: s = "\"assert\" expected"; break;
- case 68: s = "\"print\" expected"; break;
- case 69: s = "\"parallel\" expected"; break;
- case 70: s = "\"<==>\" expected"; break;
- case 71: s = "\"\\u21d4\" expected"; break;
- case 72: s = "\"==>\" expected"; break;
- case 73: s = "\"\\u21d2\" expected"; break;
- case 74: s = "\"&&\" expected"; break;
- case 75: s = "\"\\u2227\" expected"; break;
- case 76: s = "\"||\" expected"; break;
- case 77: s = "\"\\u2228\" expected"; break;
- case 78: s = "\"<=\" expected"; break;
- case 79: s = "\">=\" expected"; break;
- case 80: s = "\"!=\" expected"; break;
- case 81: s = "\"!!\" expected"; break;
- case 82: s = "\"in\" expected"; break;
- case 83: s = "\"!\" expected"; break;
- case 84: s = "\"\\u2260\" expected"; break;
- case 85: s = "\"\\u2264\" expected"; break;
- case 86: s = "\"\\u2265\" expected"; break;
- case 87: s = "\"+\" expected"; break;
- case 88: s = "\"-\" expected"; break;
- case 89: s = "\"/\" expected"; break;
- case 90: s = "\"%\" expected"; break;
- case 91: s = "\"\\u00ac\" expected"; break;
- case 92: s = "\"false\" expected"; break;
- case 93: s = "\"true\" expected"; break;
- case 94: s = "\"null\" expected"; break;
- case 95: s = "\"this\" expected"; break;
- case 96: s = "\"fresh\" expected"; break;
- case 97: s = "\"allocated\" expected"; break;
- case 98: s = "\"old\" expected"; break;
- case 99: s = "\"then\" expected"; break;
- case 100: s = "\"..\" expected"; break;
- case 101: s = "\"forall\" expected"; break;
- case 102: s = "\"\\u2200\" expected"; break;
- case 103: s = "\"exists\" expected"; break;
- case 104: s = "\"\\u2203\" expected"; break;
- case 105: s = "\"::\" expected"; break;
- case 106: s = "\"\\u2022\" expected"; break;
- case 107: s = "??? expected"; break;
- case 108: s = "invalid Dafny"; break;
- case 109: s = "invalid SubModuleDecl"; break;
+ case 47: s = "\"copredicate\" expected"; break;
+ case 48: s = "\"reads\" expected"; break;
+ case 49: s = "\"*\" expected"; break;
+ case 50: s = "\"`\" expected"; break;
+ case 51: s = "\"label\" expected"; break;
+ case 52: s = "\"break\" expected"; break;
+ case 53: s = "\"return\" expected"; break;
+ case 54: s = "\":=\" expected"; break;
+ case 55: s = "\":|\" expected"; break;
+ case 56: s = "\"assume\" expected"; break;
+ case 57: s = "\"new\" expected"; break;
+ case 58: s = "\"[\" expected"; break;
+ case 59: s = "\"]\" expected"; break;
+ case 60: s = "\"choose\" expected"; break;
+ case 61: s = "\"if\" expected"; break;
+ case 62: s = "\"else\" expected"; break;
+ case 63: s = "\"case\" expected"; break;
+ case 64: s = "\"=>\" expected"; break;
+ case 65: s = "\"while\" expected"; break;
+ case 66: s = "\"invariant\" expected"; break;
+ case 67: s = "\"match\" expected"; break;
+ case 68: s = "\"assert\" expected"; break;
+ case 69: s = "\"print\" expected"; break;
+ case 70: s = "\"parallel\" expected"; break;
+ case 71: s = "\"<==>\" expected"; break;
+ case 72: s = "\"\\u21d4\" expected"; break;
+ case 73: s = "\"==>\" expected"; break;
+ case 74: s = "\"\\u21d2\" expected"; break;
+ case 75: s = "\"&&\" expected"; break;
+ case 76: s = "\"\\u2227\" expected"; break;
+ case 77: s = "\"||\" expected"; break;
+ case 78: s = "\"\\u2228\" expected"; break;
+ case 79: s = "\"<=\" expected"; break;
+ case 80: s = "\">=\" expected"; break;
+ case 81: s = "\"!=\" expected"; break;
+ case 82: s = "\"!!\" expected"; break;
+ case 83: s = "\"in\" expected"; break;
+ case 84: s = "\"!\" expected"; break;
+ case 85: s = "\"\\u2260\" expected"; break;
+ case 86: s = "\"\\u2264\" expected"; break;
+ case 87: s = "\"\\u2265\" expected"; break;
+ case 88: s = "\"+\" expected"; break;
+ case 89: s = "\"-\" expected"; break;
+ case 90: s = "\"/\" expected"; break;
+ case 91: s = "\"%\" expected"; break;
+ case 92: s = "\"\\u00ac\" expected"; break;
+ case 93: s = "\"false\" expected"; break;
+ case 94: s = "\"true\" expected"; break;
+ case 95: s = "\"null\" expected"; break;
+ case 96: s = "\"this\" expected"; break;
+ case 97: s = "\"fresh\" expected"; break;
+ case 98: s = "\"allocated\" expected"; break;
+ case 99: s = "\"old\" expected"; break;
+ case 100: s = "\"then\" expected"; break;
+ case 101: s = "\"..\" expected"; break;
+ case 102: s = "\"forall\" expected"; break;
+ case 103: s = "\"\\u2200\" expected"; break;
+ case 104: s = "\"exists\" expected"; break;
+ case 105: s = "\"\\u2203\" expected"; break;
+ case 106: s = "\"::\" expected"; break;
+ case 107: s = "\"\\u2022\" expected"; break;
+ case 108: s = "??? expected"; break;
+ case 109: s = "invalid Dafny"; break;
case 110: s = "invalid SubModuleDecl"; break;
- case 111: s = "this symbol not expected in ClassDecl"; break;
- case 112: s = "this symbol not expected in DatatypeDecl"; break;
- case 113: s = "invalid DatatypeDecl"; break;
- case 114: s = "this symbol not expected in DatatypeDecl"; break;
- case 115: s = "this symbol not expected in ArbitraryTypeDecl"; break;
- case 116: s = "invalid ClassMemberDecl"; break;
- case 117: s = "this symbol not expected in FieldDecl"; break;
+ case 111: s = "invalid SubModuleDecl"; break;
+ case 112: s = "this symbol not expected in ClassDecl"; break;
+ case 113: s = "this symbol not expected in DatatypeDecl"; break;
+ case 114: s = "invalid DatatypeDecl"; break;
+ case 115: s = "this symbol not expected in DatatypeDecl"; break;
+ case 116: s = "this symbol not expected in ArbitraryTypeDecl"; break;
+ case 117: s = "invalid ClassMemberDecl"; break;
case 118: s = "this symbol not expected in FieldDecl"; break;
- case 119: s = "invalid FunctionDecl"; break;
+ case 119: s = "this symbol not expected in FieldDecl"; break;
case 120: s = "invalid FunctionDecl"; break;
case 121: s = "invalid FunctionDecl"; break;
- case 122: s = "this symbol not expected in MethodDecl"; break;
- case 123: s = "invalid MethodDecl"; break;
- case 124: s = "invalid MethodDecl"; break;
- case 125: s = "invalid TypeAndToken"; break;
- case 126: s = "this symbol not expected in MethodSpec"; break;
- case 127: s = "this symbol not expected in MethodSpec"; break;
+ case 122: s = "invalid FunctionDecl"; break;
+ case 123: s = "invalid FunctionDecl"; break;
+ case 124: s = "this symbol not expected in MethodDecl"; break;
+ case 125: s = "invalid MethodDecl"; break;
+ case 126: s = "invalid MethodDecl"; break;
+ case 127: s = "invalid TypeAndToken"; break;
case 128: s = "this symbol not expected in MethodSpec"; break;
case 129: s = "this symbol not expected in MethodSpec"; break;
- case 130: s = "invalid MethodSpec"; break;
+ case 130: s = "this symbol not expected in MethodSpec"; break;
case 131: s = "this symbol not expected in MethodSpec"; break;
case 132: s = "invalid MethodSpec"; break;
- case 133: s = "invalid ReferenceType"; break;
- case 134: s = "this symbol not expected in FunctionSpec"; break;
- case 135: s = "this symbol not expected in FunctionSpec"; break;
+ case 133: s = "this symbol not expected in MethodSpec"; break;
+ case 134: s = "invalid MethodSpec"; break;
+ case 135: s = "invalid ReferenceType"; break;
case 136: s = "this symbol not expected in FunctionSpec"; break;
case 137: s = "this symbol not expected in FunctionSpec"; break;
case 138: s = "this symbol not expected in FunctionSpec"; break;
- case 139: s = "invalid FunctionSpec"; break;
- case 140: s = "invalid PossiblyWildFrameExpression"; break;
- case 141: s = "invalid PossiblyWildExpression"; break;
- case 142: s = "this symbol not expected in OneStmt"; break;
- case 143: s = "invalid OneStmt"; break;
+ case 139: s = "this symbol not expected in FunctionSpec"; break;
+ case 140: s = "this symbol not expected in FunctionSpec"; break;
+ case 141: s = "invalid FunctionSpec"; break;
+ case 142: s = "invalid PossiblyWildFrameExpression"; break;
+ case 143: s = "invalid PossiblyWildExpression"; break;
case 144: s = "this symbol not expected in OneStmt"; break;
case 145: s = "invalid OneStmt"; break;
- case 146: s = "invalid AssertStmt"; break;
- case 147: s = "invalid AssumeStmt"; break;
- case 148: s = "invalid UpdateStmt"; break;
- case 149: s = "invalid UpdateStmt"; break;
- case 150: s = "invalid IfStmt"; break;
- case 151: s = "invalid IfStmt"; break;
- case 152: s = "invalid WhileStmt"; break;
- case 153: s = "invalid WhileStmt"; break;
- case 154: s = "invalid Rhs"; break;
- case 155: s = "invalid Lhs"; break;
- case 156: s = "invalid Guard"; break;
- case 157: s = "this symbol not expected in LoopSpec"; break;
- case 158: s = "this symbol not expected in LoopSpec"; break;
+ case 146: s = "this symbol not expected in OneStmt"; break;
+ case 147: s = "invalid OneStmt"; break;
+ case 148: s = "invalid AssertStmt"; break;
+ case 149: s = "invalid AssumeStmt"; break;
+ case 150: s = "invalid UpdateStmt"; break;
+ case 151: s = "invalid UpdateStmt"; break;
+ case 152: s = "invalid IfStmt"; break;
+ case 153: s = "invalid IfStmt"; break;
+ case 154: s = "invalid WhileStmt"; break;
+ case 155: s = "invalid WhileStmt"; break;
+ case 156: s = "invalid Rhs"; break;
+ case 157: s = "invalid Lhs"; break;
+ case 158: s = "invalid Guard"; break;
case 159: s = "this symbol not expected in LoopSpec"; break;
case 160: s = "this symbol not expected in LoopSpec"; break;
case 161: s = "this symbol not expected in LoopSpec"; break;
- case 162: s = "this symbol not expected in Invariant"; break;
- case 163: s = "invalid AttributeArg"; break;
- case 164: s = "invalid EquivOp"; break;
- case 165: s = "invalid ImpliesOp"; break;
- case 166: s = "invalid AndOp"; break;
- case 167: s = "invalid OrOp"; break;
- case 168: s = "invalid RelOp"; break;
- case 169: s = "invalid AddOp"; break;
- case 170: s = "invalid UnaryExpression"; break;
- case 171: s = "invalid MulOp"; break;
- case 172: s = "invalid NegOp"; break;
- case 173: s = "invalid EndlessExpression"; break;
- case 174: s = "invalid Suffix"; break;
- case 175: s = "invalid Suffix"; break;
+ case 162: s = "this symbol not expected in LoopSpec"; break;
+ case 163: s = "this symbol not expected in LoopSpec"; break;
+ case 164: s = "this symbol not expected in Invariant"; break;
+ case 165: s = "invalid AttributeArg"; break;
+ case 166: s = "invalid EquivOp"; break;
+ case 167: s = "invalid ImpliesOp"; break;
+ case 168: s = "invalid AndOp"; break;
+ case 169: s = "invalid OrOp"; break;
+ case 170: s = "invalid RelOp"; break;
+ case 171: s = "invalid AddOp"; break;
+ case 172: s = "invalid UnaryExpression"; break;
+ case 173: s = "invalid MulOp"; break;
+ case 174: s = "invalid NegOp"; break;
+ case 175: s = "invalid EndlessExpression"; break;
case 176: s = "invalid Suffix"; break;
- case 177: s = "invalid DisplayExpr"; break;
- case 178: s = "invalid MultiSetExpr"; break;
- case 179: s = "invalid MapExpr"; break;
- case 180: s = "invalid ConstAtomExpression"; break;
- case 181: s = "invalid QSep"; break;
- case 182: s = "invalid QuantifierGuts"; break;
- case 183: s = "invalid Forall"; break;
- case 184: s = "invalid Exists"; break;
+ case 177: s = "invalid Suffix"; break;
+ case 178: s = "invalid Suffix"; break;
+ case 179: s = "invalid DisplayExpr"; break;
+ case 180: s = "invalid MultiSetExpr"; break;
+ case 181: s = "invalid MapExpr"; break;
+ case 182: s = "invalid ConstAtomExpression"; break;
+ case 183: s = "invalid QSep"; break;
+ case 184: s = "invalid QuantifierGuts"; break;
+ case 185: s = "invalid Forall"; break;
+ case 186: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index a49a906e..a9064e9a 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -223,7 +223,7 @@ namespace Microsoft.Dafny { Contract.Requires(f != null);
var isPredicate = f is Predicate;
Indent(indent);
- string k = isPredicate ? "predicate" : "function";
+ string k = isPredicate ? "predicate" : f is CoPredicate ? "copredicate" : "function";
if (f.IsStatic) { k = "static " + k; }
if (!f.IsGhost) { k += " method"; }
PrintClassMethodHelper(k, f.Attributes, f.Name, f.TypeArgs);
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 0d32e24e..bc394f04 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -62,13 +62,14 @@ namespace Microsoft.Dafny { private Queue<Action> postTasks = new Queue<Action>(); // empty whenever moduleUnderConstruction==null, these tasks are for the post-resolve phase of module moduleUnderConstruction
public void PreResolve(ModuleDefinition m) {
- Contract.Requires(m != null);
- Contract.Requires(m.RefinementBase != null);
+ if (m.RefinementBase == null) {
+ // This Rewriter doesn't do anything
+ return;
+ }
if (moduleUnderConstruction != null) {
postTasks.Clear();
}
-
moduleUnderConstruction = m;
var prev = m.RefinementBase;
@@ -643,6 +644,9 @@ namespace Microsoft.Dafny { if (f is Predicate) {
return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,
req, reads, ens, decreases, body, moreBody != null, null, false);
+ } else if (f is CoPredicate) {
+ return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,
+ req, reads, ens, body, null, false);
} else {
return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, CloneType(f.ResultType),
req, reads, ens, decreases, body, null, false);
@@ -703,8 +707,9 @@ namespace Microsoft.Dafny { } else if (nwMember is Function) {
var f = (Function)nwMember;
bool isPredicate = f is Predicate;
- string s = isPredicate ? "predicate" : "function";
- if (!(member is Function) || isPredicate && !(member is Predicate)) {
+ bool isCoPredicate = f is CoPredicate;
+ string s = isPredicate ? "predicate" : isCoPredicate ? "copredicate" : "function";
+ if (!(member is Function) || (isPredicate && !(member is Predicate)) || (isCoPredicate && !(member is CoPredicate))) {
reporter.Error(nwMember, "a {0} declaration ({1}) can only refine a {0}", s, nwMember.Name);
} else {
var prevFunction = (Function)member;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 098bcc2e..6d0584c1 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -212,23 +212,16 @@ namespace Microsoft.Dafny { }
// compute IsRecursive bit for mutually recursive functions
foreach (ModuleDefinition m in prog.Modules) {
- foreach (TopLevelDecl decl in m.TopLevelDecls) {
- ClassDecl cl = decl as ClassDecl;
- if (cl != null) {
- foreach (MemberDecl member in cl.Members) {
- Function fn = member as Function;
- if (fn != null && !fn.IsRecursive) { // note, self-recursion has already been determined
- int n = m.CallGraph.GetSCCSize(fn);
- if (2 <= n) {
- // the function is mutually recursive (note, the SCC does not determine self recursion)
- fn.IsRecursive = true;
- }
- }
+ foreach (var fn in ModuleDefinition.AllFunctions(m.TopLevelDecls)) {
+ if (!fn.IsRecursive) { // note, self-recursion has already been determined
+ int n = m.CallGraph.GetSCCSize(fn);
+ if (2 <= n) {
+ // the function is mutually recursive (note, the SCC does not determine self recursion)
+ fn.IsRecursive = true;
}
}
}
}
-
}
@@ -574,6 +567,9 @@ namespace Microsoft.Dafny { if (f is Predicate) {
return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,
req, reads, ens, decreases, body, false, null, false);
+ } else if (f is CoPredicate) {
+ return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,
+ req, reads, ens, body, null, false);
} else {
return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, CloneType(f.ResultType),
req, reads, ens, decreases, body, null, false);
@@ -829,29 +825,25 @@ namespace Microsoft.Dafny { DetermineEqualitySupport(dtd, datatypeDependencies);
}
}
+
if (ErrorCount == prevErrorCount) { // because CheckCoCalls requires the given expression to have been successfully resolved
// Perform the guardedness check on co-datatypes
- foreach (var decl in declarations) {
- var cl = decl as ClassDecl;
- if (cl != null) {
- foreach (var member in cl.Members) {
- var fn = member as Function;
- if (fn != null && fn.Body != null && cl.Module.CallGraph.GetSCCRepresentative(fn) == fn) {
- bool dealsWithCodatatypes = false;
- foreach (var m in cl.Module.CallGraph.GetSCC(fn)) {
- var f = (Function)m;
- if (f.ResultType.InvolvesCoDatatype) {
- dealsWithCodatatypes = true;
- break;
- }
- }
- foreach (var m in cl.Module.CallGraph.GetSCC(fn)) {
- var f = (Function)m;
- var checker = new CoCallResolution(f, dealsWithCodatatypes);
- checker.CheckCoCalls(f.Body);
- }
+ foreach (var fn in ModuleDefinition.AllFunctions(declarations)) {
+ var module = fn.EnclosingClass.Module;
+ if (fn.Body != null && module.CallGraph.GetSCCRepresentative(fn) == fn) {
+ bool dealsWithCodatatypes = false;
+ foreach (var m in module.CallGraph.GetSCC(fn)) {
+ var f = (Function)m;
+ if (f.ResultType.InvolvesCoDatatype) {
+ dealsWithCodatatypes = true;
+ break;
}
}
+ foreach (var m in module.CallGraph.GetSCC(fn)) {
+ var f = (Function)m;
+ var checker = new CoCallResolution(f, dealsWithCodatatypes);
+ checker.CheckCoCalls(f.Body);
+ }
}
}
// Inferred required equality support for datatypes and for Function and Method signatures
@@ -978,9 +970,85 @@ namespace Microsoft.Dafny { }
}
}
+ // Check that copredicates are not recursive with non-copredicate functions.
+ foreach (var fn in ModuleDefinition.AllFunctions(declarations)) {
+ if (fn.Body != null && (fn is CoPredicate || fn.IsRecursive)) {
+ CoPredicateChecks(fn.Body, fn, CallingPosition.Positive);
+ }
+ }
}
}
+ enum CallingPosition { Positive, Negative, Neither }
+
+ static CallingPosition Invert(CallingPosition cp) {
+ switch (cp) {
+ case CallingPosition.Positive: return CallingPosition.Negative;
+ case CallingPosition.Negative: return CallingPosition.Positive;
+ default: return CallingPosition.Neither;
+ }
+ }
+
+ void CoPredicateChecks(Expression expr, Function context, CallingPosition cp) {
+ Contract.Requires(expr != null);
+ Contract.Requires(context != null);
+ if (expr is ConcreteSyntaxExpression) {
+ var e = (ConcreteSyntaxExpression)expr;
+ CoPredicateChecks(e.Resolved, context, cp);
+ return;
+ } else if (expr is FunctionCallExpr) {
+ var e = (FunctionCallExpr)expr;
+ var moduleCaller = context.EnclosingClass.Module;
+ var moduleCallee = e.Function.EnclosingClass.Module;
+ if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(e.Function)) {
+ // we're looking at a recursive call
+ if (context is CoPredicate) {
+ if (!(e.Function is CoPredicate)) {
+ Error(e, "a recursive call from a copredicate can go only to other copredicates");
+ } else if (cp != CallingPosition.Positive) {
+ Error(e, "a recursive copredicate call can only be done in positive positions");
+ }
+ } else if (e.Function is CoPredicate) {
+ Error(e, "a recursive call from a non-copredicate can go only to other non-copredicates");
+ }
+ }
+ // fall through to do the subexpressions
+ } else if (expr is UnaryExpr) {
+ var e = (UnaryExpr)expr;
+ if (e.Op == UnaryExpr.Opcode.Not) {
+ CoPredicateChecks(e.E, context, Invert(cp));
+ return;
+ }
+ } else if (expr is BinaryExpr) {
+ var e = (BinaryExpr)expr;
+ switch (e.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.And:
+ case BinaryExpr.ResolvedOpcode.Or:
+ CoPredicateChecks(e.E0, context, cp);
+ CoPredicateChecks(e.E1, context, cp);
+ return;
+ case BinaryExpr.ResolvedOpcode.Imp:
+ CoPredicateChecks(e.E0, context, Invert(cp));
+ CoPredicateChecks(e.E1, context, cp);
+ return;
+ default:
+ break;
+ }
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ CoPredicateChecks(e.Body, context, cp);
+ return;
+ } else if (expr is QuantifierExpr) {
+ var e = (QuantifierExpr)expr;
+ if (e.Range != null) {
+ CoPredicateChecks(e.Range, context, e is ExistsExpr ? Invert(cp) : cp);
+ }
+ CoPredicateChecks(e.Term, context, cp);
+ return;
+ }
+ expr.SubExpressions.Iter(ee => CoPredicateChecks(ee, context, CallingPosition.Neither));
+ }
+
void CheckEqualityTypes_Stmt(Statement stmt) {
Contract.Requires(stmt != null);
if (stmt.IsGhost) {
@@ -4331,6 +4399,9 @@ namespace Microsoft.Dafny { } else {
Function function = (Function)member;
e.Function = function;
+ if (function is CoPredicate) {
+ ((CoPredicate)function).Uses.Add(e);
+ }
if (e.Receiver is StaticReceiverExpr && !function.IsStatic) {
Error(e, "an instance function must be selected via an object, not just a class name");
}
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index af41a679..4dea968e 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -322,7 +322,7 @@ namespace Microsoft.Dafny return true;
}
- BinaryExpr BinBoolExpr(Boogie.IToken tok, BinaryExpr.ResolvedOpcode rop, Expression e0, Expression e1) {
+ public static BinaryExpr BinBoolExpr(Boogie.IToken tok, BinaryExpr.ResolvedOpcode rop, Expression e0, Expression e1) {
var p = new BinaryExpr(tok, BinaryExpr.ResolvedOp2SyntacticOp(rop), e0, e1);
p.ResolvedOp = rop;
p.Type = Type.Bool;
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 32c92a8b..e2d1b438 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer { public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 107;
- const int noSym = 107;
+ const int maxT = 108;
+ const int noSym = 108;
[ContractInvariantMethod]
@@ -516,33 +516,34 @@ public class Scanner { case "object": t.kind = 44; break;
case "function": t.kind = 45; break;
case "predicate": t.kind = 46; break;
- case "reads": t.kind = 47; break;
- case "label": t.kind = 50; break;
- case "break": t.kind = 51; break;
- case "return": t.kind = 52; break;
- case "assume": t.kind = 55; break;
- case "new": t.kind = 56; break;
- case "choose": t.kind = 59; break;
- case "if": t.kind = 60; break;
- case "else": t.kind = 61; break;
- case "case": t.kind = 62; break;
- case "while": t.kind = 64; break;
- case "invariant": t.kind = 65; break;
- case "match": t.kind = 66; break;
- case "assert": t.kind = 67; break;
- case "print": t.kind = 68; break;
- case "parallel": t.kind = 69; break;
- case "in": t.kind = 82; break;
- case "false": t.kind = 92; break;
- case "true": t.kind = 93; break;
- case "null": t.kind = 94; break;
- case "this": t.kind = 95; break;
- case "fresh": t.kind = 96; break;
- case "allocated": t.kind = 97; break;
- case "old": t.kind = 98; break;
- case "then": t.kind = 99; break;
- case "forall": t.kind = 101; break;
- case "exists": t.kind = 103; break;
+ case "copredicate": t.kind = 47; break;
+ case "reads": t.kind = 48; break;
+ case "label": t.kind = 51; break;
+ case "break": t.kind = 52; break;
+ case "return": t.kind = 53; break;
+ case "assume": t.kind = 56; break;
+ case "new": t.kind = 57; break;
+ case "choose": t.kind = 60; break;
+ case "if": t.kind = 61; break;
+ case "else": t.kind = 62; break;
+ case "case": t.kind = 63; break;
+ case "while": t.kind = 65; break;
+ case "invariant": t.kind = 66; break;
+ case "match": t.kind = 67; break;
+ case "assert": t.kind = 68; break;
+ case "print": t.kind = 69; break;
+ case "parallel": t.kind = 70; break;
+ case "in": t.kind = 83; break;
+ case "false": t.kind = 93; break;
+ case "true": t.kind = 94; break;
+ case "null": t.kind = 95; break;
+ case "this": t.kind = 96; break;
+ case "fresh": t.kind = 97; break;
+ case "allocated": t.kind = 98; break;
+ case "old": t.kind = 99; break;
+ case "then": t.kind = 100; break;
+ case "forall": t.kind = 102; break;
+ case "exists": t.kind = 104; break;
default: break;
}
}
@@ -658,71 +659,71 @@ public class Scanner { case 23:
{t.kind = 31; break;}
case 24:
- {t.kind = 48; break;}
- case 25:
{t.kind = 49; break;}
+ case 25:
+ {t.kind = 50; break;}
case 26:
- {t.kind = 53; break;}
- case 27:
{t.kind = 54; break;}
+ case 27:
+ {t.kind = 55; break;}
case 28:
- {t.kind = 57; break;}
- case 29:
{t.kind = 58; break;}
+ case 29:
+ {t.kind = 59; break;}
case 30:
- {t.kind = 63; break;}
+ {t.kind = 64; break;}
case 31:
if (ch == '>') {AddCh(); goto case 32;}
else {goto case 0;}
case 32:
- {t.kind = 70; break;}
- case 33:
{t.kind = 71; break;}
- case 34:
+ case 33:
{t.kind = 72; break;}
- case 35:
+ case 34:
{t.kind = 73; break;}
+ case 35:
+ {t.kind = 74; break;}
case 36:
if (ch == '&') {AddCh(); goto case 37;}
else {goto case 0;}
case 37:
- {t.kind = 74; break;}
- case 38:
{t.kind = 75; break;}
- case 39:
+ case 38:
{t.kind = 76; break;}
- case 40:
+ case 39:
{t.kind = 77; break;}
+ case 40:
+ {t.kind = 78; break;}
case 41:
- {t.kind = 79; break;}
- case 42:
{t.kind = 80; break;}
- case 43:
+ case 42:
{t.kind = 81; break;}
+ case 43:
+ {t.kind = 82; break;}
case 44:
- {t.kind = 84; break;}
- case 45:
{t.kind = 85; break;}
- case 46:
+ case 45:
{t.kind = 86; break;}
- case 47:
+ case 46:
{t.kind = 87; break;}
- case 48:
+ case 47:
{t.kind = 88; break;}
- case 49:
+ case 48:
{t.kind = 89; break;}
- case 50:
+ case 49:
{t.kind = 90; break;}
- case 51:
+ case 50:
{t.kind = 91; break;}
+ case 51:
+ {t.kind = 92; break;}
case 52:
- {t.kind = 102; break;}
+ {t.kind = 103; break;}
case 53:
- {t.kind = 104; break;}
- case 54:
{t.kind = 105; break;}
- case 55:
+ case 54:
{t.kind = 106; break;}
+ case 55:
+ {t.kind = 107; break;}
case 56:
recEnd = pos; recKind = 5;
if (ch == '=') {AddCh(); goto case 26;}
@@ -751,22 +752,22 @@ public class Scanner { if (ch == '=') {AddCh(); goto case 41;}
else {t.kind = 27; break;}
case 62:
- recEnd = pos; recKind = 83;
+ recEnd = pos; recKind = 84;
if (ch == '=') {AddCh(); goto case 42;}
else if (ch == '!') {AddCh(); goto case 43;}
- else {t.kind = 83; break;}
+ else {t.kind = 84; break;}
case 63:
recEnd = pos; recKind = 24;
if (ch == '>') {AddCh(); goto case 34;}
else {t.kind = 24; break;}
case 64:
- recEnd = pos; recKind = 100;
+ recEnd = pos; recKind = 101;
if (ch == '.') {AddCh(); goto case 23;}
- else {t.kind = 100; break;}
+ else {t.kind = 101; break;}
case 65:
- recEnd = pos; recKind = 78;
+ recEnd = pos; recKind = 79;
if (ch == '=') {AddCh(); goto case 31;}
- else {t.kind = 78; break;}
+ else {t.kind = 79; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 75a1e174..d1dabec7 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -596,6 +596,9 @@ namespace Microsoft.Dafny { }
AddFrameAxiom(f);
AddWellformednessCheck(f);
+ if (f is CoPredicate) {
+ AddCoinductionPrinciple((CoPredicate)f);
+ }
} else if (member is Method) {
Method m = (Method)member;
@@ -706,7 +709,7 @@ namespace Microsoft.Dafny { }
void AddFunctionAxiom(Function/*!*/ f, Expression body, List<Expression/*!*/>/*!*/ ens, Specialization specialization, int layerOffset) {
- if (f is Predicate) {
+ if (f is Predicate || f is CoPredicate) {
var ax = FunctionAxiom(f, FunctionAxiomVisibility.IntraModuleOnly, body, ens, specialization, layerOffset);
sink.TopLevelDeclarations.Add(ax);
ax = FunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, body, ens, specialization, layerOffset);
@@ -865,11 +868,11 @@ namespace Microsoft.Dafny { if (layerOffset == 0) {
meat = Bpl.Expr.And(
CanCallAssumption(bodyWithSubst, etran),
- visibility == FunctionAxiomVisibility.ForeignModuleOnly && f is Predicate ?
+ visibility == FunctionAxiomVisibility.ForeignModuleOnly && (f is Predicate || f is CoPredicate) ?
Bpl.Expr.Imp(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)) :
Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)));
} else {
- meat = visibility == FunctionAxiomVisibility.ForeignModuleOnly && f is Predicate ?
+ meat = visibility == FunctionAxiomVisibility.ForeignModuleOnly && (f is Predicate || f is CoPredicate) ?
Bpl.Expr.Imp(funcAppl, etran.TrExpr(bodyWithSubst)) :
Bpl.Expr.Eq(funcAppl, etran.TrExpr(bodyWithSubst));
}
@@ -2376,7 +2379,7 @@ namespace Microsoft.Dafny { CheckFrameSubset(expr.tok, e.Function.Reads, e.Receiver, substMap, etran, builder, "insufficient reads clause to invoke function", options.AssertKv);
}
- if (options.Decr != null && e.CoCall != FunctionCallExpr.CoCallResolution.Yes) {
+ if (options.Decr != null && e.CoCall != FunctionCallExpr.CoCallResolution.Yes && !(e.Function is CoPredicate)) {
// check that the decreases measure goes down
ModuleDefinition module = cce.NonNull(e.Function.EnclosingClass).Module;
if (module == cce.NonNull(options.Decr.EnclosingClass).Module) {
@@ -7463,6 +7466,229 @@ namespace Microsoft.Dafny { }
}
+ void AddCoinductionPrinciple(CoPredicate coPredicate) {
+ Contract.Requires(coPredicate != null);
+ if (coPredicate.Body == null) {
+ return; // we can't generate any useful coinduction principle if the copredicate doesn't have a body
+ } else if (2 <= coPredicate.EnclosingClass.Module.CallGraph.GetSCCSize(coPredicate)) {
+ return; // this copredicate involves mutually recursive calls; for now, we don't handle those
+ }
+ var n = (coPredicate.IsStatic ? 0 : 1) + coPredicate.Formals.Count;
+ var templates = new List<FunctionCallExpr[/*of length n*/]>();
+ foreach (var fce in coPredicate.Uses) {
+ // Compute a template of instantiation for this use: for each actual argument, record
+ // a function F if the argument is a call to F, or record null otherwise.
+ var t = new FunctionCallExpr[n];
+ var i = 0;
+ if (!coPredicate.IsStatic) {
+ t[i] = fce.Receiver.Resolved as FunctionCallExpr;
+ i++;
+ }
+ foreach (var a in fce.Args) {
+ t[i] = a.Resolved as FunctionCallExpr;
+ i++;
+ }
+ Contract.Assert(i == t.Length);
+ // See if this template has been done before (for now, this is a slow check; it would be nice to speed it up)
+ foreach (var prev in templates) {
+ var j = 0;
+ for (; j < n; j++) {
+ if (prev[j] == null && t[j] == null) {
+ // things are equal
+ } else if (prev[j] != null && t[j] != null && prev[j].Function == t[j].Function) {
+ // things are equal
+ } else {
+ // we found an unequal part of the template
+ break;
+ }
+ }
+ if (j == n) {
+ // template 't' matches 'prev', so we've already spilled out an axiom for this template
+ // TODO: this is not the complete test, because of possible type parameters
+ goto Next_Use;
+ }
+ // 't' does not match this 'prev'; try the next 'prev'
+ }
+ // No 'prev' matches the current template 't'. So, generate an axiom for 't'.
+ string comment = string.Format("Coinduction principle for copredicate {0} instantiated like:", coPredicate.FullName);
+ foreach (var tf in t) {
+ comment += tf == null ? " ." : " " + tf.Name;
+ }
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(fce.tok, CoinductionPrinciple(coPredicate, fce, t), comment));
+ templates.Add(t);
+ Next_Use: ;
+ }
+ }
+
+ /// <summary>
+ /// It's the "callOfInterest" that determines the (type-parameter instantiated) types of the arguments
+ /// </summary>
+ Bpl.Expr CoinductionPrinciple(CoPredicate coPredicate, FunctionCallExpr callOfInterest, FunctionCallExpr[] t) {
+ Contract.Requires(coPredicate != null);
+ Contract.Requires(coPredicate.Body != null);
+ Contract.Requires(t != null);
+ Contract.Requires(t.Length == (coPredicate.IsStatic ? 0 : 1) + coPredicate.Formals.Count);
+ // Let C be the name of the coPredicate, and suppose it is defined by:
+ // copredicate C(x)
+ // requires PreC(x);
+ // {
+ // Body[C]
+ // }
+ // where the notation Body[_] means an expression Body with holes and in particular one whole
+ // for every recursive use of C.
+ // The general form of the coinduction principle of which we will generate an instance is:
+ // forall P ::
+ // forall s :: // where s is a list of arguments to coPredicate
+ // P(s) &&
+ // (forall s' :: P(s') ==> Body[P][x := s'])
+ // ==>
+ // C(s)
+ // We will pick particular P's, and will therefore instead generate the axiom once for each
+ // such P. We will also redistribute the terms as follows:
+ // (forall s :: P(s) ==> Body[P][x := s])
+ // ==>
+ // (forall s :: P(s) ==> C(s))
+ // Furthermore, if the C of interest has actual parameters that are function-call expressions,
+ // then the P will be chosen to fit that pattern. As a specific example, suppose C takes 3
+ // parameters (that is, 's' is a triple (s0,s1,s2)) and that the actual arguments for these, in
+ // the C use of interest, are of the form C(E0,F(E1),G(E2,E3)), where E0 denotes an expression that
+ // is not a function-call expression and E1,E2,E3 are any expressions. Also, suppose the
+ // preconditions of C,F,G are PreC(s0,s1,s2), PreF(f), PreG(g0,g1).
+ // Then, we pick P(s0,s1,s2) :=
+ // exists a,b,c,d :: PreF(b) && PreG(c,d) && PredC(a,F(b),G(c,d)) && (s0,s1,s2) == (a,F(b),G(c,d))
+ // So, the axiom looks like:
+ // (forall a,b,c,d :: PreF(b) && PreG(c,d) && PredC(a,F(b),G(c,d))
+ // ==> Body[P][x0,x1,x2 := a,F(b),G(c,d)])
+ // ==>
+ // (forall a,b,c,d { C(a,F(b),G(c,d)) } ::
+ // PreF(b) && PreG(c,d) && PredC(a,F(b),G(c,d))
+ // ==> C(a,F(b),G(c,d)))
+ //
+ // To be usable, we need to do more. In particular, we need to do some preprocessing of the expressions
+ // of the form C(E0,E1,E2) in Body, which are turned into P(E0,E1,E2) in Body[P] (where these are any
+ // expressions E0,E1,E2, not necessarily the ones as above). We know that such C(E0,E1,E2) occurrences
+ // sit only in positive positions. Hence, we can soundly replace each (exists a,b,c,d :: Q(a,b,c,d))
+ // expressions in Body[P] in the axiom with Q(A,B,C,D) for any A,B,C,D. For this to be useful, we need
+ // good guesses for A,B,C,D.
+ //
+ // TODO: also need a module/function-height antecedent for the axiom!
+ var tok = coPredicate.tok;
+ var bvs = new Bpl.VariableSeq();
+ Bpl.BoundVariable heapVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$h", predef.HeapType));
+ bvs.Add(heapVar);
+ var bHeap = new Bpl.IdentifierExpr(tok, heapVar);
+ Bpl.Expr typeAntecedents = FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, bHeap);
+ var etran = new ExpressionTranslator(this, predef, bHeap);
+ Expression pre = new LiteralExpr(tok, true);
+ var i = 0;
+ Expression receiverReplacement = null;
+ if (!coPredicate.IsStatic) {
+ Expression preF;
+ receiverReplacement = FG(tok, callOfInterest.Receiver.Type, t[i], bvs, ref typeAntecedents, out preF, etran);
+ typeAntecedents = BplAnd(typeAntecedents, Bpl.Expr.Neq(etran.TrExpr(receiverReplacement), predef.Null));
+ if (preF != null) {
+ pre = AutoContractsRewriter.BinBoolExpr(receiverReplacement.tok, BinaryExpr.ResolvedOpcode.And, pre, preF);
+ }
+ i++;
+ }
+ var substMap = new Dictionary<IVariable, Expression>();
+ var j = 0;
+ foreach (var p in coPredicate.Formals) {
+ Expression preF;
+ var e = FG(tok, callOfInterest.Args[j].Type, t[i], bvs, ref typeAntecedents, out preF, etran);
+ substMap.Add(p, e);
+ if (preF != null) {
+ pre = AutoContractsRewriter.BinBoolExpr(e.tok, BinaryExpr.ResolvedOpcode.And, pre, preF);
+ }
+ i++; j++;
+ }
+ // conjoin subst(preC) to pre
+ foreach (var req in coPredicate.Req) {
+ var preC = Substitute(req, receiverReplacement, substMap);
+ pre = AutoContractsRewriter.BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, pre, preC);
+ }
+ // build up the term C(a,F(b),G(c,d))
+ var args = new List<Expression>();
+ foreach (var p in coPredicate.Formals) {
+ args.Add(substMap[p]);
+ }
+ var C = new FunctionCallExpr(tok, coPredicate.Name, receiverReplacement, tok, args);
+ C.Function = coPredicate;
+ C.Type = coPredicate.ResultType;
+ // We are now ready to produce the Conclusion of the axiom
+ var preStuff = Bpl.Expr.And(typeAntecedents, etran.TrExpr(pre));
+ Bpl.Expr Conclusion = new Bpl.ForallExpr(tok, bvs, new Bpl.Trigger(tok, true, new ExprSeq(etran.TrExpr(C))),
+ Bpl.Expr.Imp(preStuff, etran.TrExpr(C)));
+ // Now for the antecedent of the axiom
+ // TODO: if e.Body uses a 'match' expression, first desugar it into an ordinary expression
+ var s = new CoinductionSubstituter(receiverReplacement, substMap, coPredicate);
+ var body = s.Substitute(coPredicate.Body);
+ // TODO: replace C(...) with P(...) in "body"
+ Bpl.Expr Antecedent = new Bpl.ForallExpr(tok, bvs, Bpl.Expr.Imp(preStuff, etran.TrExpr(body)));
+ // Put it all together and we're ready to go
+ return Bpl.Expr.Imp(Antecedent, Conclusion);
+ }
+
+ /// <summary>
+ /// "templateFunc" is passed in as "null", then "precondition" is guaranteed to come out as "null".
+ /// </summary>
+ Expression FG(IToken tok, Type argumentType, FunctionCallExpr templateFunc, Bpl.VariableSeq bvs, ref Bpl.Expr typeAntecedents, out Expression precondition, ExpressionTranslator etran) {
+ Contract.Requires(tok != null);
+ Contract.Requires(argumentType != null);
+ Contract.Requires(bvs != null);
+ Contract.Requires(etran != null);
+ Contract.Ensures(Contract.Result<Expression>() != null);
+ Contract.Ensures(Contract.ValueAtReturn<Expression>(out precondition) != null);
+ // TODO: also need to return type antecedents
+ precondition = new LiteralExpr(tok, true);
+ if (templateFunc == null) {
+ // generate a fresh variable of type "argumentType"
+ BoundVar k = new BoundVar(tok, "_coind" + otherTmpVarCount, argumentType);
+ otherTmpVarCount++;
+ // convert it to a Boogie variable and add it to "bvs"
+ var bvar = new Bpl.BoundVariable(k.tok, new Bpl.TypedIdent(k.tok, k.UniqueName, TrType(k.Type)));
+ bvs.Add(bvar);
+ // update typeAntecedents
+ var wh = GetWhereClause(k.tok, new Bpl.IdentifierExpr(k.tok, bvar), k.Type, etran);
+ if (wh != null) {
+ typeAntecedents = BplAnd(typeAntecedents, wh);
+ }
+ // make an IdentifierExpr out of it and return it
+ IdentifierExpr ie = new IdentifierExpr(k.tok, k.UniqueName);
+ ie.Var = k; ie.Type = ie.Var.Type; // resolve it here
+ return ie;
+
+ } else {
+ // for each formal parameter to "templateFunc", generate a fresh variable
+ // for each one, convert it to a Boogie variable and add it to "bvs"
+ // make a FunctionCallExpr, passing in these variables as arguments, and then returning the FunctionCallExpr
+ Expression preIgnore;
+ Expression receiver = null;
+ if (!templateFunc.Function.IsStatic) {
+ receiver = FG(tok, templateFunc.Receiver.Type, null, bvs, ref typeAntecedents, out preIgnore, etran);
+ typeAntecedents = BplAnd(typeAntecedents, Bpl.Expr.Neq(etran.TrExpr(receiver), predef.Null));
+ }
+ var args = new List<Expression>();
+ var i = 0;
+ var substMap = new Dictionary<IVariable, Expression>();
+ foreach (var arg in templateFunc.Args) {
+ var e = FG(tok, arg.Type, null, bvs, ref typeAntecedents, out preIgnore, etran);
+ args.Add(e);
+ substMap.Add(templateFunc.Function.Formals[i], e);
+ i++;
+ }
+ var F = new FunctionCallExpr(tok, templateFunc.Name, receiver, tok, args);
+ F.Function = templateFunc.Function;
+ F.Type = templateFunc.Function.ResultType;
+
+ foreach (var req in templateFunc.Function.Req) {
+ var pre = Substitute(req, receiver, substMap);
+ precondition = AutoContractsRewriter.BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, precondition, pre);
+ }
+ return F;
+ }
+ }
+
/// <summary>
/// Returns true iff 'v' occurs as a free variable in 'expr'.
/// Parameter 'v' is allowed to be a ThisSurrogate, in which case the method return true iff 'this'
@@ -7507,6 +7733,298 @@ namespace Microsoft.Dafny { Contract.Requires(expr != null);
Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
Contract.Ensures(Contract.Result<Expression>() != null);
+ var s = new Substituter(receiverReplacement, substMap);
+ return s.Substitute(expr);
+ }
+
+ public class CoinductionSubstituter : Substituter
+ {
+ CoPredicate coPredicate;
+ public CoinductionSubstituter(Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, CoPredicate coPredicate)
+ : base(receiverReplacement, substMap)
+ {
+ Contract.Requires(substMap != null);
+ Contract.Requires(coPredicate != null);
+ this.coPredicate = coPredicate;
+ }
+ public override Expression Substitute(Expression expr) {
+ if (expr is FunctionCallExpr) {
+ var e = (FunctionCallExpr)expr;
+ if (e.Function == coPredicate) {
+ // TODO
+ return new LiteralExpr(e.tok, true); // BOGUS
+ }
+ }
+ return base.Substitute(expr);
+ }
+ }
+
+ public class Substituter
+ {
+ public readonly Expression receiverReplacement;
+ public readonly Dictionary<IVariable, Expression/*!*/>/*!*/ substMap;
+ public Substituter(Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {
+ Contract.Requires(substMap != null);
+ this.receiverReplacement = receiverReplacement;
+ this.substMap = substMap;
+ }
+ public virtual Expression Substitute(Expression expr) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<Expression>() != null);
+
+ Expression newExpr = null; // set to non-null value only if substitution has any effect; if non-null, newExpr will be resolved at end
+
+ if (expr is LiteralExpr || expr is WildcardExpr || expr is BoogieWrapper) {
+ // nothing to substitute
+ } else if (expr is ThisExpr) {
+ return receiverReplacement == null ? expr : receiverReplacement;
+ } else if (expr is IdentifierExpr) {
+ IdentifierExpr e = (IdentifierExpr)expr;
+ Expression substExpr;
+ if (substMap.TryGetValue(e.Var, out substExpr)) {
+ return cce.NonNull(substExpr);
+ }
+ } else if (expr is DisplayExpression) {
+ DisplayExpression e = (DisplayExpression)expr;
+ List<Expression> newElements = SubstituteExprList(e.Elements);
+ if (newElements != e.Elements) {
+ if (expr is SetDisplayExpr) {
+ newExpr = new SetDisplayExpr(expr.tok, newElements);
+ } else if (expr is MultiSetDisplayExpr) {
+ newExpr = new MultiSetDisplayExpr(expr.tok, newElements);
+ } else {
+ newExpr = new SeqDisplayExpr(expr.tok, newElements);
+ }
+ }
+
+ } else if (expr is FieldSelectExpr) {
+ FieldSelectExpr fse = (FieldSelectExpr)expr;
+ Expression substE = Substitute(fse.Obj);
+ if (substE != fse.Obj) {
+ FieldSelectExpr fseNew = new FieldSelectExpr(fse.tok, substE, fse.FieldName);
+ fseNew.Field = fse.Field; // resolve on the fly (and fseExpr.Type is set at end of method)
+ newExpr = fseNew;
+ }
+
+ } else if (expr is SeqSelectExpr) {
+ SeqSelectExpr sse = (SeqSelectExpr)expr;
+ Expression seq = Substitute(sse.Seq);
+ Expression e0 = sse.E0 == null ? null : Substitute(sse.E0);
+ Expression e1 = sse.E1 == null ? null : Substitute(sse.E1);
+ if (seq != sse.Seq || e0 != sse.E0 || e1 != sse.E1) {
+ newExpr = new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);
+ }
+
+ } else if (expr is SeqUpdateExpr) {
+ SeqUpdateExpr sse = (SeqUpdateExpr)expr;
+ Expression seq = Substitute(sse.Seq);
+ Expression index = Substitute(sse.Index);
+ Expression val = Substitute(sse.Value);
+ if (seq != sse.Seq || index != sse.Index || val != sse.Value) {
+ newExpr = new SeqUpdateExpr(sse.tok, seq, index, val);
+ }
+
+ } else if (expr is MultiSelectExpr) {
+ MultiSelectExpr mse = (MultiSelectExpr)expr;
+ Expression array = Substitute(mse.Array);
+ List<Expression> newArgs = SubstituteExprList(mse.Indices);
+ if (array != mse.Array || newArgs != mse.Indices) {
+ newExpr = new MultiSelectExpr(mse.tok, array, newArgs);
+ }
+
+ } else if (expr is FunctionCallExpr) {
+ FunctionCallExpr e = (FunctionCallExpr)expr;
+ Expression receiver = Substitute(e.Receiver);
+ List<Expression> newArgs = SubstituteExprList(e.Args);
+ if (receiver != e.Receiver || newArgs != e.Args) {
+ FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs);
+ newFce.Function = e.Function; // resolve on the fly (and set newFce.Type below, at end)
+ newExpr = newFce;
+ }
+
+ } else if (expr is DatatypeValue) {
+ DatatypeValue dtv = (DatatypeValue)expr;
+ List<Expression> newArgs = SubstituteExprList(dtv.Arguments);
+ if (newArgs != dtv.Arguments) {
+ DatatypeValue newDtv = new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArgs);
+ newDtv.Ctor = dtv.Ctor; // resolve on the fly (and set newDtv.Type below, at end)
+ newExpr = newDtv;
+ }
+
+ } else if (expr is OldExpr) {
+ OldExpr e = (OldExpr)expr;
+ // Note, it is up to the caller to avoid variable capture. In most cases, this is not a
+ // problem, since variables have unique declarations. However, it is an issue if the substitution
+ // takes place inside an OldExpr. In those cases (see LetExpr), the caller can use a
+ // BoogieWrapper before calling Substitute.
+ Expression se = Substitute(e.E);
+ if (se != e.E) {
+ newExpr = new OldExpr(expr.tok, se);
+ }
+ } else if (expr is FreshExpr) {
+ FreshExpr e = (FreshExpr)expr;
+ Expression se = Substitute(e.E);
+ if (se != e.E) {
+ newExpr = new FreshExpr(expr.tok, se);
+ }
+ } else if (expr is AllocatedExpr) {
+ AllocatedExpr e = (AllocatedExpr)expr;
+ Expression se = Substitute(e.E);
+ if (se != e.E) {
+ newExpr = new AllocatedExpr(expr.tok, se);
+ }
+ } else if (expr is UnaryExpr) {
+ UnaryExpr e = (UnaryExpr)expr;
+ Expression se = Substitute(e.E);
+ if (se != e.E) {
+ newExpr = new UnaryExpr(expr.tok, e.Op, se);
+ }
+ } else if (expr is BinaryExpr) {
+ BinaryExpr e = (BinaryExpr)expr;
+ Expression e0 = Substitute(e.E0);
+ Expression e1 = Substitute(e.E1);
+ if (e0 != e.E0 || e1 != e.E1) {
+ BinaryExpr newBin = new BinaryExpr(expr.tok, e.Op, e0, e1);
+ newBin.ResolvedOp = e.ResolvedOp; // part of what needs to be done to resolve on the fly (newBin.Type is set below, at end)
+ newExpr = newBin;
+ }
+
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ var rhss = new List<Expression>();
+ bool anythingChanged = false;
+ foreach (var rhs in e.RHSs) {
+ var r = Substitute(rhs);
+ if (r != rhs) {
+ anythingChanged = true;
+ }
+ rhss.Add(r);
+ }
+ var body = Substitute(e.Body);
+ if (anythingChanged || body != e.Body) {
+ newExpr = new LetExpr(e.tok, e.Vars, rhss, body);
+ }
+
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ Expression newRange = e.Range == null ? null : Substitute(e.Range);
+ Expression newTerm = Substitute(e.Term);
+ Attributes newAttrs = SubstAttributes(e.Attributes);
+ if (e is SetComprehension) {
+ if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {
+ newExpr = new SetComprehension(expr.tok, e.BoundVars, newRange, newTerm);
+ }
+ } else if (e is MapComprehension) {
+ if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {
+ newExpr = new MapComprehension(expr.tok, e.BoundVars, newRange, newTerm);
+ }
+ } else if (e is QuantifierExpr) {
+ var q = (QuantifierExpr)e;
+ if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {
+ if (expr is ForallExpr) {
+ newExpr = new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);
+ } else {
+ newExpr = new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);
+ }
+ }
+ } else {
+ Contract.Assert(false); // unexpected ComprehensionExpr
+ }
+
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ Expression g = Substitute(e.Guard);
+ Expression b = Substitute(e.Body);
+ if (g != e.Guard || b != e.Body) {
+ if (expr is AssertExpr) {
+ newExpr = new AssertExpr(e.tok, g, b);
+ } else {
+ newExpr = new AssumeExpr(e.tok, g, b);
+ }
+ }
+
+ } else if (expr is ITEExpr) {
+ ITEExpr e = (ITEExpr)expr;
+ Expression test = Substitute(e.Test);
+ Expression thn = Substitute(e.Thn);
+ Expression els = Substitute(e.Els);
+ if (test != e.Test || thn != e.Thn || els != e.Els) {
+ newExpr = new ITEExpr(expr.tok, test, thn, els);
+ }
+
+ } else if (expr is ConcreteSyntaxExpression) {
+ var e = (ConcreteSyntaxExpression)expr;
+ return Substitute(e.ResolvedExpression);
+ }
+
+ if (newExpr == null) {
+ return expr;
+ } else {
+ newExpr.Type = expr.Type; // resolve on the fly (any additional resolution must be done above)
+ return newExpr;
+ }
+ }
+
+ List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist) {
+ Contract.Requires(cce.NonNullElements(elist));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));
+
+ List<Expression> newElist = null; // initialized lazily
+ for (int i = 0; i < elist.Count; i++) {
+ cce.LoopInvariant(newElist == null || newElist.Count == i);
+
+ Expression substE = Substitute(elist[i]);
+ if (substE != elist[i] && newElist == null) {
+ newElist = new List<Expression>();
+ for (int j = 0; j < i; j++) {
+ newElist.Add(elist[j]);
+ }
+ }
+ if (newElist != null) {
+ newElist.Add(substE);
+ }
+ }
+ if (newElist == null) {
+ return elist;
+ } else {
+ return newElist;
+ }
+ }
+
+ Attributes SubstAttributes(Attributes attrs) {
+ Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
+ if (attrs != null) {
+ List<Attributes.Argument> newArgs = new List<Attributes.Argument>(); // allocate it eagerly, what the heck, it doesn't seem worth the extra complexity in the code to do it lazily for the infrequently occurring attributes
+ bool anyArgSubst = false;
+ foreach (Attributes.Argument arg in attrs.Args) {
+ Attributes.Argument newArg = arg;
+ if (arg.E != null) {
+ Expression newE = Substitute(arg.E);
+ if (newE != arg.E) {
+ newArg = new Attributes.Argument(arg.Tok, newE);
+ anyArgSubst = true;
+ }
+ }
+ newArgs.Add(newArg);
+ }
+ if (!anyArgSubst) {
+ newArgs = attrs.Args;
+ }
+
+ Attributes prev = SubstAttributes(attrs.Prev);
+ if (newArgs != attrs.Args || prev != attrs.Prev) {
+ return new Attributes(attrs.Name, newArgs, prev);
+ }
+ }
+ return attrs;
+ }
+ }
+
+#if OLD_SUBSTITUTE
+ public static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {
+ Contract.Requires(expr != null);
+ Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
+ Contract.Ensures(Contract.Result<Expression>() != null);
Expression newExpr = null; // set to non-null value only if substitution has any effect; if non-null, newExpr will be resolved at end
@@ -7756,6 +8274,7 @@ namespace Microsoft.Dafny { }
return attrs;
}
+#endif
}
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 85958099..7879483d 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1273,7 +1273,11 @@ Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
-4 resolution/type errors detected in Coinductive.dfy
+Coinductive.dfy(90,8): Error: a recursive copredicate call can only be done in positive positions
+Coinductive.dfy(91,8): Error: a recursive copredicate call can only be done in positive positions
+Coinductive.dfy(92,8): Error: a recursive copredicate call can only be done in positive positions
+Coinductive.dfy(92,21): Error: a recursive copredicate call can only be done in positive positions
+8 resolution/type errors detected in Coinductive.dfy
-------------------- Corecursion.dfy --------------------
Corecursion.dfy(15,13): Error: failure to decrease termination measure (note that only functions without side effects can called co-recursively)
diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy index 35f17c1c..431d6bb1 100644 --- a/Test/dafny0/Coinductive.dfy +++ b/Test/dafny0/Coinductive.dfy @@ -62,4 +62,45 @@ module TestCoinductiveDatatypes }
+// --------------- CoPredicates --------------------------
+
+module CoPredicateResolutionErrors {
+
+ codatatype Stream<T> = StreamCons(head: T, tail: Stream);
+
+ function Upward(n: int): Stream<int>
+ {
+ StreamCons(n, Upward(n + 1))
+ }
+
+ function Doubles(n: int): Stream<int>
+ {
+ StreamCons(2*n, Doubles(n + 1))
+ }
+
+ copredicate Pos(s: Stream<int>)
+ {
+ 0 < s.head && Pos(s.tail) && Even(s)
+ }
+
+ copredicate Even(s: Stream<int>)
+ {
+ s.head % 2 == 0 && Even(s.tail)
+ && (s.head == 17 ==> Pos(s))
+ && (Pos(s) ==> s.head == 17) // error: cannot make recursive copredicate call in negative position
+ && !Even(s) // error: cannot make recursive copredicate call in negative position
+ && (Even(s) <==> Even(s)) // error (x2): recursive copredicate calls allowed only in positive positions
+ }
+
+ copredicate Another(s: Stream<int>)
+ {
+ !Even(s) // here, negation is fine
+ }
+
+ ghost method Lemma(n: int)
+ ensures Even(Doubles(n));
+ {
+ }
+}
+
// --------------------------------------------------
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 05f06b41..cf2b357f 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -30,7 +30,8 @@ ]\\)*" . font-lock-comment-face)
`(,(dafny-regexp-opt '(
- "class" "datatype" "codatatype" "type" "function" "predicate" "ghost" "var" "method" "constructor"
+ "class" "datatype" "codatatype" "type" "function" "predicate" "copredicate"
+ "ghost" "var" "method" "constructor"
"module" "imports" "static" "refines"
"returns" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 627353bf..01767ca6 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -24,7 +24,7 @@ namespace Demo "break", "label", "return", "parallel", "havoc", "print",
"returns", "requires", "ensures", "modifies", "reads", "decreases",
"bool", "nat", "int", "false", "true", "null",
- "function", "predicate", "free",
+ "function", "predicate", "copredicate", "free",
"in", "forall", "exists",
"seq", "set", "map", "multiset", "array", "array2", "array3",
"match", "case",
@@ -303,6 +303,7 @@ namespace Demo | "null"
| "function"
| "predicate"
+ | "copredicate"
| "free"
| "in"
| "forall"
@@ -358,53 +359,6 @@ namespace Demo | stringLiteral
;
- idType.Rule
- = ident + ":" + typeDecl
- | ident
- ;
-
- typeDecl.Rule
- = (ToTerm("int") | "nat" | "bool" | ident | "seq" | "set" | "array") + (("<" + MakePlusRule(typeDecl, ToTerm(","), typeDecl) + ">") | Empty)
- | ToTerm("token") + "<" + (typeDecl + ".") + ident + ">"
- ;
-
- fieldDecl.Rule
- = ToTerm("var") + idType + Semi
- | ToTerm("ghost") + "var" + idType + Semi
- ;
-
- methodSpec.Rule = (ToTerm("requires") | "ensures" | "lockchange") + expression + Semi;
-
- formalsList.Rule = MakeStarRule(formalsList, comma, idType);
- formalParameters.Rule = LParen + formalsList + RParen;
- methodDecl.Rule = "method" + ident + formalParameters
- + (("returns" + formalParameters) | Empty)
- + methodSpec.Star()
- + blockStatement;
- functionDecl.Rule
- = ToTerm("function") + ident + formalParameters + ":" + typeDecl + methodSpec.Star() + "{" + expression + "}";
- predicateDecl.Rule
- = ToTerm("predicate") + ident + "{" + expression + "}";
- invariantDecl.Rule
- = ToTerm("invariant") + expression + Semi;
-
- memberDecl.Rule
- = fieldDecl
- | invariantDecl
- | methodDecl
- //| conditionDecl
- | predicateDecl
- | functionDecl
- ;
- classDecl.Rule
- = (ToTerm("external") | Empty) + "class" + ident + ("module" + ident | Empty) + "{" + memberDecl.Star() + "}";
- channelDecl.Rule
- = ToTerm("channel") + ident + formalParameters + "where" + expression + Semi
- | ToTerm("channel") + ident + formalParameters + Semi;
- declaration.Rule = classDecl | channelDecl
- ;
-
-
Terminal Comment = new CommentTerminal("Comment", "/*", "*/");
NonGrammarTerminals.Add(Comment);
Terminal LineComment = new CommentTerminal("LineComment", "//", "\n");
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index d621b1a9..80976499 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -244,6 +244,7 @@ namespace DafnyLanguage case "class":
case "codatatype":
case "constructor":
+ case "copredicate":
case "datatype":
case "decreases":
case "else":
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index af789102..cfd8863f 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -6,7 +6,7 @@ \lstdefinelanguage{dafny}{
morekeywords={class,datatype,codatatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,%
- function,predicate,
+ function,predicate,copredicate,
ghost,var,static,refines,
method,constructor,returns,module,imports,in,
requires,modifies,ensures,reads,decreases,free,
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index 6af28094..33d447fe 100644 --- a/Util/vim/syntax/dafny.vim +++ b/Util/vim/syntax/dafny.vim @@ -5,7 +5,7 @@ syntax clear syntax case match -syntax keyword dafnyFunction function predicate method constructor +syntax keyword dafnyFunction function predicate copredicate method constructor syntax keyword dafnyTypeDef class datatype codatatype type syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat while parallel |