diff options
37 files changed, 2639 insertions, 897 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":
diff --git a/Test/dafny0/Trait/Trait.dfy b/Test/dafny0/Trait/Trait.dfy new file mode 100644 index 00000000..cf76e860 --- /dev/null +++ b/Test/dafny0/Trait/Trait.dfy @@ -0,0 +1,95 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module m1
+{
+ trait I1
+ {
+ function M1(x:int,y:int) :int
+ {
+ x*y
+ }
+ }
+
+
+ trait I2 //all is fine in this trait
+ {
+ var x: int;
+
+ function method Twice(): int
+ reads this;
+ {
+ x + x
+ }
+
+ function method F(z: int): int
+ reads this;
+
+
+ method Compute(s: bool) returns (t: int, u: int)
+ modifies this;
+ {
+ if s {
+ t, u := F(F(15)), Twice();
+ } else {
+ t := Twice();
+ x := F(45);
+ u := Twice();
+ var p := Customizable(u);
+ return t+p, u;
+ }
+ }
+
+ method Customizable(w: int) returns (p: int)
+ modifies this;
+
+
+ static method StaticM(a: int) returns (b: int)
+ {
+ b := a;
+ }
+
+ static method SS(a: int) returns (b:int)
+ {
+ b:=a*2;
+ }
+ }
+
+ method I2Client(j: I2) returns (p: int) //all is fine in this client method
+ requires j != null;
+ modifies j;
+ {
+ j.x := 100;
+ var h := j.Twice() + j.F(j.Twice());
+ var a, b := j.Compute(h < 33);
+ var c, d := j.Compute(33 <= h);
+ p := j.Customizable(a + b + c + d);
+ p := I2.StaticM(p);
+ }
+
+ class I0Child extends I2 //errors, body-less methods/functions in the parent have not implemented here
+ {
+ function method F(z: int): int
+ reads this;
+ {
+ z
+ }
+ var x: int; //error, x has been declared in the parent trait
+ }
+
+ class I0Child2 extends I2
+ {
+ method Customizable(w: int) returns (p: int)
+ modifies this;
+ {
+ w:=w+1;
+ }
+
+ var c1: I0Child;
+ }
+
+ class IXChild extends IX //error, IX trait is undefined
+ {
+
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/Trait.dfy.expect b/Test/dafny0/Trait/Trait.dfy.expect new file mode 100644 index 00000000..253144ea --- /dev/null +++ b/Test/dafny0/Trait/Trait.dfy.expect @@ -0,0 +1,5 @@ +Trait.dfy(77,13): Error: member in the class has been already inherited from its parent trait
+Trait.dfy(70,7): Error: class: I0Child does not implement trait member: Customizable
+Trait.dfy(80,7): Error: class: I0Child2 does not implement trait member: F
+Trait.dfy(91,7): Error: unresolved identifier: IX
+4 resolution/type errors detected in Trait.dfy
diff --git a/Test/dafny0/Trait/TraitBasics.dfy b/Test/dafny0/Trait/TraitBasics.dfy new file mode 100644 index 00000000..6bfe76bb --- /dev/null +++ b/Test/dafny0/Trait/TraitBasics.dfy @@ -0,0 +1,79 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait I0
+{
+ var x: int;
+ constructor I0(x0: int) // error: constructor is not allowed in a trait
+ {
+ x:=x0;
+ }
+}
+
+trait I1
+{
+ function M1(x:int,y:int) :int
+ {
+ x*y
+ }
+}
+
+method TestI1()
+{
+ var i1 := new I1; //error: new is not allowed in a trait
+}
+
+trait I2 //all is fine in this trait
+{
+ var x: int;
+
+ function method Twice(): int
+ reads this;
+ {
+ x + x
+ }
+
+ function method F(z: int): int
+ reads this;
+
+
+ method Compute(s: bool) returns (t: int, u: int)
+ modifies this;
+ {
+ if s {
+ t, u := F(F(15)), Twice();
+ } else {
+ t := Twice();
+ x := F(45);
+ u := Twice();
+ var p := Customizable(u);
+ return t+p, u;
+ }
+ }
+
+ method Customizable(w: int) returns (p: int)
+ modifies this;
+
+
+ static method StaticM(a: int) returns (b: int)
+ {
+ b := a;
+ }
+
+ static method SS(a: int) returns (b:int)
+ {
+ b:=a*2;
+ }
+}
+
+method I2Client(j: I2) returns (p: int) //all is fine in this client method
+ requires j != null;
+ modifies j;
+{
+ j.x := 100;
+ var h := j.Twice() + j.F(j.Twice());
+ var a, b := j.Compute(h < 33);
+ var c, d := j.Compute(33 <= h);
+ p := j.Customizable(a + b + c + d);
+ p := I2.StaticM(p);
+}
diff --git a/Test/dafny0/Trait/TraitBasics.dfy.expect b/Test/dafny0/Trait/TraitBasics.dfy.expect new file mode 100644 index 00000000..c9fb096e --- /dev/null +++ b/Test/dafny0/Trait/TraitBasics.dfy.expect @@ -0,0 +1,3 @@ +TraitBasics.dfy(4,6): Error: a trait is not allowed to declare a constructor
+TraitBasics.dfy(23,10): Error: new can not be applied to a trait
+2 resolution/type errors detected in TraitBasics.dfy
diff --git a/Test/dafny0/Trait/TraitExtend.dfy b/Test/dafny0/Trait/TraitExtend.dfy new file mode 100644 index 00000000..1a59439c --- /dev/null +++ b/Test/dafny0/Trait/TraitExtend.dfy @@ -0,0 +1,43 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait t
+{
+ var f: int;
+
+ function method Plus (x:int, y:int) : int
+ requires x>y;
+ {
+ x + y
+ }
+
+ function method Mul (x:int, y:int, z:int) : int
+ requires x>y;
+ {
+ x * y * z
+ }
+
+ //function method BodyLess1() : int
+
+ static method GetPhoneNumber (code:int, n:int) returns (z:int)
+ {
+ z := code + n;
+ }
+
+ method TestPhone ()
+ {
+ var num : int;
+ num := GetPhoneNumber (10, 30028);
+ }
+}
+
+class c1 extends t
+{
+ method P2(x:int, y:int) returns (z:int)
+ requires x>y;
+ {
+ z:= Plus(x,y) + Mul (x,y,1);
+ var j:int := Mul (x,y); //error, too few parameters in calling inherited method
+ var k:int := Plus(x,y,1); //error, too many parameters in calling inherited method
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitExtend.dfy.expect b/Test/dafny0/Trait/TraitExtend.dfy.expect new file mode 100644 index 00000000..73a24ad8 --- /dev/null +++ b/Test/dafny0/Trait/TraitExtend.dfy.expect @@ -0,0 +1,3 @@ +TraitExtend.dfy(40,20): Error: wrong number of function arguments (got 2, expected 3)
+TraitExtend.dfy(41,20): Error: wrong number of function arguments (got 3, expected 2)
+2 resolution/type errors detected in TraitExtend.dfy
diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy b/Test/dafny0/Trait/TraitMultiModule.dfy new file mode 100644 index 00000000..f60db7b4 --- /dev/null +++ b/Test/dafny0/Trait/TraitMultiModule.dfy @@ -0,0 +1,26 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module M1
+{
+ trait T1
+ {
+ method M1 (a:int)
+ }
+ class C1 extends T1
+ {
+ method M1 (x:int)
+ {
+ var y: int := x;
+ }
+ }
+}
+
+module M2
+{
+ class C2 extends T1
+ {
+
+ }
+
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy.expect b/Test/dafny0/Trait/TraitMultiModule.dfy.expect new file mode 100644 index 00000000..589fba07 --- /dev/null +++ b/Test/dafny0/Trait/TraitMultiModule.dfy.expect @@ -0,0 +1,2 @@ +TraitMultiModule.dfy(21,9): Error: class M2.C2 is in a different module than trait M1.T1. A class may only extend a trait in the same module
+1 resolution/type errors detected in TraitMultiModule.dfy
diff --git a/Test/dafny0/Trait/TraitOverride0.dfy b/Test/dafny0/Trait/TraitOverride0.dfy new file mode 100644 index 00000000..a8fb8596 --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride0.dfy @@ -0,0 +1,81 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T1
+{
+ var f: int;
+
+ function method Plus (x:int, y:int) : int
+ requires x>y;
+ {
+ x + y
+ }
+
+ function method Mul (x:int, y:int, z:int) : int
+ requires x>y;
+ {
+ x * y * z
+ }
+
+ function method BodyLess1() : int
+
+ function method BodyLess2(a:int, b:int) : int
+
+ static method GetPhoneNumber (code:int, n:int) returns (z:int)
+ {
+ z := code + n;
+ }
+
+ method TestPhone ()
+ {
+ var num : int;
+ num := GetPhoneNumber (10, 30028);
+ }
+}
+
+trait T2
+{
+}
+
+class C1 extends T1
+{
+ method P2(x:int, y:int) returns (z:int)
+ requires x>y;
+ {
+ z:= Plus(x,y) + Mul (x,y,1);
+ }
+
+ function method BodyLess1(i:int) : int //error, overriding function has too many parameters
+ {
+ 12
+ }
+
+ function method Mul (x:int, y:int, z:int) : int //error, can not override implemented methods
+ requires x>y;
+ {
+ x * y * z
+ }
+
+ function method BodyLess2(a:int, b:int) : int
+ {
+ a+b
+ }
+}
+
+class C2 extends T1
+{
+ //error, there are body-less methods in the parent trait that must be implemented
+}
+
+abstract module AM1
+{
+ trait T2
+ {
+ method Calc(i:int, j:int) returns (k:int)
+ }
+
+ class T2Client extends T2
+ {
+ method Calc(ii:int, jj:int) returns (kk:int)
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitOverride0.dfy.expect b/Test/dafny0/Trait/TraitOverride0.dfy.expect new file mode 100644 index 00000000..4020b880 --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride0.dfy.expect @@ -0,0 +1,5 @@ +TraitOverride0.dfy(53,20): Error: a class can not override implemented functions
+TraitOverride0.dfy(48,20): Error: function 'BodyLess1' is declared with a different number of parameter (1 instead of 0) than the corresponding function in the module it overrides
+TraitOverride0.dfy(65,6): Error: class: C2 does not implement trait member: BodyLess1
+TraitOverride0.dfy(65,6): Error: class: C2 does not implement trait member: BodyLess2
+4 resolution/type errors detected in TraitOverride0.dfy
diff --git a/Test/dafny0/Trait/TraitOverride1.dfy b/Test/dafny0/Trait/TraitOverride1.dfy new file mode 100644 index 00000000..980054ee --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride1.dfy @@ -0,0 +1,54 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T1
+{
+ function method Plus (x:int, y:int) : int
+ requires x>y;
+ {
+ x + y
+ }
+
+ function method bb(x:int):int
+ requires x>10;
+
+ function method BodyLess1(a:int) : int
+ requires a > 0;
+
+ function method dd(a:int) : int
+
+ method Testing()
+}
+
+class C1 extends T1
+{
+ function method dd(x:int):int
+ {
+ 2
+ }
+
+ method Testing()
+ {
+ var x:int := 11;
+ x := bb(x);
+ }
+
+ function method bb(x:int):int
+ requires x >10;
+ {
+ x
+ }
+ function method BodyLess1(bda:int) : int
+ requires bda > (-10);
+ {
+ 2
+ }
+
+ method CallBodyLess(x:int)
+ requires x > (-10);
+ {
+ var k:int := BodyLess1(x);
+ assert (k==2);
+ }
+}
+
diff --git a/Test/dafny0/Trait/TraitOverride1.dfy.expect b/Test/dafny0/Trait/TraitOverride1.dfy.expect new file mode 100644 index 00000000..5f41963f --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride1.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 17 verified, 0 errors
diff --git a/Test/dafny0/Trait/TraitOverride2.dfy b/Test/dafny0/Trait/TraitOverride2.dfy new file mode 100644 index 00000000..fca79b2e --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride2.dfy @@ -0,0 +1,30 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait J
+{
+ function method F(x: int): int
+ requires x < 100;
+ ensures F(x) < 100;
+
+ method M(x: int) returns (y: int)
+ requires 0 <= x;
+ ensures x < y;
+}
+
+class C extends J
+{
+ function method F(x: int): int
+ requires x < 100;
+ ensures F(x) < 100;
+ {
+ x
+ }
+
+ method M(x: int) returns (y: int)
+ requires -2000 <= x; // a more permissive precondition than in the interface
+ ensures 2*x < y; // a more detailed postcondition than in the interface
+ {
+ y := (2 * x) + 1;
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitOverride2.dfy.expect b/Test/dafny0/Trait/TraitOverride2.dfy.expect new file mode 100644 index 00000000..76f19e0d --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride2.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 7 verified, 0 errors
diff --git a/Test/dafny0/Trait/TraitOverride3.dfy b/Test/dafny0/Trait/TraitOverride3.dfy new file mode 100644 index 00000000..498a0a6b --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride3.dfy @@ -0,0 +1,28 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+//related compiler changes
+//everything works OK in the following code
+trait J
+{
+ function method F(y: int): int
+ function method G(y: int): int { 12 }
+ method M(y: int)
+ method N(y: int) {
+ var a:int := 100;
+ assert a==100;
+ }
+}
+class C extends J
+{
+ function method NewFunc (a:int, b:int) : int
+ {
+ a + b
+ }
+ function method F(y: int): int { 20 }
+ method M(y: int) {
+ var a:int := 100;
+ assert a==100;
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitOverride3.dfy.expect b/Test/dafny0/Trait/TraitOverride3.dfy.expect new file mode 100644 index 00000000..f5019f3b --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride3.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 14 verified, 0 errors
diff --git a/Test/dafny0/Trait/TraitOverride4.dfy b/Test/dafny0/Trait/TraitOverride4.dfy new file mode 100644 index 00000000..c9cc3953 --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride4.dfy @@ -0,0 +1,41 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+trait J
+{
+ function method F(y: int): int
+
+ function method G(y: int): int
+ {
+ 100
+ }
+
+ method M(y: int) returns (kobra:int)
+ requires y > 0;
+ ensures kobra > 0;
+
+ method N(y: int)
+ {
+ var x: int;
+ var y : int;
+ y := 10;
+ x := 1000;
+ y := y + x;
+ }
+}
+
+class C extends J
+{
+ function method F(y: int): int
+ {
+ 200
+ }
+
+ method M(kk:int) returns (ksos:int)
+ requires kk > (-1);
+ ensures ksos > 0;
+ {
+ ksos:=10;
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitOverride4.dfy.expect b/Test/dafny0/Trait/TraitOverride4.dfy.expect new file mode 100644 index 00000000..aeb37948 --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride4.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 13 verified, 0 errors
diff --git a/Test/dafny0/Trait/TraitPolymorphism.dfy b/Test/dafny0/Trait/TraitPolymorphism.dfy new file mode 100644 index 00000000..b1ee9eea --- /dev/null +++ b/Test/dafny0/Trait/TraitPolymorphism.dfy @@ -0,0 +1,65 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T1
+{
+ var f: int;
+
+ function method Plus (x:int, y:int) : int
+ requires x>y;
+ {
+ x + y
+ }
+
+ function method Mul (x:int, y:int, z:int) : int
+ requires x>y;
+ {
+ x * y * z
+ }
+
+ //function method BodyLess1() : int
+
+ static method GetPhoneNumber (code:int, n:int) returns (z:int)
+ {
+ z := code + n;
+ }
+
+ method TestPhone ()
+ {
+ var num : int;
+ num := GetPhoneNumber (10, 30028);
+ }
+}
+
+trait T2
+{
+}
+
+class C1 extends T1
+{
+ method P2(x:int, y:int) returns (z:int)
+ requires x>y;
+ {
+ z:= Plus(x,y) + Mul (x,y,1);
+ }
+}
+
+
+
+method Good(c: C1) returns (t: T1)
+ensures c == t;
+{
+ t := c;
+}
+
+method Bad1(c: C1) returns (t: T2)
+ensures c == t;
+{
+ t := c; //error, C1 has not implemented T2
+}
+
+method Bad2(c: C1) returns (t: T1)
+ensures c == t;
+{
+ c := t; //error, can not assign a trait to a class
+}
diff --git a/Test/dafny0/Trait/TraitPolymorphism.dfy.expect b/Test/dafny0/Trait/TraitPolymorphism.dfy.expect new file mode 100644 index 00000000..8c68b4b9 --- /dev/null +++ b/Test/dafny0/Trait/TraitPolymorphism.dfy.expect @@ -0,0 +1,4 @@ +TraitPolymorphism.dfy(56,10): Error: arguments must have the same type (got C1 and T2)
+TraitPolymorphism.dfy(58,6): Error: RHS (of type C1) not assignable to LHS (of type T2)
+TraitPolymorphism.dfy(64,4): Error: LHS of assignment must denote a mutable variable
+3 resolution/type errors detected in TraitPolymorphism.dfy
diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy b/Test/dafny0/Trait/TraitSpecsOverride0.dfy new file mode 100644 index 00000000..5b4417c3 --- /dev/null +++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy @@ -0,0 +1,41 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+trait J
+{
+ function method F(k:int, y: array<int>): int
+ reads y;
+ decreases k;
+
+ function method G(y: int): int
+ {
+ 100
+ }
+
+ method M(y: int) returns (kobra:int)
+ requires y > 0;
+ ensures kobra > 0;
+
+ method N(y: int)
+ {
+ var x: int;
+ var y : int;
+ y := 10;
+ x := 1000;
+ y := y + x;
+ }
+}
+
+class C extends J
+{
+ function method F(kk:int, yy: array<int>): int
+ {
+ 200
+ }
+
+ method M(kk:int) returns (ksos:int) //errors here, M must provide its own specifications
+ {
+ ksos:=10;
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect new file mode 100644 index 00000000..cbdcdf05 --- /dev/null +++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect @@ -0,0 +1,5 @@ +TraitSpecsOverride0.dfy(32,17): Error: Function must provide its own Reads clauses anew
+TraitSpecsOverride0.dfy(32,17): Error: Function must provide its own Decreases clauses anew
+TraitSpecsOverride0.dfy(37,8): Error: Method must provide its own Requires clauses anew
+TraitSpecsOverride0.dfy(37,8): Error: Method must provide its own Ensures clauses anew
+4 resolution/type errors detected in TraitSpecsOverride0.dfy
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 6c59c50a..d589fb78 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -31,6 +31,7 @@ `(,(dafny-regexp-opt '(
"class" "datatype" "codatatype" "type" "iterator"
+ "trait" "extends"
"function" "predicate" "copredicate"
"ghost" "var" "method" "lemma" "constructor" "colemma"
"abstract" "module" "import" "default" "as" "opened" "static" "refines"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 785cf6f1..40b994ba 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -5,7 +5,7 @@ \usepackage{listings}
\lstdefinelanguage{dafny}{
- morekeywords={class,datatype,codatatype,type,iterator,
+ morekeywords={class,datatype,codatatype,type,iterator,trait,extends,
bool,nat,int,real,object,set,multiset,seq,array,array2,array3,map,
function,predicate,copredicate,
ghost,var,static,refines,
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim index c706ac5f..58820c0f 100644 --- a/Util/vim/dafny.vim +++ b/Util/vim/dafny.vim @@ -7,7 +7,7 @@ syntax clear syntax case match syntax keyword dafnyFunction function predicate copredicate syntax keyword dafnyMethod method lemma constructor colemma -syntax keyword dafnyTypeDef class datatype codatatype type iterator +syntax keyword dafnyTypeDef class datatype codatatype type iterator trait extends syntax keyword dafnyModule abstract module import opened as default syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat while |