summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Reza Ahmadi <reza.ahmadi@uta.fi>2014-07-18 21:16:40 +0300
committerGravatar Reza Ahmadi <reza.ahmadi@uta.fi>2014-07-18 21:16:40 +0300
commit77143c833cbb14a20c704fb60fc28dd94edb44eb (patch)
tree7da7588d8dccb94fb1c5c42f23ec69c4edab2785 /Source
parentc377658acba5472b6d0c1e1452ce4c4c8f1fc28e (diff)
added trait feature:
-possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods
Diffstat (limited to 'Source')
-rw-r--r--Source/Dafny/Cloner.cs40
-rw-r--r--Source/Dafny/Compiler.cs306
-rw-r--r--Source/Dafny/Dafny.atg40
-rw-r--r--Source/Dafny/DafnyAst.cs26
-rw-r--r--Source/Dafny/Parser.cs1398
-rw-r--r--Source/Dafny/Printer.cs2
-rw-r--r--Source/Dafny/RefinementTransformer.cs84
-rw-r--r--Source/Dafny/Resolver.cs184
-rw-r--r--Source/Dafny/Scanner.cs226
-rw-r--r--Source/Dafny/Translator.cs603
-rw-r--r--Source/DafnyDriver/DafnyDriver.cs2
-rw-r--r--Source/DafnyExtension/TokenTagger.cs2
12 files changed, 2018 insertions, 895 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index bb644825..5dfc67d5 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -67,14 +67,34 @@ namespace Microsoft.Dafny
req, ens, yreq, yens,
body, CloneAttributes(dd.Attributes), dd.SignatureEllipsis);
return iter;
- } else if (d is ClassDecl) {
+ }
+ else if (d is TraitDecl)
+ {
+ if (d is DefaultClassDecl)
+ {
+ var dd = (TraitDecl)d;
+ var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+ var mm = dd.Members.ConvertAll(CloneMember);
+ var cl = new DefaultClassDecl(m, mm);
+ return cl;
+ }
+ else
+ {
+ var dd = (TraitDecl)d;
+ var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+ var mm = dd.Members.ConvertAll(CloneMember);
+ var cl = new TraitDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes));
+ return cl;
+ }
+ }
+ else if (d is ClassDecl) {
var dd = (ClassDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var mm = dd.Members.ConvertAll(CloneMember);
if (d is DefaultClassDecl) {
return new DefaultClassDecl(m, mm);
} else {
- return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes));
+ return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), new List<IToken> { dd.TraitId });
}
} else if (d is ModuleDecl) {
if (d is LiteralModuleDecl) {
@@ -115,13 +135,23 @@ namespace Microsoft.Dafny
if (member is Field) {
Contract.Assert(!(member is SpecialField)); // we don't expect a SpecialField to be cloned (or do we?)
var f = (Field)member;
- return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, f.IsUserMutable, CloneType(f.Type), CloneAttributes(f.Attributes));
+ Field field = new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, f.IsUserMutable, CloneType(f.Type), CloneAttributes(f.Attributes));
+ field.Inherited = member.Inherited; //we do need this information in ResolveClassMemberTypes method
+ if (field.Type is UserDefinedType)
+ ((UserDefinedType)field.Type).ResolvedClass = ((UserDefinedType)(((Field)(member)).Type)).ResolvedClass;
+ return field;
} else if (member is Function) {
var f = (Function)member;
- return CloneFunction(f);
+ f.Inherited = member.Inherited;
+ Function func = CloneFunction(f);
+ func.Inherited = member.Inherited;
+ return func;
} else {
var m = (Method)member;
- return CloneMethod(m);
+ m.Inherited = member.Inherited;
+ Method method = CloneMethod(m);
+ method.Inherited = member.Inherited;
+ return method;
}
}
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index c665026c..7be7f58f 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -206,10 +206,51 @@ namespace Microsoft.Dafny {
// end of the class
Indent(indent); wr.WriteLine("}");
- } else if (d is ClassDecl) {
+ }
+ else if (d is TraitDecl)
+ {
+ //writing the trait
+ var trait = (TraitDecl)d;
+ Indent(indent);
+ wr.Write("public interface @{0}", trait.CompileName);
+ wr.WriteLine(" {");
+ CompileClassMembers(trait, indent + IndentAmount);
+ Indent(indent); wr.WriteLine("}");
+
+ //writing the _Companion class
+ List<MemberDecl> members = new List<MemberDecl>();
+ foreach (MemberDecl mem in trait.Members)
+ {
+ if (mem.IsStatic)
+ {
+ if (mem is Function)
+ {
+ if (((Function)mem).Body != null)
+ members.Add(mem);
+ }
+ if (mem is Method)
+ {
+ if (((Method)mem).Body != null)
+ members.Add(mem);
+ }
+ }
+ }
+ var cl = new ClassDecl(d.tok, d.Name, d.Module, d.TypeArgs, members, d.Attributes, null);
+ Indent(indent);
+ wr.Write("public class @_Companion_{0}", cl.CompileName);
+ wr.WriteLine(" {");
+ CompileClassMembers(cl, indent + IndentAmount);
+ Indent(indent); wr.WriteLine("}");
+ }
+ else if (d is ClassDecl) {
var cl = (ClassDecl)d;
Indent(indent);
- wr.Write("public class @{0}", cl.CompileName);
+ if (cl.Trait != null && cl.Trait is TraitDecl)
+ {
+ wr.WriteLine("public class @{0} : @{1}", cl.CompileName, cl.TraitId.val);
+ }
+ else
+ wr.Write("public class @{0}", cl.CompileName);
if (cl.TypeArgs.Count != 0) {
wr.Write("<{0}>", TypeParameters(cl.TypeArgs));
}
@@ -708,98 +749,186 @@ namespace Microsoft.Dafny {
if (member is Field) {
Field f = (Field)member;
if (!f.IsGhost) {
- Indent(indent);
- wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.CompileName, DefaultValue(f.Type));
+ if (c is TraitDecl)
+ {
+ {
+ Indent(indent);
+ wr.Write("{0} @{1}", TypeName(f.Type), f.CompileName);
+ wr.Write(" {");
+ wr.Write(" get; set; ");
+ wr.WriteLine("}");
+ }
+ }
+ else
+ {
+ if (f.Inherited)
+ {
+ Indent(indent);
+ wr.WriteLine("public {0} @{1};", TypeName(f.Type), f.CompileName);
+ wr.Write("{0} @{1}.@{2}", TypeName(f.Type), c.Trait.CompileName, f.CompileName);
+ wr.WriteLine(" {");
+ wr.WriteLine(" get { ");
+ wr.Write("return this.@{0};", f.CompileName);
+ wr.WriteLine("}");
+ wr.WriteLine(" set { ");
+ wr.WriteLine("this.@{0} = value;", f.CompileName);
+ wr.WriteLine("}");
+ wr.WriteLine("}");
+ }
+ else
+ {
+ Indent(indent);
+ wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.CompileName, DefaultValue(f.Type));
+ }
+ }
}
-
} else if (member is Function) {
Function f = (Function)member;
- if (f.Body == null) {
- if (!Attributes.Contains(f.Attributes, "axiom")) {
- Error("Function {0} has no body", f.FullName);
- }
- } else if (f.IsGhost) {
- var v = new CheckHasNoAssumes_Visitor(this);
- v.Visit(f.Body);
- } else {
- Indent(indent);
- wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.CompileName);
- if (f.TypeArgs.Count != 0) {
- wr.Write("<{0}>", TypeParameters(f.TypeArgs));
- }
- wr.Write("(");
- WriteFormals("", f.Formals);
- wr.WriteLine(") {");
- CompileReturnBody(f.Body, indent + IndentAmount);
- Indent(indent); wr.WriteLine("}");
+ if (c is TraitDecl)
+ {
+ if (member.IsStatic && f.Body == null)
+ {
+ Error("Function {0} has no body", f.FullName);
+ }
+ else if (!member.IsStatic) //static members are not included in the target trait
+ {
+ Indent(indent);
+ wr.Write("{0} @{1}", TypeName(f.ResultType), f.CompileName);
+ wr.Write("(");
+ WriteFormals("", f.Formals);
+ wr.WriteLine(");");
+ }
+ }
+ else
+ {
+ if (f.Body == null)
+ {
+ if (!Attributes.Contains(f.Attributes, "axiom"))
+ {
+ Error("Function {0} has no body", f.FullName);
+ }
+ }
+ else if (f.IsGhost)
+ {
+ var v = new CheckHasNoAssumes_Visitor(this);
+ v.Visit(f.Body);
+ }
+ else
+ {
+ Indent(indent);
+ wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.CompileName);
+ if (f.TypeArgs.Count != 0)
+ {
+ wr.Write("<{0}>", TypeParameters(f.TypeArgs));
+ }
+ wr.Write("(");
+ WriteFormals("", f.Formals);
+ wr.WriteLine(") {");
+ CompileReturnBody(f.Body, indent + IndentAmount);
+ Indent(indent); wr.WriteLine("}");
+ }
}
-
} else if (member is Method) {
Method m = (Method)member;
- if (m.Body == null) {
- if (!Attributes.Contains(m.Attributes, "axiom")) {
- Error("Method {0} has no body", m.FullName);
- }
- } else if (m.IsGhost) {
- var v = new CheckHasNoAssumes_Visitor(this);
- v.Visit(m.Body);
- } else {
- Indent(indent);
- wr.Write("public {0}void @{1}", m.IsStatic ? "static " : "", m.CompileName);
- if (m.TypeArgs.Count != 0) {
- wr.Write("<{0}>", TypeParameters(m.TypeArgs));
- }
- wr.Write("(");
- int nIns = WriteFormals("", m.Ins);
- WriteFormals(nIns == 0 ? "" : ", ", m.Outs);
- wr.WriteLine(")");
- Indent(indent); wr.WriteLine("{");
- foreach (Formal p in m.Outs) {
- if (!p.IsGhost) {
- Indent(indent + IndentAmount);
- wr.WriteLine("@{0} = {1};", p.CompileName, DefaultValue(p.Type));
+ if (c is TraitDecl)
+ {
+ if (member.IsStatic && m.Body == null)
+ {
+ Error("Method {0} has no body", m.FullName);
}
- }
- if (m.Body == null) {
- Error("Method {0} has no body", m.FullName);
- } else {
- if (m.IsTailRecursive) {
- Indent(indent); wr.WriteLine("TAIL_CALL_START: ;");
- if (!m.IsStatic) {
- Indent(indent + IndentAmount); wr.WriteLine("var _this = this;");
- }
+ else if (!member.IsStatic) //static members are not included in the target trait
+ {
+ Indent(indent);
+ wr.Write("void @{0}", m.CompileName);
+ wr.Write("(");
+ int nIns = WriteFormals("", m.Ins);
+ WriteFormals(nIns == 0 ? "" : ", ", m.Outs);
+ wr.WriteLine(");");
}
- Contract.Assert(enclosingMethod == null);
- enclosingMethod = m;
- TrStmtList(m.Body.Body, indent);
- Contract.Assert(enclosingMethod == m);
- enclosingMethod = null;
- }
- Indent(indent); wr.WriteLine("}");
-
- // allow the Main method to be an instance method
- if (!m.IsStatic && m.Name == "Main" && m.TypeArgs.Count == 0 && m.Ins.Count == 0 && m.Outs.Count == 0 && m.Req.Count == 0) {
- Indent(indent);
- wr.WriteLine("public static void Main(string[] args) {");
- Contract.Assert(m.EnclosingClass == c);
- Indent(indent + IndentAmount);
- wr.Write("@{0} b = new @{0}", c.CompileName);
- if (c.TypeArgs.Count != 0) {
- // instantiate every parameter, it doesn't particularly matter how
- wr.Write("<");
- string sep = "";
- for (int i = 0; i < c.TypeArgs.Count; i++) {
- wr.Write("{0}int", sep);
- sep = ", ";
- }
- wr.Write(">");
+ }
+ else
+ {
+ if (m.Body == null)
+ {
+ if (!Attributes.Contains(m.Attributes, "axiom"))
+ {
+ Error("Method {0} has no body", m.FullName);
+ }
+ }
+ else if (m.IsGhost)
+ {
+ var v = new CheckHasNoAssumes_Visitor(this);
+ v.Visit(m.Body);
+ }
+ else
+ {
+ Indent(indent);
+ wr.Write("public {0}void @{1}", m.IsStatic ? "static " : "", m.CompileName);
+ if (m.TypeArgs.Count != 0)
+ {
+ wr.Write("<{0}>", TypeParameters(m.TypeArgs));
+ }
+ wr.Write("(");
+ int nIns = WriteFormals("", m.Ins);
+ WriteFormals(nIns == 0 ? "" : ", ", m.Outs);
+ wr.WriteLine(")");
+ Indent(indent); wr.WriteLine("{");
+ foreach (Formal p in m.Outs)
+ {
+ if (!p.IsGhost)
+ {
+ Indent(indent + IndentAmount);
+ wr.WriteLine("@{0} = {1};", p.CompileName, DefaultValue(p.Type));
+ }
+ }
+ if (m.Body == null)
+ {
+ Error("Method {0} has no body", m.FullName);
+ }
+ else
+ {
+ if (m.IsTailRecursive)
+ {
+ Indent(indent); wr.WriteLine("TAIL_CALL_START: ;");
+ if (!m.IsStatic)
+ {
+ Indent(indent + IndentAmount); wr.WriteLine("var _this = this;");
+ }
+ }
+ Contract.Assert(enclosingMethod == null);
+ enclosingMethod = m;
+ TrStmtList(m.Body.Body, indent);
+ Contract.Assert(enclosingMethod == m);
+ enclosingMethod = null;
+ }
+ Indent(indent); wr.WriteLine("}");
+
+ // allow the Main method to be an instance method
+ if (!m.IsStatic && m.Name == "Main" && m.TypeArgs.Count == 0 && m.Ins.Count == 0 && m.Outs.Count == 0 && m.Req.Count == 0)
+ {
+ Indent(indent);
+ wr.WriteLine("public static void Main(string[] args) {");
+ Contract.Assert(m.EnclosingClass == c);
+ Indent(indent + IndentAmount);
+ wr.Write("@{0} b = new @{0}", c.CompileName);
+ if (c.TypeArgs.Count != 0)
+ {
+ // instantiate every parameter, it doesn't particularly matter how
+ wr.Write("<");
+ string sep = "";
+ for (int i = 0; i < c.TypeArgs.Count; i++)
+ {
+ wr.Write("{0}int", sep);
+ sep = ", ";
+ }
+ wr.Write(">");
+ }
+ wr.WriteLine("();");
+ Indent(indent + IndentAmount); wr.WriteLine("b.@Main();");
+ Indent(indent); wr.WriteLine("}");
+ }
}
- wr.WriteLine("();");
- Indent(indent + IndentAmount); wr.WriteLine("b.@Main();");
- Indent(indent); wr.WriteLine("}");
- }
}
-
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member
}
@@ -1771,7 +1900,14 @@ namespace Microsoft.Dafny {
wr.Write("@" + receiverReplacement);
} else if (s.Method.IsStatic) {
Indent(indent);
- wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));
+ if (s.Receiver.Type is UserDefinedType && ((UserDefinedType)s.Receiver.Type).ResolvedClass is TraitDecl)
+ {
+ wr.Write("@_Companion_{0}", TypeName(cce.NonNull(s.Receiver.Type)).Replace("@", string.Empty));
+ }
+ else
+ {
+ wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));
+ }
} else {
SpillLetVariableDecls(s.Receiver, indent);
Indent(indent);
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index c870dc81..753b156f 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -195,6 +195,7 @@ Dafny
// to support multiple files, create a default module only if theModule is null
DefaultModuleDecl defaultModule = (DefaultModuleDecl)((LiteralModuleDecl)theModule).ModuleDef;
// theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl)
+ TraitDecl/*!*/ trait;
Contract.Assert(defaultModule != null);
.)
{ "include" string (. {
@@ -215,7 +216,7 @@ Dafny
| DatatypeDecl<defaultModule, out dt> (. defaultModule.TopLevelDecls.Add(dt); .)
| OtherTypeDecl<defaultModule, out td> (. defaultModule.TopLevelDecls.Add(td); .)
| IteratorDecl<defaultModule, out iter> (. defaultModule.TopLevelDecls.Add(iter); .)
-
+ | TraitDecl<defaultModule, out trait> (. defaultModule.TopLevelDecls.Add(trait); .)
| ClassMemberDecl<membersDefaultClass, false>
}
(. // find the default class in the default module, then append membersDefaultClass to its member list
@@ -236,7 +237,8 @@ Dafny
SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter;
Attributes attrs = null; IToken/*!*/ id;
- List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;
+ TraitDecl/*!*/ trait;
+ List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;
List<IToken> idRefined = null, idPath = null, idAssignment = null;
ModuleDefinition module;
ModuleDecl sm;
@@ -253,7 +255,8 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
"{" (. module.BodyStartTok = t; .)
{ SubModuleDecl<module, out sm> (. module.TopLevelDecls.Add(sm); .)
| ClassDecl<module, out c> (. module.TopLevelDecls.Add(c); .)
- | DatatypeDecl<module, out dt> (. module.TopLevelDecls.Add(dt); .)
+ | TraitDecl<module, out trait> (. module.TopLevelDecls.Add(trait); .)
+ | DatatypeDecl<module, out dt> (. module.TopLevelDecls.Add(dt); .)
| OtherTypeDecl<module, out td> (. module.TopLevelDecls.Add(td); .)
| IteratorDecl<module, out iter> (. module.TopLevelDecls.Add(iter); .)
| ClassMemberDecl<namedModuleDefaultClassMembers, false>
@@ -298,7 +301,8 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ id;
- Attributes attrs = null;
+ List<IToken>/*!*/ traitId=null;
+ Attributes attrs = null;
List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
@@ -308,15 +312,41 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
{ Attribute<ref attrs> }
NoUSIdent<out id>
[ GenericParameters<typeArgs> ]
+ ["extends" QualifiedName<out traitId>]
"{" (. bodyStart = t; .)
{ ClassMemberDecl<members, true>
}
"}"
- (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
+ (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traitId);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
.)
.
+
+ TraitDecl<ModuleDefinition/*!*/ module, out TraitDecl/*!*/ trait>
+ = (. Contract.Requires(module != null);
+ Contract.Ensures(Contract.ValueAtReturn(out trait) != null);
+ IToken/*!*/ id;
+ Attributes attrs = null;
+ List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>(); //traits should not support type parameters at the moment
+ List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
+ IToken bodyStart;
+ .)
+ SYNC
+ "trait"
+ { Attribute<ref attrs> }
+ NoUSIdent<out id>
+ [ GenericParameters<typeArgs> ]
+ "{" (. bodyStart = t; .)
+ { ClassMemberDecl<members, true>
+ }
+ "}"
+ (. trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs);
+ trait.BodyStartTok = bodyStart;
+ trait.BodyEndTok = t;
+ .)
+ .
+
ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>
= (. Contract.Requires(cce.NonNullElements(mm));
Method/*!*/ m;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 21227dd6..e757257c 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -92,7 +92,7 @@ namespace Microsoft.Dafny {
public readonly ClassDecl ObjectDecl;
public BuiltIns() {
// create class 'object'
- ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), DontCompile());
+ ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), DontCompile(), null);
SystemModule.TopLevelDecls.Add(ObjectDecl);
// add one-dimensional arrays, since they may arise during type checking
// Arrays of other dimensions may be added during parsing as the parser detects the need for these
@@ -1433,8 +1433,18 @@ namespace Microsoft.Dafny {
}
}
+ public class TraitDecl : ClassDecl
+ {
+ public bool IsParent { set; get; }
+ public TraitDecl(IToken tok, string name, ModuleDefinition module,
+ List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes)
+ : base(tok, name, module, typeArgs, members, attributes, null) { }
+ }
+
public class ClassDecl : TopLevelDecl {
public readonly List<MemberDecl> Members;
+ public TraitDecl Trait;
+ public readonly IToken TraitId;
public bool HasConstructor; // filled in (early) during resolution; true iff there exists a member that is a Constructor
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -1442,7 +1452,7 @@ namespace Microsoft.Dafny {
}
public ClassDecl(IToken tok, string name, ModuleDefinition module,
- List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes)
+ List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes, List<IToken> traitId)
: base(tok, name, module, typeArgs, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
@@ -1450,6 +1460,8 @@ namespace Microsoft.Dafny {
Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(members));
Members = members;
+ if (traitId != null && traitId.Count > 0)
+ TraitId = traitId[0]; //there are at most one inheriting trait at the moment
}
public virtual bool IsDefaultClass {
get {
@@ -1460,7 +1472,7 @@ namespace Microsoft.Dafny {
public class DefaultClassDecl : ClassDecl {
public DefaultClassDecl(ModuleDefinition module, [Captured] List<MemberDecl> members)
- : base(Token.NoToken, "_default", module, new List<TypeParameter>(), members, null) {
+ : base(Token.NoToken, "_default", module, new List<TypeParameter>(), members, null,null) {
Contract.Requires(module != null);
Contract.Requires(cce.NonNullElements(members));
}
@@ -1476,7 +1488,7 @@ namespace Microsoft.Dafny {
public ArrayClassDecl(int dims, ModuleDefinition module, Attributes attrs)
: base(Token.NoToken, BuiltIns.ArrayClassName(dims), module,
new List<TypeParameter>(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}),
- new List<MemberDecl>(), attrs)
+ new List<MemberDecl>(), attrs,null)
{
Contract.Requires(1 <= dims);
Contract.Requires(module != null);
@@ -1731,7 +1743,7 @@ namespace Microsoft.Dafny {
List<MaybeFreeExpression> yieldRequires,
List<MaybeFreeExpression> yieldEnsures,
BlockStmt body, Attributes attributes, IToken signatureEllipsis)
- : base(tok, name, module, typeArgs, new List<MemberDecl>(), attributes)
+ : base(tok, name, module, typeArgs, new List<MemberDecl>(), attributes,null)
{
Contract.Requires(tok != null);
Contract.Requires(name != null);
@@ -1805,7 +1817,7 @@ namespace Microsoft.Dafny {
public readonly bool IsGhost;
public TopLevelDecl EnclosingClass; // filled in during resolution
public MemberDecl RefinementBase; // filled in during the pre-resolution refinement transformation; null if the member is new here
-
+ public bool Inherited;
public MemberDecl(IToken tok, string name, bool isStatic, bool isGhost, Attributes attributes)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
@@ -2267,6 +2279,7 @@ namespace Microsoft.Dafny {
public bool SignatureIsOmitted { get { return SignatureEllipsis != null; } } // is "false" for all Function objects that survive into resolution
public readonly IToken SignatureEllipsis;
public bool IsBuiltin;
+ public Function OverriddenFunction;
/// <summary>
/// The "AllCalls" field is used for non-CoPredicate, non-PrefixPredicate functions only (so its value should not be relied upon for CoPredicate and PrefixPredicate functions).
@@ -2436,6 +2449,7 @@ namespace Microsoft.Dafny {
public bool IsRecursive; // filled in during resolution
public bool IsTailRecursive; // filled in during resolution
public readonly ISet<IVariable> AssignedAssumptionVariables = new HashSet<IVariable>();
+ public Method OverriddenMethod;
[ContractInvariantMethod]
void ObjectInvariant() {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 63c555aa..d6e06321 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -28,7 +28,7 @@ public class Parser {
public const int _closeparen = 12;
public const int _star = 13;
public const int _notIn = 14;
- public const int maxT = 126;
+ public const int maxT = 128;
const bool T = true;
const bool x = false;
@@ -243,6 +243,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
// to support multiple files, create a default module only if theModule is null
DefaultModuleDecl defaultModule = (DefaultModuleDecl)((LiteralModuleDecl)theModule).ModuleDef;
// theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl)
+ TraitDecl/*!*/ trait;
Contract.Assert(defaultModule != null);
while (la.kind == 15) {
@@ -273,22 +274,27 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
defaultModule.TopLevelDecls.Add(c);
break;
}
- case 27: case 28: {
+ case 29: case 30: {
DatatypeDecl(defaultModule, out dt);
defaultModule.TopLevelDecls.Add(dt);
break;
}
- case 32: {
+ case 34: {
OtherTypeDecl(defaultModule, out td);
defaultModule.TopLevelDecls.Add(td);
break;
}
- case 34: {
+ case 36: {
IteratorDecl(defaultModule, out iter);
defaultModule.TopLevelDecls.Add(iter);
break;
}
- case 25: case 26: case 30: case 40: case 41: case 42: case 43: case 44: case 62: case 63: case 64: {
+ case 26: {
+ TraitDecl(defaultModule, out trait);
+ defaultModule.TopLevelDecls.Add(trait);
+ break;
+ }
+ case 27: case 28: case 32: case 42: case 43: case 44: case 45: case 46: case 64: case 65: case 66: {
ClassMemberDecl(membersDefaultClass, false);
break;
}
@@ -312,6 +318,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
void SubModuleDecl(ModuleDefinition parent, out ModuleDecl submodule) {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter;
Attributes attrs = null; IToken/*!*/ id;
+ TraitDecl/*!*/ trait;
List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;
List<IToken> idRefined = null, idPath = null, idAssignment = null;
ModuleDefinition module;
@@ -349,22 +356,27 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
module.TopLevelDecls.Add(c);
break;
}
- case 27: case 28: {
+ case 26: {
+ TraitDecl(module, out trait);
+ module.TopLevelDecls.Add(trait);
+ break;
+ }
+ case 29: case 30: {
DatatypeDecl(module, out dt);
module.TopLevelDecls.Add(dt);
break;
}
- case 32: {
+ case 34: {
OtherTypeDecl(module, out td);
module.TopLevelDecls.Add(td);
break;
}
- case 34: {
+ case 36: {
IteratorDecl(module, out iter);
module.TopLevelDecls.Add(iter);
break;
}
- case 25: case 26: case 30: case 40: case 41: case 42: case 43: case 44: case 62: case 63: case 64: {
+ case 27: case 28: case 32: case 42: case 43: case 44: case 45: case 46: case 64: case 65: case 66: {
ClassMemberDecl(namedModuleDefaultClassMembers, false);
break;
}
@@ -397,7 +409,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
}
if (la.kind == 8) {
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(127); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(129); Get();}
Get();
}
if (submodule == null) {
@@ -406,34 +418,39 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
submodule = new AliasModuleDecl(idPath, id, parent, opened);
}
- } else SynErr(128);
+ } else SynErr(130);
}
void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {
Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ id;
+ List<IToken>/*!*/ traitId=null;
Attributes attrs = null;
List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 24)) {SynErr(129); Get();}
+ while (!(la.kind == 0 || la.kind == 24)) {SynErr(131); Get();}
Expect(24);
while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 38) {
+ if (la.kind == 40) {
GenericParameters(typeArgs);
}
+ if (la.kind == 25) {
+ Get();
+ QualifiedName(out traitId);
+ }
Expect(9);
bodyStart = t;
while (StartOf(2)) {
ClassMemberDecl(members, true);
}
Expect(10);
- c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
+ c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traitId);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
@@ -449,29 +466,29 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
IToken bodyStart = Token.NoToken; // dummy assignment
bool co = false;
- while (!(la.kind == 0 || la.kind == 27 || la.kind == 28)) {SynErr(130); Get();}
- if (la.kind == 27) {
+ while (!(la.kind == 0 || la.kind == 29 || la.kind == 30)) {SynErr(132); Get();}
+ if (la.kind == 29) {
Get();
- } else if (la.kind == 28) {
+ } else if (la.kind == 30) {
Get();
co = true;
- } else SynErr(131);
+ } else SynErr(133);
while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 38) {
+ if (la.kind == 40) {
GenericParameters(typeArgs);
}
Expect(21);
bodyStart = t;
DatatypeMemberDecl(ctors);
- while (la.kind == 29) {
+ while (la.kind == 31) {
Get();
DatatypeMemberDecl(ctors);
}
if (la.kind == 8) {
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(132); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(134); Get();}
Get();
}
if (co) {
@@ -492,21 +509,21 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
td = null;
Type ty;
- Expect(32);
+ Expect(34);
while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (la.kind == 11) {
Get();
- Expect(33);
+ Expect(35);
Expect(12);
eqSupport = TypeParameter.EqualitySupportValue.Required;
- if (la.kind == 38) {
+ if (la.kind == 40) {
GenericParameters(typeArgs);
}
} else if (StartOf(3)) {
- if (la.kind == 38) {
+ if (la.kind == 40) {
GenericParameters(typeArgs);
}
if (la.kind == 21) {
@@ -514,13 +531,13 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Type(out ty);
td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs);
}
- } else SynErr(133);
+ } else SynErr(135);
if (td == null) {
td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);
}
if (la.kind == 8) {
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(134); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(136); Get();}
Get();
}
}
@@ -549,19 +566,19 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 34)) {SynErr(135); Get();}
- Expect(34);
+ while (!(la.kind == 0 || la.kind == 36)) {SynErr(137); Get();}
+ Expect(36);
while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 11 || la.kind == 38) {
- if (la.kind == 38) {
+ if (la.kind == 11 || la.kind == 40) {
+ if (la.kind == 40) {
GenericParameters(typeArgs);
}
Formals(true, true, ins, out openParen);
- if (la.kind == 35 || la.kind == 36) {
- if (la.kind == 35) {
+ if (la.kind == 37 || la.kind == 38) {
+ if (la.kind == 37) {
Get();
} else {
Get();
@@ -569,10 +586,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
Formals(false, true, outs, out openParen);
}
- } else if (la.kind == 37) {
+ } else if (la.kind == 39) {
Get();
signatureEllipsis = t; openParen = Token.NoToken;
- } else SynErr(136);
+ } else SynErr(138);
while (StartOf(4)) {
IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs);
}
@@ -590,14 +607,44 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
+ void TraitDecl(ModuleDefinition/*!*/ module, out TraitDecl/*!*/ trait) {
+ Contract.Requires(module != null);
+ Contract.Ensures(Contract.ValueAtReturn(out trait) != null);
+ IToken/*!*/ id;
+ Attributes attrs = null;
+ List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>(); //traits should not support type parameters at the moment
+ List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
+ IToken bodyStart;
+
+ while (!(la.kind == 0 || la.kind == 26)) {SynErr(139); Get();}
+ Expect(26);
+ while (la.kind == 9) {
+ Attribute(ref attrs);
+ }
+ NoUSIdent(out id);
+ if (la.kind == 40) {
+ GenericParameters(typeArgs);
+ }
+ Expect(9);
+ bodyStart = t;
+ while (StartOf(2)) {
+ ClassMemberDecl(members, true);
+ }
+ Expect(10);
+ trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs);
+ trait.BodyStartTok = bodyStart;
+ trait.BodyEndTok = t;
+
+ }
+
void ClassMemberDecl(List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors) {
Contract.Requires(cce.NonNullElements(mm));
Method/*!*/ m;
Function/*!*/ f;
MemberModifiers mmod = new MemberModifiers();
- while (la.kind == 25 || la.kind == 26) {
- if (la.kind == 25) {
+ while (la.kind == 27 || la.kind == 28) {
+ if (la.kind == 27) {
Get();
mmod.IsGhost = true;
} else {
@@ -605,15 +652,15 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
mmod.IsStatic = true;
}
}
- if (la.kind == 30) {
+ if (la.kind == 32) {
FieldDecl(mmod, mm);
- } else if (la.kind == 62 || la.kind == 63 || la.kind == 64) {
+ } else if (la.kind == 64 || la.kind == 65 || la.kind == 66) {
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (StartOf(5)) {
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
- } else SynErr(137);
+ } else SynErr(140);
}
void Attribute(ref Attributes attrs) {
@@ -636,7 +683,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
IToken id; IToken idPrime; ids = new List<IToken>();
Ident(out id);
ids.Add(id);
- while (la.kind == 61) {
+ while (la.kind == 63) {
IdentOrDigitsSuffix(out id, out idPrime);
ids.Add(id);
if (idPrime != null) { ids.Add(idPrime); }
@@ -655,7 +702,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
x = Token.NoToken;
y = null;
- Expect(61);
+ Expect(63);
if (la.kind == 1) {
Get();
x = t;
@@ -683,7 +730,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
}
- } else SynErr(138);
+ } else SynErr(141);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -691,29 +738,29 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
IToken/*!*/ id;
TypeParameter.EqualitySupportValue eqSupport;
- Expect(38);
+ Expect(40);
NoUSIdent(out id);
eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
if (la.kind == 11) {
Get();
- Expect(33);
+ Expect(35);
Expect(12);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
NoUSIdent(out id);
eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
if (la.kind == 11) {
Get();
- Expect(33);
+ Expect(35);
Expect(12);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
}
- Expect(39);
+ Expect(41);
}
void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {
@@ -721,8 +768,8 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
- while (!(la.kind == 0 || la.kind == 30)) {SynErr(139); Get();}
- Expect(30);
+ while (!(la.kind == 0 || la.kind == 32)) {SynErr(142); Get();}
+ Expect(32);
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
while (la.kind == 9) {
@@ -730,12 +777,12 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
FIdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
FIdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(140); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(143); Get();}
Expect(8);
}
@@ -758,9 +805,9 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
IToken bodyEnd = Token.NoToken;
IToken signatureEllipsis = null;
- if (la.kind == 62) {
+ if (la.kind == 64) {
Get();
- if (la.kind == 40) {
+ if (la.kind == 42) {
Get();
isFunctionMethod = true;
}
@@ -770,22 +817,22 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 11 || la.kind == 38) {
- if (la.kind == 38) {
+ if (la.kind == 11 || la.kind == 40) {
+ if (la.kind == 40) {
GenericParameters(typeArgs);
}
Formals(true, isFunctionMethod, formals, out openParen);
Expect(7);
Type(out returnType);
- } else if (la.kind == 37) {
+ } else if (la.kind == 39) {
Get();
signatureEllipsis = t;
openParen = Token.NoToken;
- } else SynErr(141);
- } else if (la.kind == 63) {
+ } else SynErr(144);
+ } else if (la.kind == 65) {
Get();
isPredicate = true;
- if (la.kind == 40) {
+ if (la.kind == 42) {
Get();
isFunctionMethod = true;
}
@@ -796,7 +843,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
NoUSIdent(out id);
if (StartOf(6)) {
- if (la.kind == 38) {
+ if (la.kind == 40) {
GenericParameters(typeArgs);
}
if (la.kind == 11) {
@@ -806,12 +853,12 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
SemErr(t, "predicates do not have an explicitly declared return type; it is always bool");
}
}
- } else if (la.kind == 37) {
+ } else if (la.kind == 39) {
Get();
signatureEllipsis = t;
openParen = Token.NoToken;
- } else SynErr(142);
- } else if (la.kind == 64) {
+ } else SynErr(145);
+ } else if (la.kind == 66) {
Get();
isCoPredicate = true;
if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
@@ -821,7 +868,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
NoUSIdent(out id);
if (StartOf(6)) {
- if (la.kind == 38) {
+ if (la.kind == 40) {
GenericParameters(typeArgs);
}
if (la.kind == 11) {
@@ -831,12 +878,12 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool");
}
}
- } else if (la.kind == 37) {
+ } else if (la.kind == 39) {
Get();
signatureEllipsis = t;
openParen = Token.NoToken;
- } else SynErr(143);
- } else SynErr(144);
+ } else SynErr(146);
+ } else SynErr(147);
decreases = isCoPredicate ? null : new List<Expression/*!*/>();
while (StartOf(7)) {
FunctionSpec(reqs, reads, ens, decreases);
@@ -887,21 +934,21 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(StartOf(8))) {SynErr(145); Get();}
- if (la.kind == 40) {
+ while (!(StartOf(8))) {SynErr(148); Get();}
+ if (la.kind == 42) {
Get();
- } else if (la.kind == 41) {
+ } else if (la.kind == 43) {
Get();
isLemma = true;
- } else if (la.kind == 42) {
+ } else if (la.kind == 44) {
Get();
isCoLemma = true;
- } else if (la.kind == 43) {
+ } else if (la.kind == 45) {
Get();
isCoLemma = true;
errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'");
- } else if (la.kind == 44) {
+ } else if (la.kind == 46) {
Get();
if (allowConstructor) {
isConstructor = true;
@@ -909,7 +956,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
SemErr(t, "constructors are only allowed in classes");
}
- } else SynErr(146);
+ } else SynErr(149);
keywordToken = t;
if (isLemma) {
if (mmod.IsGhost) {
@@ -942,20 +989,20 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
}
- if (la.kind == 11 || la.kind == 38) {
- if (la.kind == 38) {
+ if (la.kind == 11 || la.kind == 40) {
+ if (la.kind == 40) {
GenericParameters(typeArgs);
}
Formals(true, !mmod.IsGhost, ins, out openParen);
- if (la.kind == 36) {
+ if (la.kind == 38) {
Get();
if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); }
Formals(false, !mmod.IsGhost, outs, out openParen);
}
- } else if (la.kind == 37) {
+ } else if (la.kind == 39) {
Get();
signatureEllipsis = t; openParen = Token.NoToken;
- } else SynErr(147);
+ } else SynErr(150);
while (StartOf(9)) {
MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
}
@@ -1011,7 +1058,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
if (StartOf(10)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
@@ -1029,7 +1076,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
} else if (la.kind == 2) {
Get();
id = t;
- } else SynErr(148);
+ } else SynErr(151);
Expect(7);
Type(out ty);
}
@@ -1043,7 +1090,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
isGhost = false;
- if (la.kind == 25) {
+ if (la.kind == 27) {
Get();
if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); }
}
@@ -1101,7 +1148,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);
string name = null; id = Token.NoToken; ty = new BoolType()/*dummy*/; isGhost = false;
- if (la.kind == 25) {
+ if (la.kind == 27) {
Get();
isGhost = true;
}
@@ -1123,7 +1170,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
id = t; name = id.val;
Expect(7);
Type(out ty);
- } else SynErr(149);
+ } else SynErr(152);
if (name != null) {
identName = name;
} else {
@@ -1138,30 +1185,30 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
List<Type> gt;
switch (la.kind) {
- case 52: {
+ case 54: {
Get();
tok = t;
break;
}
- case 53: {
+ case 55: {
Get();
tok = t; ty = new NatType();
break;
}
- case 54: {
+ case 56: {
Get();
tok = t; ty = new IntType();
break;
}
- case 55: {
+ case 57: {
Get();
tok = t; ty = new RealType();
break;
}
- case 56: {
+ case 58: {
Get();
tok = t; gt = new List<Type/*!*/>();
- if (la.kind == 38) {
+ if (la.kind == 40) {
GenericInstantiation(gt);
}
if (gt.Count > 1) {
@@ -1171,10 +1218,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
break;
}
- case 57: {
+ case 59: {
Get();
tok = t; gt = new List<Type/*!*/>();
- if (la.kind == 38) {
+ if (la.kind == 40) {
GenericInstantiation(gt);
}
if (gt.Count > 1) {
@@ -1184,10 +1231,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
break;
}
- case 58: {
+ case 60: {
Get();
tok = t; gt = new List<Type/*!*/>();
- if (la.kind == 38) {
+ if (la.kind == 40) {
GenericInstantiation(gt);
}
if (gt.Count > 1) {
@@ -1197,10 +1244,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
break;
}
- case 59: {
+ case 61: {
Get();
tok = t; gt = new List<Type/*!*/>();
- if (la.kind == 38) {
+ if (la.kind == 40) {
GenericInstantiation(gt);
}
if (gt.Count == 0) {
@@ -1220,7 +1267,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
if (StartOf(11)) {
Type(out ty);
gt.Add(ty);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
Type(out ty);
gt.Add(ty);
@@ -1238,11 +1285,11 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
break;
}
- case 1: case 5: case 60: {
+ case 1: case 5: case 62: {
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(150); break;
+ default: SynErr(153); break;
}
}
@@ -1250,10 +1297,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost;
Expect(11);
openParen = t;
- if (la.kind == 1 || la.kind == 25) {
+ if (la.kind == 1 || la.kind == 27) {
GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
@@ -1268,8 +1315,8 @@ List<MaybeFreeExpression/*!*/>/*!*/ yieldReq, List<MaybeFreeExpression/*!*/>/*!*
ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null;
- while (!(StartOf(12))) {SynErr(151); Get();}
- if (la.kind == 50) {
+ while (!(StartOf(12))) {SynErr(154); Get();}
+ if (la.kind == 52) {
Get();
while (IsAttribute()) {
Attribute(ref readsAttrs);
@@ -1277,15 +1324,15 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
if (StartOf(13)) {
FrameExpression(out fe);
reads.Add(fe);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
FrameExpression(out fe);
reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(152); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(155); Get();}
Expect(8);
- } else if (la.kind == 45) {
+ } else if (la.kind == 47) {
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -1293,27 +1340,27 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
if (StartOf(13)) {
FrameExpression(out fe);
mod.Add(fe);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
FrameExpression(out fe);
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(153); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(156); Get();}
Expect(8);
} else if (StartOf(14)) {
- if (la.kind == 46) {
+ if (la.kind == 48) {
Get();
isFree = true;
}
- if (la.kind == 51) {
+ if (la.kind == 53) {
Get();
isYield = true;
}
- if (la.kind == 47) {
+ if (la.kind == 49) {
Get();
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(154); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(157); Get();}
Expect(8);
if (isYield) {
yieldReq.Add(new MaybeFreeExpression(e, isFree));
@@ -1321,13 +1368,13 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
req.Add(new MaybeFreeExpression(e, isFree));
}
- } else if (la.kind == 48) {
+ } else if (la.kind == 50) {
Get();
while (IsAttribute()) {
Attribute(ref ensAttrs);
}
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(155); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(158); Get();}
Expect(8);
if (isYield) {
yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
@@ -1335,16 +1382,16 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
}
- } else SynErr(156);
- } else if (la.kind == 49) {
+ } else SynErr(159);
+ } else if (la.kind == 51) {
Get();
while (IsAttribute()) {
Attribute(ref decrAttrs);
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(157); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(160); Get();}
Expect(8);
- } else SynErr(158);
+ } else SynErr(161);
}
void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -1366,8 +1413,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null;
- while (!(StartOf(16))) {SynErr(159); Get();}
- if (la.kind == 45) {
+ while (!(StartOf(16))) {SynErr(162); Get();}
+ if (la.kind == 47) {
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -1375,44 +1422,44 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (StartOf(13)) {
FrameExpression(out fe);
mod.Add(fe);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
FrameExpression(out fe);
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(160); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(163); Get();}
Expect(8);
- } else if (la.kind == 46 || la.kind == 47 || la.kind == 48) {
- if (la.kind == 46) {
+ } else if (la.kind == 48 || la.kind == 49 || la.kind == 50) {
+ if (la.kind == 48) {
Get();
isFree = true;
}
- if (la.kind == 47) {
+ if (la.kind == 49) {
Get();
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(161); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(164); Get();}
Expect(8);
req.Add(new MaybeFreeExpression(e, isFree));
- } else if (la.kind == 48) {
+ } else if (la.kind == 50) {
Get();
while (IsAttribute()) {
Attribute(ref ensAttrs);
}
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(162); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(165); Get();}
Expect(8);
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
- } else SynErr(163);
- } else if (la.kind == 49) {
+ } else SynErr(166);
+ } else if (la.kind == 51) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(164); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(167); Get();}
Expect(8);
- } else SynErr(165);
+ } else SynErr(168);
}
void FrameExpression(out FrameExpression/*!*/ fe) {
@@ -1425,18 +1472,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (StartOf(17)) {
Expression(out e, false);
feTok = e.tok;
- if (la.kind == 65) {
+ if (la.kind == 67) {
Get();
Ident(out id);
fieldName = id.val; feTok = id;
}
fe = new FrameExpression(feTok, e, fieldName);
- } else if (la.kind == 65) {
+ } else if (la.kind == 67) {
Get();
Ident(out id);
fieldName = id.val;
fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName);
- } else SynErr(166);
+ } else SynErr(169);
}
void Expression(out Expression e, bool allowSemi) {
@@ -1462,7 +1509,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
decreases.Add(e);
}
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
PossiblyWildExpression(out e);
if (!allowWildcard && e is WildcardExpr) {
@@ -1476,15 +1523,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {
Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty;
- Expect(38);
+ Expect(40);
Type(out ty);
gt.Add(ty);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
Type(out ty);
gt.Add(ty);
}
- Expect(39);
+ Expect(41);
}
void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {
@@ -1493,13 +1540,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Type> gt;
List<IToken> path;
- if (la.kind == 60) {
+ if (la.kind == 62) {
Get();
tok = t; ty = new ObjectType();
} else if (la.kind == 5) {
Get();
tok = t; gt = new List<Type>();
- if (la.kind == 38) {
+ if (la.kind == 40) {
GenericInstantiation(gt);
}
int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));
@@ -1509,16 +1556,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Ident(out tok);
gt = new List<Type>();
path = new List<IToken>();
- while (la.kind == 61) {
+ while (la.kind == 63) {
path.Add(tok);
Get();
Ident(out tok);
}
- if (la.kind == 38) {
+ if (la.kind == 40) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt, path);
- } else SynErr(167);
+ } else SynErr(170);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {
@@ -1526,33 +1573,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Requires(cce.NonNullElements(reads));
Contract.Requires(decreases == null || cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
- if (la.kind == 47) {
- while (!(la.kind == 0 || la.kind == 47)) {SynErr(168); Get();}
+ if (la.kind == 49) {
+ while (!(la.kind == 0 || la.kind == 49)) {SynErr(171); Get();}
Get();
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(169); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(172); Get();}
Expect(8);
reqs.Add(e);
- } else if (la.kind == 50) {
+ } else if (la.kind == 52) {
Get();
if (StartOf(18)) {
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(170); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(173); Get();}
Expect(8);
- } else if (la.kind == 48) {
+ } else if (la.kind == 50) {
Get();
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(171); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(174); Get();}
Expect(8);
ens.Add(e);
- } else if (la.kind == 49) {
+ } else if (la.kind == 51) {
Get();
if (decreases == null) {
SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");
@@ -1560,9 +1607,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(172); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(175); Get();}
Expect(8);
- } else SynErr(173);
+ } else SynErr(176);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -1581,7 +1628,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
fe = new FrameExpression(t, new WildcardExpr(t), null);
} else if (StartOf(13)) {
FrameExpression(out fe);
- } else SynErr(174);
+ } else SynErr(177);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -1592,7 +1639,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new WildcardExpr(t);
} else if (StartOf(17)) {
Expression(out e, false);
- } else SynErr(175);
+ } else SynErr(178);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1609,58 +1656,58 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken bodyStart, bodyEnd;
int breakCount;
- while (!(StartOf(19))) {SynErr(176); Get();}
+ while (!(StartOf(19))) {SynErr(179); Get();}
switch (la.kind) {
case 9: {
BlockStmt(out bs, out bodyStart, out bodyEnd);
s = bs;
break;
}
- case 83: {
+ case 85: {
AssertStmt(out s);
break;
}
- case 72: {
+ case 74: {
AssumeStmt(out s);
break;
}
- case 84: {
+ case 86: {
PrintStmt(out s);
break;
}
- case 1: case 2: case 3: case 4: case 11: case 29: case 54: case 55: case 113: case 114: case 115: case 116: case 117: case 118: {
+ case 1: case 2: case 3: case 4: case 11: case 31: case 56: case 57: case 115: case 116: case 117: case 118: case 119: case 120: {
UpdateStmt(out s);
break;
}
- case 25: case 30: {
+ case 27: case 32: {
VarDeclStatement(out s);
break;
}
- case 76: {
+ case 78: {
IfStmt(out s);
break;
}
- case 80: {
+ case 82: {
WhileStmt(out s);
break;
}
- case 82: {
+ case 84: {
MatchStmt(out s);
break;
}
- case 85: case 86: {
+ case 87: case 88: {
ForallStmt(out s);
break;
}
- case 88: {
+ case 90: {
CalcStmt(out s);
break;
}
- case 87: {
+ case 89: {
ModifyStmt(out s);
break;
}
- case 66: {
+ case 68: {
Get();
x = t;
NoUSIdent(out id);
@@ -1669,32 +1716,32 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
s.Labels = new LList<Label>(new Label(x, id.val), s.Labels);
break;
}
- case 67: {
+ case 69: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
NoUSIdent(out id);
label = id.val;
- } else if (la.kind == 8 || la.kind == 67) {
- while (la.kind == 67) {
+ } else if (la.kind == 8 || la.kind == 69) {
+ while (la.kind == 69) {
Get();
breakCount++;
}
- } else SynErr(177);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(178); Get();}
+ } else SynErr(180);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(181); Get();}
Expect(8);
s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount);
break;
}
- case 51: case 70: {
+ case 53: case 72: {
ReturnStmt(out s);
break;
}
- case 37: {
+ case 39: {
SkeletonStmt(out s);
break;
}
- default: SynErr(179); break;
+ default: SynErr(182); break;
}
}
@@ -1703,17 +1750,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression e = dummyExpr; Attributes attrs = null;
IToken dotdotdot = null;
- Expect(83);
+ Expect(85);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
}
if (StartOf(17)) {
Expression(out e, false);
- } else if (la.kind == 37) {
+ } else if (la.kind == 39) {
Get();
dotdotdot = t;
- } else SynErr(180);
+ } else SynErr(183);
Expect(8);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssertStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
@@ -1728,17 +1775,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression e = dummyExpr; Attributes attrs = null;
IToken dotdotdot = null;
- Expect(72);
+ Expect(74);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
}
if (StartOf(17)) {
Expression(out e, false);
- } else if (la.kind == 37) {
+ } else if (la.kind == 39) {
Get();
dotdotdot = t;
- } else SynErr(181);
+ } else SynErr(184);
Expect(8);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssumeStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
@@ -1752,11 +1799,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
- Expect(84);
+ Expect(86);
x = t;
AttributeArg(out arg, false);
args.Add(arg);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
AttributeArg(out arg, false);
args.Add(arg);
@@ -1783,38 +1830,38 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(8);
endTok = t; rhss.Add(new ExprRhs(e, attrs));
- } else if (la.kind == 31 || la.kind == 69 || la.kind == 71) {
+ } else if (la.kind == 33 || la.kind == 71 || la.kind == 73) {
lhss.Add(e); lhs0 = e;
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
Lhs(out e);
lhss.Add(e);
}
- if (la.kind == 69) {
+ if (la.kind == 71) {
Get();
x = t;
Rhs(out r, lhs0);
rhss.Add(r);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
Rhs(out r, lhs0);
rhss.Add(r);
}
- } else if (la.kind == 71) {
+ } else if (la.kind == 73) {
Get();
x = t;
- if (la.kind == 72) {
+ if (la.kind == 74) {
Get();
suchThatAssume = t;
}
Expression(out suchThat, false);
- } else SynErr(182);
+ } else SynErr(185);
Expect(8);
endTok = t;
} else if (la.kind == 7) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(183);
+ } else SynErr(186);
if (suchThat != null) {
s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume);
} else {
@@ -1838,18 +1885,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Attributes attrs = null;
IToken endTok;
- if (la.kind == 25) {
+ if (la.kind == 27) {
Get();
isGhost = true; x = t;
}
- Expect(30);
+ Expect(32);
if (!isGhost) { x = t; }
while (la.kind == 9) {
Attribute(ref attrs);
}
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d); d.Attributes = attrs; attrs = null;
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
while (la.kind == 9) {
Attribute(ref attrs);
@@ -1857,15 +1904,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d); d.Attributes = attrs; attrs = null;
}
- if (la.kind == 69 || la.kind == 71) {
- if (la.kind == 69) {
+ if (la.kind == 71 || la.kind == 73) {
+ if (la.kind == 71) {
Get();
assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
Rhs(out r, lhs0);
rhss.Add(r);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
Rhs(out r, lhs0);
rhss.Add(r);
@@ -1873,7 +1920,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else {
Get();
assignTok = t;
- if (la.kind == 72) {
+ if (la.kind == 74) {
Get();
suchThatAssume = t;
}
@@ -1913,7 +1960,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(76);
+ Expect(78);
x = t;
if (IsAlternative()) {
AlternativeBlock(out alternatives, out endTok);
@@ -1927,15 +1974,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
BlockStmt(out thn, out bodyStart, out bodyEnd);
endTok = thn.EndTok;
- if (la.kind == 77) {
+ if (la.kind == 79) {
Get();
- if (la.kind == 76) {
+ if (la.kind == 78) {
IfStmt(out s);
els = s; endTok = s.EndTok;
} else if (la.kind == 9) {
BlockStmt(out bs, out bodyStart, out bodyEnd);
els = bs; endTok = bs.EndTok;
- } else SynErr(184);
+ } else SynErr(187);
}
if (guardEllipsis != null) {
ifStmt = new SkeletonStatement(new IfStmt(x, endTok, guard, thn, els), guardEllipsis, null);
@@ -1943,7 +1990,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ifStmt = new IfStmt(x, endTok, guard, thn, els);
}
- } else SynErr(185);
+ } else SynErr(188);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1959,7 +2006,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(80);
+ Expect(82);
x = t;
if (IsLoopSpecOrAlternative()) {
LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
@@ -1977,10 +2024,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 9) {
BlockStmt(out body, out bodyStart, out bodyEnd);
endTok = body.EndTok;
- } else if (la.kind == 37) {
+ } else if (la.kind == 39) {
Get();
bodyEllipsis = t; endTok = t;
- } else SynErr(186);
+ } else SynErr(189);
if (guardEllipsis != null || bodyEllipsis != null) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -1996,7 +2043,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
}
- } else SynErr(187);
+ } else SynErr(190);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -2005,14 +2052,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
bool usesOptionalBrace = false;
- Expect(82);
+ Expect(84);
x = t;
Expression(out e, true);
if (la.kind == 9) {
Get();
usesOptionalBrace = true;
}
- while (la.kind == 78) {
+ while (la.kind == 80) {
CaseStatement(out c);
cases.Add(c);
}
@@ -2020,7 +2067,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(10);
} else if (StartOf(22)) {
if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); }
- } else SynErr(188);
+ } else SynErr(191);
s = new MatchStmt(x, t, e, cases, usesOptionalBrace);
}
@@ -2038,15 +2085,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken bodyStart, bodyEnd;
IToken tok = Token.NoToken;
- if (la.kind == 85) {
+ if (la.kind == 87) {
Get();
x = t; tok = x;
- } else if (la.kind == 86) {
+ } else if (la.kind == 88) {
Get();
x = t;
errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");
- } else SynErr(189);
+ } else SynErr(192);
if (la.kind == 11) {
Get();
usesOptionalParen = true;
@@ -2064,14 +2111,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(12);
} else if (StartOf(23)) {
if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); }
- } else SynErr(190);
- while (la.kind == 46 || la.kind == 48) {
+ } else SynErr(193);
+ while (la.kind == 48 || la.kind == 50) {
isFree = false;
- if (la.kind == 46) {
+ if (la.kind == 48) {
Get();
isFree = true;
}
- Expect(48);
+ Expect(50);
Expression(out e, false);
ens.Add(new MaybeFreeExpression(e, isFree));
Expect(8);
@@ -2105,7 +2152,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken opTok;
IToken danglingOperator = null;
- Expect(88);
+ Expect(90);
x = t;
if (StartOf(24)) {
CalcOp(out opTok, out calcOp);
@@ -2158,7 +2205,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
BlockStmt body = null; IToken bodyStart;
IToken ellipsisToken = null;
- Expect(87);
+ Expect(89);
tok = t;
while (IsAttribute()) {
Attribute(ref attrs);
@@ -2167,7 +2214,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (StartOf(13)) {
FrameExpression(out fe);
mod.Add(fe);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
FrameExpression(out fe);
mod.Add(fe);
@@ -2180,10 +2227,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 9) {
BlockStmt(out body, out bodyStart, out endTok);
} else if (la.kind == 8) {
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(191); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(194); Get();}
Get();
endTok = t;
- } else SynErr(192);
+ } else SynErr(195);
s = new ModifyStmt(tok, endTok, mod, attrs, body);
if (ellipsisToken != null) {
s = new SkeletonStatement(s, ellipsisToken, null);
@@ -2197,17 +2244,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
AssignmentRhs r;
bool isYield = false;
- if (la.kind == 70) {
+ if (la.kind == 72) {
Get();
returnTok = t;
- } else if (la.kind == 51) {
+ } else if (la.kind == 53) {
Get();
returnTok = t; isYield = true;
- } else SynErr(193);
+ } else SynErr(196);
if (StartOf(26)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
Rhs(out r, null);
rhss.Add(r);
@@ -2227,22 +2274,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Expression> exprs = null;
IToken tok, dotdotdot, whereTok;
Expression e;
- Expect(37);
+ Expect(39);
dotdotdot = t;
- if (la.kind == 68) {
+ if (la.kind == 70) {
Get();
names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;
Ident(out tok);
names.Add(tok);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
Ident(out tok);
names.Add(tok);
}
- Expect(69);
+ Expect(71);
Expression(out e, false);
exprs.Add(e);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
Expression(out e, false);
exprs.Add(e);
@@ -2266,21 +2313,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
r = dummyRhs; // to please compiler
Attributes attrs = null;
- if (la.kind == 73) {
+ if (la.kind == 75) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 11 || la.kind == 61 || la.kind == 74) {
- if (la.kind == 74) {
+ if (la.kind == 11 || la.kind == 63 || la.kind == 76) {
+ if (la.kind == 76) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(75);
+ Expect(77);
var tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
} else {
x = null; args = new List<Expression/*!*/>();
- if (la.kind == 61) {
+ if (la.kind == 63) {
Get();
Ident(out x);
}
@@ -2305,7 +2352,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(17)) {
Expression(out e, false);
r = new ExprRhs(e);
- } else SynErr(194);
+ } else SynErr(197);
while (la.kind == 9) {
Attribute(ref attrs);
}
@@ -2317,23 +2364,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 61 || la.kind == 74) {
+ while (la.kind == 63 || la.kind == 76) {
Suffix(ref e);
}
} else if (StartOf(27)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 61 || la.kind == 74) {
+ while (la.kind == 63 || la.kind == 76) {
Suffix(ref e);
}
- } else SynErr(195);
+ } else SynErr(198);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e;
Expression(out e, true);
args.Add(e);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
Expression(out e, true);
args.Add(e);
@@ -2347,11 +2394,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Statement> body;
Expect(9);
- while (la.kind == 78) {
+ while (la.kind == 80) {
Get();
x = t;
Expression(out e, true);
- Expect(79);
+ Expect(81);
body = new List<Statement>();
while (StartOf(15)) {
Stmt(body);
@@ -2375,7 +2422,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(17)) {
Expression(out ee, true);
e = ee;
- } else SynErr(196);
+ } else SynErr(199);
}
void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs) {
@@ -2386,22 +2433,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod = null;
while (StartOf(28)) {
- if (la.kind == 46 || la.kind == 81) {
+ if (la.kind == 48 || la.kind == 83) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(197); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(200); Get();}
Expect(8);
invariants.Add(invariant);
- } else if (la.kind == 49) {
- while (!(la.kind == 0 || la.kind == 49)) {SynErr(198); Get();}
+ } else if (la.kind == 51) {
+ while (!(la.kind == 0 || la.kind == 51)) {SynErr(201); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(199); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(202); Get();}
Expect(8);
} else {
- while (!(la.kind == 0 || la.kind == 45)) {SynErr(200); Get();}
+ while (!(la.kind == 0 || la.kind == 47)) {SynErr(203); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -2410,13 +2457,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (StartOf(13)) {
FrameExpression(out fe);
mod.Add(fe);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
FrameExpression(out fe);
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(201); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(204); Get();}
Expect(8);
}
}
@@ -2424,12 +2471,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void Invariant(out MaybeFreeExpression/*!*/ invariant) {
bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null;
- while (!(la.kind == 0 || la.kind == 46 || la.kind == 81)) {SynErr(202); Get();}
- if (la.kind == 46) {
+ while (!(la.kind == 0 || la.kind == 48 || la.kind == 83)) {SynErr(205); Get();}
+ if (la.kind == 48) {
Get();
isFree = true;
}
- Expect(81);
+ Expect(83);
while (IsAttribute()) {
Attribute(ref attrs);
}
@@ -2444,21 +2491,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
BoundVar/*!*/ bv;
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(78);
+ Expect(80);
x = t;
Ident(out id);
if (la.kind == 11) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
}
Expect(12);
}
- Expect(79);
+ Expect(81);
while (StartOf(15)) {
Stmt(body);
}
@@ -2473,7 +2520,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(17)) {
Expression(out e, allowSemi);
arg = new Attributes.Argument(t, e);
- } else SynErr(203);
+ } else SynErr(206);
}
void QuantifierDomain(out List<BoundVar> bvars, out Attributes attrs, out Expression range) {
@@ -2484,7 +2531,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IdentTypeOptional(out bv);
bvars.Add(bv);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
IdentTypeOptional(out bv);
bvars.Add(bv);
@@ -2492,7 +2539,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
while (IsAttribute()) {
Attribute(ref attrs);
}
- if (la.kind == 29) {
+ if (la.kind == 31) {
Get();
Expression(out range, true);
}
@@ -2504,73 +2551,73 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = null;
switch (la.kind) {
- case 33: {
+ case 35: {
Get();
x = t; binOp = BinaryExpr.Opcode.Eq;
- if (la.kind == 89) {
+ if (la.kind == 91) {
Get();
- Expect(74);
+ Expect(76);
Expression(out k, true);
- Expect(75);
+ Expect(77);
}
break;
}
- case 38: {
+ case 40: {
Get();
x = t; binOp = BinaryExpr.Opcode.Lt;
break;
}
- case 39: {
+ case 41: {
Get();
x = t; binOp = BinaryExpr.Opcode.Gt;
break;
}
- case 90: {
+ case 92: {
Get();
x = t; binOp = BinaryExpr.Opcode.Le;
break;
}
- case 91: {
+ case 93: {
Get();
x = t; binOp = BinaryExpr.Opcode.Ge;
break;
}
- case 92: {
+ case 94: {
Get();
x = t; binOp = BinaryExpr.Opcode.Neq;
break;
}
- case 93: {
+ case 95: {
Get();
x = t; binOp = BinaryExpr.Opcode.Neq;
break;
}
- case 94: {
+ case 96: {
Get();
x = t; binOp = BinaryExpr.Opcode.Le;
break;
}
- case 95: {
+ case 97: {
Get();
x = t; binOp = BinaryExpr.Opcode.Ge;
break;
}
- case 96: case 97: {
+ case 98: case 99: {
EquivOp();
x = t; binOp = BinaryExpr.Opcode.Iff;
break;
}
- case 98: case 99: {
+ case 100: case 101: {
ImpliesOp();
x = t; binOp = BinaryExpr.Opcode.Imp;
break;
}
- case 100: case 101: {
+ case 102: case 103: {
ExpliesOp();
x = t; binOp = BinaryExpr.Opcode.Exp;
break;
}
- default: SynErr(204); break;
+ default: SynErr(207); break;
}
if (k == null) {
op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
@@ -2589,7 +2636,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Token x = la;
IToken endTok = x;
- while (la.kind == 9 || la.kind == 88) {
+ while (la.kind == 9 || la.kind == 90) {
if (la.kind == 9) {
BlockStmt(out block, out bodyStart, out bodyEnd);
endTok = block.EndTok; subhints.Add(block);
@@ -2603,33 +2650,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void EquivOp() {
- if (la.kind == 96) {
+ if (la.kind == 98) {
Get();
- } else if (la.kind == 97) {
+ } else if (la.kind == 99) {
Get();
- } else SynErr(205);
+ } else SynErr(208);
}
void ImpliesOp() {
- if (la.kind == 98) {
+ if (la.kind == 100) {
Get();
- } else if (la.kind == 99) {
+ } else if (la.kind == 101) {
Get();
- } else SynErr(206);
+ } else SynErr(209);
}
void ExpliesOp() {
- if (la.kind == 100) {
+ if (la.kind == 102) {
Get();
- } else if (la.kind == 101) {
+ } else if (la.kind == 103) {
Get();
- } else SynErr(207);
+ } else SynErr(210);
}
void EquivExpression(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpliesExpression(out e0, allowSemi);
- while (la.kind == 96 || la.kind == 97) {
+ while (la.kind == 98 || la.kind == 99) {
EquivOp();
x = t;
ImpliesExpliesExpression(out e1, allowSemi);
@@ -2641,7 +2688,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0, allowSemi);
if (StartOf(29)) {
- if (la.kind == 98 || la.kind == 99) {
+ if (la.kind == 100 || la.kind == 101) {
ImpliesOp();
x = t;
ImpliesExpression(out e1, allowSemi);
@@ -2651,7 +2698,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t;
LogicalExpression(out e1, allowSemi);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1);
- while (la.kind == 100 || la.kind == 101) {
+ while (la.kind == 102 || la.kind == 103) {
ExpliesOp();
x = t;
LogicalExpression(out e1, allowSemi);
@@ -2665,12 +2712,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0, allowSemi);
if (StartOf(30)) {
- if (la.kind == 102 || la.kind == 103) {
+ if (la.kind == 104 || la.kind == 105) {
AndOp();
x = t;
RelationalExpression(out e1, allowSemi);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 102 || la.kind == 103) {
+ while (la.kind == 104 || la.kind == 105) {
AndOp();
x = t;
RelationalExpression(out e1, allowSemi);
@@ -2681,7 +2728,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t;
RelationalExpression(out e1, allowSemi);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 104 || la.kind == 105) {
+ while (la.kind == 106 || la.kind == 107) {
OrOp();
x = t;
RelationalExpression(out e1, allowSemi);
@@ -2694,7 +2741,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void ImpliesExpression(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0, allowSemi);
- if (la.kind == 98 || la.kind == 99) {
+ if (la.kind == 100 || la.kind == 101) {
ImpliesOp();
x = t;
ImpliesExpression(out e1, allowSemi);
@@ -2804,25 +2851,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void AndOp() {
- if (la.kind == 102) {
+ if (la.kind == 104) {
Get();
- } else if (la.kind == 103) {
+ } else if (la.kind == 105) {
Get();
- } else SynErr(208);
+ } else SynErr(211);
}
void OrOp() {
- if (la.kind == 104) {
+ if (la.kind == 106) {
Get();
- } else if (la.kind == 105) {
+ } else if (la.kind == 107) {
Get();
- } else SynErr(209);
+ } else SynErr(212);
}
void Term(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0, allowSemi);
- while (la.kind == 108 || la.kind == 109) {
+ while (la.kind == 110 || la.kind == 111) {
AddOp(out x, out op);
Factor(out e1, allowSemi);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2836,49 +2883,49 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
k = null;
switch (la.kind) {
- case 33: {
+ case 35: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
- if (la.kind == 89) {
+ if (la.kind == 91) {
Get();
- Expect(74);
+ Expect(76);
Expression(out k, true);
- Expect(75);
+ Expect(77);
}
break;
}
- case 38: {
+ case 40: {
Get();
x = t; op = BinaryExpr.Opcode.Lt;
break;
}
- case 39: {
+ case 41: {
Get();
x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 90: {
+ case 92: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 91: {
+ case 93: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 92: {
+ case 94: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
- if (la.kind == 89) {
+ if (la.kind == 91) {
Get();
- Expect(74);
+ Expect(76);
Expression(out k, true);
- Expect(75);
+ Expect(77);
}
break;
}
- case 106: {
+ case 108: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
@@ -2888,10 +2935,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 107: {
+ case 109: {
Get();
x = t; y = Token.NoToken;
- if (la.kind == 107) {
+ if (la.kind == 109) {
Get();
y = t;
}
@@ -2906,29 +2953,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
break;
}
- case 93: {
+ case 95: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 94: {
+ case 96: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 95: {
+ case 97: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(210); break;
+ default: SynErr(213); break;
}
}
void Factor(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0, allowSemi);
- while (la.kind == 13 || la.kind == 110 || la.kind == 111) {
+ while (la.kind == 13 || la.kind == 112 || la.kind == 113) {
MulOp(out x, out op);
UnaryExpression(out e1, allowSemi);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2937,80 +2984,80 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void AddOp(out IToken x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 108) {
+ if (la.kind == 110) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 109) {
+ } else if (la.kind == 111) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(211);
+ } else SynErr(214);
}
void UnaryExpression(out Expression e, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 109: {
+ case 111: {
Get();
x = t;
UnaryExpression(out e, allowSemi);
e = new NegationExpression(x, e);
break;
}
- case 107: case 112: {
+ case 109: case 114: {
NegOp();
x = t;
UnaryExpression(out e, allowSemi);
e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Not, e);
break;
}
- case 25: case 30: case 56: case 66: case 72: case 76: case 82: case 83: case 85: case 88: case 121: case 122: case 123: {
+ case 27: case 32: case 58: case 68: case 74: case 78: case 84: case 85: case 87: case 90: case 123: case 124: case 125: {
EndlessExpression(out e, allowSemi);
break;
}
case 1: {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 61 || la.kind == 74) {
+ while (la.kind == 63 || la.kind == 76) {
Suffix(ref e);
}
break;
}
- case 9: case 74: {
+ case 9: case 76: {
DisplayExpr(out e);
- while (la.kind == 61 || la.kind == 74) {
+ while (la.kind == 63 || la.kind == 76) {
Suffix(ref e);
}
break;
}
- case 57: {
+ case 59: {
MultiSetExpr(out e);
- while (la.kind == 61 || la.kind == 74) {
+ while (la.kind == 63 || la.kind == 76) {
Suffix(ref e);
}
break;
}
- case 59: {
+ case 61: {
Get();
x = t;
- if (la.kind == 74) {
+ if (la.kind == 76) {
MapDisplayExpr(x, out e);
- while (la.kind == 61 || la.kind == 74) {
+ while (la.kind == 63 || la.kind == 76) {
Suffix(ref e);
}
} else if (la.kind == 1) {
MapComprehensionExpr(x, out e, allowSemi);
} else if (StartOf(32)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(212);
+ } else SynErr(215);
break;
}
- case 2: case 3: case 4: case 11: case 29: case 54: case 55: case 113: case 114: case 115: case 116: case 117: case 118: {
+ case 2: case 3: case 4: case 11: case 31: case 56: case 57: case 115: case 116: case 117: case 118: case 119: case 120: {
ConstAtomExpression(out e);
- while (la.kind == 61 || la.kind == 74) {
+ while (la.kind == 63 || la.kind == 76) {
Suffix(ref e);
}
break;
}
- default: SynErr(213); break;
+ default: SynErr(216); break;
}
}
@@ -3019,21 +3066,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 13) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 110) {
+ } else if (la.kind == 112) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 111) {
+ } else if (la.kind == 113) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(214);
+ } else SynErr(217);
}
void NegOp() {
- if (la.kind == 107) {
+ if (la.kind == 109) {
Get();
- } else if (la.kind == 112) {
+ } else if (la.kind == 114) {
Get();
- } else SynErr(215);
+ } else SynErr(218);
}
void EndlessExpression(out Expression e, bool allowSemi) {
@@ -3043,44 +3090,44 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = dummyExpr;
switch (la.kind) {
- case 76: {
+ case 78: {
Get();
x = t;
Expression(out e, true);
- Expect(119);
+ Expect(121);
Expression(out e0, true);
- Expect(77);
+ Expect(79);
Expression(out e1, allowSemi);
e = new ITEExpr(x, e, e0, e1);
break;
}
- case 82: {
+ case 84: {
MatchExpression(out e, allowSemi);
break;
}
- case 85: case 121: case 122: case 123: {
+ case 87: case 123: case 124: case 125: {
QuantifierGuts(out e, allowSemi);
break;
}
- case 56: {
+ case 58: {
ComprehensionExpr(out e, allowSemi);
break;
}
- case 72: case 83: case 88: {
+ case 74: case 85: case 90: {
StmtInExpr(out s);
Expression(out e, allowSemi);
e = new StmtExpr(s.Tok, s, e);
break;
}
- case 25: case 30: {
+ case 27: case 32: {
LetExpr(out e, allowSemi);
break;
}
- case 66: {
+ case 68: {
NamedExpr(out e, allowSemi);
break;
}
- default: SynErr(216); break;
+ default: SynErr(219); break;
}
}
@@ -3091,20 +3138,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Ident(out id);
idents.Add(id);
- while (la.kind == 61) {
+ while (la.kind == 63) {
IdentOrDigitsSuffix(out id, out idPrime);
idents.Add(id);
if (idPrime != null) { idents.Add(idPrime); id = idPrime; }
}
- if (la.kind == 11 || la.kind == 89) {
+ if (la.kind == 11 || la.kind == 91) {
args = new List<Expression>();
- if (la.kind == 89) {
+ if (la.kind == 91) {
Get();
id.val = id.val + "#"; Expression k;
- Expect(74);
+ Expect(76);
Expression(out k, true);
- Expect(75);
+ Expect(77);
args.Add(k);
}
Expect(11);
@@ -3123,7 +3170,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 61) {
+ if (la.kind == 63) {
IdentOrDigitsSuffix(out id, out x);
if (x != null) {
// process id as a Suffix in its own right
@@ -3131,14 +3178,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
id = x; // move to the next Suffix
}
- if (la.kind == 11 || la.kind == 89) {
+ if (la.kind == 11 || la.kind == 91) {
args = new List<Expression/*!*/>(); func = true;
- if (la.kind == 89) {
+ if (la.kind == 91) {
Get();
id.val = id.val + "#"; Expression k;
- Expect(74);
+ Expect(76);
Expression(out k, true);
- Expect(75);
+ Expect(77);
args.Add(k);
}
Expect(11);
@@ -3150,24 +3197,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new FunctionCallExpr(id, id.val, e, openParen, args);
}
if (!func) { e = new ExprDotName(id, e, id.val); }
- } else if (la.kind == 74) {
+ } else if (la.kind == 76) {
Get();
x = t;
if (StartOf(17)) {
Expression(out ee, true);
e0 = ee;
- if (la.kind == 120) {
+ if (la.kind == 122) {
Get();
anyDots = true;
if (StartOf(17)) {
Expression(out ee, true);
e1 = ee;
}
- } else if (la.kind == 69) {
+ } else if (la.kind == 71) {
Get();
Expression(out ee, true);
e1 = ee;
- } else if (la.kind == 7 || la.kind == 75) {
+ } else if (la.kind == 7 || la.kind == 77) {
while (la.kind == 7) {
Get();
if (multipleLengths == null) {
@@ -3183,8 +3230,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
}
- } else if (la.kind == 31 || la.kind == 75) {
- while (la.kind == 31) {
+ } else if (la.kind == 33 || la.kind == 77) {
+ while (la.kind == 33) {
Get();
Expression(out ee, true);
if (multipleIndices == null) {
@@ -3194,15 +3241,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
multipleIndices.Add(ee);
}
- } else SynErr(217);
- } else if (la.kind == 120) {
+ } else SynErr(220);
+ } else if (la.kind == 122) {
Get();
anyDots = true;
if (StartOf(17)) {
Expression(out ee, true);
e1 = ee;
}
- } else SynErr(218);
+ } else SynErr(221);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -3242,8 +3289,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
}
- Expect(75);
- } else SynErr(219);
+ Expect(77);
+ } else SynErr(222);
}
void DisplayExpr(out Expression e) {
@@ -3259,15 +3306,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
e = new SetDisplayExpr(x, elements);
Expect(10);
- } else if (la.kind == 74) {
+ } else if (la.kind == 76) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(17)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(75);
- } else SynErr(220);
+ Expect(77);
+ } else SynErr(223);
}
void MultiSetExpr(out Expression e) {
@@ -3275,7 +3322,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
- Expect(57);
+ Expect(59);
x = t;
if (la.kind == 9) {
Get();
@@ -3293,7 +3340,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(12);
} else if (StartOf(33)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(221);
+ } else SynErr(224);
}
void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {
@@ -3301,12 +3348,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;
e = dummyExpr;
- Expect(74);
+ Expect(76);
if (StartOf(17)) {
MapLiteralExpressions(out elements);
}
e = new MapDisplayExpr(mapToken, elements);
- Expect(75);
+ Expect(77);
}
void MapComprehensionExpr(IToken mapToken, out Expression e, bool allowSemi) {
@@ -3318,7 +3365,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IdentTypeOptional(out bv);
bvars.Add(bv);
- if (la.kind == 29) {
+ if (la.kind == 31) {
Get();
Expression(out range, true);
}
@@ -3334,17 +3381,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = dummyExpr; Type toType = null;
switch (la.kind) {
- case 113: {
+ case 115: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 114: {
+ case 116: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 115: {
+ case 117: {
Get();
e = new LiteralExpr(t);
break;
@@ -3359,12 +3406,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new LiteralExpr(t, d);
break;
}
- case 116: {
+ case 118: {
Get();
e = new ThisExpr(t);
break;
}
- case 117: {
+ case 119: {
Get();
x = t;
Expect(11);
@@ -3373,7 +3420,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Fresh, e);
break;
}
- case 118: {
+ case 120: {
Get();
x = t;
Expect(11);
@@ -3382,16 +3429,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new OldExpr(x, e);
break;
}
- case 29: {
+ case 31: {
Get();
x = t;
Expression(out e, true);
e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Cardinality, e);
- Expect(29);
+ Expect(31);
break;
}
- case 54: case 55: {
- if (la.kind == 54) {
+ case 56: case 57: {
+ if (la.kind == 56) {
Get();
x = t; toType = new IntType();
} else {
@@ -3408,7 +3455,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ParensExpression(out e);
break;
}
- default: SynErr(222); break;
+ default: SynErr(225); break;
}
}
@@ -3433,7 +3480,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
n = BigInteger.Zero;
}
- } else SynErr(223);
+ } else SynErr(226);
}
void Dec(out Basetypes.BigDec d) {
@@ -3461,7 +3508,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(17)) {
Expression(out e, true);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
if (args == null) {
args = new List<Expression>();
@@ -3480,31 +3527,31 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args);
}
- } else SynErr(224);
+ } else SynErr(227);
}
void MapLiteralExpressions(out List<ExpressionPair> elements) {
Expression/*!*/ d, r;
elements = new List<ExpressionPair/*!*/>();
Expression(out d, true);
- Expect(69);
+ Expect(71);
Expression(out r, true);
elements.Add(new ExpressionPair(d,r));
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
Expression(out d, true);
- Expect(69);
+ Expect(71);
Expression(out r, true);
elements.Add(new ExpressionPair(d,r));
}
}
void QSep() {
- if (la.kind == 124) {
+ if (la.kind == 126) {
Get();
- } else if (la.kind == 125) {
+ } else if (la.kind == 127) {
Get();
- } else SynErr(225);
+ } else SynErr(228);
}
void MatchExpression(out Expression e, bool allowSemi) {
@@ -3512,14 +3559,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
bool usesOptionalBrace = false;
- Expect(82);
+ Expect(84);
x = t;
Expression(out e, allowSemi);
if (la.kind == 9) {
Get();
usesOptionalBrace = true;
}
- while (la.kind == 78) {
+ while (la.kind == 80) {
CaseExpression(out c, allowSemi);
cases.Add(c);
}
@@ -3527,7 +3574,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(10);
} else if (StartOf(32)) {
if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); }
- } else SynErr(226);
+ } else SynErr(229);
e = new MatchExpr(x, e, cases, usesOptionalBrace);
}
@@ -3539,13 +3586,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression range;
Expression/*!*/ body;
- if (la.kind == 85 || la.kind == 121) {
+ if (la.kind == 87 || la.kind == 123) {
Forall();
x = t; univ = true;
- } else if (la.kind == 122 || la.kind == 123) {
+ } else if (la.kind == 124 || la.kind == 125) {
Exists();
x = t;
- } else SynErr(227);
+ } else SynErr(230);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body, allowSemi);
@@ -3565,18 +3612,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression range;
Expression body = null;
- Expect(56);
+ Expect(58);
x = t;
IdentTypeOptional(out bv);
bvars.Add(bv);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
IdentTypeOptional(out bv);
bvars.Add(bv);
}
- Expect(29);
+ Expect(31);
Expression(out range, allowSemi);
- if (la.kind == 124 || la.kind == 125) {
+ if (la.kind == 126 || la.kind == 127) {
QSep();
Expression(out body, allowSemi);
}
@@ -3587,13 +3634,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void StmtInExpr(out Statement s) {
s = dummyStmt;
- if (la.kind == 83) {
+ if (la.kind == 85) {
AssertStmt(out s);
- } else if (la.kind == 72) {
+ } else if (la.kind == 74) {
AssumeStmt(out s);
- } else if (la.kind == 88) {
+ } else if (la.kind == 90) {
CalcStmt(out s);
- } else SynErr(228);
+ } else SynErr(231);
}
void LetExpr(out Expression e, bool allowSemi) {
@@ -3605,26 +3652,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
bool exact = true;
e = dummyExpr;
- if (la.kind == 25) {
+ if (la.kind == 27) {
Get();
isGhost = true; x = t;
}
- Expect(30);
+ Expect(32);
if (!isGhost) { x = t; }
CasePattern(out pat);
if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); }
letLHSs.Add(pat);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
CasePattern(out pat);
if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); }
letLHSs.Add(pat);
}
- if (la.kind == 69) {
+ if (la.kind == 71) {
Get();
- } else if (la.kind == 71) {
+ } else if (la.kind == 73) {
Get();
exact = false;
foreach (var lhs in letLHSs) {
@@ -3633,10 +3680,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
}
- } else SynErr(229);
+ } else SynErr(232);
Expression(out e, false);
letRHSs.Add(e);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
Expression(out e, false);
letRHSs.Add(e);
@@ -3651,7 +3698,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = dummyExpr;
Expression expr;
- Expect(66);
+ Expect(68);
x = t;
NoUSIdent(out d);
Expect(7);
@@ -3672,7 +3719,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 1) {
CasePattern(out pat);
arguments.Add(pat);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
CasePattern(out pat);
arguments.Add(pat);
@@ -3684,7 +3731,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IdentTypeOptional(out bv);
pat = new CasePattern(bv.tok, bv);
- } else SynErr(230);
+ } else SynErr(233);
}
void CaseExpression(out MatchCaseExpr c, bool allowSemi) {
@@ -3693,39 +3740,39 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
BoundVar/*!*/ bv;
Expression/*!*/ body;
- Expect(78);
+ Expect(80);
x = t;
Ident(out id);
if (la.kind == 11) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
}
Expect(12);
}
- Expect(79);
+ Expect(81);
Expression(out body, allowSemi);
c = new MatchCaseExpr(x, id.val, arguments, body);
}
void Forall() {
- if (la.kind == 85) {
+ if (la.kind == 87) {
Get();
- } else if (la.kind == 121) {
+ } else if (la.kind == 123) {
Get();
- } else SynErr(231);
+ } else SynErr(234);
}
void Exists() {
- if (la.kind == 122) {
+ if (la.kind == 124) {
Get();
- } else if (la.kind == 123) {
+ } else if (la.kind == 125) {
Get();
- } else SynErr(232);
+ } else SynErr(235);
}
void AttributeBody(ref Attributes attrs) {
@@ -3739,7 +3786,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (StartOf(34)) {
AttributeArg(out aArg, true);
aArgs.Add(aArg);
- while (la.kind == 31) {
+ while (la.kind == 33) {
Get();
AttributeArg(out aArg, true);
aArgs.Add(aArg);
@@ -3761,41 +3808,41 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
static readonly bool[,]/*!*/ set = {
- {T,T,T,T, T,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, T,T,T,x, x,x,T,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,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,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,T,T,T, T,x,T,x, T,x,T,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,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,T,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,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},
- {T,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, T,T,T,T, T,x,T,x, T,x,T,x, x,x,T,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {T,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, T,T,x,T, x,x,x,x, T,T,T,T, T,x,T,x, T,x,T,x, x,x,T,x, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,T,x, x,T,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,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,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
- {T,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,T,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,T,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,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,T,T, T,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,T,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,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,T,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
- {x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,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,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,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,T,T, T,T,T,T, 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,T,T,T, T,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,T, x,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,T, x,T,T,x, T,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,T, T,T,T,T, T,x,x,x, T,T,x,x},
- {x,T,T,T, T,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,T, x,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,T, x,x,T,T, x,x,x,x, x,T,x,x, x,T,T,T, x,T,T,x, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,T, T,T,T,T, T,x,x,x, T,T,x,x},
- {x,T,T,T, T,x,T,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x}
+ {T,T,T,T, T,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,T, x,T,T,T, T,x,x,x, T,x,x,T, x,x,T,T, T,T,T,T, T,T,T,T, T,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,T,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,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,x, T,x,T,x, T,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, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,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, 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},
+ {T,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, T,x,T,T, T,T,T,x, T,x,T,x, T,x,x,x, T,x,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {T,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,x, T,x,T,x, T,x,x,x, T,x,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,T,x, x,T,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,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},
+ {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,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,T,x, x,x,T,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x},
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,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, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},
+ {T,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,T,x, x,x,T,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,T, 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, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},
+ {x,T,T,T, T,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,T,x, T,x,T,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, T,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,T,x, T,x,T,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T, 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, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,T, 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,T, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, T,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},
+ {x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,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,T,T,T, T,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,T,x,T, x,x,x,T, T,T,x,x, x,x,x,T, T,x,T,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,T, T,T,x,T, T,x,T,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,x,T, T,T,T,T, T,T,T,x, x,x,T,T, x,x},
+ {x,T,T,T, T,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,T,x,T, x,x,x,T, T,T,x,x, x,x,x,T, T,x,T,T, x,T,x,x, T,T,x,x, x,x,x,T, x,x,x,T, T,T,x,T, T,x,T,x, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,x,T, T,T,T,T, T,T,T,x, x,x,T,T, x,x},
+ {x,T,T,T, T,x,T,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,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, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x}
};
} // end Parser
@@ -3845,214 +3892,217 @@ public class Errors {
case 22: s = "\"as\" expected"; break;
case 23: s = "\"default\" expected"; break;
case 24: s = "\"class\" expected"; break;
- case 25: s = "\"ghost\" expected"; break;
- case 26: s = "\"static\" expected"; break;
- case 27: s = "\"datatype\" expected"; break;
- case 28: s = "\"codatatype\" expected"; break;
- case 29: s = "\"|\" expected"; break;
- case 30: s = "\"var\" expected"; break;
- case 31: s = "\",\" expected"; break;
- case 32: s = "\"type\" expected"; break;
- case 33: s = "\"==\" expected"; break;
- case 34: s = "\"iterator\" expected"; break;
- case 35: s = "\"yields\" expected"; break;
- case 36: s = "\"returns\" expected"; break;
- case 37: s = "\"...\" expected"; break;
- case 38: s = "\"<\" expected"; break;
- case 39: s = "\">\" expected"; break;
- case 40: s = "\"method\" expected"; break;
- case 41: s = "\"lemma\" expected"; break;
- case 42: s = "\"colemma\" expected"; break;
- case 43: s = "\"comethod\" expected"; break;
- case 44: s = "\"constructor\" expected"; break;
- case 45: s = "\"modifies\" expected"; break;
- case 46: s = "\"free\" expected"; break;
- case 47: s = "\"requires\" expected"; break;
- case 48: s = "\"ensures\" expected"; break;
- case 49: s = "\"decreases\" expected"; break;
- case 50: s = "\"reads\" expected"; break;
- case 51: s = "\"yield\" expected"; break;
- case 52: s = "\"bool\" expected"; break;
- case 53: s = "\"nat\" expected"; break;
- case 54: s = "\"int\" expected"; break;
- case 55: s = "\"real\" expected"; break;
- case 56: s = "\"set\" expected"; break;
- case 57: s = "\"multiset\" expected"; break;
- case 58: s = "\"seq\" expected"; break;
- case 59: s = "\"map\" expected"; break;
- case 60: s = "\"object\" expected"; break;
- case 61: s = "\".\" expected"; break;
- case 62: s = "\"function\" expected"; break;
- case 63: s = "\"predicate\" expected"; break;
- case 64: s = "\"copredicate\" expected"; break;
- case 65: s = "\"`\" expected"; break;
- case 66: s = "\"label\" expected"; break;
- case 67: s = "\"break\" expected"; break;
- case 68: s = "\"where\" expected"; break;
- case 69: s = "\":=\" expected"; break;
- case 70: s = "\"return\" expected"; break;
- case 71: s = "\":|\" expected"; break;
- case 72: s = "\"assume\" expected"; break;
- case 73: s = "\"new\" expected"; break;
- case 74: s = "\"[\" expected"; break;
- case 75: s = "\"]\" expected"; break;
- case 76: s = "\"if\" expected"; break;
- case 77: s = "\"else\" expected"; break;
- case 78: s = "\"case\" expected"; break;
- case 79: s = "\"=>\" expected"; break;
- case 80: s = "\"while\" expected"; break;
- case 81: s = "\"invariant\" expected"; break;
- case 82: s = "\"match\" expected"; break;
- case 83: s = "\"assert\" expected"; break;
- case 84: s = "\"print\" expected"; break;
- case 85: s = "\"forall\" expected"; break;
- case 86: s = "\"parallel\" expected"; break;
- case 87: s = "\"modify\" expected"; break;
- case 88: s = "\"calc\" expected"; break;
- case 89: s = "\"#\" expected"; break;
- case 90: s = "\"<=\" expected"; break;
- case 91: s = "\">=\" expected"; break;
- case 92: s = "\"!=\" expected"; break;
- case 93: s = "\"\\u2260\" expected"; break;
- case 94: s = "\"\\u2264\" expected"; break;
- case 95: s = "\"\\u2265\" expected"; break;
- case 96: s = "\"<==>\" expected"; break;
- case 97: s = "\"\\u21d4\" expected"; break;
- case 98: s = "\"==>\" expected"; break;
- case 99: s = "\"\\u21d2\" expected"; break;
- case 100: s = "\"<==\" expected"; break;
- case 101: s = "\"\\u21d0\" expected"; break;
- case 102: s = "\"&&\" expected"; break;
- case 103: s = "\"\\u2227\" expected"; break;
- case 104: s = "\"||\" expected"; break;
- case 105: s = "\"\\u2228\" expected"; break;
- case 106: s = "\"in\" expected"; break;
- case 107: s = "\"!\" expected"; break;
- case 108: s = "\"+\" expected"; break;
- case 109: s = "\"-\" expected"; break;
- case 110: s = "\"/\" expected"; break;
- case 111: s = "\"%\" expected"; break;
- case 112: s = "\"\\u00ac\" expected"; break;
- case 113: s = "\"false\" expected"; break;
- case 114: s = "\"true\" expected"; break;
- case 115: s = "\"null\" expected"; break;
- case 116: s = "\"this\" expected"; break;
- case 117: s = "\"fresh\" expected"; break;
- case 118: s = "\"old\" expected"; break;
- case 119: s = "\"then\" expected"; break;
- case 120: s = "\"..\" expected"; break;
- case 121: s = "\"\\u2200\" expected"; break;
- case 122: s = "\"exists\" expected"; break;
- case 123: s = "\"\\u2203\" expected"; break;
- case 124: s = "\"::\" expected"; break;
- case 125: s = "\"\\u2022\" expected"; break;
- case 126: s = "??? expected"; break;
- case 127: s = "this symbol not expected in SubModuleDecl"; break;
- case 128: s = "invalid SubModuleDecl"; break;
- case 129: s = "this symbol not expected in ClassDecl"; break;
- case 130: s = "this symbol not expected in DatatypeDecl"; break;
- case 131: s = "invalid DatatypeDecl"; break;
+ case 25: s = "\"extends\" expected"; break;
+ case 26: s = "\"trait\" expected"; break;
+ case 27: s = "\"ghost\" expected"; break;
+ case 28: s = "\"static\" expected"; break;
+ case 29: s = "\"datatype\" expected"; break;
+ case 30: s = "\"codatatype\" expected"; break;
+ case 31: s = "\"|\" expected"; break;
+ case 32: s = "\"var\" expected"; break;
+ case 33: s = "\",\" expected"; break;
+ case 34: s = "\"type\" expected"; break;
+ case 35: s = "\"==\" expected"; break;
+ case 36: s = "\"iterator\" expected"; break;
+ case 37: s = "\"yields\" expected"; break;
+ case 38: s = "\"returns\" expected"; break;
+ case 39: s = "\"...\" expected"; break;
+ case 40: s = "\"<\" expected"; break;
+ case 41: s = "\">\" expected"; break;
+ case 42: s = "\"method\" expected"; break;
+ case 43: s = "\"lemma\" expected"; break;
+ case 44: s = "\"colemma\" expected"; break;
+ case 45: s = "\"comethod\" expected"; break;
+ case 46: s = "\"constructor\" expected"; break;
+ case 47: s = "\"modifies\" expected"; break;
+ case 48: s = "\"free\" expected"; break;
+ case 49: s = "\"requires\" expected"; break;
+ case 50: s = "\"ensures\" expected"; break;
+ case 51: s = "\"decreases\" expected"; break;
+ case 52: s = "\"reads\" expected"; break;
+ case 53: s = "\"yield\" expected"; break;
+ case 54: s = "\"bool\" expected"; break;
+ case 55: s = "\"nat\" expected"; break;
+ case 56: s = "\"int\" expected"; break;
+ case 57: s = "\"real\" expected"; break;
+ case 58: s = "\"set\" expected"; break;
+ case 59: s = "\"multiset\" expected"; break;
+ case 60: s = "\"seq\" expected"; break;
+ case 61: s = "\"map\" expected"; break;
+ case 62: s = "\"object\" expected"; break;
+ case 63: s = "\".\" expected"; break;
+ case 64: s = "\"function\" expected"; break;
+ case 65: s = "\"predicate\" expected"; break;
+ case 66: s = "\"copredicate\" expected"; break;
+ case 67: s = "\"`\" expected"; break;
+ case 68: s = "\"label\" expected"; break;
+ case 69: s = "\"break\" expected"; break;
+ case 70: s = "\"where\" expected"; break;
+ case 71: s = "\":=\" expected"; break;
+ case 72: s = "\"return\" expected"; break;
+ case 73: s = "\":|\" expected"; break;
+ case 74: s = "\"assume\" expected"; break;
+ case 75: s = "\"new\" expected"; break;
+ case 76: s = "\"[\" expected"; break;
+ case 77: s = "\"]\" expected"; break;
+ case 78: s = "\"if\" expected"; break;
+ case 79: s = "\"else\" expected"; break;
+ case 80: s = "\"case\" expected"; break;
+ case 81: s = "\"=>\" expected"; break;
+ case 82: s = "\"while\" expected"; break;
+ case 83: s = "\"invariant\" expected"; break;
+ case 84: s = "\"match\" expected"; break;
+ case 85: s = "\"assert\" expected"; break;
+ case 86: s = "\"print\" expected"; break;
+ case 87: s = "\"forall\" expected"; break;
+ case 88: s = "\"parallel\" expected"; break;
+ case 89: s = "\"modify\" expected"; break;
+ case 90: s = "\"calc\" expected"; break;
+ case 91: s = "\"#\" expected"; break;
+ case 92: s = "\"<=\" expected"; break;
+ case 93: s = "\">=\" expected"; break;
+ case 94: s = "\"!=\" expected"; break;
+ case 95: s = "\"\\u2260\" expected"; break;
+ case 96: s = "\"\\u2264\" expected"; break;
+ case 97: s = "\"\\u2265\" expected"; break;
+ case 98: s = "\"<==>\" expected"; break;
+ case 99: s = "\"\\u21d4\" expected"; break;
+ case 100: s = "\"==>\" expected"; break;
+ case 101: s = "\"\\u21d2\" expected"; break;
+ case 102: s = "\"<==\" expected"; break;
+ case 103: s = "\"\\u21d0\" expected"; break;
+ case 104: s = "\"&&\" expected"; break;
+ case 105: s = "\"\\u2227\" expected"; break;
+ case 106: s = "\"||\" expected"; break;
+ case 107: s = "\"\\u2228\" expected"; break;
+ case 108: s = "\"in\" expected"; break;
+ case 109: s = "\"!\" expected"; break;
+ case 110: s = "\"+\" expected"; break;
+ case 111: s = "\"-\" expected"; break;
+ case 112: s = "\"/\" expected"; break;
+ case 113: s = "\"%\" expected"; break;
+ case 114: s = "\"\\u00ac\" expected"; break;
+ case 115: s = "\"false\" expected"; break;
+ case 116: s = "\"true\" expected"; break;
+ case 117: s = "\"null\" expected"; break;
+ case 118: s = "\"this\" expected"; break;
+ case 119: s = "\"fresh\" expected"; break;
+ case 120: s = "\"old\" expected"; break;
+ case 121: s = "\"then\" expected"; break;
+ case 122: s = "\"..\" expected"; break;
+ case 123: s = "\"\\u2200\" expected"; break;
+ case 124: s = "\"exists\" expected"; break;
+ case 125: s = "\"\\u2203\" expected"; break;
+ case 126: s = "\"::\" expected"; break;
+ case 127: s = "\"\\u2022\" expected"; break;
+ case 128: s = "??? expected"; break;
+ case 129: s = "this symbol not expected in SubModuleDecl"; break;
+ case 130: s = "invalid SubModuleDecl"; break;
+ case 131: s = "this symbol not expected in ClassDecl"; break;
case 132: s = "this symbol not expected in DatatypeDecl"; break;
- case 133: s = "invalid OtherTypeDecl"; break;
- case 134: s = "this symbol not expected in OtherTypeDecl"; break;
- case 135: s = "this symbol not expected in IteratorDecl"; break;
- case 136: s = "invalid IteratorDecl"; break;
- case 137: s = "invalid ClassMemberDecl"; break;
- case 138: s = "invalid IdentOrDigitsSuffix"; break;
- case 139: s = "this symbol not expected in FieldDecl"; break;
- case 140: s = "this symbol not expected in FieldDecl"; break;
- case 141: s = "invalid FunctionDecl"; break;
- case 142: s = "invalid FunctionDecl"; break;
- case 143: s = "invalid FunctionDecl"; break;
+ case 133: s = "invalid DatatypeDecl"; break;
+ case 134: s = "this symbol not expected in DatatypeDecl"; break;
+ case 135: s = "invalid OtherTypeDecl"; break;
+ case 136: s = "this symbol not expected in OtherTypeDecl"; break;
+ case 137: s = "this symbol not expected in IteratorDecl"; break;
+ case 138: s = "invalid IteratorDecl"; break;
+ case 139: s = "this symbol not expected in TraitDecl"; break;
+ case 140: s = "invalid ClassMemberDecl"; break;
+ case 141: s = "invalid IdentOrDigitsSuffix"; break;
+ case 142: s = "this symbol not expected in FieldDecl"; break;
+ case 143: s = "this symbol not expected in FieldDecl"; break;
case 144: s = "invalid FunctionDecl"; break;
- case 145: s = "this symbol not expected in MethodDecl"; break;
- case 146: s = "invalid MethodDecl"; break;
- case 147: s = "invalid MethodDecl"; break;
- case 148: s = "invalid FIdentType"; break;
- case 149: s = "invalid TypeIdentOptional"; break;
- case 150: s = "invalid TypeAndToken"; break;
- case 151: s = "this symbol not expected in IteratorSpec"; break;
- case 152: s = "this symbol not expected in IteratorSpec"; break;
- case 153: s = "this symbol not expected in IteratorSpec"; break;
+ case 145: s = "invalid FunctionDecl"; break;
+ case 146: s = "invalid FunctionDecl"; break;
+ case 147: s = "invalid FunctionDecl"; break;
+ case 148: s = "this symbol not expected in MethodDecl"; break;
+ case 149: s = "invalid MethodDecl"; break;
+ case 150: s = "invalid MethodDecl"; break;
+ case 151: s = "invalid FIdentType"; break;
+ case 152: s = "invalid TypeIdentOptional"; break;
+ case 153: s = "invalid TypeAndToken"; break;
case 154: s = "this symbol not expected in IteratorSpec"; break;
case 155: s = "this symbol not expected in IteratorSpec"; break;
- case 156: s = "invalid IteratorSpec"; break;
+ case 156: s = "this symbol not expected in IteratorSpec"; break;
case 157: s = "this symbol not expected in IteratorSpec"; break;
- case 158: s = "invalid IteratorSpec"; break;
- case 159: s = "this symbol not expected in MethodSpec"; break;
- case 160: s = "this symbol not expected in MethodSpec"; break;
- case 161: s = "this symbol not expected in MethodSpec"; break;
+ case 158: s = "this symbol not expected in IteratorSpec"; break;
+ case 159: s = "invalid IteratorSpec"; break;
+ case 160: s = "this symbol not expected in IteratorSpec"; break;
+ case 161: s = "invalid IteratorSpec"; break;
case 162: s = "this symbol not expected in MethodSpec"; break;
- case 163: s = "invalid MethodSpec"; break;
+ case 163: s = "this symbol not expected in MethodSpec"; break;
case 164: s = "this symbol not expected in MethodSpec"; break;
- case 165: s = "invalid MethodSpec"; break;
- case 166: s = "invalid FrameExpression"; break;
- case 167: s = "invalid ReferenceType"; break;
- case 168: s = "this symbol not expected in FunctionSpec"; break;
- case 169: s = "this symbol not expected in FunctionSpec"; break;
- case 170: s = "this symbol not expected in FunctionSpec"; break;
+ case 165: s = "this symbol not expected in MethodSpec"; break;
+ case 166: s = "invalid MethodSpec"; break;
+ case 167: s = "this symbol not expected in MethodSpec"; break;
+ case 168: s = "invalid MethodSpec"; break;
+ case 169: s = "invalid FrameExpression"; break;
+ case 170: s = "invalid ReferenceType"; break;
case 171: s = "this symbol not expected in FunctionSpec"; break;
case 172: s = "this symbol not expected in FunctionSpec"; break;
- case 173: s = "invalid FunctionSpec"; break;
- case 174: s = "invalid PossiblyWildFrameExpression"; break;
- case 175: s = "invalid PossiblyWildExpression"; break;
- case 176: s = "this symbol not expected in OneStmt"; break;
- case 177: s = "invalid OneStmt"; break;
- case 178: s = "this symbol not expected in OneStmt"; break;
- case 179: s = "invalid OneStmt"; break;
- case 180: s = "invalid AssertStmt"; break;
- case 181: s = "invalid AssumeStmt"; break;
- case 182: s = "invalid UpdateStmt"; break;
- case 183: s = "invalid UpdateStmt"; break;
- case 184: s = "invalid IfStmt"; break;
- case 185: s = "invalid IfStmt"; break;
- case 186: s = "invalid WhileStmt"; break;
- case 187: s = "invalid WhileStmt"; break;
- case 188: s = "invalid MatchStmt"; break;
- case 189: s = "invalid ForallStmt"; break;
- case 190: s = "invalid ForallStmt"; break;
- case 191: s = "this symbol not expected in ModifyStmt"; break;
- case 192: s = "invalid ModifyStmt"; break;
- case 193: s = "invalid ReturnStmt"; break;
- case 194: s = "invalid Rhs"; break;
- case 195: s = "invalid Lhs"; break;
- case 196: s = "invalid Guard"; break;
- case 197: s = "this symbol not expected in LoopSpec"; break;
- case 198: s = "this symbol not expected in LoopSpec"; break;
- case 199: s = "this symbol not expected in LoopSpec"; break;
+ case 173: s = "this symbol not expected in FunctionSpec"; break;
+ case 174: s = "this symbol not expected in FunctionSpec"; break;
+ case 175: s = "this symbol not expected in FunctionSpec"; break;
+ case 176: s = "invalid FunctionSpec"; break;
+ case 177: s = "invalid PossiblyWildFrameExpression"; break;
+ case 178: s = "invalid PossiblyWildExpression"; break;
+ case 179: s = "this symbol not expected in OneStmt"; break;
+ case 180: s = "invalid OneStmt"; break;
+ case 181: s = "this symbol not expected in OneStmt"; break;
+ case 182: s = "invalid OneStmt"; break;
+ case 183: s = "invalid AssertStmt"; break;
+ case 184: s = "invalid AssumeStmt"; break;
+ case 185: s = "invalid UpdateStmt"; break;
+ case 186: s = "invalid UpdateStmt"; break;
+ case 187: s = "invalid IfStmt"; break;
+ case 188: s = "invalid IfStmt"; break;
+ case 189: s = "invalid WhileStmt"; break;
+ case 190: s = "invalid WhileStmt"; break;
+ case 191: s = "invalid MatchStmt"; break;
+ case 192: s = "invalid ForallStmt"; break;
+ case 193: s = "invalid ForallStmt"; break;
+ case 194: s = "this symbol not expected in ModifyStmt"; break;
+ case 195: s = "invalid ModifyStmt"; break;
+ case 196: s = "invalid ReturnStmt"; break;
+ case 197: s = "invalid Rhs"; break;
+ case 198: s = "invalid Lhs"; break;
+ case 199: s = "invalid Guard"; break;
case 200: s = "this symbol not expected in LoopSpec"; break;
case 201: s = "this symbol not expected in LoopSpec"; break;
- case 202: s = "this symbol not expected in Invariant"; break;
- case 203: s = "invalid AttributeArg"; break;
- case 204: s = "invalid CalcOp"; break;
- case 205: s = "invalid EquivOp"; break;
- case 206: s = "invalid ImpliesOp"; break;
- case 207: s = "invalid ExpliesOp"; break;
- case 208: s = "invalid AndOp"; break;
- case 209: s = "invalid OrOp"; break;
- case 210: s = "invalid RelOp"; break;
- case 211: s = "invalid AddOp"; break;
- case 212: s = "invalid UnaryExpression"; break;
- case 213: s = "invalid UnaryExpression"; break;
- case 214: s = "invalid MulOp"; break;
- case 215: s = "invalid NegOp"; break;
- case 216: s = "invalid EndlessExpression"; break;
- case 217: s = "invalid Suffix"; break;
- case 218: s = "invalid Suffix"; break;
- case 219: s = "invalid Suffix"; break;
- case 220: s = "invalid DisplayExpr"; break;
- case 221: s = "invalid MultiSetExpr"; break;
- case 222: s = "invalid ConstAtomExpression"; break;
- case 223: s = "invalid Nat"; break;
- case 224: s = "invalid ParensExpression"; break;
- case 225: s = "invalid QSep"; break;
- case 226: s = "invalid MatchExpression"; break;
- case 227: s = "invalid QuantifierGuts"; break;
- case 228: s = "invalid StmtInExpr"; break;
- case 229: s = "invalid LetExpr"; break;
- case 230: s = "invalid CasePattern"; break;
- case 231: s = "invalid Forall"; break;
- case 232: s = "invalid Exists"; break;
+ case 202: s = "this symbol not expected in LoopSpec"; break;
+ case 203: s = "this symbol not expected in LoopSpec"; break;
+ case 204: s = "this symbol not expected in LoopSpec"; break;
+ case 205: s = "this symbol not expected in Invariant"; break;
+ case 206: s = "invalid AttributeArg"; break;
+ case 207: s = "invalid CalcOp"; break;
+ case 208: s = "invalid EquivOp"; break;
+ case 209: s = "invalid ImpliesOp"; break;
+ case 210: s = "invalid ExpliesOp"; break;
+ case 211: s = "invalid AndOp"; break;
+ case 212: s = "invalid OrOp"; break;
+ case 213: s = "invalid RelOp"; break;
+ case 214: s = "invalid AddOp"; break;
+ case 215: s = "invalid UnaryExpression"; break;
+ case 216: s = "invalid UnaryExpression"; break;
+ case 217: s = "invalid MulOp"; break;
+ case 218: s = "invalid NegOp"; break;
+ case 219: s = "invalid EndlessExpression"; break;
+ case 220: s = "invalid Suffix"; break;
+ case 221: s = "invalid Suffix"; break;
+ case 222: s = "invalid Suffix"; break;
+ case 223: s = "invalid DisplayExpr"; break;
+ case 224: s = "invalid MultiSetExpr"; break;
+ case 225: s = "invalid ConstAtomExpression"; break;
+ case 226: s = "invalid Nat"; break;
+ case 227: s = "invalid ParensExpression"; break;
+ case 228: s = "invalid QSep"; break;
+ case 229: s = "invalid MatchExpression"; break;
+ case 230: s = "invalid QuantifierGuts"; break;
+ case 231: s = "invalid StmtInExpr"; break;
+ case 232: s = "invalid LetExpr"; break;
+ case 233: s = "invalid CasePattern"; break;
+ case 234: s = "invalid Forall"; break;
+ case 235: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 1da5e7b2..6e10e7a1 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -264,7 +264,7 @@ namespace Microsoft.Dafny {
public void PrintClass(ClassDecl c, int indent) {
Contract.Requires(c != null);
Indent(indent);
- PrintClassMethodHelper("class", c.Attributes, c.Name, c.TypeArgs);
+ PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);
if (c.Members.Count == 0) {
wr.WriteLine(" { }");
} else {
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index d23aadc8..78784c0f 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -830,6 +830,90 @@ namespace Microsoft.Dafny
}
}
+ public void CheckOverride_FunctionParameters(Function nw, Function f)
+ {
+ CheckOverride_TypeParameters(nw.tok, f.TypeArgs, nw.TypeArgs, nw.Name, "function", false);
+ CheckOverrideResolvedParameters(nw.tok, f.Formals, nw.Formals, nw.Name, "function", "parameter");
+ if (!ResolvedTypesAreTheSame(nw.ResultType, f.ResultType))
+ {
+ reporter.Error(nw, "the result type of function '{0}' ({1}) differs from the result type of the corresponding function in the module it overrides ({2})", nw.Name, nw.ResultType, f.ResultType);
+ }
+ }
+
+ public void CheckOverride_MethodParameters(Method nw, Method f)
+ {
+ CheckOverride_TypeParameters(nw.tok, f.TypeArgs, nw.TypeArgs, nw.Name, "method", false);
+ CheckOverrideResolvedParameters(nw.tok, f.Ins, nw.Ins, nw.Name, "method", "in-parameter");
+ CheckOverrideResolvedParameters(nw.tok, f.Outs, nw.Outs, nw.Name, "method", "out-parameter");
+ }
+
+ public void CheckOverride_TypeParameters(IToken tok, List<TypeParameter> old, List<TypeParameter> nw, string name, string thing, bool checkNames = true)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(old != null);
+ Contract.Requires(nw != null);
+ Contract.Requires(name != null);
+ Contract.Requires(thing != null);
+ if (old.Count != nw.Count)
+ {
+ reporter.Error(tok, "{0} '{1}' is declared with a different number of type parameters ({2} instead of {3}) than the corresponding {0} in the module it overrides", thing, name, nw.Count, old.Count);
+ }
+ else
+ {
+ for (int i = 0; i < old.Count; i++)
+ {
+ var o = old[i];
+ var n = nw[i];
+ if (o.Name != n.Name && checkNames)
+ { // if checkNames is false, then just treat the parameters positionally.
+ reporter.Error(n.tok, "type parameters are not allowed to be renamed from the names given in the {0} in the module being overriden (expected '{1}', found '{2}')", thing, o.Name, n.Name);
+ }
+ else
+ {
+ // Here's how we actually compute it:
+ if (o.EqualitySupport != TypeParameter.EqualitySupportValue.InferredRequired && o.EqualitySupport != n.EqualitySupport)
+ {
+ reporter.Error(n.tok, "type parameter '{0}' is not allowed to change the requirement of supporting equality", n.Name);
+ }
+ }
+ }
+ }
+ }
+
+ public void CheckOverrideResolvedParameters(IToken tok, List<Formal> old, List<Formal> nw, string name, string thing, string parameterKind)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(old != null);
+ Contract.Requires(nw != null);
+ Contract.Requires(name != null);
+ Contract.Requires(thing != null);
+ Contract.Requires(parameterKind != null);
+ if (old.Count != nw.Count)
+ {
+ reporter.Error(tok, "{0} '{1}' is declared with a different number of {2} ({3} instead of {4}) than the corresponding {0} in the module it overrides", thing, name, parameterKind, nw.Count, old.Count);
+ }
+ else
+ {
+ for (int i = 0; i < old.Count; i++)
+ {
+ var o = old[i];
+ var n = nw[i];
+ if (!o.IsGhost && n.IsGhost)
+ {
+ reporter.Error(n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it overrides, from non-ghost to ghost", parameterKind, n.Name, thing, name);
+ }
+ else if (o.IsGhost && !n.IsGhost)
+ {
+ reporter.Error(n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it overrides, from ghost to non-ghost", parameterKind, n.Name, thing, name);
+ }
+ else if (!ResolvedTypesAreTheSame(o.Type, n.Type))
+ {
+ reporter.Error(n.tok, "the type of {0} '{1}' is different from the type of the same {0} in the corresponding {2} in the module it overrides ('{3}' instead of '{4}')", parameterKind, n.Name, thing, n.Type, o.Type);
+ }
+ }
+ }
+ }
+
void CheckAgreement_Parameters(IToken tok, List<Formal> old, List<Formal> nw, string name, string thing, string parameterKind) {
Contract.Requires(tok != null);
Contract.Requires(old != null);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 5e7381d9..d503076c 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -144,6 +144,7 @@ namespace Microsoft.Dafny
readonly Graph<ModuleDecl/*!*/>/*!*/ dependencies = new Graph<ModuleDecl/*!*/>();
private ModuleSignature systemNameInfo = null;
private bool useCompileSignatures = false;
+ private RefinementTransformer refinementTransformer = null;
public Resolver(Program prog) {
Contract.Requires(prog != null);
@@ -956,7 +957,11 @@ namespace Microsoft.Dafny
}
}
cl.HasConstructor = hasConstructor;
- if (cl.IsDefaultClass) {
+ if (cl is TraitDecl && cl.HasConstructor)
+ {
+ Error(cl, "a trait is not allowed to declare a constructor");
+ }
+ if (cl.IsDefaultClass) {
foreach (MemberDecl m in cl.Members) {
if (m.IsStatic && (m is Function || m is Method)) {
sig.StaticMembers[m.Name] = m;
@@ -1065,9 +1070,10 @@ namespace Microsoft.Dafny
var dd = (ClassDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var mm = dd.Members.ConvertAll(CloneMember);
+ List<IToken> trait = null;
if (dd is DefaultClassDecl) {
return new DefaultClassDecl(m, mm);
- } else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null);
+ } else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null,trait);
} else if (d is ModuleDecl) {
if (d is LiteralModuleDecl) {
return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m);
@@ -1469,6 +1475,10 @@ namespace Microsoft.Dafny
// Resolve the meat of classes and iterators, the definitions of type synonyms, and the type parameters of all top-level type declarations
foreach (TopLevelDecl d in declarations) {
Contract.Assert(d != null);
+ if (d is TraitDecl && d.TypeArgs != null && d.TypeArgs.Count > 0)
+ {
+ Error(d, "a trait can not declare type parameters");
+ }
allTypeParameters.PushMarker();
ResolveTypeParameters(d.TypeArgs, false, d);
if (!(d is IteratorDecl)) {
@@ -2758,6 +2768,7 @@ namespace Microsoft.Dafny
Contract.Ensures(currentClass == null);
currentClass = cl;
+ RefinementCloner cloner = new RefinementCloner(cl.Module);
foreach (MemberDecl member in cl.Members) {
member.EnclosingClass = cl;
if (member is Field) {
@@ -2801,6 +2812,157 @@ namespace Microsoft.Dafny
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type
}
}
+
+ //merging class members with parent members if any
+ if (cl.TraitId != null)
+ {
+ //resolving trait: making sure if the given qualifed name is a Trait
+ var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == cl.TraitId.val);
+ if (trait != null && trait is TraitDecl)
+ {
+ //disallowing inheritance in multi module case
+ string clModName = cl.Module.CompileName.Replace("_Compile", string.Empty);
+ string traitModName = trait.Module.CompileName.Replace("_Compile", string.Empty);
+ if (clModName != traitModName)
+ {
+ Error(cl, string.Format("class {0} is in a different module than trait {1}. A class may only extend a trait in the same module",
+ cl.FullName, trait.FullName));
+ }
+ else
+ {
+ cl.Trait = (TraitDecl)trait;
+ var traitMembers = classMembers[trait];
+ //merging current class members with the inheriting trait
+ foreach (KeyValuePair<string, MemberDecl> traitMem in traitMembers)
+ {
+ object clMember = cl.Members.FirstOrDefault(clMem => clMem.CompileName == traitMem.Key);
+ if (clMember != null)
+ {
+ //check if the signature of the members are equal and the member is body-less
+ if (traitMem.Value is Method)
+ {
+ Method traitMethod = (Method)traitMem.Value;
+ Method classMethod = (Method)clMember;
+ //refinementTransformer.CheckMethodsAreRefinements(classMethod, traitMethod);
+ if (traitMethod.Body != null && !classMembers[cl][classMethod.CompileName].Inherited) //if the existing method in the class is not that inherited one from the parent
+ Error(classMethod, "a class can not override implemented methods");
+ else
+ {
+ classMethod.OverriddenMethod = traitMethod;
+ //adding a call graph edge from the trait method to that of class
+ cl.Module.CallGraph.AddEdge(traitMethod, classMethod);
+
+ //checking specifications
+ //class method must provide its own specifications in case the overriden method has provided any
+ if ((classMethod.Req == null || classMethod.Req.Count == 0) && (classMethod.OverriddenMethod.Req != null && classMethod.OverriddenMethod.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req
+ {
+ Error(classMethod, "Method must provide its own Requires clauses anew");
+ }
+ if ((classMethod.Ens == null || classMethod.Ens.Count == 0) && (classMethod.OverriddenMethod.Ens != null && classMethod.OverriddenMethod.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens
+ {
+ Error(classMethod, "Method must provide its own Ensures clauses anew");
+ }
+ if ((classMethod.Mod == null || classMethod.Mod.Expressions == null || classMethod.Mod.Expressions.Count == 0) && (classMethod.OverriddenMethod.Mod != null && classMethod.OverriddenMethod.Mod.Expressions != null && classMethod.OverriddenMethod.Mod.Expressions.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod
+ {
+ Error(classMethod, "Method must provide its own Modifies clauses anew");
+ }
+ if ((classMethod.Decreases == null || classMethod.Decreases.Expressions == null || classMethod.Decreases.Expressions.Count == 0) && (classMethod.OverriddenMethod.Decreases != null && classMethod.OverriddenMethod.Decreases.Expressions != null && classMethod.OverriddenMethod.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases
+ {
+ Error(classMethod, "Method must provide its own Decreases clauses anew");
+ }
+ }
+ }
+ else if (traitMem.Value is Function)
+ {
+ Function traitFunction = (Function)traitMem.Value;
+ Function classFunction = (Function)clMember;
+ //refinementTransformer.CheckFunctionsAreRefinements(classFunction, traitFunction);
+ if (traitFunction.Body != null && !classMembers[cl][classFunction.CompileName].Inherited)
+ Error(classFunction, "a class can not override implemented functions");
+ else
+ {
+ classFunction.OverriddenFunction = traitFunction;
+ //adding a call graph edge from the trait method to that of class
+ cl.Module.CallGraph.AddEdge(traitFunction, classFunction);
+
+ //checking specifications
+ //class function must provide its own specifications in case the overriden function has provided any
+ if ((classFunction.Req == null || classFunction.Req.Count == 0) && (classFunction.OverriddenFunction.Req != null && classFunction.OverriddenFunction.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req
+ {
+ Error(classFunction, "Function must provide its own Requires clauses anew");
+ }
+ if ((classFunction.Ens == null || classFunction.Ens.Count == 0) && (classFunction.OverriddenFunction.Ens != null && classFunction.OverriddenFunction.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens
+ {
+ Error(classFunction, "Function must provide its own Ensures clauses anew");
+ }
+ if ((classFunction.Reads == null || classFunction.Reads.Count == 0) && (classFunction.OverriddenFunction.Reads != null && classFunction.OverriddenFunction.Reads.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod
+ {
+ Error(classFunction, "Function must provide its own Reads clauses anew");
+ }
+ if ((classFunction.Decreases == null || classFunction.Decreases.Expressions == null || classFunction.Decreases.Expressions.Count == 0) && (classFunction.OverriddenFunction.Decreases != null && classFunction.OverriddenFunction.Decreases.Expressions != null && classFunction.OverriddenFunction.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases
+ {
+ Error(classFunction, "Function must provide its own Decreases clauses anew");
+ }
+ }
+ }
+ else if (traitMem.Value is Field)
+ {
+ Field traitField = (Field)traitMem.Value;
+ Field classField = (Field)clMember;
+ if (!classMembers[cl][classField.CompileName].Inherited)
+ Error(classField, "member in the class has been already inherited from its parent trait");
+ }
+ }
+ else //the member is not already in the class
+ {
+ MemberDecl classNewMember = cloner.CloneMember(traitMem.Value);
+ classNewMember.EnclosingClass = cl;
+ classNewMember.Inherited = true;
+ classMembers[cl].Add(traitMem.Key, classNewMember);
+ cl.Members.Add(classNewMember);
+ //traitMem.Value.Inherited = true;
+ //classMembers[cl].Add(traitMem.Key, traitMem.Value);
+ //cl.Members.Add(traitMem.Value);
+ }
+ }//foreach
+
+ //checking to make sure all body-less methods/functions have been implemented in the child class
+ if (refinementTransformer == null)
+ refinementTransformer = new RefinementTransformer(this, AdditionalInformationReporter, null);
+ foreach (MemberDecl traitMember in trait.Members.Where(mem => mem is Function || mem is Method))
+ {
+ if (traitMember is Function)
+ {
+ Function traitFunc = (Function)traitMember;
+ var classMem = cl.Members.Where(clMem => clMem is Function).FirstOrDefault(clMem => ((Function)clMem).Body != null && clMem.CompileName == traitMember.CompileName);
+ if (classMem != null)
+ {
+ Function classFunc = (Function)classMem;
+ refinementTransformer.CheckOverride_FunctionParameters(classFunc, traitFunc);
+ }
+ else if (!cl.Module.IsAbstract && traitFunc.Body == null && classMem == null)
+ Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitFunc.CompileName);
+ }
+ if (traitMember is Method)
+ {
+ Method traitMethod = (Method)traitMember;
+
+ var classMem = cl.Members.Where(clMem => clMem is Method).FirstOrDefault(clMem => ((Method)clMem).Body != null && clMem.CompileName == traitMember.CompileName);
+ if (classMem != null)
+ {
+ Method classMethod = (Method)classMem;
+ refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod);
+ }
+ if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null)
+ Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName);
+ }
+ }
+ }
+ }
+ else
+ Error(cl, string.Format("unresolved identifier: {0}", cl.TraitId.val));
+ }
+
currentClass = null;
}
@@ -3933,7 +4095,16 @@ namespace Microsoft.Dafny
}
}
return successSoFar;
- } else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) {
+ }
+ else if ((bb.ResolvedClass is ClassDecl) && (aa.ResolvedClass is TraitDecl))
+ {
+ return ((ClassDecl)bb.ResolvedClass).Trait.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName;
+ }
+ else if ((aa.ResolvedClass is ClassDecl) && (bb.ResolvedClass is TraitDecl))
+ {
+ return ((ClassDecl)aa.ResolvedClass).Trait.FullCompileName == ((TraitDecl)bb.ResolvedClass).FullCompileName;
+ }
+ else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) {
// type parameters
if (aa.TypeArgs.Count != bb.TypeArgs.Count) {
return false;
@@ -5690,6 +5861,13 @@ namespace Microsoft.Dafny
// ---------- new C
Contract.Assert(rr.ArrayDimensions == null && rr.OptionalNameComponent == null && rr.InitCall == null);
}
+ if (rr.EType is UserDefinedType)
+ {
+ if (((UserDefinedType)rr.EType).ResolvedClass is TraitDecl)
+ {
+ Error(stmt, "new can not be applied to a trait");
+ }
+ }
if (!callsConstructor && rr.EType is UserDefinedType) {
var udt = (UserDefinedType)rr.EType;
var cl = (ClassDecl)udt.ResolvedClass; // cast is guaranteed by the call to rr.EType.IsRefType above, together with the "rr.EType is UserDefinedType" test
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 87dee5aa..ee65a927 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 126;
- const int noSym = 126;
+ const int maxT = 128;
+ const int noSym = 128;
[ContractInvariantMethod]
@@ -500,66 +500,68 @@ public class Scanner {
case "as": t.kind = 22; break;
case "default": t.kind = 23; break;
case "class": t.kind = 24; break;
- case "ghost": t.kind = 25; break;
- case "static": t.kind = 26; break;
- case "datatype": t.kind = 27; break;
- case "codatatype": t.kind = 28; break;
- case "var": t.kind = 30; break;
- case "type": t.kind = 32; break;
- case "iterator": t.kind = 34; break;
- case "yields": t.kind = 35; break;
- case "returns": t.kind = 36; break;
- case "method": t.kind = 40; break;
- case "lemma": t.kind = 41; break;
- case "colemma": t.kind = 42; break;
- case "comethod": t.kind = 43; break;
- case "constructor": t.kind = 44; break;
- case "modifies": t.kind = 45; break;
- case "free": t.kind = 46; break;
- case "requires": t.kind = 47; break;
- case "ensures": t.kind = 48; break;
- case "decreases": t.kind = 49; break;
- case "reads": t.kind = 50; break;
- case "yield": t.kind = 51; break;
- case "bool": t.kind = 52; break;
- case "nat": t.kind = 53; break;
- case "int": t.kind = 54; break;
- case "real": t.kind = 55; break;
- case "set": t.kind = 56; break;
- case "multiset": t.kind = 57; break;
- case "seq": t.kind = 58; break;
- case "map": t.kind = 59; break;
- case "object": t.kind = 60; break;
- case "function": t.kind = 62; break;
- case "predicate": t.kind = 63; break;
- case "copredicate": t.kind = 64; break;
- case "label": t.kind = 66; break;
- case "break": t.kind = 67; break;
- case "where": t.kind = 68; break;
- case "return": t.kind = 70; break;
- case "assume": t.kind = 72; break;
- case "new": t.kind = 73; break;
- case "if": t.kind = 76; break;
- case "else": t.kind = 77; break;
- case "case": t.kind = 78; break;
- case "while": t.kind = 80; break;
- case "invariant": t.kind = 81; break;
- case "match": t.kind = 82; break;
- case "assert": t.kind = 83; break;
- case "print": t.kind = 84; break;
- case "forall": t.kind = 85; break;
- case "parallel": t.kind = 86; break;
- case "modify": t.kind = 87; break;
- case "calc": t.kind = 88; break;
- case "in": t.kind = 106; break;
- case "false": t.kind = 113; break;
- case "true": t.kind = 114; break;
- case "null": t.kind = 115; break;
- case "this": t.kind = 116; break;
- case "fresh": t.kind = 117; break;
- case "old": t.kind = 118; break;
- case "then": t.kind = 119; break;
- case "exists": t.kind = 122; break;
+ case "extends": t.kind = 25; break;
+ case "trait": t.kind = 26; break;
+ case "ghost": t.kind = 27; break;
+ case "static": t.kind = 28; break;
+ case "datatype": t.kind = 29; break;
+ case "codatatype": t.kind = 30; break;
+ case "var": t.kind = 32; break;
+ case "type": t.kind = 34; break;
+ case "iterator": t.kind = 36; break;
+ case "yields": t.kind = 37; break;
+ case "returns": t.kind = 38; break;
+ case "method": t.kind = 42; break;
+ case "lemma": t.kind = 43; break;
+ case "colemma": t.kind = 44; break;
+ case "comethod": t.kind = 45; break;
+ case "constructor": t.kind = 46; break;
+ case "modifies": t.kind = 47; break;
+ case "free": t.kind = 48; break;
+ case "requires": t.kind = 49; break;
+ case "ensures": t.kind = 50; break;
+ case "decreases": t.kind = 51; break;
+ case "reads": t.kind = 52; break;
+ case "yield": t.kind = 53; break;
+ case "bool": t.kind = 54; break;
+ case "nat": t.kind = 55; break;
+ case "int": t.kind = 56; break;
+ case "real": t.kind = 57; break;
+ case "set": t.kind = 58; break;
+ case "multiset": t.kind = 59; break;
+ case "seq": t.kind = 60; break;
+ case "map": t.kind = 61; break;
+ case "object": t.kind = 62; break;
+ case "function": t.kind = 64; break;
+ case "predicate": t.kind = 65; break;
+ case "copredicate": t.kind = 66; break;
+ case "label": t.kind = 68; break;
+ case "break": t.kind = 69; break;
+ case "where": t.kind = 70; break;
+ case "return": t.kind = 72; break;
+ case "assume": t.kind = 74; break;
+ case "new": t.kind = 75; break;
+ case "if": t.kind = 78; break;
+ case "else": t.kind = 79; break;
+ case "case": t.kind = 80; break;
+ case "while": t.kind = 82; break;
+ case "invariant": t.kind = 83; break;
+ case "match": t.kind = 84; break;
+ case "assert": t.kind = 85; break;
+ case "print": t.kind = 86; break;
+ case "forall": t.kind = 87; break;
+ case "parallel": t.kind = 88; break;
+ case "modify": t.kind = 89; break;
+ case "calc": t.kind = 90; break;
+ case "in": t.kind = 108; break;
+ case "false": t.kind = 115; break;
+ case "true": t.kind = 116; break;
+ case "null": t.kind = 117; break;
+ case "this": t.kind = 118; break;
+ case "fresh": t.kind = 119; break;
+ case "old": t.kind = 120; break;
+ case "then": t.kind = 121; break;
+ case "exists": t.kind = 124; break;
default: break;
}
}
@@ -706,72 +708,72 @@ public class Scanner {
else if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;}
else {t.kind = 5; break;}
case 31:
- {t.kind = 31; break;}
+ {t.kind = 33; break;}
case 32:
- {t.kind = 37; break;}
+ {t.kind = 39; break;}
case 33:
- {t.kind = 65; break;}
+ {t.kind = 67; break;}
case 34:
- {t.kind = 69; break;}
- case 35:
{t.kind = 71; break;}
+ case 35:
+ {t.kind = 73; break;}
case 36:
- {t.kind = 74; break;}
+ {t.kind = 76; break;}
case 37:
- {t.kind = 75; break;}
+ {t.kind = 77; break;}
case 38:
- {t.kind = 79; break;}
+ {t.kind = 81; break;}
case 39:
- {t.kind = 89; break;}
- case 40:
{t.kind = 91; break;}
+ case 40:
+ {t.kind = 93; break;}
case 41:
- {t.kind = 92; break;}
+ {t.kind = 94; break;}
case 42:
- {t.kind = 93; break;}
+ {t.kind = 95; break;}
case 43:
- {t.kind = 94; break;}
+ {t.kind = 96; break;}
case 44:
- {t.kind = 95; break;}
+ {t.kind = 97; break;}
case 45:
- {t.kind = 96; break;}
+ {t.kind = 98; break;}
case 46:
- {t.kind = 97; break;}
+ {t.kind = 99; break;}
case 47:
- {t.kind = 98; break;}
+ {t.kind = 100; break;}
case 48:
- {t.kind = 99; break;}
- case 49:
{t.kind = 101; break;}
+ case 49:
+ {t.kind = 103; break;}
case 50:
if (ch == '&') {AddCh(); goto case 51;}
else {goto case 0;}
case 51:
- {t.kind = 102; break;}
+ {t.kind = 104; break;}
case 52:
- {t.kind = 103; break;}
+ {t.kind = 105; break;}
case 53:
- {t.kind = 104; break;}
+ {t.kind = 106; break;}
case 54:
- {t.kind = 105; break;}
+ {t.kind = 107; break;}
case 55:
- {t.kind = 108; break;}
+ {t.kind = 110; break;}
case 56:
- {t.kind = 109; break;}
+ {t.kind = 111; break;}
case 57:
- {t.kind = 110; break;}
+ {t.kind = 112; break;}
case 58:
- {t.kind = 111; break;}
+ {t.kind = 113; break;}
case 59:
- {t.kind = 112; break;}
+ {t.kind = 114; break;}
case 60:
- {t.kind = 121; break;}
- case 61:
{t.kind = 123; break;}
+ case 61:
+ {t.kind = 125; break;}
case 62:
- {t.kind = 124; break;}
+ {t.kind = 126; break;}
case 63:
- {t.kind = 125; break;}
+ {t.kind = 127; break;}
case 64:
recEnd = pos; recKind = 7;
if (ch == '=') {AddCh(); goto case 34;}
@@ -779,47 +781,47 @@ public class Scanner {
else if (ch == ':') {AddCh(); goto case 62;}
else {t.kind = 7; break;}
case 65:
- recEnd = pos; recKind = 107;
+ recEnd = pos; recKind = 109;
if (ch == 'i') {AddCh(); goto case 19;}
else if (ch == '=') {AddCh(); goto case 41;}
- else {t.kind = 107; break;}
+ else {t.kind = 109; break;}
case 66:
recEnd = pos; recKind = 21;
if (ch == '=') {AddCh(); goto case 71;}
else if (ch == '>') {AddCh(); goto case 38;}
else {t.kind = 21; break;}
case 67:
- recEnd = pos; recKind = 29;
+ recEnd = pos; recKind = 31;
if (ch == '|') {AddCh(); goto case 53;}
- else {t.kind = 29; break;}
+ else {t.kind = 31; break;}
case 68:
- recEnd = pos; recKind = 61;
+ recEnd = pos; recKind = 63;
if (ch == '.') {AddCh(); goto case 72;}
- else {t.kind = 61; break;}
+ else {t.kind = 63; break;}
case 69:
- recEnd = pos; recKind = 38;
+ recEnd = pos; recKind = 40;
if (ch == '=') {AddCh(); goto case 73;}
- else {t.kind = 38; break;}
+ else {t.kind = 40; break;}
case 70:
- recEnd = pos; recKind = 39;
+ recEnd = pos; recKind = 41;
if (ch == '=') {AddCh(); goto case 40;}
- else {t.kind = 39; break;}
+ else {t.kind = 41; break;}
case 71:
- recEnd = pos; recKind = 33;
+ recEnd = pos; recKind = 35;
if (ch == '>') {AddCh(); goto case 47;}
- else {t.kind = 33; break;}
+ else {t.kind = 35; break;}
case 72:
- recEnd = pos; recKind = 120;
+ recEnd = pos; recKind = 122;
if (ch == '.') {AddCh(); goto case 32;}
- else {t.kind = 120; break;}
+ else {t.kind = 122; break;}
case 73:
- recEnd = pos; recKind = 90;
+ recEnd = pos; recKind = 92;
if (ch == '=') {AddCh(); goto case 74;}
- else {t.kind = 90; break;}
+ else {t.kind = 92; break;}
case 74:
- recEnd = pos; recKind = 100;
+ recEnd = pos; recKind = 102;
if (ch == '>') {AddCh(); goto case 45;}
- else {t.kind = 100; break;}
+ else {t.kind = 102; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a936200e..585ebf85 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1086,7 +1086,18 @@ namespace Microsoft.Dafny {
if (c == program.BuiltIns.ObjectDecl) {
rhs = Bpl.Expr.True;
} else {
- rhs = BplOr(o_null, DType(o, o_ty));
+ //generating $o == null || implements$J(dtype(x))
+ if (c is TraitDecl)
+ {
+ var t = (TraitDecl)c;
+ var dtypeFunc = FunctionCall(o.tok, BuiltinFunction.DynamicType, null, o);
+ Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.Name, Bpl.Type.Bool, new List<Expr> { dtypeFunc });
+ rhs = BplOr(o_null, implementsFunc);
+ }
+ else
+ {
+ rhs = BplOr(o_null, DType(o, o_ty));
+ }
}
body = BplIff(is_o, rhs);
}
@@ -1094,6 +1105,31 @@ namespace Microsoft.Dafny {
sink.TopLevelDeclarations.Add(new Bpl.Axiom(c.tok, BplForall(vars, BplTrigger(is_o), body), name));
});
+ //this adds: function implements$J(ClassName): bool;
+ if (c is TraitDecl)
+ {
+ var arg_ref = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.Ty), true);
+ var res = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
+ var implement_intr = new Bpl.Function(c.tok, "implements$" + c.Name, new List<Variable> { arg_ref }, res);
+ sink.TopLevelDeclarations.Add(implement_intr);
+ }
+ //this adds: axiom implements$J(class.C);
+ else if (c is ClassDecl)
+ {
+ if (c.Trait != null)
+ {
+ //var dtypeFunc = FunctionCall(c.tok, BuiltinFunction.DynamicType, null, o);
+ //Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.Name, Bpl.Type.Bool, new List<Expr> { dtypeFunc });
+
+ var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
+ var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
+ var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "implements$" + c.TraitId.val, new List<Variable> { args }, ret_value));
+ var expr = new Bpl.NAryExpr(c.tok, funCall, new List<Expr> { new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType) });
+ var implements_axiom = new Bpl.Axiom(c.tok, expr);
+ sink.TopLevelDeclarations.Add(implements_axiom);
+ }
+ }
+
foreach (MemberDecl member in c.Members) {
currentDeclaration = member;
if (member is Field) {
@@ -1114,6 +1150,10 @@ namespace Microsoft.Dafny {
AddClassMember_Function(f);
if (!IsOpaqueFunction(f) && !f.IsBuiltin && !(f.tok is IncludeToken)) { // Opaque function's well-formedness is checked on the full version
AddWellformednessCheck(f);
+ if (f.OverriddenFunction != null) //it means that f is overriding its associated parent function
+ {
+ AddFunctionOverrideCheckImpl(f);
+ }
}
var cop = f as CoPredicate;
if (cop != null) {
@@ -1133,6 +1173,12 @@ namespace Microsoft.Dafny {
if (!(m.tok is IncludeToken)) {
AddMethodImpl(m, proc, true);
}
+ if (m.OverriddenMethod != null) //method has overrided a parent method
+ {
+ var procOverrideChk = AddMethod(m, MethodTranslationKind.OverrideCheck);
+ sink.TopLevelDeclarations.Add(procOverrideChk);
+ AddMethodOverrideCheckImpl(m, procOverrideChk);
+ }
}
// the method spec itself
sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.InterModuleCall));
@@ -2540,6 +2586,552 @@ namespace Microsoft.Dafny {
_tmpIEs.Clear();
}
+ private void AddFunctionOverrideCheckImpl(Function f)
+ {
+ Contract.Requires(f != null);
+ //Contract.Requires(proc != null);
+ Contract.Requires(sink != null && predef != null);
+ Contract.Requires(f.OverriddenFunction != null);
+ Contract.Requires(f.Formals.Count == f.OverriddenFunction.Formals.Count);
+ Contract.Requires(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
+ Contract.Ensures(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
+
+ #region first procedure, no impl yet
+ //Function nf = new Function(f.tok, "OverrideCheck_" + f.Name, f.IsStatic, f.IsGhost, f.TypeArgs, f.OpenParen, f.Formals, f.ResultType, f.Req, f.Reads, f.Ens, f.Decreases, f.Body, f.Attributes, f.SignatureEllipsis);
+ //AddFunction(f);
+ currentModule = f.EnclosingClass.Module;
+ codeContext = f;
+
+ ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
+ // parameters of the procedure
+ List<Variable> inParams = new List<Variable>();
+ if (!f.IsStatic)
+ {
+ Bpl.Expr wh = Bpl.Expr.And(
+ Bpl.Expr.Neq(new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), predef.Null),
+ etran.GoodRef(f.tok, new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), Resolver.GetReceiverType(f.tok, f)));
+ Bpl.Formal thVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType, wh), true);
+ inParams.Add(thVar);
+ }
+ foreach (Formal p in f.Formals)
+ {
+ Bpl.Type varType = TrType(p.Type);
+ Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(f), varType), p.Type, etran);
+ inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(f), varType, wh), true));
+ }
+ List<TypeVariable> typeParams = TrTypeParamDecls(f.TypeArgs);
+ // the procedure itself
+ var req = new List<Bpl.Requires>();
+ // free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
+ req.Add(Requires(f.tok, true, etran.HeightContext(f), null, null));
+ // modifies $Heap, $Tick
+ var mod = new List<Bpl.IdentifierExpr> { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr, etran.Tick() };
+ // check that postconditions hold
+ var ens = new List<Bpl.Ensures>();
+ foreach (Expression p in f.Ens)
+ {
+ var functionHeight = currentModule.CallGraph.GetSCCRepresentativeId(f);
+ var splits = new List<SplitExprInfo>();
+ bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight,false, etran);
+ foreach (var s in splits)
+ {
+ if (s.IsChecked && !RefinementToken.IsInherited(s.E.tok, currentModule))
+ {
+ ens.Add(Ensures(s.E.tok, false, s.E, null, null));
+ }
+ }
+ }
+ Bpl.Procedure proc = new Bpl.Procedure(f.tok, "OverrideCheck$$" + f.FullSanitizedName, typeParams, inParams, new List<Variable>(),
+ req, mod, ens, etran.TrAttributes(f.Attributes, null));
+ sink.TopLevelDeclarations.Add(proc);
+ var implInParams = Bpl.Formal.StripWhereClauses(inParams);
+
+ #endregion
+
+ //List<Variable> outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);
+
+ Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
+ List<Variable> localVariables = new List<Variable>();
+ //GenerateImplPrelude(m, wellformednessProc, inParams, outParams, builder, localVariables);
+
+ var substMap = new Dictionary<IVariable, Expression>();
+ for (int i = 0; i < f.Formals.Count; i++)
+ {
+ //get corresponsing formal in the class
+ var ie = new IdentifierExpr(f.Formals[i].tok, f.Formals[i].AssignUniqueName(f));
+ ie.Var = f.Formals[i]; ie.Type = ie.Var.Type;
+ substMap.Add(f.OverriddenFunction.Formals[i], ie);
+ }
+
+ Bpl.StmtList stmts;
+ //adding assume Pre’; assert P; // this checks that Pre’ implies P
+ AddFunctionOverrideReqsChk(f, builder, etran, substMap);
+
+ //adding assert R <= Rank’;
+ AddFunctionOverrideTerminationChk(f, builder, etran, substMap);
+
+ //adding assert W <= Frame’
+ AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap);
+
+ //change the heap at locations W
+ HavocFunctionFrameLocations(f, builder, etran, localVariables);
+
+ //adding assume Q; assert Post’;
+ AddFunctionOverrideEnsChk(f, builder, etran, substMap, implInParams);
+
+ //creating an axiom that conncets J.F and C.F
+ //which is a class function and overridden trait function
+ AddFunctionOverrideAxiom(f);
+
+ stmts = builder.Collect(f.tok);
+
+ QKeyValue kv = etran.TrAttributes(f.Attributes, null);
+
+ Bpl.Implementation impl = new Bpl.Implementation(f.tok, proc.Name, typeParams, implInParams, new List<Variable>(), localVariables, stmts, kv);
+ sink.TopLevelDeclarations.Add(impl);
+
+ if (InsertChecksums)
+ {
+ InsertChecksum(f, proc, true);
+ }
+
+ currentModule = null;
+ codeContext = null;
+ loopHeapVarCount = 0;
+ otherTmpVarCount = 0;
+ _tmpIEs.Clear();
+ }
+
+ private void AddFunctionOverrideAxiom(Function f)
+ {
+ Contract.Requires(f != null);
+ Contract.Requires(sink != null && predef != null);
+ // function override axiom
+ // axiom (forall $heap: HeapType, this: ref, x#0: int ::
+ // { J.F($heap, this, x#0) }
+ // this != null && dtype(this) == class.C
+ // ==>
+ // J.F($heap, this, x#0) == C.F($heap, this, x#0));
+
+ var formals = new List<Variable>();
+ var argsC = new List<Bpl.Expr>();
+ var argsT = new List<Bpl.Expr>();
+
+ var bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType));
+ var s = new Bpl.IdentifierExpr(f.tok, bv);
+ if (f.IsRecursive)
+ {
+ formals.Add(bv);
+ argsC.Add(FunctionCall(f.tok, BuiltinFunction.LayerSucc, null, s));
+ argsT.Add(FunctionCall(f.tok, BuiltinFunction.LayerSucc, null, s));
+ }
+
+ bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
+ formals.Add(bv);
+ s = new Bpl.IdentifierExpr(f.tok, bv);
+ argsC.Add(s);
+ argsT.Add(s);
+
+ if (!f.IsStatic)
+ {
+ bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
+ formals.Add(bv);
+ s = new Bpl.IdentifierExpr(f.tok, bv);
+ argsC.Add(s);
+ argsT.Add(s);
+ }
+ foreach (var p in f.Formals)
+ {
+ bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, f.FullSanitizedName + "_" + p.AssignUniqueName(f), TrType(p.Type)));
+ formals.Add(bv);
+ s = new Bpl.IdentifierExpr(f.tok, bv);
+ argsC.Add(s);
+ }
+ foreach (var p in f.OverriddenFunction.Formals)
+ {
+ bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, f.OverriddenFunction.FullSanitizedName + "_" + p.AssignUniqueName(f.OverriddenFunction), TrType(p.Type)));
+ formals.Add(bv);
+ s = new Bpl.IdentifierExpr(f.OverriddenFunction.tok, bv);
+ argsT.Add(s);
+ }
+
+ var funcIdC = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
+ var funcIdT = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.OverriddenFunction.tok, f.OverriddenFunction.FullSanitizedName, TrType(f.OverriddenFunction.ResultType)));
+ var funcApplC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
+ var funcApplT = new Bpl.NAryExpr(f.OverriddenFunction.tok, funcIdT, argsT);
+
+ var typeParams = TrTypeParamDecls(f.TypeArgs);
+
+ Bpl.Trigger tr = new Bpl.Trigger(f.OverriddenFunction.tok, true, new List<Bpl.Expr> { funcApplT, funcApplC });
+ Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Eq(funcApplC, funcApplT));
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax, "function override axiom"));
+ }
+
+ private void AddFunctionOverrideEnsChk(Function f, StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap, List<Variable> implInParams)
+ {
+ //generating class post-conditions
+ foreach (var en in f.Ens)
+ {
+ builder.Add(new Bpl.AssumeCmd(f.tok, etran.TrExpr(en)));
+ }
+
+ //generating assume J.F(ins) == C.F(ins)
+ Bpl.FunctionCall funcIdC = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
+ Bpl.FunctionCall funcIdT = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.OverriddenFunction.tok, f.OverriddenFunction.FullSanitizedName, TrType(f.OverriddenFunction.ResultType)));
+ List<Bpl.Expr> argsC = new List<Bpl.Expr>();
+ List<Bpl.Expr> argsT = new List<Bpl.Expr>();
+ if (f.IsRecursive)
+ {
+ argsC.Add(etran.LayerN(1));
+ }
+ if (f.OverriddenFunction.IsRecursive)
+ {
+ argsT.Add(etran.LayerN(1));
+ }
+ argsC.Add(etran.HeapExpr);
+ argsT.Add(etran.HeapExpr);
+ foreach (Variable p in implInParams)
+ {
+ argsC.Add(new Bpl.IdentifierExpr(f.tok, p));
+ argsT.Add(new Bpl.IdentifierExpr(f.OverriddenFunction.tok, p));
+ }
+ Bpl.Expr funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
+ Bpl.Expr funcExpT = new Bpl.NAryExpr(f.OverriddenFunction.tok, funcIdT, argsT);
+ builder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, funcExpT)));
+
+ //generating trait post-conditions with class variables
+ foreach (var en in f.OverriddenFunction.Ens)
+ {
+ Expression postcond = Substitute(en, null, substMap);
+ bool splitHappened;
+ var reqSplitedE = TrSplitExpr(postcond, etran,false, out splitHappened);
+ foreach (var s in reqSplitedE)
+ {
+ var assert = new Bpl.AssertCmd(f.tok, s.E);
+ assert.ErrorData = "Error: the function must provide an equal or more detailed postcondition than in its parent trait";
+ builder.Add(assert);
+ }
+ }
+ }
+
+ private void HavocFunctionFrameLocations(Function f, StmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables)
+ {
+ // play havoc with the heap according to the modifies clause
+ builder.Add(new Bpl.HavocCmd(f.tok, new List<Bpl.IdentifierExpr> { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr }));
+ // assume the usual two-state boilerplate information
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(f.tok, f.Reads, f.IsGhost, etran.Old, etran, etran.Old))
+ {
+ if (tri.IsFree)
+ {
+ builder.Add(new Bpl.AssumeCmd(f.tok, tri.Expr));
+ }
+ }
+ }
+
+ private void AddFunctionOverrideSubsetChk(Function func, StmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables, Dictionary<IVariable, Expression> substMap)
+ {
+ //getting framePrime
+ List<FrameExpression> traitFrameExps = new List<FrameExpression>();
+ foreach (var e in func.OverriddenFunction.Reads)
+ {
+ var newE = Substitute(e.E, null, substMap);
+ FrameExpression fe = new FrameExpression(e.tok, newE, e.FieldName);
+ traitFrameExps.Add(fe);
+ }
+
+ QKeyValue kv = etran.TrAttributes(func.Attributes, null);
+
+ IToken tok = func.tok;
+ // Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool
+ Bpl.IdentifierExpr traitFrame = etran.TheFrame(func.OverriddenFunction.tok); // this is a throw-away expression, used only to extract the type and name of the $_Frame variable
+ traitFrame.Name = func.EnclosingClass.Name + "_" + traitFrame.Name;
+ Contract.Assert(traitFrame.Type != null); // follows from the postcondition of TheFrame
+ Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, null ?? traitFrame.Name, traitFrame.Type));
+ localVariables.Add(frame);
+ // $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && $Heap[$o,alloc] ==> ($o,$f) in Modifies/Reads-Clause);
+ Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
+ Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
+ Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
+ Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));
+ Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar);
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o));
+ Bpl.Expr consequent = InRWClause(tok, o, f, traitFrameExps, etran, null, null);
+ Bpl.Expr lambda = new Bpl.LambdaExpr(tok, new List<TypeVariable> { alpha }, new List<Variable> { oVar, fVar }, null,
+ Bpl.Expr.Imp(ante, consequent));
+
+ //to initialize $_Frame variable to Frame'
+ builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda));
+
+ // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in subFrame ==> $_Frame[o,f]);
+ Bpl.Expr oInCallee = InRWClause(tok, o, f, func.Reads, etran, null, null);
+ Bpl.Expr consequent2 = InRWClause(tok, o, f, traitFrameExps, etran, null, null);
+ Bpl.Expr q = new Bpl.ForallExpr(tok, new List<TypeVariable> { alpha }, new List<Variable> { oVar, fVar },
+ Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), consequent2));
+ builder.Add(Assert(tok, q, "expression may read an object not in the parent trait context's reads clause", kv));
+ }
+
+ private void AddFunctionOverrideTerminationChk(Function f, StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap)
+ {
+ var decrToks = new List<IToken>();
+ var decrTypes1 = new List<Type>();
+ var decrTypes2 = new List<Type>();
+ var decrClass = new List<Expr>();
+ var decrTrait = new List<Expr>();
+ if (f.Decreases != null)
+ {
+ foreach (var decC in f.Decreases.Expressions)
+ {
+ decrToks.Add(decC.tok);
+ decrTypes1.Add(decC.Type);
+ decrClass.Add(etran.TrExpr(decC));
+ }
+ }
+ if (f.OverriddenFunction.Decreases != null)
+ {
+ foreach (var decT in f.OverriddenFunction.Decreases.Expressions)
+ {
+ var decCNew = Substitute(decT, null, substMap);
+ decrTypes2.Add(decCNew.Type);
+ decrTrait.Add(etran.TrExpr(decCNew));
+ }
+ }
+ var decrChk = DecreasesCheck(decrToks, decrTypes1, decrTypes2, decrClass, decrTrait, null, null, true, false);
+ builder.Add(new Bpl.AssertCmd(f.tok, decrChk));
+ }
+
+ private void AddFunctionOverrideReqsChk(Function f, StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap)
+ {
+ //generating trait pre-conditions with class variables
+ foreach (var req in f.OverriddenFunction.Req)
+ {
+ Expression precond = Substitute(req, null, substMap);
+ builder.Add(new Bpl.AssumeCmd(f.tok, etran.TrExpr(precond)));
+ }
+ //generating class pre-conditions
+ foreach (var req in f.Req)
+ {
+ bool splitHappened;
+ var reqSplitedE = TrSplitExpr(req, etran,false, out splitHappened);
+ foreach (var s in reqSplitedE)
+ {
+ var assert = new Bpl.AssertCmd(f.tok, s.E);
+ assert.ErrorData = "Error: the function must provide an equal or more permissive precondition than in its parent trait";
+ builder.Add(assert);
+ }
+ }
+ }
+
+ private void AddMethodOverrideCheckImpl(Method m, Bpl.Procedure proc)
+ {
+ Contract.Requires(m != null);
+ Contract.Requires(proc != null);
+ Contract.Requires(sink != null && predef != null);
+ Contract.Requires(m.OverriddenMethod != null);
+ Contract.Requires(m.Ins.Count == m.OverriddenMethod.Ins.Count);
+ Contract.Requires(m.Outs.Count == m.OverriddenMethod.Outs.Count);
+ //Contract.Requires(wellformednessProc || m.Body != null);
+ Contract.Requires(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
+ Contract.Ensures(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
+
+ currentModule = m.EnclosingClass.Module;
+ codeContext = m;
+
+ List<TypeVariable> typeParams = TrTypeParamDecls(m.TypeArgs);
+ List<Variable> inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
+ List<Variable> outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);
+
+ Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
+ ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
+ List<Variable> localVariables = new List<Variable>();
+ //GenerateImplPrelude(m, wellformednessProc, inParams, outParams, builder, localVariables);
+
+ var substMap = new Dictionary<IVariable, Expression>();
+ for (int i = 0; i < m.Ins.Count; i++)
+ {
+ //get corresponsing formal in the class
+ var ie = new IdentifierExpr(m.Ins[i].tok, m.Ins[i].AssignUniqueName(m));
+ ie.Var = m.Ins[i]; ie.Type = ie.Var.Type;
+ substMap.Add(m.OverriddenMethod.Ins[i], ie);
+ }
+ for (int i = 0; i < m.Outs.Count; i++)
+ {
+ //get corresponsing formal in the class
+ var ie = new IdentifierExpr(m.Outs[i].tok, m.Outs[i].AssignUniqueName(m));
+ ie.Var = m.Outs[i]; ie.Type = ie.Var.Type;
+ substMap.Add(m.OverriddenMethod.Outs[i], ie);
+ }
+
+ Bpl.StmtList stmts;
+ //adding assume Pre’; assert P; // this checks that Pre’ implies P
+ AddMethodOverrideReqsChk(m, builder, etran, substMap);
+
+ //adding assert R <= Rank’;
+ AddMethodOverrideTerminationChk(m, builder, etran, substMap);
+
+ //adding assert W <= Frame’
+ AddMethodOverrideSubsetChk(m, builder, etran, localVariables, substMap);
+
+ //change the heap at locations W
+ HavocMethodFrameLocations(m, builder, etran, localVariables);
+
+ //adding assume Q; assert Post’;
+ AddMethodOverrideEnsChk(m, builder, etran, substMap);
+
+ stmts = builder.Collect(m.tok);
+
+ QKeyValue kv = etran.TrAttributes(m.Attributes, null);
+
+ Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name, typeParams, inParams, outParams, localVariables, stmts, kv);
+ sink.TopLevelDeclarations.Add(impl);
+
+ if (InsertChecksums)
+ {
+ InsertChecksum(m, impl);
+ }
+
+ currentModule = null;
+ codeContext = null;
+ loopHeapVarCount = 0;
+ otherTmpVarCount = 0;
+ _tmpIEs.Clear();
+ }
+
+ private void HavocMethodFrameLocations(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables)
+ {
+ Contract.Requires(m != null);
+ Contract.Requires(m.EnclosingClass != null && m.EnclosingClass is ClassDecl);
+
+ // play havoc with the heap according to the modifies clause
+ builder.Add(new Bpl.HavocCmd(m.tok, new List<Bpl.IdentifierExpr> { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr }));
+ // assume the usual two-state boilerplate information
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, etran.Old, etran, etran.Old))
+ {
+ if (tri.IsFree)
+ {
+ builder.Add(new Bpl.AssumeCmd(m.tok, tri.Expr));
+ }
+ }
+ }
+
+ private void AddMethodOverrideEnsChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap)
+ {
+ //generating class post-conditions
+ foreach (var en in m.Ens)
+ {
+ builder.Add(new Bpl.AssumeCmd(m.tok, etran.TrExpr(en.E)));
+ }
+ //generating trait post-conditions with class variables
+ foreach (var en in m.OverriddenMethod.Ens)
+ {
+ Expression postcond = Substitute(en.E, null, substMap);
+ bool splitHappened;
+ var reqSplitedE = TrSplitExpr(postcond, etran,false, out splitHappened);
+ foreach (var s in reqSplitedE)
+ {
+ var assert = new Bpl.AssertCmd(m.tok, s.E);
+ assert.ErrorData = "Error: the method must provide an equal or more detailed postcondition than in its parent trait";
+ builder.Add(assert);
+ }
+ }
+ }
+
+ private void AddMethodOverrideReqsChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap)
+ {
+ //generating trait pre-conditions with class variables
+ foreach (var req in m.OverriddenMethod.Req)
+ {
+ Expression precond = Substitute(req.E, null, substMap);
+ builder.Add(new Bpl.AssumeCmd(m.tok, etran.TrExpr(precond)));
+ }
+ //generating class pre-conditions
+ foreach (var req in m.Req)
+ {
+ bool splitHappened;
+ var reqSplitedE = TrSplitExpr(req.E, etran,false, out splitHappened);
+ foreach (var s in reqSplitedE)
+ {
+ var assert = new Bpl.AssertCmd(m.tok, s.E);
+ assert.ErrorData = "Error: the method must provide an equal or more permissive precondition than in its parent trait";
+ builder.Add(assert);
+ }
+ }
+ }
+
+ private void AddMethodOverrideTerminationChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap)
+ {
+ var decrToks = new List<IToken>();
+ var decrTypes1 = new List<Type>();
+ var decrTypes2 = new List<Type>();
+ var decrClass = new List<Expr>();
+ var decrTrait = new List<Expr>();
+ if (m.Decreases != null)
+ {
+ foreach (var decC in m.Decreases.Expressions)
+ {
+ decrToks.Add(decC.tok);
+ decrTypes1.Add(decC.Type);
+ decrClass.Add(etran.TrExpr(decC));
+ }
+ }
+ if (m.OverriddenMethod.Decreases != null)
+ {
+ foreach (var decT in m.OverriddenMethod.Decreases.Expressions)
+ {
+ var decCNew = Substitute(decT, null, substMap);
+ decrTypes2.Add(decCNew.Type);
+ decrTrait.Add(etran.TrExpr(decCNew));
+ }
+ }
+ var decrChk = DecreasesCheck(decrToks, decrTypes1, decrTypes2, decrClass, decrTrait, null, null, true, false);
+ builder.Add(new Bpl.AssertCmd(m.tok, decrChk));
+ }
+
+ private void AddMethodOverrideSubsetChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables, Dictionary<IVariable, Expression> substMap)
+ {
+ //getting framePrime
+ List<FrameExpression> traitFrameExps = new List<FrameExpression>();
+ List<FrameExpression> classFrameExps = m.Mod != null ? m.Mod.Expressions : new List<FrameExpression>();
+ if (m.OverriddenMethod.Mod != null)
+ {
+ foreach (var e in m.OverriddenMethod.Mod.Expressions)
+ {
+ var newE = Substitute(e.E, null, substMap);
+ FrameExpression fe = new FrameExpression(e.tok, newE, e.FieldName);
+ traitFrameExps.Add(fe);
+ }
+ }
+
+ QKeyValue kv = etran.TrAttributes(m.Attributes, null);
+
+ IToken tok = m.tok;
+ // Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool
+ Bpl.IdentifierExpr traitFrame = etran.TheFrame(m.OverriddenMethod.tok); // this is a throw-away expression, used only to extract the type and name of the $_Frame variable
+ traitFrame.Name = m.EnclosingClass.Name + "_" + traitFrame.Name;
+ Contract.Assert(traitFrame.Type != null); // follows from the postcondition of TheFrame
+ Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, null ?? traitFrame.Name, traitFrame.Type));
+ localVariables.Add(frame);
+ // $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && $Heap[$o,alloc] ==> ($o,$f) in Modifies/Reads-Clause);
+ Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
+ Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
+ Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
+ Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));
+ Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar);
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o));
+ Bpl.Expr consequent = InRWClause(tok, o, f, traitFrameExps, etran, null, null);
+ Bpl.Expr lambda = new Bpl.LambdaExpr(tok, new List<TypeVariable> { alpha }, new List<Variable> { oVar, fVar }, null,
+ Bpl.Expr.Imp(ante, consequent));
+
+ //to initialize $_Frame variable to Frame'
+ builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda));
+
+ // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in subFrame ==> $_Frame[o,f]);
+ Bpl.Expr oInCallee = InRWClause(tok, o, f, classFrameExps, etran, null, null);
+ Bpl.Expr consequent2 = InRWClause(tok, o, f, traitFrameExps, etran, null, null);
+ Bpl.Expr q = new Bpl.ForallExpr(tok, new List<TypeVariable> { alpha }, new List<Variable> { oVar, fVar },
+ Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), consequent2));
+ builder.Add(Assert(tok, q, "expression may modify an object not in the parent trait context's modifies clause", kv));
+ }
+
private void InsertChecksum(Method m, Bpl.Declaration decl, bool specificationOnly = false)
{
byte[] data;
@@ -4341,7 +4933,7 @@ namespace Microsoft.Dafny {
/// Note that SpecWellformedness and Implementation have procedure implementations
/// but no callers, and vice versa for InterModuleCall, IntraModuleCall, and CoCall.
/// </summary>
- enum MethodTranslationKind { SpecWellformedness, InterModuleCall, IntraModuleCall, CoCall, Implementation }
+ enum MethodTranslationKind { SpecWellformedness, InterModuleCall, IntraModuleCall, CoCall, Implementation, OverrideCheck }
/// <summary>
/// This method is expected to be called at most once for each parameter combination, and in particular
@@ -4368,7 +4960,7 @@ namespace Microsoft.Dafny {
var mod = new List<Bpl.IdentifierExpr>();
var ens = new List<Bpl.Ensures>();
// FREE PRECONDITIONS
- if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation) { // the other cases have no need for a free precondition
+ if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation || kind== MethodTranslationKind.OverrideCheck) { // the other cases have no need for a free precondition
// free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
req.Add(Requires(m.tok, true, etran.HeightContext(m), null, null));
}
@@ -4377,7 +4969,8 @@ namespace Microsoft.Dafny {
var bodyKind = kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation;
- if (kind != MethodTranslationKind.SpecWellformedness) {
+ if (kind != MethodTranslationKind.SpecWellformedness && kind != MethodTranslationKind.OverrideCheck)
+ {
// USER-DEFINED SPECIFICATIONS
var comment = "user-defined preconditions";
foreach (var p in m.Req) {
@@ -4458,6 +5051,8 @@ namespace Microsoft.Dafny {
return "CoCall$$" + m.FullSanitizedName;
case MethodTranslationKind.Implementation:
return "Impl$$" + m.FullSanitizedName;
+ case MethodTranslationKind.OverrideCheck:
+ return "OverrideCheck$$" + m.FullSanitizedName;
default:
Contract.Assert(false); // unexpected kind
throw new cce.UnreachableException();
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index e3e29c58..cb645d2f 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -39,6 +39,8 @@ namespace Microsoft.Dafny
exitValue = ExitValue.PREPROCESSING_ERROR;
goto END;
}
+ //CommandLineOptions.Clo.Files = new List<string> { @"C:\dafny\Test\dafny0\Trait\TraitOverride1.dfy" };
+
if (CommandLineOptions.Clo.Files.Count == 0)
{
printer.ErrorWriteLine(Console.Out, "*** Error: No input files were specified.");
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index 5068354a..438d9be6 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -284,6 +284,8 @@ namespace DafnyLanguage
case "calc":
case "case":
case "class":
+ case "trait":
+ case "extends":
case "codatatype":
case "colemma":
case "constructor":
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 01:56:17 +0000