diff options
| -rw-r--r-- | Source/Dafny/Dafny.atg | 51 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.ssc | 50 | ||||
| -rw-r--r-- | Source/Dafny/Parser.ssc | 1000 | ||||
| -rw-r--r-- | Source/Dafny/Printer.ssc | 28 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.ssc | 97 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.ssc | 208 | ||||
| -rw-r--r-- | Source/Dafny/Translator.ssc | 191 |
7 files changed, 1027 insertions, 598 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index d69bf19a..6ae97b5c 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -183,16 +183,25 @@ ClassDecl<ModuleDecl! module, out ClassDecl! c> = (. IToken! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
+ IToken! idRefined;
+ IToken optionalId = null;
List<MemberDecl!> members = new List<MemberDecl!>();
.)
"class"
{ Attribute<ref attrs> }
Ident<out id>
[ GenericParameters<typeArgs> ]
+ [ "refines" Ident<out idRefined> (. optionalId = idRefined; .)
+ ]
"{"
{ ClassMemberDecl<members>
}
- "}" (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs); .)
+ "}"
+ (. if (optionalId == null)
+ c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
+ else
+ c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);
+ .)
.
ClassMemberDecl<.List<MemberDecl!>! mm.>
@@ -204,9 +213,10 @@ ClassMemberDecl<.List<MemberDecl!>! mm.> | "static" (. mmod.IsStatic = true; .)
| "unlimited" (. mmod.IsUnlimited = true; .)
}
- ( FieldDecl<mmod, mm>
+ ( FieldDecl<mmod, mm>
| FunctionDecl<mmod, out f> (. mm.Add(f); .)
| MethodDecl<mmod, out m> (. mm.Add(m); .)
+ | CouplingInvDecl<mmod, mm>
)
.
@@ -258,6 +268,31 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl!>! mm.> ";"
.
+CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl!>! mm.>
+= (. Attributes attrs = null;
+ List<IToken!> ids = new List<IToken!>();;
+ IToken! id;
+ Expression! e;
+ parseVarScope.PushMarker();
+ .)
+ "replaces"
+ (. if (mmod.IsUnlimited) { SemErr(t, "coupling invariants cannot be declared 'unlimited'"); }
+ if (mmod.IsStatic) { SemErr(t, "coupling invariants cannot be declared 'static'"); }
+ if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }
+ .)
+ { Attribute<ref attrs> }
+ Ident<out id> (. ids.Add(id); parseVarScope.Push(id.val, id.val); .)
+ { "," Ident<out id> (. ids.Add(id); parseVarScope.Push(id.val, id.val); .)
+ }
+ "by"
+ Expression<out e>
+ ";"
+ (. mm.Add(new CouplingInvariant(ids, e, attrs));
+ parseVarScope.PopMarker();
+ .)
+ .
+
+
GIdentType<bool allowGhost, out IToken! id, out Type! ty, out bool isGhost>
/* isGhost always returns as false if allowGhost is false */
= (. isGhost = false; .)
@@ -329,8 +364,11 @@ MethodDecl<MemberModifiers mmod, out Method! m> List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();
List<Expression!> dec = new List<Expression!>();
Statement! bb; BlockStmt body = null;
+ bool isRefinement = false;
.)
- "method"
+ ( "method"
+ | "refines" (. isRefinement = true; .)
+ )
(. if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
.)
{ Attribute<ref attrs> }
@@ -347,8 +385,11 @@ MethodDecl<MemberModifiers mmod, out Method! m> )
(. parseVarScope.PopMarker();
- m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
- .)
+ if (isRefinement)
+ m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
+ else
+ m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
+ .)
.
MethodSpec<.List<MaybeFreeExpression!>! req, List<FrameExpression!>! mod, List<MaybeFreeExpression!>! ens,
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc index 1d9dfd1c..b5f21655 100644 --- a/Source/Dafny/DafnyAst.ssc +++ b/Source/Dafny/DafnyAst.ssc @@ -4,6 +4,7 @@ //
//-----------------------------------------------------------------------------
using System;
+using System.Text;
using System.Collections.Generic;
using Microsoft.Contracts;
using System.Numerics;
@@ -438,6 +439,15 @@ namespace Microsoft.Dafny }
}
+ public class ClassRefinementDecl : ClassDecl {
+ public readonly IToken! RefinedClass;
+ public ClassDecl Refined; // filled in during resolution
+ public ClassRefinementDecl(IToken! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, [Captured] List<MemberDecl!>! members, Attributes attributes, IToken! refinedClass) {
+ RefinedClass = refinedClass;
+ base(tok, name, module, typeArgs, members, attributes);
+ }
+ }
+
public class DefaultClassDecl : ClassDecl {
public DefaultClassDecl(DefaultModuleDecl! module, [Captured] List<MemberDecl!>! members) {
base(Token.NoToken, "_default", module, new List<TypeParameter!>(), members, null);
@@ -508,6 +518,32 @@ namespace Microsoft.Dafny }
}
+ public class CouplingInvariant : MemberDecl {
+ public readonly Expression! Expr;
+ public readonly List<IToken!>! Toks;
+ public List<Formal!> Formals; // filled in during resolution
+ public List<Field!> Refined; // filled in during resolution
+
+ public CouplingInvariant(List<IToken!>! toks, Expression! expr, Attributes attributes)
+ requires toks.Count > 0;
+ {
+ Expr = expr;
+ Toks = toks;
+ StringBuilder sb = new StringBuilder();
+ foreach (IToken tok in toks)
+ sb.Append("_").Append(tok.val);
+
+ base(toks[0], "_coupling_invariant" + sb.ToString(), attributes);
+ }
+
+ public string[] Tokens() {
+ string[] result = new string[Toks.Count];
+ for (int i = 0; i < Toks.Count; i++)
+ result[i] = Toks[i].val;
+ return result;
+ }
+ }
+
public interface IVariable {
string! Name { get; }
string! UniqueName { get; }
@@ -635,6 +671,20 @@ namespace Microsoft.Dafny base(tok, name, attributes);
}
}
+
+ public class MethodRefinement : Method {
+ public Method Refined; // filled in during resolution
+ public MethodRefinement(IToken! tok, string! name,
+ bool isStatic, bool isGhost,
+ [Captured] List<TypeParameter!>! typeArgs,
+ [Captured] List<Formal!>! ins, [Captured] List<Formal!>! outs,
+ [Captured] List<MaybeFreeExpression!>! req, [Captured] List<FrameExpression!>! mod, [Captured] List<MaybeFreeExpression!>! ens,
+ [Captured] List<Expression!>! decreases,
+ [Captured] BlockStmt body,
+ Attributes attributes) {
+ base(tok, name, isStatic, isGhost, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes);
+ }
+ }
// ------------------------------------------------------------------------------------------------------
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index 1ed06227..d35fb5d3 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -19,7 +19,7 @@ public class Parser { public const int _ident = 1;
public const int _digits = 2;
public const int _string = 3;
- public const int maxT = 100;
+ public const int maxT = 103;
const bool T = true;
const bool x = false;
@@ -210,7 +210,7 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules }
module = new ModuleDecl(id, id.val, theImports, attrs);
Expect(6);
- while (la.kind == 8 || la.kind == 12) {
+ while (la.kind == 8 || la.kind == 13) {
if (la.kind == 8) {
ClassDecl(module, out c);
module.TopLevelDecls.Add(c);
@@ -224,7 +224,7 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules } else if (la.kind == 8) {
ClassDecl(defaultModule, out c);
defaultModule.TopLevelDecls.Add(c);
- } else if (la.kind == 12) {
+ } else if (la.kind == 13) {
DatatypeDecl(defaultModule, out dt);
defaultModule.TopLevelDecls.Add(dt);
} else {
@@ -263,7 +263,7 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules IToken! id;
Ident(out id);
ids.Add(id.val);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
Ident(out id);
ids.Add(id.val);
@@ -274,6 +274,8 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules IToken! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
+ IToken! idRefined;
+ IToken optionalId = null;
List<MemberDecl!> members = new List<MemberDecl!>();
Expect(8);
@@ -281,15 +283,24 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 17) {
+ if (la.kind == 20) {
GenericParameters(typeArgs);
}
+ if (la.kind == 9) {
+ Get();
+ Ident(out idRefined);
+ optionalId = idRefined;
+ }
Expect(6);
while (StartOf(2)) {
ClassMemberDecl(members);
}
Expect(7);
- c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
+ if (optionalId == null)
+ c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
+ else
+ c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);
+
}
void DatatypeDecl(ModuleDecl! module, out DatatypeDecl! dt) {
@@ -298,12 +309,12 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules List<TypeParameter!> typeArgs = new List<TypeParameter!>();
List<DatatypeCtor!> ctors = new List<DatatypeCtor!>();
- Expect(12);
+ Expect(13);
while (la.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 17) {
+ if (la.kind == 20) {
GenericParameters(typeArgs);
}
Expect(6);
@@ -319,11 +330,11 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules Function! f;
MemberModifiers mmod = new MemberModifiers();
- while (la.kind == 9 || la.kind == 10 || la.kind == 11) {
- if (la.kind == 9) {
+ while (la.kind == 10 || la.kind == 11 || la.kind == 12) {
+ if (la.kind == 10) {
Get();
mmod.IsGhost = true;
- } else if (la.kind == 10) {
+ } else if (la.kind == 11) {
Get();
mmod.IsStatic = true;
} else {
@@ -331,35 +342,37 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules mmod.IsUnlimited = true;
}
}
- if (la.kind == 14) {
+ if (la.kind == 15) {
FieldDecl(mmod, mm);
- } else if (la.kind == 34) {
+ } else if (la.kind == 37) {
FunctionDecl(mmod, out f);
mm.Add(f);
- } else if (la.kind == 19) {
+ } else if (la.kind == 9 || la.kind == 22) {
MethodDecl(mmod, out m);
mm.Add(m);
- } else SynErr(101);
+ } else if (la.kind == 17) {
+ CouplingInvDecl(mmod, mm);
+ } else SynErr(104);
}
void GenericParameters(List<TypeParameter!>! typeArgs) {
IToken! id;
- Expect(17);
+ Expect(20);
Ident(out id);
typeArgs.Add(new TypeParameter(id, id.val));
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
Ident(out id);
typeArgs.Add(new TypeParameter(id, id.val));
}
- Expect(18);
+ Expect(21);
}
void FieldDecl(MemberModifiers mmod, List<MemberDecl!>! mm) {
Attributes attrs = null;
IToken! id; Type! ty;
- Expect(14);
+ Expect(15);
if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
@@ -368,12 +381,12 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules }
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
- Expect(13);
+ Expect(14);
}
void FunctionDecl(MemberModifiers mmod, out Function! f) {
@@ -388,8 +401,8 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules Expression! bb; Expression body = null;
bool isFunctionMethod = false;
- Expect(34);
- if (la.kind == 19) {
+ Expect(37);
+ if (la.kind == 22) {
Get();
isFunctionMethod = true;
}
@@ -399,25 +412,25 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 17) {
+ if (la.kind == 20) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
Formals(true, false, formals);
- Expect(16);
+ Expect(19);
Type(out returnType);
- if (la.kind == 13) {
+ if (la.kind == 14) {
Get();
- while (la.kind == 23 || la.kind == 25 || la.kind == 35) {
+ while (la.kind == 26 || la.kind == 28 || la.kind == 38) {
FunctionSpec(reqs, reads, decreases);
}
} else if (StartOf(3)) {
- while (la.kind == 23 || la.kind == 25 || la.kind == 35) {
+ while (la.kind == 26 || la.kind == 28 || la.kind == 38) {
FunctionSpec(reqs, reads, decreases);
}
FunctionBody(out bb);
body = bb;
- } else SynErr(102);
+ } else SynErr(105);
parseVarScope.PopMarker();
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
@@ -434,24 +447,30 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();
List<Expression!> dec = new List<Expression!>();
Statement! bb; BlockStmt body = null;
+ bool isRefinement = false;
- Expect(19);
+ if (la.kind == 22) {
+ Get();
+ } else if (la.kind == 9) {
+ Get();
+ isRefinement = true;
+ } else SynErr(106);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
while (la.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 17) {
+ if (la.kind == 20) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
Formals(true, true, ins);
- if (la.kind == 20) {
+ if (la.kind == 23) {
Get();
Formals(false, true, outs);
}
- if (la.kind == 13) {
+ if (la.kind == 14) {
Get();
while (StartOf(4)) {
MethodSpec(req, mod, ens, dec);
@@ -462,9 +481,42 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules }
BlockStmt(out bb);
body = (BlockStmt)bb;
- } else SynErr(103);
+ } else SynErr(107);
+ parseVarScope.PopMarker();
+ if (isRefinement)
+ m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
+ else
+ m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
+
+ }
+
+ void CouplingInvDecl(MemberModifiers mmod, List<MemberDecl!>! mm) {
+ Attributes attrs = null;
+ List<IToken!> ids = new List<IToken!>();;
+ IToken! id;
+ Expression! e;
+ parseVarScope.PushMarker();
+
+ Expect(17);
+ if (mmod.IsUnlimited) { SemErr(t, "coupling invariants cannot be declared 'unlimited'"); }
+ if (mmod.IsStatic) { SemErr(t, "coupling invariants cannot be declared 'static'"); }
+ if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }
+
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ Ident(out id);
+ ids.Add(id); parseVarScope.Push(id.val, id.val);
+ while (la.kind == 16) {
+ Get();
+ Ident(out id);
+ ids.Add(id); parseVarScope.Push(id.val, id.val);
+ }
+ Expect(18);
+ Expression(out e);
+ Expect(14);
+ mm.Add(new CouplingInvariant(ids, e, attrs));
parseVarScope.PopMarker();
- m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
}
@@ -478,43 +530,61 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 17) {
+ if (la.kind == 20) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
- if (la.kind == 26) {
+ if (la.kind == 29) {
FormalsOptionalIds(formals);
}
parseVarScope.PopMarker();
ctors.Add(new DatatypeCtor(id, id.val, typeArgs, formals, attrs));
- Expect(13);
+ Expect(14);
}
void FormalsOptionalIds(List<Formal!>! formals) {
IToken! id; Type! ty; string! name; bool isGhost;
- Expect(26);
+ Expect(29);
if (StartOf(6)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
}
}
- Expect(27);
+ Expect(30);
}
void IdentType(out IToken! id, out Type! ty) {
Ident(out id);
- Expect(16);
+ Expect(19);
Type(out ty);
}
+ void Expression(out Expression! e) {
+ IToken! x; Expression! e0; Expression! e1 = dummyExpr;
+ e = dummyExpr;
+
+ if (la.kind == 52) {
+ Get();
+ x = t;
+ Expression(out e);
+ Expect(64);
+ Expression(out e0);
+ Expect(53);
+ Expression(out e1);
+ e = new ITEExpr(x, e, e0, e1);
+ } else if (StartOf(7)) {
+ EquivExpression(out e);
+ } else SynErr(108);
+ }
+
void GIdentType(bool allowGhost, out IToken! id, out Type! ty, out bool isGhost) {
isGhost = false;
- if (la.kind == 9) {
+ if (la.kind == 10) {
Get();
if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); }
}
@@ -530,7 +600,7 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules IToken! id; Type! ty; Type optType = null;
Ident(out id);
- if (la.kind == 16) {
+ if (la.kind == 19) {
Get();
Type(out ty);
optType = ty;
@@ -540,12 +610,12 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules void TypeIdentOptional(out IToken! id, out string! identName, out Type! ty, out bool isGhost) {
string name = null; isGhost = false;
- if (la.kind == 9) {
+ if (la.kind == 10) {
Get();
isGhost = true;
}
TypeAndToken(out id, out ty);
- if (la.kind == 16) {
+ if (la.kind == 19) {
Get();
UserDefinedType udt = ty as UserDefinedType;
if (udt != null && udt.TypeArgs.Count == 0) {
@@ -568,13 +638,13 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type!>! gt;
- if (la.kind == 28) {
+ if (la.kind == 31) {
Get();
tok = t;
- } else if (la.kind == 29) {
+ } else if (la.kind == 32) {
Get();
tok = t; ty = new IntType();
- } else if (la.kind == 30) {
+ } else if (la.kind == 33) {
Get();
tok = t; gt = new List<Type!>();
GenericInstantiation(gt);
@@ -583,7 +653,7 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules }
ty = new SetType(gt[0]);
- } else if (la.kind == 31) {
+ } else if (la.kind == 34) {
Get();
tok = t; gt = new List<Type!>();
GenericInstantiation(gt);
@@ -592,63 +662,63 @@ public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules }
ty = new SeqType(gt[0]);
- } else if (la.kind == 1 || la.kind == 32 || la.kind == 33) {
+ } else if (la.kind == 1 || la.kind == 35 || la.kind == 36) {
ReferenceType(out tok, out ty);
- } else SynErr(104);
+ } else SynErr(109);
}
void Formals(bool incoming, bool allowGhosts, List<Formal!>! formals) {
IToken! id; Type! ty; bool isGhost;
- Expect(26);
- if (la.kind == 1 || la.kind == 9) {
+ Expect(29);
+ if (la.kind == 1 || la.kind == 10) {
GIdentType(allowGhosts, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
GIdentType(allowGhosts, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val);
}
}
- Expect(27);
+ Expect(30);
}
void MethodSpec(List<MaybeFreeExpression!>! req, List<FrameExpression!>! mod, List<MaybeFreeExpression!>! ens,
List<Expression!>! decreases) {
Expression! e; FrameExpression! fe; bool isFree = false;
- if (la.kind == 21) {
+ if (la.kind == 24) {
Get();
- if (StartOf(7)) {
+ if (StartOf(8)) {
FrameExpression(out fe);
mod.Add(fe);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
FrameExpression(out fe);
mod.Add(fe);
}
}
- Expect(13);
- } else if (la.kind == 22 || la.kind == 23 || la.kind == 24) {
- if (la.kind == 22) {
+ Expect(14);
+ } else if (la.kind == 25 || la.kind == 26 || la.kind == 27) {
+ if (la.kind == 25) {
Get();
isFree = true;
}
- if (la.kind == 23) {
+ if (la.kind == 26) {
Get();
Expression(out e);
- Expect(13);
+ Expect(14);
req.Add(new MaybeFreeExpression(e, isFree));
- } else if (la.kind == 24) {
+ } else if (la.kind == 27) {
Get();
Expression(out e);
- Expect(13);
+ Expect(14);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else SynErr(105);
- } else if (la.kind == 25) {
+ } else SynErr(110);
+ } else if (la.kind == 28) {
Get();
Expressions(decreases);
- Expect(13);
- } else SynErr(106);
+ Expect(14);
+ } else SynErr(111);
}
void BlockStmt(out Statement! block) {
@@ -659,7 +729,7 @@ List<Expression!>! decreases) { parseVarScope.PushMarker();
Expect(6);
x = t;
- while (StartOf(8)) {
+ while (StartOf(9)) {
Stmt(body);
}
Expect(7);
@@ -670,7 +740,7 @@ List<Expression!>! decreases) { void FrameExpression(out FrameExpression! fe) {
Expression! e; IToken! id; string fieldName = null;
Expression(out e);
- if (la.kind == 37) {
+ if (la.kind == 40) {
Get();
Ident(out id);
fieldName = id.val;
@@ -678,29 +748,11 @@ List<Expression!>! decreases) { fe = new FrameExpression(e, fieldName);
}
- void Expression(out Expression! e) {
- IToken! x; Expression! e0; Expression! e1 = dummyExpr;
- e = dummyExpr;
-
- if (la.kind == 49) {
- Get();
- x = t;
- Expression(out e);
- Expect(61);
- Expression(out e0);
- Expect(50);
- Expression(out e1);
- e = new ITEExpr(x, e, e0, e1);
- } else if (StartOf(9)) {
- EquivExpression(out e);
- } else SynErr(107);
- }
-
void Expressions(List<Expression!>! args) {
Expression! e;
Expression(out e);
args.Add(e);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
Expression(out e);
args.Add(e);
@@ -709,25 +761,25 @@ List<Expression!>! decreases) { void GenericInstantiation(List<Type!>! gt) {
Type! ty;
- Expect(17);
+ Expect(20);
Type(out ty);
gt.Add(ty);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
Type(out ty);
gt.Add(ty);
}
- Expect(18);
+ Expect(21);
}
void ReferenceType(out IToken! tok, out Type! ty) {
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type!>! gt;
- if (la.kind == 32) {
+ if (la.kind == 35) {
Get();
tok = t; ty = new ObjectType();
- } else if (la.kind == 33) {
+ } else if (la.kind == 36) {
Get();
tok = t; gt = new List<Type!>();
GenericInstantiation(gt);
@@ -739,78 +791,78 @@ List<Expression!>! decreases) { } else if (la.kind == 1) {
Ident(out tok);
gt = new List<Type!>();
- if (la.kind == 17) {
+ if (la.kind == 20) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else SynErr(108);
+ } else SynErr(112);
}
void FunctionSpec(List<Expression!>! reqs, List<FrameExpression!>! reads, List<Expression!>! decreases) {
Expression! e; FrameExpression! fe;
- if (la.kind == 23) {
+ if (la.kind == 26) {
Get();
Expression(out e);
- Expect(13);
+ Expect(14);
reqs.Add(e);
- } else if (la.kind == 35) {
+ } else if (la.kind == 38) {
Get();
if (StartOf(10)) {
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
}
}
- Expect(13);
- } else if (la.kind == 25) {
+ Expect(14);
+ } else if (la.kind == 28) {
Get();
Expressions(decreases);
- Expect(13);
- } else SynErr(109);
+ Expect(14);
+ } else SynErr(113);
}
void FunctionBody(out Expression! e) {
e = dummyExpr;
Expect(6);
- if (la.kind == 38) {
+ if (la.kind == 41) {
MatchExpression(out e);
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
Expression(out e);
- } else SynErr(110);
+ } else SynErr(114);
Expect(7);
}
void PossiblyWildFrameExpression(out FrameExpression! fe) {
fe = dummyFrameExpr;
- if (la.kind == 36) {
+ if (la.kind == 39) {
Get();
fe = new FrameExpression(new WildcardExpr(t), null);
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
FrameExpression(out fe);
- } else SynErr(111);
+ } else SynErr(115);
}
void PossiblyWildExpression(out Expression! e) {
e = dummyExpr;
- if (la.kind == 36) {
+ if (la.kind == 39) {
Get();
e = new WildcardExpr(t);
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
Expression(out e);
- } else SynErr(112);
+ } else SynErr(116);
}
void MatchExpression(out Expression! e) {
IToken! x; MatchCaseExpr! c;
List<MatchCaseExpr!> cases = new List<MatchCaseExpr!>();
- Expect(38);
+ Expect(41);
x = t;
Expression(out e);
- while (la.kind == 39) {
+ while (la.kind == 42) {
CaseExpression(out c);
cases.Add(c);
}
@@ -822,23 +874,23 @@ List<Expression!>! decreases) { List<BoundVar!> arguments = new List<BoundVar!>();
Expression! body;
- Expect(39);
+ Expect(42);
x = t; parseVarScope.PushMarker();
Ident(out id);
- if (la.kind == 26) {
+ if (la.kind == 29) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val);
}
- Expect(27);
+ Expect(30);
}
- Expect(40);
+ Expect(43);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
parseVarScope.PopMarker();
@@ -853,9 +905,9 @@ List<Expression!>! decreases) { if (StartOf(11)) {
OneStmt(out s);
ss.Add(s);
- } else if (la.kind == 9 || la.kind == 14) {
+ } else if (la.kind == 10 || la.kind == 15) {
VarDeclStmts(ss);
- } else SynErr(113);
+ } else SynErr(117);
}
void OneStmt(out Statement! s) {
@@ -863,121 +915,121 @@ List<Expression!>! decreases) { s = dummyStmt; /* to please the compiler */
switch (la.kind) {
- case 57: {
+ case 60: {
AssertStmt(out s);
break;
}
- case 58: {
+ case 61: {
AssumeStmt(out s);
break;
}
- case 59: {
+ case 62: {
UseStmt(out s);
break;
}
- case 60: {
+ case 63: {
PrintStmt(out s);
break;
}
- case 1: case 26: case 92: case 93: {
+ case 1: case 29: case 95: case 96: {
AssignStmt(out s);
break;
}
- case 48: {
+ case 51: {
HavocStmt(out s);
break;
}
- case 53: {
+ case 56: {
CallStmt(out s);
break;
}
- case 49: {
+ case 52: {
IfStmt(out s);
break;
}
- case 51: {
+ case 54: {
WhileStmt(out s);
break;
}
- case 38: {
+ case 41: {
MatchStmt(out s);
break;
}
- case 54: {
+ case 57: {
ForeachStmt(out s);
break;
}
- case 41: {
+ case 44: {
Get();
x = t;
Ident(out id);
- Expect(16);
+ Expect(19);
s = new LabelStmt(x, id.val);
break;
}
- case 42: {
+ case 45: {
Get();
x = t;
if (la.kind == 1) {
Ident(out id);
label = id.val;
}
- Expect(13);
+ Expect(14);
s = new BreakStmt(x, label);
break;
}
- case 43: {
+ case 46: {
Get();
x = t;
- Expect(13);
+ Expect(14);
s = new ReturnStmt(x);
break;
}
- default: SynErr(114); break;
+ default: SynErr(118); break;
}
}
void VarDeclStmts(List<Statement!>! ss) {
VarDecl! d; bool isGhost = false;
- if (la.kind == 9) {
+ if (la.kind == 10) {
Get();
isGhost = true;
}
- Expect(14);
+ Expect(15);
IdentTypeRhs(out d, isGhost);
ss.Add(d); parseVarScope.Push(d.Name, d.Name);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
IdentTypeRhs(out d, isGhost);
ss.Add(d); parseVarScope.Push(d.Name, d.Name);
}
- Expect(13);
+ Expect(14);
}
void AssertStmt(out Statement! s) {
IToken! x; Expression! e;
- Expect(57);
+ Expect(60);
x = t;
Expression(out e);
- Expect(13);
+ Expect(14);
s = new AssertStmt(x, e);
}
void AssumeStmt(out Statement! s) {
IToken! x; Expression! e;
- Expect(58);
+ Expect(61);
x = t;
Expression(out e);
- Expect(13);
+ Expect(14);
s = new AssumeStmt(x, e);
}
void UseStmt(out Statement! s) {
IToken! x; Expression! e;
- Expect(59);
+ Expect(62);
x = t;
Expression(out e);
- Expect(13);
+ Expect(14);
s = new UseStmt(x, e);
}
@@ -985,16 +1037,16 @@ List<Expression!>! decreases) { IToken! x; Attributes.Argument! arg;
List<Attributes.Argument!> args = new List<Attributes.Argument!>();
- Expect(60);
+ Expect(63);
x = t;
AttributeArg(out arg);
args.Add(arg);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
AttributeArg(out arg);
args.Add(arg);
}
- Expect(13);
+ Expect(14);
s = new PrintStmt(x, args);
}
@@ -1006,7 +1058,7 @@ List<Expression!>! decreases) { s = dummyStmt;
LhsExpr(out lhs);
- Expect(44);
+ Expect(47);
x = t;
AssignRhs(out rhs, out ty);
if (ty == null) {
@@ -1018,15 +1070,15 @@ List<Expression!>! decreases) { s = new AssignStmt(x, lhs, ty, rhs);
}
- Expect(13);
+ Expect(14);
}
void HavocStmt(out Statement! s) {
IToken! x; Expression! lhs;
- Expect(48);
+ Expect(51);
x = t;
LhsExpr(out lhs);
- Expect(13);
+ Expect(14);
s = new AssignStmt(x, lhs);
}
@@ -1036,11 +1088,11 @@ List<Expression!>! decreases) { List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
List<AutoVarDecl!> newVars = new List<AutoVarDecl!>();
- Expect(53);
+ Expect(56);
x = t;
CallStmtSubExpr(out e);
- if (la.kind == 15 || la.kind == 44) {
- if (la.kind == 15) {
+ if (la.kind == 16 || la.kind == 47) {
+ if (la.kind == 16) {
Get();
e = ConvertToLocal(e);
if (e is IdentifierExpr) {
@@ -1053,12 +1105,12 @@ List<Expression!>! decreases) { Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
}
- Expect(44);
+ Expect(47);
CallStmtSubExpr(out e);
} else {
Get();
@@ -1074,7 +1126,7 @@ List<Expression!>! decreases) { CallStmtSubExpr(out e);
}
}
- Expect(13);
+ Expect(14);
if (e is FunctionCallExpr) {
FunctionCallExpr fce = (FunctionCallExpr)e;
s = new CallStmt(x, newVars, lhs, fce.Receiver, fce.Name, fce.Args); // this actually does an ownership transfer of fce.Args
@@ -1092,19 +1144,19 @@ List<Expression!>! decreases) { Statement! s;
Statement els = null;
- Expect(49);
+ Expect(52);
x = t;
Guard(out guard);
BlockStmt(out thn);
- if (la.kind == 50) {
+ if (la.kind == 53) {
Get();
- if (la.kind == 49) {
+ if (la.kind == 52) {
IfStmt(out s);
els = s;
} else if (la.kind == 6) {
BlockStmt(out s);
els = s;
- } else SynErr(115);
+ } else SynErr(119);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -1117,31 +1169,31 @@ List<Expression!>! decreases) { List<Expression!> decreases = new List<Expression!>();
Statement! body;
- Expect(51);
+ Expect(54);
x = t;
Guard(out guard);
assume guard == null || Owner.None(guard);
- while (la.kind == 22 || la.kind == 25 || la.kind == 52) {
- if (la.kind == 22 || la.kind == 52) {
+ while (la.kind == 25 || la.kind == 28 || la.kind == 55) {
+ if (la.kind == 25 || la.kind == 55) {
isFree = false;
- if (la.kind == 22) {
+ if (la.kind == 25) {
Get();
isFree = true;
}
- Expect(52);
+ Expect(55);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
- Expect(13);
+ Expect(14);
} else {
Get();
PossiblyWildExpression(out e);
decreases.Add(e);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
PossiblyWildExpression(out e);
decreases.Add(e);
}
- Expect(13);
+ Expect(14);
}
}
BlockStmt(out body);
@@ -1151,11 +1203,11 @@ List<Expression!>! decreases) { void MatchStmt(out Statement! s) {
Token x; Expression! e; MatchCaseStmt! c;
List<MatchCaseStmt!> cases = new List<MatchCaseStmt!>();
- Expect(38);
+ Expect(41);
x = t;
Expression(out e);
Expect(6);
- while (la.kind == 39) {
+ while (la.kind == 42) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1172,31 +1224,31 @@ List<Expression!>! decreases) { AssignStmt bodyAssign = null;
parseVarScope.PushMarker();
- Expect(54);
+ Expect(57);
x = t;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
- Expect(26);
+ Expect(29);
Ident(out boundVar);
- if (la.kind == 16) {
+ if (la.kind == 19) {
Get();
Type(out ty);
}
- Expect(55);
+ Expect(58);
Expression(out collection);
parseVarScope.Push(boundVar.val, boundVar.val);
- if (la.kind == 56) {
+ if (la.kind == 59) {
Get();
Expression(out range);
}
- Expect(27);
+ Expect(30);
Expect(6);
- while (la.kind == 57 || la.kind == 58 || la.kind == 59) {
- if (la.kind == 57) {
+ while (la.kind == 60 || la.kind == 61 || la.kind == 62) {
+ if (la.kind == 60) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- } else if (la.kind == 58) {
+ } else if (la.kind == 61) {
AssumeStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -1207,10 +1259,10 @@ List<Expression!>! decreases) { if (StartOf(12)) {
AssignStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else if (la.kind == 48) {
+ } else if (la.kind == 51) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else SynErr(116);
+ } else SynErr(120);
Expect(7);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1229,20 +1281,20 @@ List<Expression!>! decreases) { IToken! x; Expression! ee; Type! tt;
e = null; ty = null;
- if (la.kind == 45) {
+ if (la.kind == 48) {
Get();
TypeAndToken(out x, out tt);
ty = tt;
- if (la.kind == 46) {
+ if (la.kind == 49) {
Get();
Expression(out ee);
- Expect(47);
+ Expect(50);
e = ee;
}
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(117);
+ } else SynErr(121);
if (e == null && ty == null) { e = dummyExpr; }
}
@@ -1250,10 +1302,10 @@ List<Expression!>! decreases) { IToken! id; e = dummyExpr;
if (la.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (la.kind == 26 || la.kind == 92 || la.kind == 93) {
+ } else if (la.kind == 29 || la.kind == 95 || la.kind == 96) {
ObjectExpression(out e);
- } else SynErr(118);
- while (la.kind == 46 || la.kind == 89) {
+ } else SynErr(122);
+ while (la.kind == 49 || la.kind == 92) {
SelectOrCallSuffix(ref e);
}
}
@@ -1264,12 +1316,12 @@ List<Expression!>! decreases) { Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null;
Ident(out id);
- if (la.kind == 16) {
+ if (la.kind == 19) {
Get();
Type(out ty);
optionalType = ty;
}
- if (la.kind == 44) {
+ if (la.kind == 47) {
Get();
AssignRhs(out rhs, out newType);
}
@@ -1290,15 +1342,15 @@ List<Expression!>! decreases) { void Guard(out Expression e) {
Expression! ee; e = null;
- Expect(26);
- if (la.kind == 36) {
+ Expect(29);
+ if (la.kind == 39) {
Get();
e = null;
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(119);
- Expect(27);
+ } else SynErr(123);
+ Expect(30);
}
void CaseStatement(out MatchCaseStmt! c) {
@@ -1306,25 +1358,25 @@ List<Expression!>! decreases) { List<BoundVar!> arguments = new List<BoundVar!>();
List<Statement!> body = new List<Statement!>();
- Expect(39);
+ Expect(42);
x = t; parseVarScope.PushMarker();
Ident(out id);
- if (la.kind == 26) {
+ if (la.kind == 29) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val);
}
- Expect(27);
+ Expect(30);
}
- Expect(40);
+ Expect(43);
parseVarScope.PushMarker();
- while (StartOf(8)) {
+ while (StartOf(9)) {
Stmt(body);
}
parseVarScope.PopMarker();
@@ -1336,11 +1388,11 @@ List<Expression!>! decreases) { e = dummyExpr;
if (la.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (la.kind == 26 || la.kind == 92 || la.kind == 93) {
+ } else if (la.kind == 29 || la.kind == 95 || la.kind == 96) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else SynErr(120);
- while (la.kind == 46 || la.kind == 89) {
+ } else SynErr(124);
+ while (la.kind == 49 || la.kind == 92) {
SelectOrCallSuffix(ref e);
}
}
@@ -1350,16 +1402,16 @@ List<Expression!>! decreases) { if (la.kind == 3) {
Get();
arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2));
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else SynErr(121);
+ } else SynErr(125);
}
void EquivExpression(out Expression! e0) {
IToken! x; Expression! e1;
ImpliesExpression(out e0);
- while (la.kind == 62 || la.kind == 63) {
+ while (la.kind == 65 || la.kind == 66) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -1370,7 +1422,7 @@ List<Expression!>! decreases) { void ImpliesExpression(out Expression! e0) {
IToken! x; Expression! e1;
LogicalExpression(out e0);
- if (la.kind == 64 || la.kind == 65) {
+ if (la.kind == 67 || la.kind == 68) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -1379,23 +1431,23 @@ List<Expression!>! decreases) { }
void EquivOp() {
- if (la.kind == 62) {
+ if (la.kind == 65) {
Get();
- } else if (la.kind == 63) {
+ } else if (la.kind == 66) {
Get();
- } else SynErr(122);
+ } else SynErr(126);
}
void LogicalExpression(out Expression! e0) {
IToken! x; Expression! e1;
RelationalExpression(out e0);
if (StartOf(13)) {
- if (la.kind == 66 || la.kind == 67) {
+ if (la.kind == 69 || la.kind == 70) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 66 || la.kind == 67) {
+ while (la.kind == 69 || la.kind == 70) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1406,7 +1458,7 @@ List<Expression!>! decreases) { x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 68 || la.kind == 69) {
+ while (la.kind == 71 || la.kind == 72) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1417,11 +1469,11 @@ List<Expression!>! decreases) { }
void ImpliesOp() {
- if (la.kind == 64) {
+ if (la.kind == 67) {
Get();
- } else if (la.kind == 65) {
+ } else if (la.kind == 68) {
Get();
- } else SynErr(123);
+ } else SynErr(127);
}
void RelationalExpression(out Expression! e0) {
@@ -1435,25 +1487,25 @@ List<Expression!>! decreases) { }
void AndOp() {
- if (la.kind == 66) {
+ if (la.kind == 69) {
Get();
- } else if (la.kind == 67) {
+ } else if (la.kind == 70) {
Get();
- } else SynErr(124);
+ } else SynErr(128);
}
void OrOp() {
- if (la.kind == 68) {
+ if (la.kind == 71) {
Get();
- } else if (la.kind == 69) {
+ } else if (la.kind == 72) {
Get();
- } else SynErr(125);
+ } else SynErr(129);
}
void Term(out Expression! e0) {
IToken! x; Expression! e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (la.kind == 79 || la.kind == 80) {
+ while (la.kind == 82 || la.kind == 83) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1463,74 +1515,74 @@ List<Expression!>! decreases) { void RelOp(out IToken! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
switch (la.kind) {
- case 70: {
+ case 73: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
break;
}
- case 17: {
+ case 20: {
Get();
x = t; op = BinaryExpr.Opcode.Lt;
break;
}
- case 18: {
+ case 21: {
Get();
x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 71: {
+ case 74: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 72: {
+ case 75: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 73: {
+ case 76: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 74: {
+ case 77: {
Get();
x = t; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 55: {
+ case 58: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 75: {
+ case 78: {
Get();
x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 76: {
+ case 79: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 77: {
+ case 80: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 78: {
+ case 81: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(126); break;
+ default: SynErr(130); break;
}
}
void Factor(out Expression! e0) {
IToken! x; Expression! e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 36 || la.kind == 81 || la.kind == 82) {
+ while (la.kind == 39 || la.kind == 84 || la.kind == 85) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1539,23 +1591,23 @@ List<Expression!>! decreases) { void AddOp(out IToken! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 79) {
+ if (la.kind == 82) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 80) {
+ } else if (la.kind == 83) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(127);
+ } else SynErr(131);
}
void UnaryExpression(out Expression! e) {
IToken! x; e = dummyExpr;
- if (la.kind == 80) {
+ if (la.kind == 83) {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (la.kind == 83 || la.kind == 84) {
+ } else if (la.kind == 86 || la.kind == 87) {
NegOp();
x = t;
UnaryExpression(out e);
@@ -1564,29 +1616,29 @@ List<Expression!>! decreases) { SelectExpression(out e);
} else if (StartOf(15)) {
ConstAtomExpression(out e);
- } else SynErr(128);
+ } else SynErr(132);
}
void MulOp(out IToken! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 36) {
+ if (la.kind == 39) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 81) {
+ } else if (la.kind == 84) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 82) {
+ } else if (la.kind == 85) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(129);
+ } else SynErr(133);
}
void NegOp() {
- if (la.kind == 83) {
+ if (la.kind == 86) {
Get();
- } else if (la.kind == 84) {
+ } else if (la.kind == 87) {
Get();
- } else SynErr(130);
+ } else SynErr(134);
}
void ConstAtomExpression(out Expression! e) {
@@ -1594,17 +1646,17 @@ List<Expression!>! decreases) { e = dummyExpr;
switch (la.kind) {
- case 85: {
+ case 88: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 86: {
+ case 89: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 87: {
+ case 90: {
Get();
e = new LiteralExpr(t);
break;
@@ -1614,61 +1666,61 @@ List<Expression!>! decreases) { e = new LiteralExpr(t, n);
break;
}
- case 88: {
+ case 91: {
Get();
x = t;
Ident(out dtName);
- Expect(89);
+ Expect(92);
Ident(out id);
elements = new List<Expression!>();
- if (la.kind == 26) {
+ if (la.kind == 29) {
Get();
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expressions(elements);
}
- Expect(27);
+ Expect(30);
}
e = new DatatypeValue(t, dtName.val, id.val, elements);
break;
}
- case 90: {
+ case 93: {
Get();
x = t;
- Expect(26);
+ Expect(29);
Expression(out e);
- Expect(27);
+ Expect(30);
e = new FreshExpr(x, e);
break;
}
- case 56: {
+ case 59: {
Get();
x = t;
Expression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
- Expect(56);
+ Expect(59);
break;
}
case 6: {
Get();
x = t; elements = new List<Expression!>();
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expressions(elements);
}
e = new SetDisplayExpr(x, elements);
Expect(7);
break;
}
- case 46: {
+ case 49: {
Get();
x = t; elements = new List<Expression!>();
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(47);
+ Expect(50);
break;
}
- default: SynErr(131); break;
+ default: SynErr(135); break;
}
}
@@ -1686,13 +1738,13 @@ List<Expression!>! decreases) { void IdentOrFuncExpression(out Expression! e) {
IToken! id; e = dummyExpr; List<Expression!>! args;
Ident(out id);
- if (la.kind == 26) {
+ if (la.kind == 29) {
Get();
args = new List<Expression!>();
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expressions(args);
}
- Expect(27);
+ Expect(30);
e = new FunctionCallExpr(id, id.val, new ImplicitThisExpr(id), args);
}
if (e == dummyExpr) {
@@ -1707,25 +1759,25 @@ List<Expression!>! decreases) { void ObjectExpression(out Expression! e) {
IToken! x; e = dummyExpr;
- if (la.kind == 92) {
+ if (la.kind == 95) {
Get();
e = new ThisExpr(t);
- } else if (la.kind == 93) {
+ } else if (la.kind == 96) {
Get();
x = t;
- Expect(26);
+ Expect(29);
Expression(out e);
- Expect(27);
+ Expect(30);
e = new OldExpr(x, e);
- } else if (la.kind == 26) {
+ } else if (la.kind == 29) {
Get();
if (StartOf(16)) {
QuantifierGuts(out e);
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
Expression(out e);
- } else SynErr(132);
- Expect(27);
- } else SynErr(133);
+ } else SynErr(136);
+ Expect(30);
+ } else SynErr(137);
}
void SelectOrCallSuffix(ref Expression! e) {
@@ -1733,30 +1785,30 @@ List<Expression!>! decreases) { Expression e0 = null; Expression e1 = null; Expression! ee; bool anyDots = false;
bool func = false;
- if (la.kind == 89) {
+ if (la.kind == 92) {
Get();
Ident(out id);
- if (la.kind == 26) {
+ if (la.kind == 29) {
Get();
args = new List<Expression!>(); func = true;
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expressions(args);
}
- Expect(27);
+ Expect(30);
e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (la.kind == 46) {
+ } else if (la.kind == 49) {
Get();
x = t;
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 44 || la.kind == 91) {
- if (la.kind == 91) {
+ if (la.kind == 47 || la.kind == 94) {
+ if (la.kind == 94) {
Get();
anyDots = true;
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expression(out ee);
e1 = ee;
}
@@ -1766,11 +1818,11 @@ List<Expression!>! decreases) { e1 = ee;
}
}
- } else if (la.kind == 91) {
+ } else if (la.kind == 94) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else SynErr(134);
+ } else SynErr(138);
if (!anyDots && e0 == null) {
/* a parsing error occurred */
e0 = dummyExpr;
@@ -1787,8 +1839,8 @@ List<Expression!>! decreases) { e = new SeqUpdateExpr(x, e, e0, e1);
}
- Expect(47);
- } else SynErr(135);
+ Expect(50);
+ } else SynErr(139);
}
void QuantifierGuts(out Expression! q) {
@@ -1801,17 +1853,17 @@ List<Expression!>! decreases) { Triggers trigs = null;
Expression! body;
- if (la.kind == 94 || la.kind == 95) {
+ if (la.kind == 97 || la.kind == 98) {
Forall();
x = t; univ = true;
- } else if (la.kind == 96 || la.kind == 97) {
+ } else if (la.kind == 99 || la.kind == 100) {
Exists();
x = t;
- } else SynErr(136);
+ } else SynErr(140);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -1831,41 +1883,41 @@ List<Expression!>! decreases) { }
void Forall() {
- if (la.kind == 94) {
+ if (la.kind == 97) {
Get();
- } else if (la.kind == 95) {
+ } else if (la.kind == 98) {
Get();
- } else SynErr(137);
+ } else SynErr(141);
}
void Exists() {
- if (la.kind == 96) {
+ if (la.kind == 99) {
Get();
- } else if (la.kind == 97) {
+ } else if (la.kind == 100) {
Get();
- } else SynErr(138);
+ } else SynErr(142);
}
void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
List<Expression!> es = new List<Expression!>();
Expect(6);
- if (la.kind == 16) {
+ if (la.kind == 19) {
AttributeBody(ref attrs);
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else SynErr(139);
+ } else SynErr(143);
Expect(7);
}
void QSep() {
- if (la.kind == 98) {
+ if (la.kind == 101) {
Get();
- } else if (la.kind == 99) {
+ } else if (la.kind == 102) {
Get();
- } else SynErr(140);
+ } else SynErr(144);
}
void AttributeBody(ref Attributes attrs) {
@@ -1873,13 +1925,13 @@ List<Expression!>! decreases) { List<Attributes.Argument!> aArgs = new List<Attributes.Argument!>();
Attributes.Argument! aArg;
- Expect(16);
+ Expect(19);
Expect(1);
aName = t.val;
if (StartOf(17)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
- while (la.kind == 15) {
+ while (la.kind == 16) {
Get();
AttributeArg(out aArg);
aArgs.Add(aArg);
@@ -1900,24 +1952,24 @@ List<Expression!>! decreases) { }
static readonly bool[,]! set = {
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, T,x,x,x, T,T,T,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,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,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,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, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,T,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,T,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,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,T,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, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,T,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,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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, 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,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,T, 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,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,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},
- {x,T,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,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, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, T,x,x,x, T,T,T,T, T,T,x,T, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,x, x,x,x,x, 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, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,x,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,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,x,x, x,x,T,x, x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,T, T,x,T,x, T,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,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,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,T, x,x,x,x, x,x,x,x, x,T,x,x, T,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,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,T, T,x,T,x, T,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,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, T,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,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,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x},
+ {x,T,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x}
};
} // end Parser
@@ -1943,138 +1995,142 @@ public class Errors { case 6: s = "\"{\" expected"; break;
case 7: s = "\"}\" expected"; break;
case 8: s = "\"class\" expected"; break;
- case 9: s = "\"ghost\" expected"; break;
- case 10: s = "\"static\" expected"; break;
- case 11: s = "\"unlimited\" expected"; break;
- case 12: s = "\"datatype\" expected"; break;
- case 13: s = "\";\" expected"; break;
- case 14: s = "\"var\" expected"; break;
- case 15: s = "\",\" expected"; break;
- case 16: s = "\":\" expected"; break;
- case 17: s = "\"<\" expected"; break;
- case 18: s = "\">\" expected"; break;
- case 19: s = "\"method\" expected"; break;
- case 20: s = "\"returns\" expected"; break;
- case 21: s = "\"modifies\" expected"; break;
- case 22: s = "\"free\" expected"; break;
- case 23: s = "\"requires\" expected"; break;
- case 24: s = "\"ensures\" expected"; break;
- case 25: s = "\"decreases\" expected"; break;
- case 26: s = "\"(\" expected"; break;
- case 27: s = "\")\" expected"; break;
- case 28: s = "\"bool\" expected"; break;
- case 29: s = "\"int\" expected"; break;
- case 30: s = "\"set\" expected"; break;
- case 31: s = "\"seq\" expected"; break;
- case 32: s = "\"object\" expected"; break;
- case 33: s = "\"array\" expected"; break;
- case 34: s = "\"function\" expected"; break;
- case 35: s = "\"reads\" expected"; break;
- case 36: s = "\"*\" expected"; break;
- case 37: s = "\"`\" expected"; break;
- case 38: s = "\"match\" expected"; break;
- case 39: s = "\"case\" expected"; break;
- case 40: s = "\"=>\" expected"; break;
- case 41: s = "\"label\" expected"; break;
- case 42: s = "\"break\" expected"; break;
- case 43: s = "\"return\" expected"; break;
- case 44: s = "\":=\" expected"; break;
- case 45: s = "\"new\" expected"; break;
- case 46: s = "\"[\" expected"; break;
- case 47: s = "\"]\" expected"; break;
- case 48: s = "\"havoc\" expected"; break;
- case 49: s = "\"if\" expected"; break;
- case 50: s = "\"else\" expected"; break;
- case 51: s = "\"while\" expected"; break;
- case 52: s = "\"invariant\" expected"; break;
- case 53: s = "\"call\" expected"; break;
- case 54: s = "\"foreach\" expected"; break;
- case 55: s = "\"in\" expected"; break;
- case 56: s = "\"|\" expected"; break;
- case 57: s = "\"assert\" expected"; break;
- case 58: s = "\"assume\" expected"; break;
- case 59: s = "\"use\" expected"; break;
- case 60: s = "\"print\" expected"; break;
- case 61: s = "\"then\" expected"; break;
- case 62: s = "\"<==>\" expected"; break;
- case 63: s = "\"\\u21d4\" expected"; break;
- case 64: s = "\"==>\" expected"; break;
- case 65: s = "\"\\u21d2\" expected"; break;
- case 66: s = "\"&&\" expected"; break;
- case 67: s = "\"\\u2227\" expected"; break;
- case 68: s = "\"||\" expected"; break;
- case 69: s = "\"\\u2228\" expected"; break;
- case 70: s = "\"==\" expected"; break;
- case 71: s = "\"<=\" expected"; break;
- case 72: s = "\">=\" expected"; break;
- case 73: s = "\"!=\" expected"; break;
- case 74: s = "\"!!\" expected"; break;
- case 75: s = "\"!in\" expected"; break;
- case 76: s = "\"\\u2260\" expected"; break;
- case 77: s = "\"\\u2264\" expected"; break;
- case 78: s = "\"\\u2265\" 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 = "\"!\" expected"; break;
- case 84: s = "\"\\u00ac\" expected"; break;
- case 85: s = "\"false\" expected"; break;
- case 86: s = "\"true\" expected"; break;
- case 87: s = "\"null\" expected"; break;
- case 88: s = "\"#\" expected"; break;
- case 89: s = "\".\" expected"; break;
- case 90: s = "\"fresh\" expected"; break;
- case 91: s = "\"..\" expected"; break;
- case 92: s = "\"this\" expected"; break;
- case 93: s = "\"old\" expected"; break;
- case 94: s = "\"forall\" expected"; break;
- case 95: s = "\"\\u2200\" expected"; break;
- case 96: s = "\"exists\" expected"; break;
- case 97: s = "\"\\u2203\" expected"; break;
- case 98: s = "\"::\" expected"; break;
- case 99: s = "\"\\u2022\" expected"; break;
- case 100: s = "??? expected"; break;
- case 101: s = "invalid ClassMemberDecl"; break;
- case 102: s = "invalid FunctionDecl"; break;
- case 103: s = "invalid MethodDecl"; break;
- case 104: s = "invalid TypeAndToken"; break;
- case 105: s = "invalid MethodSpec"; break;
- case 106: s = "invalid MethodSpec"; break;
- case 107: s = "invalid Expression"; break;
- case 108: s = "invalid ReferenceType"; break;
- case 109: s = "invalid FunctionSpec"; break;
- case 110: s = "invalid FunctionBody"; break;
- case 111: s = "invalid PossiblyWildFrameExpression"; break;
- case 112: s = "invalid PossiblyWildExpression"; break;
- case 113: s = "invalid Stmt"; break;
- case 114: s = "invalid OneStmt"; break;
- case 115: s = "invalid IfStmt"; break;
- case 116: s = "invalid ForeachStmt"; break;
- case 117: s = "invalid AssignRhs"; break;
- case 118: s = "invalid SelectExpression"; break;
- case 119: s = "invalid Guard"; break;
- case 120: s = "invalid CallStmtSubExpr"; break;
- case 121: s = "invalid AttributeArg"; break;
- case 122: s = "invalid EquivOp"; break;
- case 123: s = "invalid ImpliesOp"; break;
- case 124: s = "invalid AndOp"; break;
- case 125: s = "invalid OrOp"; break;
- case 126: s = "invalid RelOp"; break;
- case 127: s = "invalid AddOp"; break;
- case 128: s = "invalid UnaryExpression"; break;
- case 129: s = "invalid MulOp"; break;
- case 130: s = "invalid NegOp"; break;
- case 131: s = "invalid ConstAtomExpression"; break;
- case 132: s = "invalid ObjectExpression"; break;
- case 133: s = "invalid ObjectExpression"; break;
- case 134: s = "invalid SelectOrCallSuffix"; break;
- case 135: s = "invalid SelectOrCallSuffix"; break;
- case 136: s = "invalid QuantifierGuts"; break;
- case 137: s = "invalid Forall"; break;
- case 138: s = "invalid Exists"; break;
- case 139: s = "invalid AttributeOrTrigger"; break;
- case 140: s = "invalid QSep"; break;
+ case 9: s = "\"refines\" expected"; break;
+ case 10: s = "\"ghost\" expected"; break;
+ case 11: s = "\"static\" expected"; break;
+ case 12: s = "\"unlimited\" expected"; break;
+ case 13: s = "\"datatype\" expected"; break;
+ case 14: s = "\";\" expected"; break;
+ case 15: s = "\"var\" expected"; break;
+ case 16: s = "\",\" expected"; break;
+ case 17: s = "\"replaces\" expected"; break;
+ case 18: s = "\"by\" expected"; break;
+ case 19: s = "\":\" expected"; break;
+ case 20: s = "\"<\" expected"; break;
+ case 21: s = "\">\" expected"; break;
+ case 22: s = "\"method\" expected"; break;
+ case 23: s = "\"returns\" expected"; break;
+ case 24: s = "\"modifies\" expected"; break;
+ case 25: s = "\"free\" expected"; break;
+ case 26: s = "\"requires\" expected"; break;
+ case 27: s = "\"ensures\" expected"; break;
+ case 28: s = "\"decreases\" expected"; break;
+ case 29: s = "\"(\" expected"; break;
+ case 30: s = "\")\" expected"; break;
+ case 31: s = "\"bool\" expected"; break;
+ case 32: s = "\"int\" expected"; break;
+ case 33: s = "\"set\" expected"; break;
+ case 34: s = "\"seq\" expected"; break;
+ case 35: s = "\"object\" expected"; break;
+ case 36: s = "\"array\" expected"; break;
+ case 37: s = "\"function\" expected"; break;
+ case 38: s = "\"reads\" expected"; break;
+ case 39: s = "\"*\" expected"; break;
+ case 40: s = "\"`\" expected"; break;
+ case 41: s = "\"match\" expected"; break;
+ case 42: s = "\"case\" expected"; break;
+ case 43: s = "\"=>\" expected"; break;
+ case 44: s = "\"label\" expected"; break;
+ case 45: s = "\"break\" expected"; break;
+ case 46: s = "\"return\" expected"; break;
+ case 47: s = "\":=\" expected"; break;
+ case 48: s = "\"new\" expected"; break;
+ case 49: s = "\"[\" expected"; break;
+ case 50: s = "\"]\" expected"; break;
+ case 51: s = "\"havoc\" expected"; break;
+ case 52: s = "\"if\" expected"; break;
+ case 53: s = "\"else\" expected"; break;
+ case 54: s = "\"while\" expected"; break;
+ case 55: s = "\"invariant\" expected"; break;
+ case 56: s = "\"call\" expected"; break;
+ case 57: s = "\"foreach\" expected"; break;
+ case 58: s = "\"in\" expected"; break;
+ case 59: s = "\"|\" expected"; break;
+ case 60: s = "\"assert\" expected"; break;
+ case 61: s = "\"assume\" expected"; break;
+ case 62: s = "\"use\" expected"; break;
+ case 63: s = "\"print\" expected"; break;
+ case 64: s = "\"then\" expected"; break;
+ case 65: s = "\"<==>\" expected"; break;
+ case 66: s = "\"\\u21d4\" expected"; break;
+ case 67: s = "\"==>\" expected"; break;
+ case 68: s = "\"\\u21d2\" expected"; break;
+ case 69: s = "\"&&\" expected"; break;
+ case 70: s = "\"\\u2227\" expected"; break;
+ case 71: s = "\"||\" expected"; break;
+ case 72: s = "\"\\u2228\" expected"; break;
+ case 73: s = "\"==\" expected"; break;
+ case 74: s = "\"<=\" expected"; break;
+ case 75: s = "\">=\" expected"; break;
+ case 76: s = "\"!=\" expected"; break;
+ case 77: s = "\"!!\" expected"; break;
+ case 78: s = "\"!in\" expected"; break;
+ case 79: s = "\"\\u2260\" expected"; break;
+ case 80: s = "\"\\u2264\" expected"; break;
+ case 81: s = "\"\\u2265\" expected"; break;
+ case 82: s = "\"+\" expected"; break;
+ case 83: s = "\"-\" expected"; break;
+ case 84: s = "\"/\" expected"; break;
+ case 85: s = "\"%\" expected"; break;
+ case 86: s = "\"!\" expected"; break;
+ case 87: s = "\"\\u00ac\" expected"; break;
+ case 88: s = "\"false\" expected"; break;
+ case 89: s = "\"true\" expected"; break;
+ case 90: s = "\"null\" expected"; break;
+ case 91: s = "\"#\" expected"; break;
+ case 92: s = "\".\" expected"; break;
+ case 93: s = "\"fresh\" expected"; break;
+ case 94: s = "\"..\" expected"; break;
+ case 95: s = "\"this\" expected"; break;
+ case 96: s = "\"old\" expected"; break;
+ case 97: s = "\"forall\" expected"; break;
+ case 98: s = "\"\\u2200\" expected"; break;
+ case 99: s = "\"exists\" expected"; break;
+ case 100: s = "\"\\u2203\" expected"; break;
+ case 101: s = "\"::\" expected"; break;
+ case 102: s = "\"\\u2022\" expected"; break;
+ case 103: s = "??? expected"; break;
+ case 104: s = "invalid ClassMemberDecl"; break;
+ case 105: s = "invalid FunctionDecl"; break;
+ case 106: s = "invalid MethodDecl"; break;
+ case 107: s = "invalid MethodDecl"; break;
+ case 108: s = "invalid Expression"; break;
+ case 109: s = "invalid TypeAndToken"; break;
+ case 110: s = "invalid MethodSpec"; break;
+ case 111: s = "invalid MethodSpec"; break;
+ case 112: s = "invalid ReferenceType"; break;
+ case 113: s = "invalid FunctionSpec"; break;
+ case 114: s = "invalid FunctionBody"; break;
+ case 115: s = "invalid PossiblyWildFrameExpression"; break;
+ case 116: s = "invalid PossiblyWildExpression"; break;
+ case 117: s = "invalid Stmt"; break;
+ case 118: s = "invalid OneStmt"; break;
+ case 119: s = "invalid IfStmt"; break;
+ case 120: s = "invalid ForeachStmt"; break;
+ case 121: s = "invalid AssignRhs"; break;
+ case 122: s = "invalid SelectExpression"; break;
+ case 123: s = "invalid Guard"; break;
+ case 124: s = "invalid CallStmtSubExpr"; break;
+ case 125: s = "invalid AttributeArg"; break;
+ case 126: s = "invalid EquivOp"; break;
+ case 127: s = "invalid ImpliesOp"; break;
+ case 128: s = "invalid AndOp"; break;
+ case 129: s = "invalid OrOp"; break;
+ case 130: s = "invalid RelOp"; break;
+ case 131: s = "invalid AddOp"; break;
+ case 132: s = "invalid UnaryExpression"; break;
+ case 133: s = "invalid MulOp"; break;
+ case 134: s = "invalid NegOp"; break;
+ case 135: s = "invalid ConstAtomExpression"; break;
+ case 136: s = "invalid ObjectExpression"; break;
+ case 137: s = "invalid ObjectExpression"; break;
+ case 138: s = "invalid SelectOrCallSuffix"; break;
+ case 139: s = "invalid SelectOrCallSuffix"; break;
+ case 140: s = "invalid QuantifierGuts"; break;
+ case 141: s = "invalid Forall"; break;
+ case 142: s = "invalid Exists"; break;
+ case 143: s = "invalid AttributeOrTrigger"; break;
+ case 144: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc index bf07e122..c269e621 100644 --- a/Source/Dafny/Printer.ssc +++ b/Source/Dafny/Printer.ssc @@ -70,9 +70,13 @@ namespace Microsoft.Dafny { }
}
- public void PrintClass(ClassDecl! c, int indent) {
+ public void PrintClass(ClassDecl! c, int indent) {
Indent(indent);
PrintClassMethodHelper("class", c.Attributes, c.Name, c.TypeArgs);
+ if (c is ClassRefinementDecl) {
+ wr.Write(" refines ");
+ wr.Write(((ClassRefinementDecl)c).RefinedClass.val);
+ }
if (c.Members.Count == 0) {
wr.WriteLine(" { }");
} else {
@@ -100,6 +104,10 @@ namespace Microsoft.Dafny { if (state != 0) { wr.WriteLine(); }
PrintFunction((Function)m, indent);
state = 2;
+ } else if (m is CouplingInvariant) {
+ wr.WriteLine();
+ PrintCouplingInvariant((CouplingInvariant)m, indent);
+ state = 2;
} else {
assert false; // unexpected member
}
@@ -174,6 +182,20 @@ namespace Microsoft.Dafny { wr.WriteLine(";");
}
+ public void PrintCouplingInvariant(CouplingInvariant! inv, int indent) {
+ Indent(indent);
+ wr.Write("replaces");
+ string sep = " ";
+ foreach (string tok in inv.Tokens()) {
+ wr.Write(sep);
+ wr.Write(tok);
+ sep = ", ";
+ }
+ wr.Write(" by ");
+ PrintExpression(inv.Expr);
+ wr.WriteLine(";");
+ }
+
public void PrintFunction(Function! f, int indent) {
Indent(indent);
string k = "function";
@@ -221,9 +243,9 @@ namespace Microsoft.Dafny { }
}
- public void PrintMethod(Method! method, int indent) {
+ public void PrintMethod(Method! method, int indent) {
Indent(indent);
- string k = "method";
+ string k = method is MethodRefinement ? "refines" : "method";
if (method.IsStatic) { k = "static " + k; }
if (method.IsGhost) { k = "ghost " + k; }
PrintClassMethodHelper(k, method.Attributes, method.Name, method.TypeArgs);
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 701668db..f1a09f9f 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -85,6 +85,13 @@ namespace Microsoft.Dafny { h++;
}
}
+
+ // resolve top-level declarations of refinements
+ foreach (ModuleDecl m in prog.Modules)
+ foreach (TopLevelDecl decl in m.TopLevelDecls)
+ if (decl is ClassRefinementDecl)
+ ResolveTopLevelRefinement((ClassRefinementDecl) decl);
+
// resolve top-level declarations
Graph<DatatypeDecl!> datatypeDependencies = new Graph<DatatypeDecl!>();
foreach (ModuleDecl m in prog.Modules) {
@@ -154,6 +161,22 @@ namespace Microsoft.Dafny { }
}
+ public void ResolveTopLevelRefinement(ClassRefinementDecl! decl) {
+ // TODO: check for loops in refinement
+ if (!classes.ContainsKey(decl.RefinedClass.val)) {
+ Error(decl.RefinedClass, "Refined class declaration is missing: {0}", decl.RefinedClass.val);
+ } else {
+ TopLevelDecl! a = classes[decl.RefinedClass.val];
+ if (!(a is ClassDecl)) {
+ Error(a, "Refined declaration is not a class declaration: {0}", a.Name);
+ return;
+ }
+ decl.Refined = (ClassDecl!) a;
+ // TODO: copy over remaining members of a
+ // TODO: extend with type parameters for refinements
+ }
+ }
+
public void ResolveTopLevelDecls_Signatures(List<TopLevelDecl!>! declarations, Graph<DatatypeDecl!>! datatypeDependencies) {
foreach (TopLevelDecl d in declarations) {
allTypeParameters.PushMarker();
@@ -216,10 +239,47 @@ namespace Microsoft.Dafny { ResolveTypeParameters(m.TypeArgs, true, m);
ResolveMethodSignature(m);
allTypeParameters.PopMarker();
-
+
+ } else if (member is CouplingInvariant) {
+ CouplingInvariant inv = (CouplingInvariant)member;
+ if (currentClass is ClassRefinementDecl) {
+ ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
+ assert refined != null;
+ assert classMembers.ContainsKey(refined);
+ Dictionary<string!,MemberDecl!> members = classMembers[refined];
+
+ // resolve abstracted fields in the refined class
+ List<Field!> fields = new List<Field!>();
+ foreach (IToken tok in inv.Toks) {
+ if (!members.ContainsKey(tok.val))
+ Error(tok, "Refined class does not declare a field: {0}", tok.val);
+ else {
+ MemberDecl! field = members[tok.val];
+ if (!(field is Field))
+ Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);
+ else if (fields.Contains((Field!)field))
+ Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);
+ else
+ fields.Add((Field!)field);
+ }
+ }
+ inv.Refined = fields;
+ } else {
+ Error(member, "Coupling invariants can only be declared in refinement classes");
+ }
} else {
assert false; // unexpected member type
}
+
+ if (currentClass is ClassRefinementDecl) {
+ ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
+ assert refined != null;
+ assert classMembers.ContainsKey(refined);
+
+ // there is a member with the same name in refined class if and only if the member is a refined method
+ if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))
+ Error(member, "Refined class has a member with the same name as in the refinement class: {0}", member.Name);
+ }
}
currentClass = null;
}
@@ -251,7 +311,40 @@ namespace Microsoft.Dafny { ResolveTypeParameters(m.TypeArgs, false, m);
ResolveMethod(m);
allTypeParameters.PopMarker();
-
+
+ // check if signature of the refined method matches the refinement method
+ if (member is MethodRefinement) {
+ MethodRefinement mf = (MethodRefinement)member;
+ assert currentClass is ClassRefinementDecl;
+ assert ((ClassRefinementDecl)currentClass).Refined != null; // should have already been resolved
+ MemberDecl d = classMembers[((ClassRefinementDecl)currentClass).Refined][mf.Name];
+ if (d is Method) {
+ mf.Refined = (Method)d;
+ if (mf.Ins.Count != mf.Refined.Ins.Count)
+ Error(mf, "Different number of input variables");
+ if (mf.Outs.Count != mf.Refined.Outs.Count)
+ Error(mf, "Different number of output variables");
+ if (mf.IsStatic || mf.Refined.IsStatic)
+ Error(mf, "Refined methods cannot be static");
+ } else {
+ Error(member, "Refined class has a non-method member with the same name: {0}", member.Name);
+ }
+ }
+
+ } else if (member is CouplingInvariant) {
+ CouplingInvariant inv = (CouplingInvariant)member;
+ assert inv.Refined != null;
+ inv.Formals = new List<Formal!>();
+ scope.PushMarker();
+ for (int i = 0; i < inv.Refined.Count; i++) {
+ Field! field = inv.Refined[i];
+ Formal! formal = new Formal(inv.Toks[i], field.Name, field.Type, true, field.IsGhost);
+ inv.Formals.Add(formal);
+ scope.Push(inv.Toks[i].val, formal);
+ }
+ ResolveExpression(inv.Expr, false, true);
+ scope.PopMarker();
+
} else {
assert false; // unexpected member type
}
diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc index 98114e54..dbff78e7 100644 --- a/Source/Dafny/Scanner.ssc +++ b/Source/Dafny/Scanner.ssc @@ -7,9 +7,10 @@ using System.Text; using Microsoft.Contracts;
using Microsoft.Boogie;
using BoogiePL;
-namespace Microsoft.Dafny {
+namespace Microsoft.Dafny {
+
//-----------------------------------------------------------------------------------
// Buffer
//-----------------------------------------------------------------------------------
@@ -202,8 +203,8 @@ public class UTF8Buffer: Buffer { public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 100;
- const int noSym = 100;
+ const int maxT = 103;
+ const int noSym = 103;
public Buffer! buffer; // scanner buffer
@@ -463,53 +464,56 @@ public class Scanner { case "module": t.kind = 4; break;
case "imports": t.kind = 5; break;
case "class": t.kind = 8; break;
- case "ghost": t.kind = 9; break;
- case "static": t.kind = 10; break;
- case "unlimited": t.kind = 11; break;
- case "datatype": t.kind = 12; break;
- case "var": t.kind = 14; break;
- case "method": t.kind = 19; break;
- case "returns": t.kind = 20; break;
- case "modifies": t.kind = 21; break;
- case "free": t.kind = 22; break;
- case "requires": t.kind = 23; break;
- case "ensures": t.kind = 24; break;
- case "decreases": t.kind = 25; break;
- case "bool": t.kind = 28; break;
- case "int": t.kind = 29; break;
- case "set": t.kind = 30; break;
- case "seq": t.kind = 31; break;
- case "object": t.kind = 32; break;
- case "array": t.kind = 33; break;
- case "function": t.kind = 34; break;
- case "reads": t.kind = 35; break;
- case "match": t.kind = 38; break;
- case "case": t.kind = 39; break;
- case "label": t.kind = 41; break;
- case "break": t.kind = 42; break;
- case "return": t.kind = 43; break;
- case "new": t.kind = 45; break;
- case "havoc": t.kind = 48; break;
- case "if": t.kind = 49; break;
- case "else": t.kind = 50; break;
- case "while": t.kind = 51; break;
- case "invariant": t.kind = 52; break;
- case "call": t.kind = 53; break;
- case "foreach": t.kind = 54; break;
- case "in": t.kind = 55; break;
- case "assert": t.kind = 57; break;
- case "assume": t.kind = 58; break;
- case "use": t.kind = 59; break;
- case "print": t.kind = 60; break;
- case "then": t.kind = 61; break;
- case "false": t.kind = 85; break;
- case "true": t.kind = 86; break;
- case "null": t.kind = 87; break;
- case "fresh": t.kind = 90; break;
- case "this": t.kind = 92; break;
- case "old": t.kind = 93; break;
- case "forall": t.kind = 94; break;
- case "exists": t.kind = 96; break;
+ case "refines": t.kind = 9; break;
+ case "ghost": t.kind = 10; break;
+ case "static": t.kind = 11; break;
+ case "unlimited": t.kind = 12; break;
+ case "datatype": t.kind = 13; break;
+ case "var": t.kind = 15; break;
+ case "replaces": t.kind = 17; break;
+ case "by": t.kind = 18; break;
+ case "method": t.kind = 22; break;
+ case "returns": t.kind = 23; break;
+ case "modifies": t.kind = 24; break;
+ case "free": t.kind = 25; break;
+ case "requires": t.kind = 26; break;
+ case "ensures": t.kind = 27; break;
+ case "decreases": t.kind = 28; break;
+ case "bool": t.kind = 31; break;
+ case "int": t.kind = 32; break;
+ case "set": t.kind = 33; break;
+ case "seq": t.kind = 34; break;
+ case "object": t.kind = 35; break;
+ case "array": t.kind = 36; break;
+ case "function": t.kind = 37; break;
+ case "reads": t.kind = 38; break;
+ case "match": t.kind = 41; break;
+ case "case": t.kind = 42; break;
+ case "label": t.kind = 44; break;
+ case "break": t.kind = 45; break;
+ case "return": t.kind = 46; break;
+ case "new": t.kind = 48; break;
+ case "havoc": t.kind = 51; break;
+ case "if": t.kind = 52; break;
+ case "else": t.kind = 53; break;
+ case "while": t.kind = 54; break;
+ case "invariant": t.kind = 55; break;
+ case "call": t.kind = 56; break;
+ case "foreach": t.kind = 57; break;
+ case "in": t.kind = 58; break;
+ case "assert": t.kind = 60; break;
+ case "assume": t.kind = 61; break;
+ case "use": t.kind = 62; break;
+ case "print": t.kind = 63; break;
+ case "then": t.kind = 64; break;
+ case "false": t.kind = 88; break;
+ case "true": t.kind = 89; break;
+ case "null": t.kind = 90; break;
+ case "fresh": t.kind = 93; break;
+ case "this": t.kind = 95; break;
+ case "old": t.kind = 96; break;
+ case "forall": t.kind = 97; break;
+ case "exists": t.kind = 99; break;
default: break;
}
}
@@ -557,125 +561,125 @@ public class Scanner { case 6:
{t.kind = 7; break;}
case 7:
- {t.kind = 13; break;}
+ {t.kind = 14; break;}
case 8:
- {t.kind = 15; break;}
+ {t.kind = 16; break;}
case 9:
- {t.kind = 26; break;}
+ {t.kind = 29; break;}
case 10:
- {t.kind = 27; break;}
+ {t.kind = 30; break;}
case 11:
- {t.kind = 36; break;}
+ {t.kind = 39; break;}
case 12:
- {t.kind = 37; break;}
- case 13:
{t.kind = 40; break;}
+ case 13:
+ {t.kind = 43; break;}
case 14:
- {t.kind = 44; break;}
+ {t.kind = 47; break;}
case 15:
- {t.kind = 46; break;}
+ {t.kind = 49; break;}
case 16:
- {t.kind = 47; break;}
+ {t.kind = 50; break;}
case 17:
if (ch == '>') {AddCh(); goto case 18;}
else {goto case 0;}
case 18:
- {t.kind = 62; break;}
+ {t.kind = 65; break;}
case 19:
- {t.kind = 63; break;}
+ {t.kind = 66; break;}
case 20:
- {t.kind = 64; break;}
+ {t.kind = 67; break;}
case 21:
- {t.kind = 65; break;}
+ {t.kind = 68; break;}
case 22:
if (ch == '&') {AddCh(); goto case 23;}
else {goto case 0;}
case 23:
- {t.kind = 66; break;}
+ {t.kind = 69; break;}
case 24:
- {t.kind = 67; break;}
+ {t.kind = 70; break;}
case 25:
- {t.kind = 68; break;}
+ {t.kind = 71; break;}
case 26:
- {t.kind = 69; break;}
- case 27:
{t.kind = 72; break;}
+ case 27:
+ {t.kind = 75; break;}
case 28:
- {t.kind = 73; break;}
+ {t.kind = 76; break;}
case 29:
- {t.kind = 74; break;}
+ {t.kind = 77; break;}
case 30:
if (ch == 'n') {AddCh(); goto case 31;}
else {goto case 0;}
case 31:
- {t.kind = 75; break;}
+ {t.kind = 78; break;}
case 32:
- {t.kind = 76; break;}
+ {t.kind = 79; break;}
case 33:
- {t.kind = 77; break;}
+ {t.kind = 80; break;}
case 34:
- {t.kind = 78; break;}
+ {t.kind = 81; break;}
case 35:
- {t.kind = 79; break;}
+ {t.kind = 82; break;}
case 36:
- {t.kind = 80; break;}
+ {t.kind = 83; break;}
case 37:
- {t.kind = 81; break;}
+ {t.kind = 84; break;}
case 38:
- {t.kind = 82; break;}
+ {t.kind = 85; break;}
case 39:
- {t.kind = 84; break;}
+ {t.kind = 87; break;}
case 40:
- {t.kind = 88; break;}
- case 41:
{t.kind = 91; break;}
+ case 41:
+ {t.kind = 94; break;}
case 42:
- {t.kind = 95; break;}
+ {t.kind = 98; break;}
case 43:
- {t.kind = 97; break;}
+ {t.kind = 100; break;}
case 44:
- {t.kind = 98; break;}
+ {t.kind = 101; break;}
case 45:
- {t.kind = 99; break;}
+ {t.kind = 102; break;}
case 46:
- recEnd = pos; recKind = 16;
+ recEnd = pos; recKind = 19;
if (ch == '=') {AddCh(); goto case 14;}
else if (ch == ':') {AddCh(); goto case 44;}
- else {t.kind = 16; break;}
+ else {t.kind = 19; break;}
case 47:
- recEnd = pos; recKind = 17;
+ recEnd = pos; recKind = 20;
if (ch == '=') {AddCh(); goto case 53;}
- else {t.kind = 17; break;}
+ else {t.kind = 20; break;}
case 48:
- recEnd = pos; recKind = 18;
+ recEnd = pos; recKind = 21;
if (ch == '=') {AddCh(); goto case 27;}
- else {t.kind = 18; break;}
+ else {t.kind = 21; break;}
case 49:
if (ch == '>') {AddCh(); goto case 13;}
else if (ch == '=') {AddCh(); goto case 54;}
else {goto case 0;}
case 50:
- recEnd = pos; recKind = 56;
+ recEnd = pos; recKind = 59;
if (ch == '|') {AddCh(); goto case 25;}
- else {t.kind = 56; break;}
+ else {t.kind = 59; break;}
case 51:
- recEnd = pos; recKind = 83;
+ recEnd = pos; recKind = 86;
if (ch == '=') {AddCh(); goto case 28;}
else if (ch == '!') {AddCh(); goto case 29;}
else if (ch == 'i') {AddCh(); goto case 30;}
- else {t.kind = 83; break;}
+ else {t.kind = 86; break;}
case 52:
- recEnd = pos; recKind = 89;
+ recEnd = pos; recKind = 92;
if (ch == '.') {AddCh(); goto case 41;}
- else {t.kind = 89; break;}
+ else {t.kind = 92; break;}
case 53:
- recEnd = pos; recKind = 71;
+ recEnd = pos; recKind = 74;
if (ch == '=') {AddCh(); goto case 17;}
- else {t.kind = 71; break;}
+ else {t.kind = 74; break;}
case 54:
- recEnd = pos; recKind = 70;
+ recEnd = pos; recKind = 73;
if (ch == '>') {AddCh(); goto case 20;}
- else {t.kind = 70; break;}
+ else {t.kind = 73; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index 06d6bb1d..58eb90bb 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -432,14 +432,24 @@ namespace Microsoft.Dafny { } else if (member is Method) {
Method m = (Method)member;
// wellformedness check for method specification
- Bpl.Procedure proc = AddMethod(m, true);
+ Bpl.Procedure proc = AddMethod(m, true, false);
+ sink.TopLevelDeclarations.Add(proc);
AddMethodImpl(m, proc, true);
// the method itself
- proc = AddMethod(m, false);
+ proc = AddMethod(m, false, false);
+ sink.TopLevelDeclarations.Add(proc);
if (m.Body != null) {
// ...and its implementation
AddMethodImpl(m, proc, false);
}
+
+ // refinement condition
+ if (member is MethodRefinement) {
+ AddMethodRefinement((MethodRefinement)member);
+ }
+
+ } else if (member is CouplingInvariant) {
+ // TODO: define a well-foundedness condition to check
} else {
assert false; // unexpected member
@@ -801,6 +811,15 @@ namespace Microsoft.Dafny { requires predef != null;
{
// Add CEV prelude
+ CEVPrelude(m, inParams, outParams, builder);
+
+ // set up the information used to verify the method's modifies clause
+ DefineFrame(m.tok, m.Mod, builder, localVariables);
+ }
+
+ void CEVPrelude(Method! m, Bpl.VariableSeq! inParams, Bpl.VariableSeq! outParams, Bpl.StmtListBuilder! builder)
+ requires predef != null;
+ {
builder.Add(Bpl.Cmd.SimpleAssign(m.tok, Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int), Bpl.Expr.Add(Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int), Bpl.Expr.Literal(1))));
foreach (Bpl.Variable p in inParams) {
assert p != null;
@@ -821,10 +840,7 @@ namespace Microsoft.Dafny { CevVariable(p.tok, p.Name),
new Bpl.IdentifierExpr(p.tok, p.Name, p.TypedIdent.Type)), // it's important not to pass in just p, because that resolves to the proc's param, not the impl's param
new Bpl.IdentifierExprSeq()));
- }
-
- // set up the information used to verify the method's modifies clause
- DefineFrame(m.tok, m.Mod, builder, localVariables);
+ }
}
void DefineFrame(IToken! tok, List<FrameExpression!>! frameClause, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! localVariables)
@@ -1602,10 +1618,12 @@ namespace Microsoft.Dafny { /// <summary>
/// This method is expected to be called just twice for each procedure in the program (once with
/// wellformednessProc set to true, once with wellformednessProc set to false).
+ /// In addition, it is used once to generate refinement conditions.
/// </summary>
- Bpl.Procedure! AddMethod(Method! m, bool wellformednessProc)
- requires predef != null && sink != null;
+ Bpl.Procedure! AddMethod(Method! m, bool wellformednessProc, bool skipEnsures)
+ requires predef != null;
requires m.EnclosingClass != null;
+ requires skipEnsures ==> !wellformednessProc;
{
ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
@@ -1665,7 +1683,7 @@ namespace Microsoft.Dafny { comment = null;
}
comment = "user-defined postconditions";
- foreach (MaybeFreeExpression p in m.Ens) {
+ if (!skipEnsures) foreach (MaybeFreeExpression p in m.Ens) {
if (p.IsFree) {
ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));
} else {
@@ -1687,7 +1705,7 @@ namespace Microsoft.Dafny { }
comment = null;
}
- foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m, etran.Old, etran)) {
+ if (!skipEnsures) foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m, etran.Old, etran)) {
ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));
}
}
@@ -1712,9 +1730,143 @@ namespace Microsoft.Dafny { Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
string name = wellformednessProc ? "CheckWellformed$$" + m.FullName : m.FullName;
Bpl.Procedure proc = new Bpl.Procedure(m.tok, name, typeParams, inParams, outParams, req, mod, ens);
- sink.TopLevelDeclarations.Add(proc);
return proc;
}
+
+ #region Refinement extension
+
+ void AddMethodRefinement(MethodRefinement! m)
+ requires sink != null && predef != null;
+ {
+ Method r = m.Refined;
+ assert r != null;
+ assert m.EnclosingClass != null;
+ string! name = "Refinement$$" + m.FullName;
+ string! that = "that";
+
+ Bpl.IdentifierExpr heap = new Bpl.IdentifierExpr(m.tok, predef.HeapVarName, predef.HeapType);
+ ExpressionTranslator etran = new ExpressionTranslator(this, predef, heap, that);
+
+ // for now, refinement is local -- if A.f is refined by B.g then f is shadowed by g in B.
+ // therefore, the abstract and concrete programs operate on different receivers thisA and thisB.
+ // there is still a possibility of A events polluting the heap that's used by B events, e.g. if another object is referenced by both thisA and thisB.
+
+ // TODO: this straight inlining does not handle recursive calls
+ // TODO: we assume frame allows anything to be changed
+
+ // generate procedure declaration with pre-condition wp(r, true)
+ Bpl.Procedure! proc = AddMethod(r, false, true);
+ proc.Name = name;
+
+ // create "that" for m
+ Bpl.Expr wh = Bpl.Expr.And(
+ Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, that, predef.RefType), predef.Null),
+ etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, that, predef.RefType), Resolver.GetThisType(m.tok, m.EnclosingClass)));
+ Bpl.Formal thatVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, that, predef.RefType, wh), true);
+ proc.InParams.Add(thatVar);
+ sink.TopLevelDeclarations.Add(proc);
+
+ // generate procedure implementation:
+ Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
+ Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
+ Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);
+ Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
+ Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
+
+ assert m.Body != null;
+ assert r.Body != null;
+
+ // declare a frame variable that allows anything to be changed (not checking modifies clauses)
+ CEVPrelude(m, inParams, outParams, builder);
+ Bpl.IdentifierExpr theFrame = etran.TheFrame(m.tok);
+ assert theFrame.Type != null;
+ Bpl.LocalVariable frame = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, theFrame.Name, theFrame.Type));
+ localVariables.Add(frame);
+ // $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: true);
+ Bpl.TypeVariable alpha = new Bpl.TypeVariable(m.tok, "alpha");
+ Bpl.BoundVariable oVar = new Bpl.BoundVariable(m.tok, new Bpl.TypedIdent(m.tok, "$o", predef.RefType));
+ Bpl.BoundVariable fVar = new Bpl.BoundVariable(m.tok, new Bpl.TypedIdent(m.tok, "$f", predef.FieldName(m.tok, alpha)));
+ Bpl.Expr lambda = new Bpl.LambdaExpr(m.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, Bpl.Expr.True);
+ builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, frame), lambda));
+
+ // assume I($Heap, $Heap)
+ builder.Add(new Bpl.AssumeCmd(m.tok, TrCouplingInvariant(m, heap, "this", heap, that)));
+
+ // call inlined m;
+ currentMethod = m;
+ TrStmt(m.Body, builder, localVariables, etran);
+ currentMethod = null;
+
+ // $Heap1 := $Heap;
+ Bpl.LocalVariable heap2 = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, heap.Name+"2", predef.HeapType));
+ localVariables.Add(heap2);
+ builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, heap2), etran.HeapExpr));
+
+ // $Heap := old($Heap);
+ builder.Add(Bpl.Cmd.SimpleAssign(m.tok, heap, new Bpl.OldExpr(m.tok, heap)));
+
+ // call inlined r;
+ currentMethod = r;
+ etran = new ExpressionTranslator(this, predef, heap, "this");
+ TrStmt(r.Body, builder, localVariables, etran);
+ currentMethod = null;
+
+ // assert I($Heap1, $Heap)
+ builder.Add(new Bpl.AssertCmd(m.tok, TrCouplingInvariant(m, heap, "this", new Bpl.IdentifierExpr(m.tok, heap2), that)));
+
+ Bpl.StmtList stmts = builder.Collect(m.tok);
+ Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,
+ typeParams, inParams, outParams,
+ localVariables, stmts);
+ sink.TopLevelDeclarations.Add(impl);
+ }
+
+ private sealed class NominalSubstituter : Duplicator
+ {
+ private readonly Dictionary<string!,Bpl.Expr!>! subst;
+ public NominalSubstituter(Dictionary<string!,Bpl.Expr!>! subst) { this.subst = subst; base(); }
+
+ public override Expr! VisitIdentifierExpr(Bpl.IdentifierExpr! node)
+ {
+ if (subst.ContainsKey(node.Name))
+ return subst[node.Name];
+ else
+ return base.VisitIdentifierExpr(node);
+ }
+ }
+
+ Bpl.Expr! TrCouplingInvariant(MethodRefinement! m, Bpl.Expr! absHeap, string! absThis, Bpl.Expr! conHeap, string! conThis)
+ requires predef != null;
+ {
+ Bpl.Expr! cond = Bpl.Expr.True;
+ ClassRefinementDecl c = m.EnclosingClass as ClassRefinementDecl;
+ assert c != null;
+ ExpressionTranslator etran = new ExpressionTranslator(this, predef, conHeap, conThis);
+
+ foreach (MemberDecl d in c.Members)
+ if (d is CouplingInvariant) {
+ CouplingInvariant inv = (CouplingInvariant)d;
+
+ assert inv.Refined != null;
+ assert inv.Formals != null;
+
+ // replace formals with field dereferences
+ Dictionary<string!,Bpl.Expr!>! map = new Dictionary<string!,Bpl.Expr!>();
+ Bpl.Expr! absVar = new Bpl.IdentifierExpr(d.tok, absThis, predef.RefType);
+ for (int i = 0; i < inv.Refined.Count; i++) {
+ // TODO: boxing/unboxing?
+ Bpl.Expr! result = Bpl.Expr.SelectTok(inv.Toks[i], absHeap, absVar, new Bpl.IdentifierExpr(inv.Toks[i], GetField((!)inv.Refined[i])));
+ map.Add(inv.Formals[i].UniqueName, result);
+ }
+
+ Bpl.Expr! e = new NominalSubstituter(map).VisitExpr(etran.TrExpr(inv.Expr));
+ cond = Bpl.Expr.And(cond, e);
+ }
+
+ return cond;
+ }
+
+ #endregion
class BoilerplateTriple { // a triple that is now a quintuple
public readonly IToken! tok;
@@ -2861,18 +3013,28 @@ namespace Microsoft.Dafny { public readonly Bpl.Expr! HeapExpr;
public readonly PredefinedDecls! predef;
public readonly Translator! translator;
+ public readonly string! This;
readonly Function applyLimited_CurrentFunction;
public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, IToken! heapToken) {
this.translator = translator;
this.predef = predef;
- HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);
+ this.HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);
+ this.This = "this";
}
public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Bpl.Expr! heap) {
this.translator = translator;
this.predef = predef;
this.HeapExpr = heap;
+ this.This = "this";
+ }
+
+ public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Bpl.Expr! heap, string! thisVar) {
+ this.translator = translator;
+ this.predef = predef;
+ this.HeapExpr = heap;
+ this.This = thisVar;
}
ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Bpl.Expr! heap, Function applyLimited_CurrentFunction) {
@@ -2880,7 +3042,8 @@ namespace Microsoft.Dafny { this.predef = predef;
this.HeapExpr = heap;
this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;
- }
+ this.This = "this";
+ }
ExpressionTranslator oldEtran;
public ExpressionTranslator! Old {
@@ -2939,7 +3102,7 @@ namespace Microsoft.Dafny { }
} else if (expr is ThisExpr) {
- return new Bpl.IdentifierExpr(expr.tok, "this", predef.RefType);
+ return new Bpl.IdentifierExpr(expr.tok, This, predef.RefType);
} else if (expr is IdentifierExpr) {
IdentifierExpr e = (IdentifierExpr)expr;
|