From 77143c833cbb14a20c704fb60fc28dd94edb44eb Mon Sep 17 00:00:00 2001 From: Reza Ahmadi Date: Fri, 18 Jul 2014 21:16:40 +0300 Subject: added trait feature: -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods --- Source/Dafny/Cloner.cs | 40 +- Source/Dafny/Compiler.cs | 306 +++-- Source/Dafny/Dafny.atg | 40 +- Source/Dafny/DafnyAst.cs | 26 +- Source/Dafny/Parser.cs | 1398 +++++++++++----------- Source/Dafny/Printer.cs | 2 +- Source/Dafny/RefinementTransformer.cs | 84 ++ Source/Dafny/Resolver.cs | 184 ++- Source/Dafny/Scanner.cs | 226 ++-- Source/Dafny/Translator.cs | 603 +++++++++- Source/DafnyDriver/DafnyDriver.cs | 2 + Source/DafnyExtension/TokenTagger.cs | 2 + Test/dafny0/Trait/Trait.dfy | 95 ++ Test/dafny0/Trait/Trait.dfy.expect | 5 + Test/dafny0/Trait/TraitBasics.dfy | 79 ++ Test/dafny0/Trait/TraitBasics.dfy.expect | 3 + Test/dafny0/Trait/TraitExtend.dfy | 43 + Test/dafny0/Trait/TraitExtend.dfy.expect | 3 + Test/dafny0/Trait/TraitMultiModule.dfy | 26 + Test/dafny0/Trait/TraitMultiModule.dfy.expect | 2 + Test/dafny0/Trait/TraitOverride0.dfy | 81 ++ Test/dafny0/Trait/TraitOverride0.dfy.expect | 5 + Test/dafny0/Trait/TraitOverride1.dfy | 54 + Test/dafny0/Trait/TraitOverride1.dfy.expect | 2 + Test/dafny0/Trait/TraitOverride2.dfy | 30 + Test/dafny0/Trait/TraitOverride2.dfy.expect | 2 + Test/dafny0/Trait/TraitOverride3.dfy | 28 + Test/dafny0/Trait/TraitOverride3.dfy.expect | 2 + Test/dafny0/Trait/TraitOverride4.dfy | 41 + Test/dafny0/Trait/TraitOverride4.dfy.expect | 2 + Test/dafny0/Trait/TraitPolymorphism.dfy | 65 + Test/dafny0/Trait/TraitPolymorphism.dfy.expect | 4 + Test/dafny0/Trait/TraitSpecsOverride0.dfy | 41 + Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect | 5 + Util/Emacs/dafny-mode.el | 1 + Util/latex/dafny.sty | 2 +- Util/vim/dafny.vim | 2 +- 37 files changed, 2639 insertions(+), 897 deletions(-) create mode 100644 Test/dafny0/Trait/Trait.dfy create mode 100644 Test/dafny0/Trait/Trait.dfy.expect create mode 100644 Test/dafny0/Trait/TraitBasics.dfy create mode 100644 Test/dafny0/Trait/TraitBasics.dfy.expect create mode 100644 Test/dafny0/Trait/TraitExtend.dfy create mode 100644 Test/dafny0/Trait/TraitExtend.dfy.expect create mode 100644 Test/dafny0/Trait/TraitMultiModule.dfy create mode 100644 Test/dafny0/Trait/TraitMultiModule.dfy.expect create mode 100644 Test/dafny0/Trait/TraitOverride0.dfy create mode 100644 Test/dafny0/Trait/TraitOverride0.dfy.expect create mode 100644 Test/dafny0/Trait/TraitOverride1.dfy create mode 100644 Test/dafny0/Trait/TraitOverride1.dfy.expect create mode 100644 Test/dafny0/Trait/TraitOverride2.dfy create mode 100644 Test/dafny0/Trait/TraitOverride2.dfy.expect create mode 100644 Test/dafny0/Trait/TraitOverride3.dfy create mode 100644 Test/dafny0/Trait/TraitOverride3.dfy.expect create mode 100644 Test/dafny0/Trait/TraitOverride4.dfy create mode 100644 Test/dafny0/Trait/TraitOverride4.dfy.expect create mode 100644 Test/dafny0/Trait/TraitPolymorphism.dfy create mode 100644 Test/dafny0/Trait/TraitPolymorphism.dfy.expect create mode 100644 Test/dafny0/Trait/TraitSpecsOverride0.dfy create mode 100644 Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect 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 { 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 members = new List(); + 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.TopLevelDecls.Add(dt); .) | OtherTypeDecl (. defaultModule.TopLevelDecls.Add(td); .) | IteratorDecl (. defaultModule.TopLevelDecls.Add(iter); .) - + | TraitDecl (. defaultModule.TopLevelDecls.Add(trait); .) | ClassMemberDecl } (. // find the default class in the default module, then append membersDefaultClass to its member list @@ -236,7 +237,8 @@ Dafny SubModuleDecl = (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter; Attributes attrs = null; IToken/*!*/ id; - List namedModuleDefaultClassMembers = new List();; + TraitDecl/*!*/ trait; + List namedModuleDefaultClassMembers = new List();; List idRefined = null, idPath = null, idAssignment = null; ModuleDefinition module; ModuleDecl sm; @@ -253,7 +255,8 @@ SubModuleDecl "{" (. module.BodyStartTok = t; .) { SubModuleDecl (. module.TopLevelDecls.Add(sm); .) | ClassDecl (. module.TopLevelDecls.Add(c); .) - | DatatypeDecl (. module.TopLevelDecls.Add(dt); .) + | TraitDecl (. module.TopLevelDecls.Add(trait); .) + | DatatypeDecl (. module.TopLevelDecls.Add(dt); .) | OtherTypeDecl (. module.TopLevelDecls.Add(td); .) | IteratorDecl (. module.TopLevelDecls.Add(iter); .) | ClassMemberDecl @@ -298,7 +301,8 @@ ClassDecl = (. Contract.Requires(module != null); Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ id; - Attributes attrs = null; + List/*!*/ traitId=null; + Attributes attrs = null; List typeArgs = new List(); List members = new List(); IToken bodyStart; @@ -308,15 +312,41 @@ ClassDecl { Attribute } NoUSIdent [ GenericParameters ] + ["extends" QualifiedName] "{" (. bodyStart = t; .) { ClassMemberDecl } "}" - (. 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 + = (. Contract.Requires(module != null); + Contract.Ensures(Contract.ValueAtReturn(out trait) != null); + IToken/*!*/ id; + Attributes attrs = null; + List typeArgs = new List(); //traits should not support type parameters at the moment + List members = new List(); + IToken bodyStart; + .) + SYNC + "trait" + { Attribute } + NoUSIdent + [ GenericParameters ] + "{" (. bodyStart = t; .) + { ClassMemberDecl + } + "}" + (. trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs); + trait.BodyStartTok = bodyStart; + trait.BodyEndTok = t; + .) + . + ClassMemberDecl<.List/*!*/ 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(), new List(), DontCompile()); + ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List(), new List(), 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 typeArgs, [Captured] List members, Attributes attributes) + : base(tok, name, module, typeArgs, members, attributes, null) { } + } + public class ClassDecl : TopLevelDecl { public readonly List 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 typeArgs, [Captured] List members, Attributes attributes) + List typeArgs, [Captured] List members, Attributes attributes, List 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 members) - : base(Token.NoToken, "_default", module, new List(), members, null) { + : base(Token.NoToken, "_default", module, new List(), 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(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}), - new List(), attrs) + new List(), attrs,null) { Contract.Requires(1 <= dims); Contract.Requires(module != null); @@ -1731,7 +1743,7 @@ namespace Microsoft.Dafny { List yieldRequires, List yieldEnsures, BlockStmt body, Attributes attributes, IToken signatureEllipsis) - : base(tok, name, module, typeArgs, new List(), attributes) + : base(tok, name, module, typeArgs, new List(), 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; /// /// 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 AssignedAssumptionVariables = new HashSet(); + 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 namedModuleDefaultClassMembers = new List();; List 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/*!*/ traitId=null; Attributes attrs = null; List typeArgs = new List(); List members = new List(); 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 typeArgs = new List(); //traits should not support type parameters at the moment + List members = new List(); + 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/*!*/ 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(); 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/*!*/ 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/*!*/ 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(); 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 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(); - 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(); - 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(); - 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(); - 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/*!*/ yieldReq, List/*!* 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void GenericInstantiation(List/*!*/ 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/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List gt; List 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(); - 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/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out tok); gt = new List(); path = new List(); - 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/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List decreases) { @@ -1526,33 +1573,33 @@ List/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ ss) { @@ -1609,58 +1656,58 @@ List/*!*/ 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/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LList - enum MethodTranslationKind { SpecWellformedness, InterModuleCall, IntraModuleCall, CoCall, Implementation } + enum MethodTranslationKind { SpecWellformedness, InterModuleCall, IntraModuleCall, CoCall, Implementation, OverrideCheck } /// /// 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(); var ens = new List(); // 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 { @"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 + 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 + { + 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 -- cgit v1.2.3 From 18f9f3e8e20c4c7c302a7e6042ffbce2dde82cdc Mon Sep 17 00:00:00 2001 From: Reza Ahmadi Date: Fri, 18 Jul 2014 21:17:50 +0300 Subject: added ignored files --- .hgignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.hgignore b/.hgignore index a1219ed2..95b7d862 100644 --- a/.hgignore +++ b/.hgignore @@ -12,3 +12,4 @@ syntax: glob *.dll *.tmp *.tmp.dfy +dafny_all_filesThat_Change.txt -- cgit v1.2.3 From 7e04037cabe8b39eab697171f1086f74fbbb7159 Mon Sep 17 00:00:00 2001 From: Reza Ahmadi Date: Sun, 20 Jul 2014 16:51:54 +0300 Subject: - fixed an issue regarding including ghost functions in the compiled interface - added one more test --- Source/Dafny/Compiler.cs | 6 +++--- Test/dafny0/Trait/TraitOverride3.dfy | 21 ++++++++++++++++++++- 2 files changed, 23 insertions(+), 4 deletions(-) diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 7be7f58f..220b5561 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -221,7 +221,7 @@ namespace Microsoft.Dafny { List members = new List(); foreach (MemberDecl mem in trait.Members) { - if (mem.IsStatic) + if (mem.IsStatic && !mem.IsGhost) { if (mem is Function) { @@ -790,7 +790,7 @@ namespace Microsoft.Dafny { { Error("Function {0} has no body", f.FullName); } - else if (!member.IsStatic) //static members are not included in the target trait + else if (!member.IsStatic && !member.IsGhost) //static and ghost members are not included in the target trait { Indent(indent); wr.Write("{0} @{1}", TypeName(f.ResultType), f.CompileName); @@ -836,7 +836,7 @@ namespace Microsoft.Dafny { { Error("Method {0} has no body", m.FullName); } - else if (!member.IsStatic) //static members are not included in the target trait + else if (!member.IsStatic && !member.IsGhost) //static and ghost members are not included in the target trait { Indent(indent); wr.Write("void @{0}", m.CompileName); diff --git a/Test/dafny0/Trait/TraitOverride3.dfy b/Test/dafny0/Trait/TraitOverride3.dfy index 498a0a6b..d602bffb 100644 --- a/Test/dafny0/Trait/TraitOverride3.dfy +++ b/Test/dafny0/Trait/TraitOverride3.dfy @@ -25,4 +25,23 @@ class C extends J var a:int := 100; assert a==100; } -} \ No newline at end of file +} + +trait t +{ + function f(s2:int):int + ensures f(s2) > 0; + //requires s != null && s.Length > 1; + //reads s, s2; +} + +class c extends t +{ + function f(s3:int):int + ensures f(s3) > 1; + //requires s0 != null && s0.Length > (0); + //reads s0; + { + 2 + } +} -- cgit v1.2.3 From 2c9d68a529b04dcb1c18025306713644a602833c Mon Sep 17 00:00:00 2001 From: Reza Ahmadi Date: Sun, 20 Jul 2014 16:54:34 +0300 Subject: fixed one .expect file. now all 11 tests related to Traits pass. --- Test/dafny0/Trait/TraitOverride3.dfy.expect | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/dafny0/Trait/TraitOverride3.dfy.expect b/Test/dafny0/Trait/TraitOverride3.dfy.expect index f5019f3b..5f41963f 100644 --- a/Test/dafny0/Trait/TraitOverride3.dfy.expect +++ b/Test/dafny0/Trait/TraitOverride3.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 14 verified, 0 errors +Dafny program verifier finished with 17 verified, 0 errors -- cgit v1.2.3 From 129744b09404197d1f84481601edd51d0d104bd4 Mon Sep 17 00:00:00 2001 From: Reza Ahmadi Date: Sun, 20 Jul 2014 19:09:18 +0300 Subject: - fixed a bug in inheriting members from a trait => ResolvedClass in userdefinedtypes used to be null-> fixed - checking only bodyless methods and functions to make sure they have been implemented in the child class - added one more test --- Source/Dafny/Cloner.cs | 7 ++-- Source/Dafny/Resolver.cs | 40 ++++++++++++-------- Test/dafny0/Trait/TraitOverride3.dfy | 16 +++++++- Test/dafny0/Trait/TraitOverride3.dfy.expect | 2 +- Test/dafny0/Trait/TraitUsingParentMembers.dfy | 44 ++++++++++++++++++++++ .../Trait/TraitUsingParentMembers.dfy.expect | 8 ++++ 6 files changed, 95 insertions(+), 22 deletions(-) create mode 100644 Test/dafny0/Trait/TraitUsingParentMembers.dfy create mode 100644 Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 5dfc67d5..b462f983 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -137,8 +137,6 @@ namespace Microsoft.Dafny var f = (Field)member; 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; @@ -184,7 +182,10 @@ namespace Microsoft.Dafny } public Formal CloneFormal(Formal formal) { - return new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost); + Formal f = new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost); + if (f.Type is UserDefinedType && formal.Type is UserDefinedType) + ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(formal.Type)).ResolvedClass; + return f; } public BoundVar CloneBoundVar(BoundVar bv) { diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index d503076c..9798e79f 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2916,13 +2916,16 @@ namespace Microsoft.Dafny else //the member is not already in the class { MemberDecl classNewMember = cloner.CloneMember(traitMem.Value); + if (classNewMember is Field) + { + Field f = (Field)classNewMember; + if (f.Type is UserDefinedType) + ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(((Field)(traitMem.Value)).Type)).ResolvedClass; + } 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 @@ -2934,27 +2937,32 @@ namespace Microsoft.Dafny 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) + if (traitFunc.Body == null) //we do this check only if trait function body is null { - Function classFunc = (Function)classMem; - refinementTransformer.CheckOverride_FunctionParameters(classFunc, traitFunc); + 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); } - 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) + if (traitMethod.Body == null) //we do this check only if trait method body is null { - Method classMethod = (Method)classMem; - refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod); + 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); } - if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null) - Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName); } } } diff --git a/Test/dafny0/Trait/TraitOverride3.dfy b/Test/dafny0/Trait/TraitOverride3.dfy index d602bffb..467ad333 100644 --- a/Test/dafny0/Trait/TraitOverride3.dfy +++ b/Test/dafny0/Trait/TraitOverride3.dfy @@ -2,8 +2,7 @@ // RUN: %diff "%s.expect" "%t" -//related compiler changes -//everything works OK in the following code +//everything should work OK in the following program trait J { function method F(y: int): int @@ -45,3 +44,16 @@ class c extends t 2 } } + +trait P1 +{ + method M(N: int, a: array) returns (sum: int) + { + sum := 1; + } +} + +class C1 extends P1 +{ + +} diff --git a/Test/dafny0/Trait/TraitOverride3.dfy.expect b/Test/dafny0/Trait/TraitOverride3.dfy.expect index 5f41963f..73727958 100644 --- a/Test/dafny0/Trait/TraitOverride3.dfy.expect +++ b/Test/dafny0/Trait/TraitOverride3.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 17 verified, 0 errors +Dafny program verifier finished with 21 verified, 0 errors diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy b/Test/dafny0/Trait/TraitUsingParentMembers.dfy new file mode 100644 index 00000000..dd45d0e6 --- /dev/null +++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy @@ -0,0 +1,44 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +trait P1 +{ + method N0() { + var a: array; + if (a != null && 5 < a.Length) { + a[5] := 12; // error: violates modifies clause + } + } + + method Mul(x: int, y: int) returns (r: int) + requires 0 <= x && 0 <= y; + ensures r == x*y; + decreases x; +} + +class C1 extends P1 +{ + method Mul(x: int, y: int) returns (r: int) + requires 0 <= x && 0 <= y; + ensures r == x*y; + decreases x; + { + if (x == 0) { + r := 0; + } else { + var m := Mul(x-1, y); + r := m + y; + } + } + + method Testing(arr:array) + requires arr != null && arr.Length == 2 && arr[0]== 1 && arr[1] == 10; + { + N0(); //calling parent trait methods + var x := 2; + var y := 5; + var z := Mul(x,y); + assert (z == 10); + } +} \ No newline at end of file diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect new file mode 100644 index 00000000..6849499c --- /dev/null +++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect @@ -0,0 +1,8 @@ +TraitUsingParentMembers.dfy(10,9): Error: assignment may update an array element not in the enclosing context's modifies clause +Execution trace: + (0,0): anon0 + (0,0): anon5_Then + (0,0): anon2 + (0,0): anon6_Then + +Dafny program verifier finished with 9 verified, 1 error -- cgit v1.2.3 From d10e53aa085cbd95198d9797bb247c6ba3a34145 Mon Sep 17 00:00:00 2001 From: Reza Ahmadi Date: Sun, 20 Jul 2014 19:25:04 +0300 Subject: added one more test. --- Test/dafny0/Trait/TraitOverride3.dfy | 17 +++++++++++++++++ Test/dafny0/Trait/TraitOverride3.dfy.expect | 2 +- 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/Test/dafny0/Trait/TraitOverride3.dfy b/Test/dafny0/Trait/TraitOverride3.dfy index 467ad333..6a5fa59f 100644 --- a/Test/dafny0/Trait/TraitOverride3.dfy +++ b/Test/dafny0/Trait/TraitOverride3.dfy @@ -57,3 +57,20 @@ class C1 extends P1 { } + +trait TT +{ + static function method M(a:int, b:int) : int + ensures M(a,b) == a + b; + { + a + b + } +} + +class CC extends TT +{ + method Testing(a:int,b:int) + { + assert (TT.M(a,b) == a + b); + } +} diff --git a/Test/dafny0/Trait/TraitOverride3.dfy.expect b/Test/dafny0/Trait/TraitOverride3.dfy.expect index 73727958..9d7e625f 100644 --- a/Test/dafny0/Trait/TraitOverride3.dfy.expect +++ b/Test/dafny0/Trait/TraitOverride3.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 21 verified, 0 errors +Dafny program verifier finished with 25 verified, 0 errors -- cgit v1.2.3 From f314be9242a07c302721701072696bdadc9a7acf Mon Sep 17 00:00:00 2001 From: leino Date: Mon, 21 Jul 2014 22:59:58 -0700 Subject: Implemented missing routine in runtime system (real-to-int conversion) --- Binaries/DafnyRuntime.cs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 6f0cab13..d6bd895a 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -656,6 +656,13 @@ namespace Dafny num = n; den = d; } + public BigInteger ToBigInteger() { + if (0 <= num) { + return num / den; + } else { + return (num - den + 1) / den; + } + } /// /// Returns values such that aa/dd == a and bb/dd == b. /// -- cgit v1.2.3 From 54b670417f5974c43ef2fd55d37ba3806ad5c72d Mon Sep 17 00:00:00 2001 From: leino Date: Wed, 23 Jul 2014 13:45:38 -0700 Subject: Test file whitespace delta --- Test/dafny0/AutoReq.dfy | 226 ++++++++++++++++++++--------------------- Test/dafny0/AutoReq.dfy.expect | 4 +- 2 files changed, 115 insertions(+), 115 deletions(-) diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy index efe88446..9e0d3b63 100644 --- a/Test/dafny0/AutoReq.dfy +++ b/Test/dafny0/AutoReq.dfy @@ -146,170 +146,170 @@ module {:autoReq} QuantifierTestsHard { function n(x:int) : bool function f1(x:int) : bool - requires x > 3; - requires x < 16; + requires x > 3; + requires x < 16; function variable_uniqueness_test(x:int) : bool { (forall y:int :: m(y)) - && - f1(x) + && + f1(x) } } module CorrectReqOrdering { - function f1(x:int) : bool - requires x > 3; + function f1(x:int) : bool + requires x > 3; - function f2(b:bool) : bool - requires b; + function f2(b:bool) : bool + requires b; - // Should pass if done correctly. - // However, if Dafny incorrectly put the requires for f2 first, - // then the requires for f1 won't be satisfied - function {:autoReq} f3(z:int) : bool - { - f2(f1(z)) - } + // Should pass if done correctly. + // However, if Dafny incorrectly put the requires for f2 first, + // then the requires for f1 won't be satisfied + function {:autoReq} f3(z:int) : bool + { + f2(f1(z)) + } } -module ShortCircuiting { - function f1(x:int) : bool - requires x > 3; +module ShortCircuiting { + function f1(x:int) : bool + requires x > 3; - function f2(y:int) : bool - requires y < 10; + function f2(y:int) : bool + requires y < 10; - function {:autoReq} test1(x':int, y':int) : bool - { - f1(x') && f2(y') - } + function {:autoReq} test1(x':int, y':int) : bool + { + f1(x') && f2(y') + } - function {:autoReq} test2(x':int, y':int) : bool - { - f1(x') ==> f2(y') - } + function {:autoReq} test2(x':int, y':int) : bool + { + f1(x') ==> f2(y') + } - function {:autoReq} test3(x':int, y':int) : bool - { - f1(x') || f2(y') - } + function {:autoReq} test3(x':int, y':int) : bool + { + f1(x') || f2(y') + } } module Lets { - function f1(x:int) : bool - requires x > 3; + function f1(x:int) : bool + requires x > 3; - function {:autoReq} test1(x':int) : bool - { - var y' := 3*x'; f1(y') - } + function {:autoReq} test1(x':int) : bool + { + var y' := 3*x'; f1(y') + } } // Test nested module specification of :autoReq attribute module {:autoReq} M1 { - module M2 { - function f(x:int) : bool - requires x > 3; - { - x > 7 - } - - // Should succeed thanks to auto-generation based on f's requirements - function {:autoReq} h(y:int) : bool - { - f(y) - } + module M2 { + function f(x:int) : bool + requires x > 3; + { + x > 7 } + + // Should succeed thanks to auto-generation based on f's requirements + function {:autoReq} h(y:int) : bool + { + f(y) + } + } } module Datatypes { - datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType); + datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType); - function f1(t:TheType):bool - requires t.TheType_builder? && t.x > 3; + function f1(t:TheType):bool + requires t.TheType_builder? && t.x > 3; - function {:autoReq} test(t:TheType) : bool - { - f1(t) - } + function {:autoReq} test(t:TheType) : bool + { + f1(t) + } - function f2(x:int) : bool - requires forall t:TheType :: t.TheType_builder? && t.x > x; - { - true - } + function f2(x:int) : bool + requires forall t:TheType :: t.TheType_builder? && t.x > x; + { + true + } - // Should cause a function-requirement violation without autoReq - function f3(y:int) : bool - { - f2(y) - } + // Should cause a function-requirement violation without autoReq + function f3(y:int) : bool + { + f2(y) + } - function {:autoReq} test2(z:int) : bool - { - f2(z) - } + function {:autoReq} test2(z:int) : bool + { + f2(z) + } } module Matches { - datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType); + datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType); - function f1(x:int):bool - requires x > 3; + function f1(x:int):bool + requires x > 3; - function {:autoReq} basic_test(t:TheType) : bool - { - match t - case TheType_builder(x) => f1(x) - case TheType_copier(t) => true - } + function {:autoReq} basic_test(t:TheType) : bool + { + match t + case TheType_builder(x) => f1(x) + case TheType_copier(t) => true + } } // Make sure :autoReq works with static functions module StaticTest { - static function f(x:int) : bool - requires x > 3; - { - x > 7 - } + static function f(x:int) : bool + requires x > 3; + { + x > 7 + } - static function {:autoReq} g(z:int) : bool - requires f(z); - { - true - } - - // Should succeed thanks to auto-generation based on f's requirements - static function {:autoReq} h(y:int) : bool - { - g(y) - } + static function {:autoReq} g(z:int) : bool + requires f(z); + { + true + } - static predicate IsEven(x:int) + // Should succeed thanks to auto-generation based on f's requirements + static function {:autoReq} h(y:int) : bool + { + g(y) + } - static function EvenDoubler(x:int) : int - requires IsEven(x); + static predicate IsEven(x:int) - // Should succeed thanks to auto-generated requirement of IsEven - static function {:autoReq} test(y:int) : int - { - EvenDoubler(y) - } + static function EvenDoubler(x:int) : int + requires IsEven(x); + + // Should succeed thanks to auto-generated requirement of IsEven + static function {:autoReq} test(y:int) : int + { + EvenDoubler(y) + } } module OpaqueTest { - static function bar(x:int) : int - requires x>7; - { - x-2 - } + static function bar(x:int) : int + requires x>7; + { + x-2 + } - static function {:autoReq} {:opaque} foo(x:int) : int - { - bar(x) - } + static function {:autoReq} {:opaque} foo(x:int) : int + { + bar(x) + } } diff --git a/Test/dafny0/AutoReq.dfy.expect b/Test/dafny0/AutoReq.dfy.expect index 617e6003..547b676d 100644 --- a/Test/dafny0/AutoReq.dfy.expect +++ b/Test/dafny0/AutoReq.dfy.expect @@ -1,5 +1,5 @@ -AutoReq.dfy(247,3): Error: possible violation of function precondition -AutoReq.dfy(239,12): Related location +AutoReq.dfy(247,5): Error: possible violation of function precondition +AutoReq.dfy(239,14): Related location Execution trace: (0,0): anon0 (0,0): anon3_Else -- cgit v1.2.3 From d7fc2974ac1945828c8180d39a7e2a91824b7273 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Thu, 31 Jul 2014 09:34:32 +0200 Subject: Changed test case to not use '/doNotUseParallelism' anymore. --- Test/dafny4/NumberRepresentations.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy index 3096616f..4269d24d 100644 --- a/Test/dafny4/NumberRepresentations.dfy +++ b/Test/dafny4/NumberRepresentations.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" /doNotUseParallelism "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" // We consider a number representation that consists of a sequence of digits. The least -- cgit v1.2.3 From c6f5d1f5ee5e869406f25d3c0603aae9fa45e699 Mon Sep 17 00:00:00 2001 From: Reza Ahmadi Date: Thu, 31 Jul 2014 17:01:45 +0300 Subject: combined two tests --- Test/dafny0/Trait/Trait.dfy | 95 ----------------- Test/dafny0/Trait/Trait.dfy.expect | 5 - Test/dafny0/Trait/TraitBasics.dfy | 79 -------------- Test/dafny0/Trait/TraitBasics.dfy.expect | 3 - Test/dafny0/Trait/TraitBasix.dfy | 173 +++++++++++++++++++++++++++++++ Test/dafny0/Trait/TraitBasix.dfy.expect | 7 ++ 6 files changed, 180 insertions(+), 182 deletions(-) delete mode 100644 Test/dafny0/Trait/Trait.dfy delete mode 100644 Test/dafny0/Trait/Trait.dfy.expect delete mode 100644 Test/dafny0/Trait/TraitBasics.dfy delete mode 100644 Test/dafny0/Trait/TraitBasics.dfy.expect create mode 100644 Test/dafny0/Trait/TraitBasix.dfy create mode 100644 Test/dafny0/Trait/TraitBasix.dfy.expect diff --git a/Test/dafny0/Trait/Trait.dfy b/Test/dafny0/Trait/Trait.dfy deleted file mode 100644 index cf76e860..00000000 --- a/Test/dafny0/Trait/Trait.dfy +++ /dev/null @@ -1,95 +0,0 @@ -// 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 deleted file mode 100644 index 253144ea..00000000 --- a/Test/dafny0/Trait/Trait.dfy.expect +++ /dev/null @@ -1,5 +0,0 @@ -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 deleted file mode 100644 index 6bfe76bb..00000000 --- a/Test/dafny0/Trait/TraitBasics.dfy +++ /dev/null @@ -1,79 +0,0 @@ -// 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 deleted file mode 100644 index c9fb096e..00000000 --- a/Test/dafny0/Trait/TraitBasics.dfy.expect +++ /dev/null @@ -1,3 +0,0 @@ -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/TraitBasix.dfy b/Test/dafny0/Trait/TraitBasix.dfy new file mode 100644 index 00000000..e16e8fc4 --- /dev/null +++ b/Test/dafny0/Trait/TraitBasix.dfy @@ -0,0 +1,173 @@ +// 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 + { + + } +} + + +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/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect new file mode 100644 index 00000000..1d44d0f6 --- /dev/null +++ b/Test/dafny0/Trait/TraitBasix.dfy.expect @@ -0,0 +1,7 @@ +TraitBasix.dfy(77,13): Error: member in the class has been already inherited from its parent trait +TraitBasix.dfy(70,7): Error: class: I0Child does not implement trait member: Customizable +TraitBasix.dfy(80,7): Error: class: I0Child2 does not implement trait member: F +TraitBasix.dfy(91,7): Error: unresolved identifier: IX +TraitBasix.dfy(98,6): Error: a trait is not allowed to declare a constructor +TraitBasix.dfy(117,10): Error: new can not be applied to a trait +6 resolution/type errors detected in TraitBasix.dfy -- cgit v1.2.3 From 47de1c8add4f4ac5c390a96bbd8d2e5acaf87540 Mon Sep 17 00:00:00 2001 From: Reza Ahmadi Date: Thu, 31 Jul 2014 17:34:27 +0300 Subject: combined few tests --- Test/dafny0/Trait/TraitOverride1.dfy | 140 ++++++++++++++++++++++++++++ Test/dafny0/Trait/TraitOverride1.dfy.expect | 2 +- Test/dafny0/Trait/TraitOverride2.dfy | 30 ------ Test/dafny0/Trait/TraitOverride2.dfy.expect | 2 - Test/dafny0/Trait/TraitOverride3.dfy | 76 --------------- Test/dafny0/Trait/TraitOverride3.dfy.expect | 2 - Test/dafny0/Trait/TraitOverride4.dfy | 41 -------- Test/dafny0/Trait/TraitOverride4.dfy.expect | 2 - 8 files changed, 141 insertions(+), 154 deletions(-) delete mode 100644 Test/dafny0/Trait/TraitOverride2.dfy delete mode 100644 Test/dafny0/Trait/TraitOverride2.dfy.expect delete mode 100644 Test/dafny0/Trait/TraitOverride3.dfy delete mode 100644 Test/dafny0/Trait/TraitOverride3.dfy.expect delete mode 100644 Test/dafny0/Trait/TraitOverride4.dfy delete mode 100644 Test/dafny0/Trait/TraitOverride4.dfy.expect diff --git a/Test/dafny0/Trait/TraitOverride1.dfy b/Test/dafny0/Trait/TraitOverride1.dfy index 980054ee..90a25f53 100644 --- a/Test/dafny0/Trait/TraitOverride1.dfy +++ b/Test/dafny0/Trait/TraitOverride1.dfy @@ -1,6 +1,7 @@ // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" +//everything should work OK in this test file trait T1 { function method Plus (x:int, y:int) : int @@ -52,3 +53,142 @@ class C1 extends T1 } } +trait T2 +{ + 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 C2 extends T2 +{ + 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; + } +} + + +trait T3 +{ + 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 C3 extends T3 +{ + 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; + } +} + +trait t +{ + function f(s2:int):int + ensures f(s2) > 0; + //requires s != null && s.Length > 1; + //reads s, s2; +} + +class c extends t +{ + function f(s3:int):int + ensures f(s3) > 1; + //requires s0 != null && s0.Length > (0); + //reads s0; + { + 2 + } +} + +trait P1 +{ + method M(N: int, a: array) returns (sum: int) + { + sum := 1; + } +} + +class CC1 extends P1 +{ + +} + +trait TT +{ + static function method M(a:int, b:int) : int + ensures M(a,b) == a + b; + { + a + b + } +} + +class CC extends TT +{ + method Testing(a:int,b:int) + { + assert (TT.M(a,b) == a + b); + } +} + + +trait T4 +{ + 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 C4 extends T4 +{ + function method F(y: int): int + { + 200 + } + + method M(kk:int) returns (ksos:int) + requires kk > (-1); + ensures ksos > 0; + { + ksos:=10; + } +} diff --git a/Test/dafny0/Trait/TraitOverride1.dfy.expect b/Test/dafny0/Trait/TraitOverride1.dfy.expect index 5f41963f..0f7b49e3 100644 --- a/Test/dafny0/Trait/TraitOverride1.dfy.expect +++ b/Test/dafny0/Trait/TraitOverride1.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 17 verified, 0 errors +Dafny program verifier finished with 62 verified, 0 errors diff --git a/Test/dafny0/Trait/TraitOverride2.dfy b/Test/dafny0/Trait/TraitOverride2.dfy deleted file mode 100644 index fca79b2e..00000000 --- a/Test/dafny0/Trait/TraitOverride2.dfy +++ /dev/null @@ -1,30 +0,0 @@ -// 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 deleted file mode 100644 index 76f19e0d..00000000 --- a/Test/dafny0/Trait/TraitOverride2.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 7 verified, 0 errors diff --git a/Test/dafny0/Trait/TraitOverride3.dfy b/Test/dafny0/Trait/TraitOverride3.dfy deleted file mode 100644 index 6a5fa59f..00000000 --- a/Test/dafny0/Trait/TraitOverride3.dfy +++ /dev/null @@ -1,76 +0,0 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - - -//everything should work OK in the following program -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; - } -} - -trait t -{ - function f(s2:int):int - ensures f(s2) > 0; - //requires s != null && s.Length > 1; - //reads s, s2; -} - -class c extends t -{ - function f(s3:int):int - ensures f(s3) > 1; - //requires s0 != null && s0.Length > (0); - //reads s0; - { - 2 - } -} - -trait P1 -{ - method M(N: int, a: array) returns (sum: int) - { - sum := 1; - } -} - -class C1 extends P1 -{ - -} - -trait TT -{ - static function method M(a:int, b:int) : int - ensures M(a,b) == a + b; - { - a + b - } -} - -class CC extends TT -{ - method Testing(a:int,b:int) - { - assert (TT.M(a,b) == a + b); - } -} diff --git a/Test/dafny0/Trait/TraitOverride3.dfy.expect b/Test/dafny0/Trait/TraitOverride3.dfy.expect deleted file mode 100644 index 9d7e625f..00000000 --- a/Test/dafny0/Trait/TraitOverride3.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 25 verified, 0 errors diff --git a/Test/dafny0/Trait/TraitOverride4.dfy b/Test/dafny0/Trait/TraitOverride4.dfy deleted file mode 100644 index c9cc3953..00000000 --- a/Test/dafny0/Trait/TraitOverride4.dfy +++ /dev/null @@ -1,41 +0,0 @@ -// 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 deleted file mode 100644 index aeb37948..00000000 --- a/Test/dafny0/Trait/TraitOverride4.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 13 verified, 0 errors -- cgit v1.2.3 From a5be808ee60f37b3e74e03660eab66c95154083e Mon Sep 17 00:00:00 2001 From: Reza Ahmadi Date: Thu, 31 Jul 2014 17:48:42 +0300 Subject: added one more test case --- Test/dafny0/Trait/TraitSpecsOverride0.dfy | 20 +++++++++++++++++++- Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect | 8 ++++---- 2 files changed, 23 insertions(+), 5 deletions(-) diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy b/Test/dafny0/Trait/TraitSpecsOverride0.dfy index 5b4417c3..614adc2d 100644 --- a/Test/dafny0/Trait/TraitSpecsOverride0.dfy +++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy @@ -25,6 +25,13 @@ trait J x := 1000; y := y + x; } + + method arrM (y: array, x: int, a: int, b: int) returns (c: int) + requires a > b; + requires y != null && y.Length > 0; + ensures c == a + b; + modifies y; + decreases x; } class C extends J @@ -37,5 +44,16 @@ class C extends J method M(kk:int) returns (ksos:int) //errors here, M must provide its own specifications { ksos:=10; - } + } + + method arrM (y1: array, x1: int, a1: int, b1: int) returns (c1: int) + requires a1 > b1; + requires y1 != null && y1.Length > 0; + ensures c1 == a1 + b1; + modifies y1; + decreases x1; + { + y1[0] := a1 + b1; + c1 := a1 + b1; + } } \ No newline at end of file diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect index cbdcdf05..750e13e0 100644 --- a/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect +++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect @@ -1,5 +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 +TraitSpecsOverride0.dfy(39,17): Error: Function must provide its own Reads clauses anew +TraitSpecsOverride0.dfy(39,17): Error: Function must provide its own Decreases clauses anew +TraitSpecsOverride0.dfy(44,8): Error: Method must provide its own Requires clauses anew +TraitSpecsOverride0.dfy(44,8): Error: Method must provide its own Ensures clauses anew 4 resolution/type errors detected in TraitSpecsOverride0.dfy -- cgit v1.2.3 From ae578ae92040975fed005d045110679e4e858c31 Mon Sep 17 00:00:00 2001 From: leino Date: Sat, 2 Aug 2014 01:05:17 -0700 Subject: Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in the resolver and translator --- Source/Dafny/Cloner.cs | 7 + Source/Dafny/Compiler.cs | 56 ++++--- Source/Dafny/DafnyAst.cs | 84 +++++++--- Source/Dafny/Resolver.cs | 127 ++++++++++----- Source/Dafny/Rewriter.cs | 6 +- Source/Dafny/Translator.cs | 268 ++++++++++++++++++-------------- Source/DafnyExtension/DafnyRuntime.cs | 7 + Test/dafny0/EqualityTypes.dfy.expect | 2 +- Test/dafny0/ResolutionErrors.dfy | 8 +- Test/dafny0/ResolutionErrors.dfy.expect | 3 +- Test/dafny0/TypeSynonyms.dfy | 7 + Test/dafny0/TypeSynonyms.dfy.expect | 2 +- Test/dafny0/TypeTests.dfy.expect | 4 +- 13 files changed, 356 insertions(+), 225 deletions(-) diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index bb644825..8ef8f0ee 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -142,6 +142,13 @@ namespace Microsoft.Dafny return new MapType(CloneType(tt.Domain), CloneType(tt.Range)); } else if (t is UserDefinedType) { var tt = (UserDefinedType)t; +#if TEST_TYPE_SYNONYM_TRANSPARENCY + if (tt.Name == "type#synonym#transparency#test") { + // time to drop the synonym wrapper + var syn = (TypeSynonymDecl)tt.ResolvedClass; + return CloneType(syn.Rhs); + } +#endif return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(Tok)); } else if (t is InferredTypeProxy) { return new InferredTypeProxy(); diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index c665026c..c8af05f4 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1543,8 +1543,6 @@ namespace Microsoft.Dafny { // ... // } if (s.Cases.Count != 0) { - var sourceType = (UserDefinedType)s.Source.Type; - SpillLetVariableDecls(s.Source, indent); string source = "_source" + tmpVarCount; tmpVarCount++; @@ -1554,6 +1552,7 @@ namespace Microsoft.Dafny { wr.WriteLine(";"); int i = 0; + var sourceType = (UserDefinedType)s.Source.Type.NormalizeExpand(); foreach (MatchCaseStmt mc in s.Cases) { MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, indent); TrStmtList(mc.Body, indent); @@ -1820,7 +1819,7 @@ namespace Microsoft.Dafny { if (tp.ArrayDimensions == null) { wr.Write("new {0}()", TypeName(tp.EType)); } else { - if (tp.EType is IntType || tp.EType.IsTypeParameter) { + if (tp.EType.IsIntegerType || tp.EType.IsTypeParameter) { // Because the default constructor for BigInteger does not generate a valid BigInteger, we have // to excplicitly initialize the elements of an integer array. This is all done in a helper routine. wr.Write("Dafny.Helpers.InitNewArray{0}<{1}>", tp.ArrayDimensions.Count, TypeName(tp.EType)); @@ -2002,24 +2001,24 @@ namespace Microsoft.Dafny { wr.Write(enclosingMethod != null && enclosingMethod.IsTailRecursive ? "_this" : "this"); } else if (expr is IdentifierExpr) { - IdentifierExpr e = (IdentifierExpr)expr; + var e = (IdentifierExpr)expr; wr.Write("@" + e.Var.CompileName); } else if (expr is SetDisplayExpr) { - SetDisplayExpr e = (SetDisplayExpr)expr; - Type elType = cce.NonNull((SetType)e.Type).Arg; + var e = (SetDisplayExpr)expr; + var elType = e.Type.AsSetType.Arg; wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType)); TrExprList(e.Elements); } else if (expr is MultiSetDisplayExpr) { - MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr; - Type elType = cce.NonNull((MultiSetType)e.Type).Arg; + var e = (MultiSetDisplayExpr)expr; + var elType = e.Type.AsMultiSetType.Arg; wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType)); TrExprList(e.Elements); } else if (expr is SeqDisplayExpr) { - SeqDisplayExpr e = (SeqDisplayExpr)expr; - Type elType = cce.NonNull((SeqType)e.Type).Arg; + var e = (SeqDisplayExpr)expr; + var elType = e.Type.AsSeqType.Arg; wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType)); TrExprList(e.Elements); @@ -2074,11 +2073,12 @@ namespace Microsoft.Dafny { } } } else if (expr is MultiSetFormingExpr) { - MultiSetFormingExpr e = (MultiSetFormingExpr)expr; - wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(((CollectionType)e.E.Type).Arg)); - if (e.E.Type is SeqType) { + var e = (MultiSetFormingExpr)expr; + wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(e.E.Type.AsCollectionType.Arg)); + var eeType = e.E.Type.NormalizeExpand(); + if (eeType is SeqType) { TrParenExpr(".FromSeq", e.E); - } else if (e.E.Type is SetType) { + } else if (eeType is SetType) { TrParenExpr(".FromSet", e.E); } else { Contract.Assert(false); throw new cce.UnreachableException(); @@ -2198,7 +2198,7 @@ namespace Microsoft.Dafny { TrParenExpr(e.E); break; case UnaryOpExpr.Opcode.Cardinality: - if (cce.NonNull(e.E.Type).IsArrayType) { + if (e.E.Type.IsArrayType) { wr.Write("new BigInteger("); TrParenExpr(e.E); wr.Write(".Length)"); @@ -2214,11 +2214,11 @@ namespace Microsoft.Dafny { } else if (expr is ConversionExpr) { var e = (ConversionExpr)expr; if (e.ToType is IntType) { - Contract.Assert(e.E.Type is RealType); + Contract.Assert(e.E.Type.IsRealType); TrParenExpr(e.E); wr.Write(".ToBigInteger()"); } else if (e.ToType is RealType) { - Contract.Assert(e.E.Type is IntType); + Contract.Assert(e.E.Type.IsIntegerType); wr.Write("new Dafny.BigRational("); TrExpr(e.E); wr.Write(", BigInteger.One)"); @@ -2243,10 +2243,9 @@ namespace Microsoft.Dafny { opString = "&&"; break; case BinaryExpr.ResolvedOpcode.EqCommon: { - Type t = cce.NonNull(e.E0.Type); - if (t.IsDatatype || t.IsTypeParameter) { + if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter) { callString = "Equals"; - } else if (t.IsRefType) { + } else if (e.E0.Type.IsRefType) { // Dafny's type rules are slightly different C#, so we may need a cast here. // For example, Dafny allows x==y if x:array and y:array and T is some // type parameter. @@ -2257,11 +2256,10 @@ namespace Microsoft.Dafny { break; } case BinaryExpr.ResolvedOpcode.NeqCommon: { - Type t = cce.NonNull(e.E0.Type); - if (t.IsDatatype || t.IsTypeParameter) { + if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter) { preOpString = "!"; callString = "Equals"; - } else if (t.IsRefType) { + } else if (e.E0.Type.IsRefType) { // Dafny's type rules are slightly different C#, so we may need a cast here. // For example, Dafny allows x==y if x:array and y:array and T is some // type parameter. @@ -2287,7 +2285,7 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.Mul: opString = "*"; break; case BinaryExpr.ResolvedOpcode.Div: - if (expr.Type is IntType) { + if (expr.Type.IsIntegerType) { wr.Write("Dafny.Helpers.EuclideanDivision("); TrParenExpr(e.E0); wr.Write(", "); @@ -2298,7 +2296,7 @@ namespace Microsoft.Dafny { } break; case BinaryExpr.ResolvedOpcode.Mod: - if (expr.Type is IntType) { + if (expr.Type.IsIntegerType) { wr.Write("Dafny.Helpers.EuclideanModulus("); TrParenExpr(e.E0); wr.Write(", "); @@ -2453,7 +2451,7 @@ namespace Microsoft.Dafny { wr.Write("throw new System.Exception();"); } else { int i = 0; - var sourceType = (UserDefinedType)e.Source.Type; + var sourceType = (UserDefinedType)e.Source.Type.NormalizeExpand(); foreach (MatchCaseExpr mc in e.Cases) { MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, 0); wr.Write("return "); @@ -2536,7 +2534,7 @@ namespace Microsoft.Dafny { // return Dafny.Set.FromCollection(_coll); // })() Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds - var typeName = TypeName(((SetType)e.Type).Arg); + var typeName = TypeName(e.Type.AsSetType.Arg); wr.Write("((Dafny.Helpers.ComprehensionDelegate<{0}>)delegate() {{ ", typeName); wr.Write("var _coll = new System.Collections.Generic.List<{0}>(); ", typeName); var n = e.BoundVars.Count; @@ -2605,8 +2603,8 @@ namespace Microsoft.Dafny { // return Dafny.Map.FromElements(_coll); // })() Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds - var domtypeName = TypeName(((MapType)e.Type).Domain); - var rantypeName = TypeName(((MapType)e.Type).Range); + var domtypeName = TypeName(e.Type.AsMapType.Domain); + var rantypeName = TypeName(e.Type.AsMapType.Range); wr.Write("((Dafny.Helpers.MapComprehensionDelegate<{0},{1}>)delegate() {{ ", domtypeName, rantypeName); wr.Write("var _coll = new System.Collections.Generic.List>(); ", domtypeName, rantypeName); var n = e.BoundVars.Count; diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 21227dd6..7f86e078 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -130,7 +130,6 @@ namespace Microsoft.Dafny { arrayTypeDecls.Add(dims, arrayClass); SystemModule.TopLevelDecls.Add(arrayClass); } - udt.ResolvedClass = arrayTypeDecls[dims]; return udt; } @@ -331,6 +330,7 @@ namespace Microsoft.Dafny { /// /// Return the type that "this" stands for, getting to the bottom of proxies and following type synonyms. /// + [Pure] public Type NormalizeExpand() { Contract.Ensures(Contract.Result() != null); Contract.Ensures(!(Contract.Result() is TypeProxy) || ((TypeProxy)Contract.Result()).T == null); // return a proxy only if .T == null @@ -357,19 +357,32 @@ namespace Microsoft.Dafny { } } + /// + /// Returns whether or not "this" and "that" denote the same type, module proxies and type synonyms. + /// [Pure] public abstract bool Equals(Type that); + public bool IsBoolType { get { return NormalizeExpand() is BoolType; } } + public bool IsIntegerType { get { return NormalizeExpand() is IntType; } } + public bool IsRealType { get { return NormalizeExpand() is RealType; } } public bool IsSubrangeType { - get { return this is NatType; } + get { return NormalizeExpand() is NatType; } } + public CollectionType AsCollectionType { get { return NormalizeExpand() as CollectionType; } } + public SetType AsSetType { get { return NormalizeExpand() as SetType; } } + public MultiSetType AsMultiSetType { get { return NormalizeExpand() as MultiSetType; } } + public SeqType AsSeqType { get { return NormalizeExpand() as SeqType; } } + public MapType AsMapType { get { return NormalizeExpand() as MapType; } } + public bool IsRefType { get { - if (this is ObjectType) { + var t = NormalizeExpand(); + if (t is ObjectType) { return true; } else { - UserDefinedType udt = this as UserDefinedType; + var udt = t as UserDefinedType; return udt != null && udt.ResolvedParam == null && udt.ResolvedClass is ClassDecl; } } @@ -381,13 +394,14 @@ namespace Microsoft.Dafny { } public ArrayClassDecl/*?*/ AsArrayType { get { - UserDefinedType udt = UserDefinedType.DenotesClass(this); + var t = NormalizeExpand(); + var udt = UserDefinedType.DenotesClass(t); return udt == null ? null : udt.ResolvedClass as ArrayClassDecl; } } public TypeSynonymDecl AsTypeSynonym { get { - var udt = this as UserDefinedType; + var udt = this as UserDefinedType; // note, it is important to use 'this' here, not 'this.NormalizeExpand()' if (udt == null) { return null; } else { @@ -402,7 +416,7 @@ namespace Microsoft.Dafny { } public DatatypeDecl AsDatatype { get { - UserDefinedType udt = this as UserDefinedType; + var udt = NormalizeExpand() as UserDefinedType; if (udt == null) { return null; } else { @@ -417,7 +431,7 @@ namespace Microsoft.Dafny { } public IndDatatypeDecl AsIndDatatype { get { - UserDefinedType udt = this as UserDefinedType; + var udt = NormalizeExpand() as UserDefinedType; if (udt == null) { return null; } else { @@ -432,7 +446,7 @@ namespace Microsoft.Dafny { } public CoDatatypeDecl AsCoDatatype { get { - UserDefinedType udt = this as UserDefinedType; + var udt = NormalizeExpand() as UserDefinedType; if (udt == null) { return null; } else { @@ -452,7 +466,7 @@ namespace Microsoft.Dafny { } public TypeParameter AsTypeParameter { get { - UserDefinedType ct = this as UserDefinedType; + var ct = NormalizeExpand() as UserDefinedType; return ct == null ? null : ct.ResolvedParam; } } @@ -466,7 +480,9 @@ namespace Microsoft.Dafny { /// Returns true if it is known how to meaningfully compare the type's inhabitants. /// public bool IsOrdered { - get { return !IsTypeParameter && !IsCoDatatype; } + get { + return !IsTypeParameter && !IsCoDatatype; + } } public void ForeachTypeComponent(Action action) { @@ -492,7 +508,7 @@ namespace Microsoft.Dafny { return "bool"; } public override bool Equals(Type that) { - return that.NormalizeExpand() is BoolType; + return that.IsBoolType; } } @@ -762,8 +778,14 @@ namespace Microsoft.Dafny { } public override bool Equals(Type that) { - var t = that.NormalizeExpand() as UserDefinedType; - return t != null && ResolvedClass == t.ResolvedClass && ResolvedParam == t.ResolvedParam; + var i = NormalizeExpand(); + if (i is UserDefinedType) { + var ii = (UserDefinedType)i; + var t = that.NormalizeExpand() as UserDefinedType; + return t != null && ii.ResolvedClass == t.ResolvedClass && ii.ResolvedParam == t.ResolvedParam; + } else { + return i.Equals(that); + } } /// @@ -800,6 +822,11 @@ namespace Microsoft.Dafny { if (BuiltIns.IsTupleTypeName(Name)) { return "(" + Util.Comma(",", TypeArgs, ty => ty.TypeName(context)) + ")"; } else { +#if TEST_TYPE_SYNONYM_TRANSPARENCY + if (Name == "type#synonym#transparency#test" && ResolvedClass is TypeSynonymDecl) { + return ((TypeSynonymDecl)ResolvedClass).Rhs.TypeName(context); + } +#endif string s = ""; foreach (var t in Path) { if (context != null && t == context.tok) { @@ -4278,6 +4305,13 @@ namespace Microsoft.Dafny { type = value.Normalize(); } } +#if TEST_TYPE_SYNONYM_TRANSPARENCY + public void DebugTest_ChangeType(Type ty) { + Contract.Requires(WasResolved()); // we're here to set it again + Contract.Requires(ty != null); + type = ty; + } +#endif public Expression(IToken tok) { Contract.Requires(tok != null); @@ -4295,7 +4329,7 @@ namespace Microsoft.Dafny { public static IEnumerable Conjuncts(Expression expr) { Contract.Requires(expr != null); - Contract.Requires(expr.Type is BoolType); + Contract.Requires(expr.Type.IsBoolType); Contract.Ensures(cce.NonNullElements(Contract.Result>())); // strip off parens @@ -4327,7 +4361,7 @@ namespace Microsoft.Dafny { public static Expression CreateAdd(Expression e0, Expression e1) { Contract.Requires(e0 != null); Contract.Requires(e1 != null); - Contract.Requires((e0.Type is IntType && e1.Type is IntType) || (e0.Type is RealType && e1.Type is RealType)); + Contract.Requires((e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType) || (e0.Type.NormalizeExpand() is RealType && e1.Type.NormalizeExpand() is RealType)); Contract.Ensures(Contract.Result() != null); var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Add, e0, e1); s.ResolvedOp = BinaryExpr.ResolvedOpcode.Add; // resolve here @@ -4341,7 +4375,7 @@ namespace Microsoft.Dafny { public static Expression CreateSubtract(Expression e0, Expression e1) { Contract.Requires(e0 != null); Contract.Requires(e1 != null); - Contract.Requires((e0.Type is IntType && e1.Type is IntType) || (e0.Type is RealType && e1.Type is RealType)); + Contract.Requires((e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType) || (e0.Type.NormalizeExpand() is RealType && e1.Type.NormalizeExpand() is RealType)); Contract.Ensures(Contract.Result() != null); var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Sub, e0, e1); s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub; // resolve here @@ -4354,7 +4388,7 @@ namespace Microsoft.Dafny { /// public static Expression CreateIncrement(Expression e, int n) { Contract.Requires(e != null); - Contract.Requires(e.Type is IntType); + Contract.Requires(e.Type.NormalizeExpand() is IntType); Contract.Requires(0 <= n); Contract.Ensures(Contract.Result() != null); if (n == 0) { @@ -4369,7 +4403,7 @@ namespace Microsoft.Dafny { /// public static Expression CreateDecrement(Expression e, int n) { Contract.Requires(e != null); - Contract.Requires(e.Type is IntType); + Contract.Requires(e.Type.NormalizeExpand() is IntType); Contract.Requires(0 <= n); Contract.Ensures(Contract.Result() != null); if (n == 0) { @@ -4406,7 +4440,7 @@ namespace Microsoft.Dafny { public static Expression CreateNot(IToken tok, Expression e) { Contract.Requires(tok != null); - Contract.Requires(e.Type is BoolType); + Contract.Requires(e.Type.IsBoolType); var un = new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Not, e); un.Type = Type.Bool; // resolve here return un; @@ -4418,7 +4452,7 @@ namespace Microsoft.Dafny { public static Expression CreateLess(Expression e0, Expression e1) { Contract.Requires(e0 != null); Contract.Requires(e1 != null); - Contract.Requires(e0.Type is IntType && e1.Type is IntType); + Contract.Requires(e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType); Contract.Ensures(Contract.Result() != null); var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Lt, e0, e1); s.ResolvedOp = BinaryExpr.ResolvedOpcode.Lt; // resolve here @@ -4432,7 +4466,7 @@ namespace Microsoft.Dafny { public static Expression CreateAtMost(Expression e0, Expression e1) { Contract.Requires(e0 != null); Contract.Requires(e1 != null); - Contract.Requires((e0.Type is IntType && e1.Type is IntType) || (e0.Type is RealType && e1.Type is RealType)); + Contract.Requires((e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType) || (e0.Type.NormalizeExpand() is RealType && e1.Type.NormalizeExpand() is RealType)); Contract.Ensures(Contract.Result() != null); var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Le, e0, e1); s.ResolvedOp = BinaryExpr.ResolvedOpcode.Le; // resolve here @@ -4466,7 +4500,7 @@ namespace Microsoft.Dafny { public static Expression CreateAnd(Expression a, Expression b) { Contract.Requires(a != null); Contract.Requires(b != null); - Contract.Requires(a.Type is BoolType && b.Type is BoolType); + Contract.Requires(a.Type.IsBoolType && b.Type.IsBoolType); Contract.Ensures(Contract.Result() != null); if (LiteralExpr.IsTrue(a)) { return b; @@ -4486,7 +4520,7 @@ namespace Microsoft.Dafny { public static Expression CreateImplies(Expression a, Expression b) { Contract.Requires(a != null); Contract.Requires(b != null); - Contract.Requires(a.Type is BoolType && b.Type is BoolType); + Contract.Requires(a.Type.IsBoolType && b.Type.IsBoolType); Contract.Ensures(Contract.Result() != null); if (LiteralExpr.IsTrue(a) || LiteralExpr.IsTrue(b)) { return b; @@ -4505,7 +4539,7 @@ namespace Microsoft.Dafny { Contract.Requires(test != null); Contract.Requires(e0 != null); Contract.Requires(e1 != null); - Contract.Requires(test.Type is BoolType && e0.Type.Equals(e1.Type)); + Contract.Requires(test.Type.IsBoolType && e0.Type.Equals(e1.Type)); Contract.Ensures(Contract.Result() != null); var ite = new ITEExpr(test.tok, test, e0, e1); ite.Type = e0.type; // resolve here diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 5e7381d9..02af6e12 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -474,16 +474,17 @@ namespace Microsoft.Dafny } else { Expression e = fe.E; // keep only fe.E, drop any fe.Field designation Contract.Assert(e.Type != null); // should have been resolved already - if (e.Type.IsRefType) { + var eType = e.Type.NormalizeExpand(); + if (eType.IsRefType) { // e represents a singleton set if (singletons == null) { singletons = new List(); } singletons.Add(e); - } else if (e.Type is SeqType) { + } else if (eType is SeqType) { // e represents a sequence // Add: set x :: x in e - var bv = new BoundVar(e.tok, "_s2s_" + tmpVarCount, ((SeqType)e.Type).Arg); + var bv = new BoundVar(e.tok, "_s2s_" + tmpVarCount, ((SeqType)eType).Arg); tmpVarCount++; var bvIE = new IdentifierExpr(e.tok, bv.Name); bvIE.Var = bv; // resolve here @@ -496,7 +497,7 @@ namespace Microsoft.Dafny sets.Add(s); } else { // e is already a set - Contract.Assert(e.Type is SetType); + Contract.Assert(eType is SetType); sets.Add(e); } } @@ -2014,7 +2015,7 @@ namespace Microsoft.Dafny Contract.Requires(tok != null); Contract.Requires(t != null); Contract.Requires(what != null); - t = t.Normalize(); + t = t.NormalizeExpand(); if (t is TypeProxy && (aggressive || !(t is InferredTypeProxy || t is ParamTypeProxy || t is ObjectTypeProxy))) { Error(tok, "the type of this {0} is underspecified, but it cannot be an opaque type.", what); return false; @@ -2884,11 +2885,12 @@ namespace Microsoft.Dafny } } - void AddDatatypeDependencyEdge(IndDatatypeDecl/*!*/ dt, Type/*!*/ tp, Graph/*!*/ dependencies) { + void AddDatatypeDependencyEdge(IndDatatypeDecl dt, Type tp, Graph dependencies) { Contract.Requires(dt != null); Contract.Requires(tp != null); Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies)); + tp = tp.NormalizeExpand(); var dependee = tp.AsIndDatatype; if (dependee != null && dt.Module == dependee.Module) { dependencies.AddEdge(dt, dependee); @@ -2981,6 +2983,7 @@ namespace Microsoft.Dafny } bool CheckCanBeConstructed(Type tp, List typeParametersUsed) { + tp = tp.NormalizeExpand(); var dependee = tp.AsIndDatatype; if (dependee == null) { // the type is not an inductive datatype, which means it is always possible to construct it @@ -3213,8 +3216,9 @@ namespace Microsoft.Dafny ResolveExpression(fe.E, false, codeContext); Type t = fe.E.Type; Contract.Assert(t != null); // follows from postcondition of ResolveExpression - if (t is CollectionType) { - t = ((CollectionType)t).Arg; + var collType = t.AsCollectionType; + if (collType != null) { + t = collType.Arg; } if (!UnifyTypes(t, new ObjectType())) { Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", kind, fe.E.Type); @@ -3756,6 +3760,10 @@ namespace Microsoft.Dafny } } else if (type is UserDefinedType) { var t = (UserDefinedType)type; + if (t.ResolvedClass != null || t.ResolvedParam != null) { + // Apparently, this type has already been resolved + return null; + } foreach (Type tt in t.TypeArgs) { ResolveType(t.tok, tt, option, defaultTypeArguments); if (tt.IsSubrangeType) { @@ -3989,7 +3997,7 @@ namespace Microsoft.Dafny // In the remaining cases, proxy is a restricted proxy and t is a non-proxy } else if (proxy is DatatypeProxy) { var dtp = (DatatypeProxy)proxy; - if (!dtp.Co && t.IsIndDatatype) { + if (!dtp.Co && t.NormalizeExpand().IsIndDatatype) { // all is fine, proxy can be redirected to t } else if (dtp.Co && t.IsCoDatatype) { // all is fine, proxy can be redirected to t @@ -4032,7 +4040,7 @@ namespace Microsoft.Dafny } else if (!UnifyTypes(iProxy.Arg, iProxy.Range)) { return false; } - } else if (iProxy.AllowArray && t.IsArrayType && (t.AsArrayType).Dims == 1) { + } else if (iProxy.AllowArray && t.IsArrayType && t.AsArrayType.Dims == 1) { Type elType = UserDefinedType.ArrayElementType(t); if (!UnifyTypes(iProxy.Domain, Type.Int)) { return false; @@ -4099,7 +4107,7 @@ namespace Microsoft.Dafny } else if (b is IndexableTypeProxy && ((IndexableTypeProxy)b).AllowArray) { var ib = (IndexableTypeProxy)b; // the intersection of ObjectTypeProxy and IndexableTypeProxy is an array type - a.T = builtIns.ArrayType(1, ib.Arg); + a.T = ResolvedArrayType(Token.NoToken, 1, ib.Arg); b.T = a.T; return UnifyTypes(ib.Arg, ib.Range); } else { @@ -4180,6 +4188,20 @@ namespace Microsoft.Dafny } } + /// + /// Returns a resolved type denoting an array type with dimension "dims" and element type "arg". + /// Callers are expected to provide "arg" as an already resolved type. (Note, a proxy type is resolved-- + /// only types that contain identifiers stand the possibility of not being resolved.) + /// + Type ResolvedArrayType(IToken tok, int dims, Type arg) { + Contract.Requires(tok != null); + Contract.Requires(1 <= dims); + Contract.Requires(arg != null); + var at = builtIns.ArrayType(tok, dims, new List { arg }, false); + ResolveType(tok, at, ResolveTypeOptionEnum.DontInfer, null); + return at; + } + /// /// "specContextOnly" means that the statement must be erasable, that is, it should be okay to omit it /// at run time. That means it must not have any side effects on non-ghost variables, for example. @@ -4367,7 +4389,7 @@ namespace Microsoft.Dafny { Error(local.Tok, "assumption variable must be ghost"); } - if (!(local.Type is BoolType)) + if (!(local.Type.IsBoolType)) { Error(s, "assumption variable must be of type 'bool'"); } @@ -4761,7 +4783,7 @@ namespace Microsoft.Dafny } UserDefinedType sourceType = null; DatatypeDecl dtd = null; - if (s.Source.Type.NormalizeExpand().IsDatatype) { + if (s.Source.Type.IsDatatype) { sourceType = (UserDefinedType)s.Source.Type.NormalizeExpand(); dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass); } @@ -4875,7 +4897,7 @@ namespace Microsoft.Dafny guess = Expression.CreateSubtract(bin.E0, bin.E1); break; case BinaryExpr.ResolvedOpcode.NeqCommon: - if (bin.E0.Type is IntType || bin.E0.Type is RealType) { + if (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType) { // for A != B where A and B are integers, use the absolute difference between A and B (that is: if A <= B then B-A else A-B) var AminusB = Expression.CreateSubtract(bin.E0, bin.E1); var BminusA = Expression.CreateSubtract(bin.E1, bin.E0); @@ -5318,7 +5340,7 @@ namespace Microsoft.Dafny } } else if (lhs is SeqSelectExpr) { var ll = (SeqSelectExpr)lhs; - if (!UnifyTypes(ll.Seq.Type, builtIns.ArrayType(1, new InferredTypeProxy()))) { + if (!UnifyTypes(ll.Seq.Type, ResolvedArrayType(ll.Seq.tok, 1, new InferredTypeProxy()))) { Error(ll.Seq, "LHS of array assignment must denote an array element (found {0})", ll.Seq.Type); } if (!ll.SelectOne) { @@ -5621,8 +5643,6 @@ namespace Microsoft.Dafny } } - - Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, ICodeContext codeContext) { Contract.Requires(rr != null); Contract.Requires(stmt != null); @@ -5639,9 +5659,6 @@ namespace Microsoft.Dafny Contract.Assert(rr.Arguments == null && rr.OptionalNameComponent == null && rr.InitCall == null); ResolveType(stmt.Tok, rr.EType, ResolveTypeOptionEnum.InferTypeProxies, null); int i = 0; - if (rr.EType.IsSubrangeType) { - Error(stmt, "sorry, cannot instantiate 'array' type with a subrange type"); - } foreach (Expression dim in rr.ArrayDimensions) { Contract.Assert(dim != null); ResolveExpression(dim, true, codeContext); @@ -5650,7 +5667,7 @@ namespace Microsoft.Dafny } i++; } - rr.Type = builtIns.ArrayType(rr.ArrayDimensions.Count, rr.EType); + rr.Type = ResolvedArrayType(stmt.Tok, rr.ArrayDimensions.Count, rr.EType); } else { var initCallTok = rr.Tok; if (rr.OptionalNameComponent == null && rr.Arguments != null) { @@ -5690,8 +5707,8 @@ namespace Microsoft.Dafny // ---------- new C Contract.Assert(rr.ArrayDimensions == null && rr.OptionalNameComponent == null && rr.InitCall == null); } - if (!callsConstructor && rr.EType is UserDefinedType) { - var udt = (UserDefinedType)rr.EType; + if (!callsConstructor && rr.EType.NormalizeExpand() is UserDefinedType) { + var udt = (UserDefinedType)rr.EType.NormalizeExpand(); var cl = (ClassDecl)udt.ResolvedClass; // cast is guaranteed by the call to rr.EType.IsRefType above, together with the "rr.EType is UserDefinedType" test if (cl.HasConstructor) { Error(stmt, "when allocating an object of type '{0}', one of its constructor methods must be called", cl.Name); @@ -5823,6 +5840,20 @@ namespace Microsoft.Dafny } } else if (t.ResolvedClass != null) { List newArgs = null; // allocate it lazily + var resolvedClass = t.ResolvedClass; +#if TEST_TYPE_SYNONYM_TRANSPARENCY + if (resolvedClass is TypeSynonymDecl && resolvedClass.Name == "type#synonym#transparency#test") { + // Usually, all type parameters mentioned in the definition of a type synonym are also type parameters + // to the type synonym itself, but in this instrumented testing, that is not so, so we also do a substitution + // in the .Rhs of the synonym. + var syn = (TypeSynonymDecl)resolvedClass; + var r = SubstType(syn.Rhs, subst); + if (r != syn.Rhs) { + resolvedClass = new TypeSynonymDecl(syn.tok, syn.Name, syn.TypeArgs, syn.Module, r, null); + newArgs = new List(); + } + } +#endif for (int i = 0; i < t.TypeArgs.Count; i++) { Type p = t.TypeArgs[i]; Type s = SubstType(p, subst); @@ -5841,7 +5872,7 @@ namespace Microsoft.Dafny // there were no substitutions return type; } else { - return new UserDefinedType(t.tok, t.Name, t.ResolvedClass, newArgs, t.Path); + return new UserDefinedType(t.tok, t.Name, resolvedClass, newArgs, t.Path); } } else { // there's neither a resolved param nor a resolved class, which means the UserDefinedType wasn't @@ -5887,6 +5918,17 @@ namespace Microsoft.Dafny /// "twoState" implies that "old" and "fresh" expressions are allowed. /// public void ResolveExpression(Expression expr, bool twoState, ICodeContext codeContext) { +#if TEST_TYPE_SYNONYM_TRANSPARENCY + ResolveExpressionX(expr, twoState, codeContext); + // For testing purposes, change the type of "expr" to a type synonym (mwo-ha-ha-ha!) + var t = expr.Type; + Contract.Assert(t != null); + var sd = new TypeSynonymDecl(expr.tok, "type#synonym#transparency#test", new List(), codeContext.EnclosingModule, t, null); + var ts = new UserDefinedType(expr.tok, "type#synonym#transparency#test", sd, new List(), null); + expr.DebugTest_ChangeType(ts); + } + public void ResolveExpressionX(Expression expr, bool twoState, ICodeContext codeContext) { +#endif Contract.Requires(expr != null); Contract.Requires(codeContext != null); Contract.Ensures(expr.Type != null); @@ -5928,7 +5970,7 @@ namespace Microsoft.Dafny e.ResolvedExpression = e.E; } else { Expression zero; - if (e.E.Type is RealType) { + if (e.E.Type.IsRealType) { // we know for sure that this is a real-unary-minus zero = new LiteralExpr(e.tok, Basetypes.BigDec.ZERO); } else { @@ -6079,7 +6121,7 @@ namespace Microsoft.Dafny ResolveExpression(e.Array, twoState, codeContext); Contract.Assert(e.Array.Type != null); // follows from postcondition of ResolveExpression Type elementType = new InferredTypeProxy(); - if (!UnifyTypes(e.Array.Type, builtIns.ArrayType(e.Indices.Count, elementType))) { + if (!UnifyTypes(e.Array.Type, ResolvedArrayType(e.Array.tok, e.Indices.Count, elementType))) { Error(e.Array, "array selection requires an array{0} (got {1})", e.Indices.Count, e.Array.Type); } int i = 0; @@ -6134,8 +6176,8 @@ namespace Microsoft.Dafny } expr.Type = e.Seq.Type; - } else if (e.Seq.Type is UserDefinedType && ((UserDefinedType)e.Seq.Type).IsDatatype) { - DatatypeDecl dt = ((UserDefinedType)e.Seq.Type).AsDatatype; + } else if (e.Seq.Type.IsDatatype) { + var dt = e.Seq.Type.AsDatatype; if (!(e.Index is IdentifierSequence || (e.Index is LiteralExpr && ((LiteralExpr)e.Index).Value is BigInteger))) { Error(expr, "datatype updates must be to datatype destructors"); @@ -6203,7 +6245,7 @@ namespace Microsoft.Dafny if (!UnifyTypes(e.E.Type, new SetType(new InferredTypeProxy())) && !UnifyTypes(e.E.Type, new SeqType(new InferredTypeProxy()))) { Error(e.tok, "can only form a multiset from a seq or set."); } - expr.Type = new MultiSetType(((CollectionType)e.E.Type).Arg); + expr.Type = new MultiSetType(e.E.Type.AsCollectionType.Arg); } else if (expr is UnaryOpExpr) { var e = (UnaryOpExpr)expr; @@ -6227,10 +6269,10 @@ namespace Microsoft.Dafny Error(expr, "fresh expressions are not allowed in this context"); } // the type of e.E must be either an object or a collection of objects - Type t = e.E.Type; + Type t = e.E.Type.NormalizeExpand(); Contract.Assert(t != null); // follows from postcondition of ResolveExpression if (t is CollectionType) { - t = ((CollectionType)t).Arg; + t = ((CollectionType)t).Arg.NormalizeExpand(); } if (t is ObjectType) { // fine @@ -6252,11 +6294,11 @@ namespace Microsoft.Dafny ResolveType(e.tok, e.ToType, new ResolveTypeOption(ResolveTypeOptionEnum.DontInfer), null); ResolveExpression(e.E, twoState, codeContext); if (e.ToType is IntType) { - if (!(e.E.Type is RealType)) { + if (!(e.E.Type.IsRealType)) { Error(expr, "type conversion to int is allowed only from real (got {0})", e.E.Type); } } else if (e.ToType is RealType) { - if (!(e.E.Type is IntType)) { + if (!(e.E.Type.IsIntegerType)) { Error(expr, "type conversion to real is allowed only from int (got {0})", e.E.Type); } } else { @@ -6322,14 +6364,14 @@ namespace Microsoft.Dafny case BinaryExpr.Opcode.Lt: case BinaryExpr.Opcode.Le: case BinaryExpr.Opcode.Add: { - if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsIndDatatype) { + if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.NormalizeExpand().IsIndDatatype) { if (UnifyTypes(e.E1.Type, new DatatypeProxy(false))) { e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankLt; } else { Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type); } expr.Type = Type.Bool; - } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsIndDatatype) { + } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.NormalizeExpand().IsIndDatatype) { if (UnifyTypes(e.E0.Type, new DatatypeProxy(false))) { e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankLt; } else { @@ -6359,14 +6401,14 @@ namespace Microsoft.Dafny case BinaryExpr.Opcode.Mul: case BinaryExpr.Opcode.Gt: case BinaryExpr.Opcode.Ge: { - if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsIndDatatype) { + if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.NormalizeExpand().IsIndDatatype) { if (UnifyTypes(e.E1.Type, new DatatypeProxy(false))) { e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankGt; } else { Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type); } expr.Type = Type.Bool; - } else if (e.Op == BinaryExpr.Opcode.Gt && e.E1.Type.IsIndDatatype) { + } else if (e.Op == BinaryExpr.Opcode.Gt && e.E1.Type.NormalizeExpand().IsIndDatatype) { if (UnifyTypes(e.E0.Type, new DatatypeProxy(false))) { e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankGt; } else { @@ -6684,7 +6726,7 @@ namespace Microsoft.Dafny Contract.Assert(me.Source.Type != null); // follows from postcondition of ResolveExpression UserDefinedType sourceType = null; DatatypeDecl dtd = null; - if (me.Source.Type.NormalizeExpand().IsDatatype) { + if (me.Source.Type.IsDatatype) { sourceType = (UserDefinedType)me.Source.Type.NormalizeExpand(); dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass); } @@ -6779,7 +6821,7 @@ namespace Microsoft.Dafny DatatypeDecl dtd = null; UserDefinedType udt = null; if (sourceType.IsDatatype) { - udt = (UserDefinedType)sourceType; + udt = (UserDefinedType)sourceType.NormalizeExpand(); dtd = (DatatypeDecl)udt.ResolvedClass; } // Find the constructor in the given datatype @@ -6870,6 +6912,8 @@ namespace Microsoft.Dafny } private bool ComparableTypes(Type A, Type B) { + A = A.NormalizeExpand(); + B = B.NormalizeExpand(); if (A.IsArrayType && B.IsArrayType) { Type a = UserDefinedType.ArrayElementType(A); Type b = UserDefinedType.ArrayElementType(B); @@ -7494,12 +7538,12 @@ namespace Microsoft.Dafny for (int j = 0; j < bvars.Count; j++) { var bv = bvars[j]; var bounds = new List(); - if (bv.Type is BoolType) { + if (bv.Type.IsBoolType) { // easy bounds.Add(new ComprehensionExpr.BoolBoundedPool()); } else { bool foundBoundsForBv = false; - if (bv.Type.IsIndDatatype && (bv.Type.AsIndDatatype).HasFinitePossibleValues) { + if (bv.Type.IsIndDatatype && bv.Type.AsIndDatatype.HasFinitePossibleValues) { bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype)); foundBoundsForBv = true; } @@ -7983,6 +8027,7 @@ namespace Microsoft.Dafny /// public static BinaryExpr.ResolvedOpcode ResolveOp(BinaryExpr.Opcode op, Type operandType) { Contract.Requires(operandType != null); + operandType = operandType.NormalizeExpand(); switch (op) { case BinaryExpr.Opcode.Iff: return BinaryExpr.ResolvedOpcode.Iff; case BinaryExpr.Opcode.Imp: return BinaryExpr.ResolvedOpcode.Imp; diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index ca3c105d..63bb2dcc 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -174,7 +174,7 @@ namespace Microsoft.Dafny } } else if (member is Function && member.Name == "Valid" && !member.IsStatic) { var fn = (Function)member; - if (fn.Formals.Count == 0 && fn.ResultType is BoolType) { + if (fn.Formals.Count == 0 && fn.ResultType.IsBoolType) { Valid = fn; } } @@ -201,7 +201,7 @@ namespace Microsoft.Dafny Boogie.IToken tok = new AutoGeneratedToken(member.tok); if (member is Function && member.Name == "Valid" && !member.IsStatic) { var valid = (Function)member; - if (valid.IsGhost && valid.ResultType is BoolType) { + if (valid.IsGhost && valid.ResultType.IsBoolType) { Expression c; if (valid.RefinementBase == null) { var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, self, Repr); // this in Repr @@ -265,7 +265,7 @@ namespace Microsoft.Dafny var valid = new FunctionCallExpr(tok, "Valid", implicitSelf, tok, new List()); valid.Function = Valid; valid.Type = Type.Bool; - // Add the identity substitution to this call + // Add the identity substitution to this call valid.TypeArgumentSubstitutions = new Dictionary(); foreach (var p in cl.TypeArgs) { valid.TypeArgumentSubstitutions.Add(p, new UserDefinedType(p)); diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index a936200e..330afd8a 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -598,17 +598,18 @@ namespace Microsoft.Dafny { sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q, "Constructor injectivity")); if (dt is IndDatatypeDecl) { - if (arg.Type.IsDatatype || arg.Type.IsTypeParameter) { + var argType = arg.Type.NormalizeExpand(); + if (argType.IsDatatype || argType.IsTypeParameter) { // for datatype: axiom (forall params :: DtRank(params_i) < DtRank(#dt.ctor(params))); // for type-parameter type: axiom (forall params :: DtRank(Unbox(params_i)) < DtRank(#dt.ctor(params))); CreateBoundVariables(ctor.Formals, out bvs, out args); Bpl.Expr lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, - arg.Type.IsDatatype ? args[i] : FunctionCall(ctor.tok, BuiltinFunction.Unbox, predef.DatatypeType, args[i])); + argType.IsDatatype ? args[i] : FunctionCall(ctor.tok, BuiltinFunction.Unbox, predef.DatatypeType, args[i])); Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs); q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Lt(lhs, rhs)); sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q, "Inductive rank")); - } else if (arg.Type is SeqType) { + } else if (argType is SeqType) { // axiom (forall params, i: int :: 0 <= i && i < |arg| ==> DtRank(arg[i]) < DtRank(#dt.ctor(params))); // that is: // axiom (forall params, i: int :: 0 <= i && i < |arg| ==> DtRank(Unbox(Seq#Index(arg,i))) < DtRank(#dt.ctor(params))); @@ -633,7 +634,7 @@ namespace Microsoft.Dafny { rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs); q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Lt(lhs, rhs)); sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q, "Inductive seq rank")); - } else if (arg.Type is SetType) { + } else if (argType is SetType) { // axiom (forall params, d: Datatype :: arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params))); // that is: // axiom (forall params, d: Datatype :: arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params))); @@ -647,7 +648,7 @@ namespace Microsoft.Dafny { rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs); q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs))); sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q, "Inductive set rank")); - } else if (arg.Type is MultiSetType) { + } else if (argType is MultiSetType) { // axiom (forall params, d: Datatype :: 0 < arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params))); // that is: // axiom (forall params, d: Datatype :: 0 < arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params))); @@ -946,6 +947,12 @@ namespace Microsoft.Dafny { // Makes a call to equality, if k is null, or otherwise prefix equality. For codatatypes. Bpl.Expr CoEqualCall(CoDatatypeDecl codecl, List largs, List rargs, Bpl.Expr k, Bpl.Expr l, Bpl.Expr A, Bpl.Expr B, IToken tok = null) { + Contract.Requires(codecl != null); + Contract.Requires(largs != null); + Contract.Requires(rargs != null); + Contract.Requires(l != null); + Contract.Requires(A != null); + Contract.Requires(B != null); if (tok == null) { tok = A.tok; } @@ -960,6 +967,12 @@ namespace Microsoft.Dafny { // Same as above, but with Dafny-typed type-argument lists Bpl.Expr CoEqualCall(CoDatatypeDecl codecl, List largs, List rargs, Bpl.Expr k, Bpl.Expr l, Bpl.Expr A, Bpl.Expr B, IToken tok = null) { + Contract.Requires(codecl != null); + Contract.Requires(largs != null); + Contract.Requires(rargs != null); + Contract.Requires(l != null); + Contract.Requires(A != null); + Contract.Requires(B != null); return CoEqualCall(codecl, Map(largs, TypeToTy), Map(rargs, TypeToTy), k, l, A, B, tok); } @@ -2447,7 +2460,7 @@ namespace Microsoft.Dafny { var decrCaller = new List(); foreach (var ee in m.Decreases.Expressions) { decrToks.Add(ee.tok); - decrTypes.Add(ee.Type); + decrTypes.Add(ee.Type.NormalizeExpand()); decrCaller.Add(exprTran.TrExpr(ee)); Expression es = Substitute(ee, receiverReplacement, substMap); es = Substitute(es, null, decrSubstMap); @@ -2951,8 +2964,8 @@ namespace Microsoft.Dafny { #endif } - Bpl.Expr/*!*/ InRWClause(IToken/*!*/ tok, Bpl.Expr/*!*/ o, Bpl.Expr/*!*/ f, List/*!*/ rw, ExpressionTranslator/*!*/ etran, - Expression receiverReplacement, Dictionary substMap) { + Bpl.Expr/*!*/ InRWClause(IToken tok, Bpl.Expr o, Bpl.Expr f, List rw, ExpressionTranslator etran, + Expression receiverReplacement, Dictionary substMap) { Contract.Requires(tok != null); Contract.Requires(o != null); Contract.Requires(f != null); @@ -2974,12 +2987,13 @@ namespace Microsoft.Dafny { e = Substitute(e, receiverReplacement, substMap); } Bpl.Expr disjunct; + var eType = e.Type.NormalizeExpand(); if (e is WildcardExpr) { disjunct = Bpl.Expr.True; - } else if (e.Type is SetType) { + } else if (eType is SetType) { // old(e)[Box(o)] - disjunct = etran.TrInSet(tok, o, e, ((SetType)e.Type).Arg); - } else if (e.Type is SeqType) { + disjunct = etran.TrInSet(tok, o, e, ((SetType)eType).Arg); + } else if (eType is SeqType) { // (exists i: int :: 0 <= i && i < Seq#Length(old(e)) && Seq#Index(old(e),i) == Box(o)) Bpl.Expr boxO = FunctionCall(tok, BuiltinFunction.Box, null, o); Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int)); @@ -3235,7 +3249,6 @@ namespace Microsoft.Dafny { } } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; - //bool isSequence = e.Seq.Type is SeqType; Bpl.Expr total = CanCallAssumption(e.Seq, etran); Bpl.Expr seq = etran.TrExpr(e.Seq); Bpl.Expr e0 = null; @@ -3571,20 +3584,21 @@ namespace Microsoft.Dafny { } } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; - bool isSequence = e.Seq.Type is SeqType; + var eSeqType = e.Seq.Type.NormalizeExpand(); + bool isSequence = eSeqType is SeqType; CheckWellformed(e.Seq, options, locals, builder, etran); Bpl.Expr seq = etran.TrExpr(e.Seq); - if (e.Seq.Type.IsArrayType) { + if (eSeqType.IsArrayType) { builder.Add(Assert(e.Seq.tok, Bpl.Expr.Neq(seq, predef.Null), "array may be null")); } Bpl.Expr e0 = null; - if (e.Seq.Type is MapType) { + if (eSeqType is MapType) { e0 = etran.TrExpr(e.E0); CheckWellformed(e.E0, options, locals, builder, etran); Bpl.Expr inDomain = FunctionCall(expr.tok, BuiltinFunction.MapDomain, predef.MapType(e.tok, predef.BoxType, predef.BoxType), seq); inDomain = Bpl.Expr.Select(inDomain, BoxIfNecessary(e.tok, e0, e.E0.Type)); builder.Add(Assert(expr.tok, inDomain, "element may not be in domain", options.AssertKv)); - } else if (e.Seq.Type is MultiSetType) { + } else if (eSeqType is MultiSetType) { // cool } else { @@ -3598,14 +3612,14 @@ namespace Microsoft.Dafny { builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true), "upper bound " + (e.E0 == null ? "" : "below lower bound or ") + "above length of " + (isSequence ? "sequence" : "array"), options.AssertKv)); } } - if (options.DoReadsChecks && e.Seq.Type.IsArrayType) { + if (options.DoReadsChecks && eSeqType.IsArrayType) { if (e.SelectOne) { Contract.Assert(e.E0 != null); Bpl.Expr fieldName = FunctionCall(expr.tok, BuiltinFunction.IndexField, null, etran.TrExpr(e.E0)); builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), seq, fieldName), "insufficient reads clause to read array element", options.AssertKv)); } else { Bpl.Expr lowerBound = e.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(e.E0); - Contract.Assert((e.Seq.Type).AsArrayType.Dims == 1); + Contract.Assert(eSeqType.AsArrayType.Dims == 1); Bpl.Expr upperBound = e.E1 == null ? ArrayLength(e.tok, seq, 1, 0) : etran.TrExpr(e.E1); // check that, for all i in lowerBound..upperBound, a[i] is in the frame Bpl.BoundVariable iVar = new Bpl.BoundVariable(e.tok, new Bpl.TypedIdent(e.tok, "$i", Bpl.Type.Int)); @@ -3645,20 +3659,14 @@ namespace Microsoft.Dafny { Bpl.Expr index = etran.TrExpr(e.Index); Bpl.Expr value = etran.TrExpr(e.Value); CheckWellformed(e.Index, options, locals, builder, etran); - if (e.Seq.Type is SeqType) - { + var eSeqType = e.Seq.Type.NormalizeExpand(); + if (eSeqType is SeqType) { builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, true, null, false), "index out of range", options.AssertKv)); - } - else if (e.Seq.Type is MapType) - { + } else if (eSeqType is MapType) { // updates to maps are always valid if the values are well formed - } - else if (e.Seq.Type is MultiSetType) - { + } else if (eSeqType is MultiSetType) { builder.Add(Assert(expr.tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), value), "new number of occurrences might be negative", options.AssertKv)); - } - else - { + } else { Contract.Assert(false); } CheckWellformed(e.Value, options, locals, builder, etran); @@ -3834,7 +3842,7 @@ namespace Microsoft.Dafny { break; case BinaryExpr.ResolvedOpcode.Div: case BinaryExpr.ResolvedOpcode.Mod: { - Bpl.Expr zero = (e.E1.Type is RealType) ? Bpl.Expr.Literal(Basetypes.BigDec.ZERO) : Bpl.Expr.Literal(0); + Bpl.Expr zero = (e.E1.Type.IsRealType) ? Bpl.Expr.Literal(Basetypes.BigDec.ZERO) : Bpl.Expr.Literal(0); CheckWellformed(e.E1, options, locals, builder, etran); builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E1), zero), "possible division by zero", options.AssertKv)); } @@ -5725,7 +5733,8 @@ namespace Microsoft.Dafny { IEnumerable GuessWitnesses(BoundVar x, Expression expr) { Contract.Requires(x != null); Contract.Requires(expr != null); - if (x.Type is BoolType) { + var xType = x.Type.NormalizeExpand(); + if (xType is BoolType) { var lit = new LiteralExpr(x.tok, false); lit.Type = Type.Bool; // resolve here yield return lit; @@ -5733,13 +5742,13 @@ namespace Microsoft.Dafny { lit.Type = Type.Bool; // resolve here yield return lit; yield break; // there are no more possible witnesses for booleans - } else if (x.Type.IsRefType) { + } else if (xType.IsRefType) { var lit = new LiteralExpr(x.tok); // null - lit.Type = x.Type; + lit.Type = xType; yield return lit; - } else if (x.Type.IsDatatype) { - var dt = x.Type.AsDatatype; - Expression zero = Zero(x.tok, x.Type); + } else if (xType.IsDatatype) { + var dt = xType.AsDatatype; + Expression zero = Zero(x.tok, xType); if (zero != null) { yield return zero; } @@ -5747,28 +5756,28 @@ namespace Microsoft.Dafny { if (ctor.Formals.Count == 0) { var v = new DatatypeValue(x.tok, dt.Name, ctor.Name, new List()); v.Ctor = ctor; // resolve here - v.InferredTypeArgs = x.Type.TypeArgs; // resolved here. + v.InferredTypeArgs = xType.TypeArgs; // resolved here. v.Type = new UserDefinedType(x.tok, dt.Name, dt, new List()); // resolve here yield return v; } } - } else if (x.Type is SetType) { + } else if (xType is SetType) { var empty = new SetDisplayExpr(x.tok, new List()); - empty.Type = x.Type; + empty.Type = xType; yield return empty; - } else if (x.Type is MultiSetType) { + } else if (xType is MultiSetType) { var empty = new MultiSetDisplayExpr(x.tok, new List()); - empty.Type = x.Type; + empty.Type = xType; yield return empty; - } else if (x.Type is SeqType) { + } else if (xType is SeqType) { var empty = new SeqDisplayExpr(x.tok, new List()); - empty.Type = x.Type; + empty.Type = xType; yield return empty; - } else if (x.Type is IntType) { + } else if (xType is IntType) { var lit = new LiteralExpr(x.tok, 0); lit.Type = Type.Int; // resolve here yield return lit; - } else if (x.Type is RealType) { + } else if (xType is RealType) { var lit = new LiteralExpr(x.tok, Basetypes.BigDec.ZERO); lit.Type = Type.Real; // resolve here yield return lit; @@ -6580,12 +6589,12 @@ namespace Microsoft.Dafny { // include a free invariant that says that all completed iterations so far have only decreased the termination metric if (initDecr != null) { - List toks = new List(); - List types = new List(); - List decrs = new List(); + var toks = new List(); + var types = new List(); + var decrs = new List(); foreach (Expression e in theDecreases) { toks.Add(e.tok); - types.Add(cce.NonNull(e.Type)); + types.Add(e.Type.NormalizeExpand()); decrs.Add(etran.TrExpr(e)); } Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, initDecr, null, null, true, false); @@ -6616,12 +6625,12 @@ namespace Microsoft.Dafny { // time for the actual loop body bodyTr(loopBodyBuilder, updatedFrameEtran); // check definedness of decreases expressions - List toks = new List(); - List types = new List(); - List decrs = new List(); + var toks = new List(); + var types = new List(); + var decrs = new List(); foreach (Expression e in theDecreases) { toks.Add(e.tok); - types.Add(cce.NonNull(e.Type)); + types.Add(e.Type.NormalizeExpand()); decrs.Add(etran.TrExpr(e)); } Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, oldBfs, loopBodyBuilder, " at end of loop iteration", false, false); @@ -7034,8 +7043,8 @@ namespace Microsoft.Dafny { break; } toks.Add(tok); - types0.Add(e0.Type); - types1.Add(e1.Type); + types0.Add(e0.Type.NormalizeExpand()); + types1.Add(e1.Type.NormalizeExpand()); callee.Add(etranCurrent.TrExpr(e0)); caller.Add(etranInitial.TrExpr(e1)); } @@ -7056,6 +7065,7 @@ namespace Microsoft.Dafny { /// or has gone down or stayed the same (if allowNoChange). /// ee0 represents the new values and ee1 represents old values. /// If builder is non-null, then the check '0 ATMOST decr' is generated to builder. + /// Requires all types in types0 and types1 to be non-proxy non-synonym types (that is, callers should invoke NormalizeExpand) /// Bpl.Expr DecreasesCheck(List toks, List types0, List types1, List ee0, List ee1, Bpl.StmtListBuilder builder, string suffixMsg, bool allowNoChange, bool includeLowerBound) @@ -7157,6 +7167,9 @@ namespace Microsoft.Dafny { else return null; } + /// + /// Requires ty0 and ty1 to be non-proxy non-synonym types (that is, caller is expected have have invoked NormalizeExpand) + /// void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out Bpl.Expr less, out Bpl.Expr atmost, out Bpl.Expr eq, bool includeLowerBound) { Contract.Requires(tok != null); @@ -7169,8 +7182,6 @@ namespace Microsoft.Dafny { Contract.Ensures(Contract.ValueAtReturn(out atmost)!=null); Contract.Ensures(Contract.ValueAtReturn(out eq)!=null); - ty0 = ty0.NormalizeExpand(); - ty1 = ty1.NormalizeExpand(); var rk0 = RankFunction(ty0); var rk1 = RankFunction(ty1); if (rk0 != null && rk1 != null && rk0 != rk1) { @@ -7442,7 +7453,7 @@ namespace Microsoft.Dafny { Contract.Requires(type != null); Contract.Ensures(Contract.Result() != null); - if (type.NormalizeExpand() is BoolType) { + if (type.IsBoolType) { return FunctionCall(box.tok, BuiltinFunction.IsCanonicalBoolBox, null, box); } else { return Bpl.Expr.True; @@ -7871,7 +7882,8 @@ namespace Microsoft.Dafny { Contract.Requires(builder != null); var cre = CheckSubrange_Expr(tok, bRhs, tp); - var msg = (tp is NatType) ? "value assigned to a nat must be non-negative" : + var msg = (tp.NormalizeExpand() is NatType) ? + "value assigned to a nat must be non-negative" : "value does not satisfy the subrange criteria"; builder.Add(Assert(tok, cre, msg)); } @@ -7883,7 +7895,7 @@ namespace Microsoft.Dafny { // Only need to check this for natural numbers for now. // We should always be able to use Is, but this is an optimisation. - if (tp is NatType) { + if (tp.NormalizeExpand() is NatType) { return MkIs(bRhs, tp); } else { return Bpl.Expr.True; @@ -8597,20 +8609,21 @@ namespace Microsoft.Dafny { } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; Bpl.Expr seq = TrExpr(e.Seq); + var seqType = e.Seq.Type.NormalizeExpand(); Type elmtType = null; Type domainType = null; - Contract.Assert(e.Seq.Type != null); // the expression has been successfully resolved - if (e.Seq.Type.IsArrayType) { + Contract.Assert(seqType != null); // the expression has been successfully resolved + if (seqType.IsArrayType) { domainType = Type.Int; - elmtType = UserDefinedType.ArrayElementType(e.Seq.Type); - } else if (e.Seq.Type is SeqType) { + elmtType = UserDefinedType.ArrayElementType(seqType); + } else if (seqType is SeqType) { domainType = Type.Int; - elmtType = ((SeqType)e.Seq.Type).Arg; - } else if (e.Seq.Type is MapType) { - domainType = ((MapType)e.Seq.Type).Domain; - elmtType = ((MapType)e.Seq.Type).Range; - } else if (e.Seq.Type is MultiSetType) { - domainType = ((MultiSetType)e.Seq.Type).Arg; + elmtType = ((SeqType)seqType).Arg; + } else if (seqType is MapType) { + domainType = ((MapType)seqType).Domain; + elmtType = ((MapType)seqType).Range; + } else if (seqType is MultiSetType) { + domainType = ((MultiSetType)seqType).Arg; elmtType = Type.Int; } else { Contract.Assert(false); } Bpl.Type elType = translator.TrType(elmtType); @@ -8620,23 +8633,23 @@ namespace Microsoft.Dafny { if (e.SelectOne) { Contract.Assert(e1 == null); Bpl.Expr x; - if (e.Seq.Type.IsArrayType) { + if (seqType.IsArrayType) { Bpl.Expr fieldName = translator.FunctionCall(expr.tok, BuiltinFunction.IndexField, null, e0); x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Seq), fieldName); - } else if(e.Seq.Type is SeqType) { + } else if (seqType is SeqType) { x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0); - } else if (e.Seq.Type is MapType) { + } else if (seqType is MapType) { x = translator.FunctionCall(expr.tok, BuiltinFunction.MapElements, predef.MapType(e.tok, predef.BoxType, predef.BoxType), seq); x = Bpl.Expr.Select(x, BoxIfNecessary(e.tok, e0, domainType)); - } else if (e.Seq.Type is MultiSetType) { + } else if (seqType is MultiSetType) { x = Bpl.Expr.SelectTok(expr.tok, TrExpr(e.Seq), BoxIfNecessary(expr.tok, e0, domainType)); } else { Contract.Assert(false); x = null; } - if (!ModeledAsBoxType(elmtType) && !(e.Seq.Type is MultiSetType)) { + if (!ModeledAsBoxType(elmtType) && !(seqType is MultiSetType)) { x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x); } return x; } else { - if (e.Seq.Type.IsArrayType) { + if (seqType.IsArrayType) { seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqFromArray, elType, HeapExpr, seq); } var isLit = translator.IsLit(seq); @@ -8665,24 +8678,25 @@ namespace Microsoft.Dafny { else { Bpl.Expr seq = TrExpr(e.Seq); - if (e.Seq.Type is SeqType) + var seqType = e.Seq.Type.NormalizeExpand(); + if (seqType is SeqType) { - Type elmtType = cce.NonNull((SeqType)e.Seq.Type).Arg; + Type elmtType = cce.NonNull((SeqType)seqType).Arg; Bpl.Expr index = TrExpr(e.Index); Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), elmtType); return translator.FunctionCall(expr.tok, BuiltinFunction.SeqUpdate, predef.BoxType, seq, index, val); } - else if (e.Seq.Type is MapType) + else if (seqType is MapType) { - MapType mt = (MapType)e.Seq.Type; + MapType mt = (MapType)seqType; Bpl.Type maptype = predef.MapType(expr.tok, predef.BoxType, predef.BoxType); Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), mt.Domain); Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), mt.Range); return translator.FunctionCall(expr.tok, "Map#Build", maptype, seq, index, val); } - else if (e.Seq.Type is MultiSetType) + else if (seqType is MultiSetType) { - Type elmtType = cce.NonNull((MultiSetType)e.Seq.Type).Arg; + Type elmtType = cce.NonNull((MultiSetType)seqType).Arg; Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), elmtType); Bpl.Expr val = TrExpr(e.Value); return Bpl.Expr.StoreTok(expr.tok, seq, index, val); @@ -8757,10 +8771,11 @@ namespace Microsoft.Dafny { } else if (expr is MultiSetFormingExpr) { MultiSetFormingExpr e = (MultiSetFormingExpr)expr; - if (e.E.Type is SetType) { - return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetFromSet, translator.TrType(cce.NonNull((SetType)e.E.Type).Arg), TrExpr(e.E)); - } else if (e.E.Type is SeqType) { - return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetFromSeq, translator.TrType(cce.NonNull((SeqType)e.E.Type).Arg), TrExpr(e.E)); + var eType = e.E.Type.NormalizeExpand(); + if (eType is SetType) { + return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetFromSet, translator.TrType(cce.NonNull((SetType)eType).Arg), TrExpr(e.E)); + } else if (eType is SeqType) { + return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetFromSeq, translator.TrType(cce.NonNull((SeqType)eType).Arg), TrExpr(e.E)); } else { Contract.Assert(false); throw new cce.UnreachableException(); } @@ -8774,29 +8789,31 @@ namespace Microsoft.Dafny { case UnaryOpExpr.Opcode.Not: return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, arg); case UnaryOpExpr.Opcode.Cardinality: - if (e.E.Type is SeqType) { + var eType = e.E.Type.NormalizeExpand(); + if (eType is SeqType) { return translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, arg); - } else if (e.E.Type is SetType) { + } else if (eType is SetType) { return translator.FunctionCall(expr.tok, BuiltinFunction.SetCard, null, arg); - } else if (e.E.Type is MultiSetType) { + } else if (eType is MultiSetType) { return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetCard, null, arg); - } else if (e.E.Type is MapType) { + } else if (eType is MapType) { return translator.FunctionCall(expr.tok, BuiltinFunction.MapCard, null, arg); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected sized type } case UnaryOpExpr.Opcode.Fresh: - if (e.E.Type is SetType) { + var eeType = e.E.Type.NormalizeExpand(); + if (eeType is SetType) { // generate: (forall $o: ref :: $o != null && X[Box($o)] ==> !old($Heap)[$o,alloc]) // TODO: trigger? Bpl.Variable oVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$o", predef.RefType)); Bpl.Expr o = new Bpl.IdentifierExpr(expr.tok, oVar); Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null); - Bpl.Expr oInSet = TrInSet(expr.tok, o, e.E, ((SetType)e.E.Type).Arg); + Bpl.Expr oInSet = TrInSet(expr.tok, o, e.E, ((SetType)eeType).Arg); Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, o)); Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInSet), oIsFresh); return new Bpl.ForallExpr(expr.tok, new List { oVar }, body); - } else if (e.E.Type is SeqType) { + } else if (eeType is SeqType) { // generate: (forall $i: int :: 0 <= $i && $i < Seq#Length(X) && Unbox(Seq#Index(X,$i)) != null ==> !old($Heap)[Unbox(Seq#Index(X,$i)),alloc]) // TODO: trigger? Bpl.Variable iVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$i", Bpl.Type.Int)); @@ -8808,9 +8825,9 @@ namespace Microsoft.Dafny { Bpl.Expr xsubiNotNull = Bpl.Expr.Neq(XsubI, predef.Null); Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(iBounds, xsubiNotNull), oIsFresh); return new Bpl.ForallExpr(expr.tok, new List { iVar }, body); - } else if (e.E.Type.IsDatatype) { - // translator.FunctionCall(e.tok, BuiltinFunction.DtAlloc, null, TrExpr(e.E), Old.HeapExpr); - Bpl.Expr alloc = translator.MkIsAlloc(TrExpr(e.E), e.E.Type, Old.HeapExpr); + } else if (eeType.IsDatatype) { + // translator.FunctionCall(e.tok, BuiltinFunction.DtAlloc, null, TrExpr(e.E), Old.HeapExpr); + Bpl.Expr alloc = translator.MkIsAlloc(TrExpr(e.E), eeType, Old.HeapExpr); return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, alloc); } else { // generate: x != null && !old($Heap)[x] @@ -8837,7 +8854,7 @@ namespace Microsoft.Dafny { } else if (expr is BinaryExpr) { BinaryExpr e = (BinaryExpr)expr; - bool isReal = e.E0.Type is RealType; + bool isReal = e.E0.Type.IsRealType; Bpl.Expr e0 = TrExpr(e.E0); if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet) { return TrInSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type)); // let TrInSet translate e.E1 @@ -8883,16 +8900,20 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.EqCommon: keepLits = true; - if (e.E0.Type.IsCoDatatype) { - var cot = e.E0.Type.AsCoDatatype; - return translator.CoEqualCall(cot, e.E0.Type.TypeArgs, e.E1.Type.TypeArgs, null, LayerN(2), e0, e1, expr.tok); + var cot = e.E0.Type.AsCoDatatype; + if (cot != null) { + var e0args = e.E0.Type.NormalizeExpand().TypeArgs; + var e1args = e.E1.Type.NormalizeExpand().TypeArgs; + return translator.CoEqualCall(cot, e0args, e1args, null, LayerN(2), e0, e1, expr.tok); } typ = Bpl.Type.Bool; bOpcode = BinaryOperator.Opcode.Eq; break; case BinaryExpr.ResolvedOpcode.NeqCommon: - if (e.E0.Type.IsCoDatatype) { - var cot = e.E0.Type.AsCoDatatype; - var x = translator.CoEqualCall(cot, e.E0.Type.TypeArgs, e.E1.Type.TypeArgs, null, LayerN(2), e0, e1, expr.tok); + var cotx = e.E0.Type.AsCoDatatype; + if (cotx != null) { + var e0args = e.E0.Type.NormalizeExpand().TypeArgs; + var e1args = e.E1.Type.NormalizeExpand().TypeArgs; + var x = translator.CoEqualCall(cotx, e0args, e1args, null, LayerN(2), e0, e1, expr.tok); return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, x); } typ = Bpl.Type.Bool; @@ -8952,11 +8973,11 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.NotInSet: Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above case BinaryExpr.ResolvedOpcode.Union: - return translator.FunctionCall(expr.tok, BuiltinFunction.SetUnion, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1); + return translator.FunctionCall(expr.tok, BuiltinFunction.SetUnion, translator.TrType(expr.Type.AsSetType.Arg), e0, e1); case BinaryExpr.ResolvedOpcode.Intersection: - return translator.FunctionCall(expr.tok, BuiltinFunction.SetIntersection, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1); + return translator.FunctionCall(expr.tok, BuiltinFunction.SetIntersection, translator.TrType(expr.Type.AsSetType.Arg), e0, e1); case BinaryExpr.ResolvedOpcode.SetDifference: - return translator.FunctionCall(expr.tok, BuiltinFunction.SetDifference, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1); + return translator.FunctionCall(expr.tok, BuiltinFunction.SetDifference, translator.TrType(expr.Type.AsSetType.Arg), e0, e1); case BinaryExpr.ResolvedOpcode.MultiSetEq: return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1); @@ -8981,11 +9002,11 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.NotInMultiSet: Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above case BinaryExpr.ResolvedOpcode.MultiSetUnion: - return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetUnion, translator.TrType(cce.NonNull((MultiSetType)expr.Type).Arg), e0, e1); + return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetUnion, translator.TrType(expr.Type.AsMultiSetType.Arg), e0, e1); case BinaryExpr.ResolvedOpcode.MultiSetIntersection: - return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetIntersection, translator.TrType(cce.NonNull((MultiSetType)expr.Type).Arg), e0, e1); + return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetIntersection, translator.TrType(expr.Type.AsMultiSetType.Arg), e0, e1); case BinaryExpr.ResolvedOpcode.MultiSetDifference: - return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetDifference, translator.TrType(cce.NonNull((MultiSetType)expr.Type).Arg), e0, e1); + return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetDifference, translator.TrType(expr.Type.AsMultiSetType.Arg), e0, e1); case BinaryExpr.ResolvedOpcode.SeqEq: return translator.FunctionCall(expr.tok, BuiltinFunction.SeqEqual, null, e0, e1); @@ -9002,7 +9023,7 @@ namespace Microsoft.Dafny { translator.FunctionCall(expr.tok, BuiltinFunction.SeqSameUntil, null, e0, e1, len0)); } case BinaryExpr.ResolvedOpcode.Concat: - return translator.FunctionCall(expr.tok, BuiltinFunction.SeqAppend, translator.TrType(cce.NonNull((SeqType)expr.Type).Arg), e0, e1); + return translator.FunctionCall(expr.tok, BuiltinFunction.SeqAppend, translator.TrType(expr.Type.AsSeqType.Arg), e0, e1); case BinaryExpr.ResolvedOpcode.InSeq: return translator.FunctionCall(expr.tok, BuiltinFunction.SeqContains, null, e1, BoxIfNecessary(expr.tok, e0, cce.NonNull(e.E0.Type))); @@ -9047,9 +9068,11 @@ namespace Microsoft.Dafny { switch (e.Op) { case TernaryExpr.Opcode.PrefixEqOp: case TernaryExpr.Opcode.PrefixNeqOp: - var cot = e.E1.Type.AsCoDatatype; + var e1type = e.E1.Type.NormalizeExpand(); + var e2type = e.E2.Type.NormalizeExpand(); + var cot = e1type.AsCoDatatype; Contract.Assert(cot != null); // the argument types of prefix equality (and prefix disequality) are codatatypes - var r = translator.CoEqualCall(cot, e.E1.Type.TypeArgs, e.E2.Type.TypeArgs, e0, LayerN(2), e1, e2); + var r = translator.CoEqualCall(cot, e1type.TypeArgs, e2type.TypeArgs, e0, LayerN(2), e1, e2); if (e.Op == TernaryExpr.Opcode.PrefixEqOp) { return r; } else { @@ -10063,7 +10086,7 @@ namespace Microsoft.Dafny { /// bool TrSplitExpr(Expression expr, List/*!*/ splits, bool position, int heightLimit, bool apply_induction, ExpressionTranslator etran) { Contract.Requires(expr != null); - Contract.Requires(expr.Type is BoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type is BoolType)); + Contract.Requires(expr.Type.IsBoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type.IsBoolType)); Contract.Requires(splits != null); Contract.Requires(etran != null); @@ -10139,7 +10162,9 @@ namespace Microsoft.Dafny { } else if (expr is TernaryExpr) { var e = (TernaryExpr)expr; if ((e.Op == TernaryExpr.Opcode.PrefixEqOp && position) || (e.Op == TernaryExpr.Opcode.PrefixNeqOp && !position)) { - var codecl = e.E1.Type.AsCoDatatype; + var e1type = e.E1.Type.NormalizeExpand(); + var e2type = e.E2.Type.NormalizeExpand(); + var codecl = e1type.AsCoDatatype; Contract.Assert(codecl != null); var k = etran.TrExpr(e.E0); var A = etran.TrExpr(e.E1); @@ -10149,7 +10174,7 @@ namespace Microsoft.Dafny { // checked $PrefixEqual#Dt(k, A, B) || (0 < k ==> A.Cons? ==> B.Cons? && A.head == B.head && $PrefixEqual#2#Dt(k - 1, A.tail, B.tail)) // note the #2 in the recursive call, just like for user-defined predicates that are inlined by TrSplitExpr // free $PrefixEqual#Dt(k, A, B); var kPos = Bpl.Expr.Lt(Bpl.Expr.Literal(0), k); - var prefixEqK = CoEqualCall(codecl, e.E1.Type.TypeArgs, e.E2.Type.TypeArgs, k, etran.LayerN(2), A, B); // FunctionCall(expr.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, A, B); + var prefixEqK = CoEqualCall(codecl, e1type.TypeArgs, e2type.TypeArgs, k, etran.LayerN(2), A, B); // FunctionCall(expr.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, A, B); var kMinusOne = Bpl.Expr.Sub(k, Bpl.Expr.Literal(1)); // for the inlining of the definition of prefix equality, translate the two main equality operands arguments with a higher offset (to obtain #2 functions) var etran2 = etran.LayerOffset(1); @@ -10158,7 +10183,7 @@ namespace Microsoft.Dafny { var needsTokenAdjust = TrSplitNeedsTokenAdjustment(expr); // Dan: dafny4/Circ.dfy needs this one to be 2+, rather than 1+ Bpl.Expr layer = LayerSucc(etran.layerInterCluster, 2); - foreach (var c in CoPrefixEquality(needsTokenAdjust ? new ForceCheckToken(expr.tok) : expr.tok, codecl, e.E1.Type.TypeArgs, e.E2.Type.TypeArgs, kMinusOne, layer, A2, B2, true)) { + foreach (var c in CoPrefixEquality(needsTokenAdjust ? new ForceCheckToken(expr.tok) : expr.tok, codecl, e1type.TypeArgs, e2type.TypeArgs, kMinusOne, layer, A2, B2, true)) { var p = Bpl.Expr.Binary(c.tok, BinaryOperator.Opcode.Or, prefixEqK, Bpl.Expr.Imp(kPos, c)); splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p)); } @@ -10306,7 +10331,7 @@ namespace Microsoft.Dafny { var substMap = new Dictionary(); foreach (var n in inductionVariables) { toks.Add(n.tok); - types.Add(n.Type); + types.Add(n.Type.NormalizeExpand()); BoundVar k = new BoundVar(n.tok, n.Name + "$ih#" + otherTmpVarCount, n.Type); otherTmpVarCount++; kvars.Add(k); @@ -10736,6 +10761,7 @@ namespace Microsoft.Dafny { } IEnumerable InductionCases(Type ty, Bpl.Expr expr, ExpressionTranslator etran) { + ty = ty.NormalizeExpand(); IndDatatypeDecl dt = ty.AsIndDatatype; if (dt == null) { yield return Bpl.Expr.True; @@ -10806,7 +10832,7 @@ namespace Microsoft.Dafny { if (ty.IsTypeParameter && ! ty.AsTypeParameter.IsAbstractTypeDeclaration) { fvs.Add(ty.AsTypeParameter); } - ty.TypeArgs.Iter(tt => ComputeFreeTypeVariables(tt, fvs)); + ty.NormalizeExpand().TypeArgs.Iter(tt => ComputeFreeTypeVariables(tt, fvs)); } static void ComputeFreeVariables(Expression expr, ISet fvs, ref bool usesHeap, ref bool usesOldHeap, ref Type usesThis, bool inOldContext) { @@ -11863,6 +11889,8 @@ namespace Microsoft.Dafny { } static List Concat(List xs, List ys) { + Contract.Requires(xs != null); + Contract.Requires(ys != null); List cpy = new List(xs); cpy.AddRange(ys); return cpy; @@ -11870,6 +11898,8 @@ namespace Microsoft.Dafny { public static List Map(IEnumerable xs, Func f) { + Contract.Requires(xs != null); + Contract.Requires(f != null); List ys = new List(); foreach (A x in xs) { ys.Add(f(x)); @@ -11879,6 +11909,8 @@ namespace Microsoft.Dafny { public static void MapM(IEnumerable xs, Action K) { + Contract.Requires(xs != null); + Contract.Requires(K != null); foreach (A x in xs) { K(x); } diff --git a/Source/DafnyExtension/DafnyRuntime.cs b/Source/DafnyExtension/DafnyRuntime.cs index 6f0cab13..d6bd895a 100644 --- a/Source/DafnyExtension/DafnyRuntime.cs +++ b/Source/DafnyExtension/DafnyRuntime.cs @@ -656,6 +656,13 @@ namespace Dafny num = n; den = d; } + public BigInteger ToBigInteger() { + if (0 <= num) { + return num / den; + } else { + return (num - den + 1) / den; + } + } /// /// Returns values such that aa/dd == a and bb/dd == b. /// diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect index 410e4507..70e46ff0 100644 --- a/Test/dafny0/EqualityTypes.dfy.expect +++ b/Test/dafny0/EqualityTypes.dfy.expect @@ -5,7 +5,7 @@ EqualityTypes.dfy(41,8): Error: opaque type 'Y' is not allowed to be replaced by EqualityTypes.dfy(45,11): Error: type 'X' is used to refine an opaque type with equality support, but 'X' does not support equality EqualityTypes.dfy(46,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt) -EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0) +EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0) (perhaps try declaring type parameter '_T0' on line 81 as '_T0(==)', which says it can only be instantiated with a type that supports equality) EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D) EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D) EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D) diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 520b2e38..aaf1291c 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1007,20 +1007,20 @@ module CycleError2 { type A = B // error: cycle: A -> B -> A type B = set } -module Good0 { +module CycleErrors3 { type A = (B, D) type B = C class C { var a: A; // this is fine } - datatype D = Make(A, B, C) // this is fine, too + datatype D = Make(A, B, C) // error: cannot construct a D } -module CycleError3 { +module CycleError4 { type A = B // error: cycle: A -> B -> A type B = C class C { } } -module CycleError4 { +module CycleError5 { type A = B // error: cycle: A -> B -> A type B = Dt datatype Dt = Make(T) diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 49cfe650..d5d12eb9 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -63,6 +63,7 @@ ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter ResolutionErrors.dfy(1000,7): Error: Cycle among type synonyms: A -> A ResolutionErrors.dfy(1003,7): Error: Cycle among type synonyms: A -> B -> A ResolutionErrors.dfy(1007,7): Error: Cycle among type synonyms: A -> B -> A +ResolutionErrors.dfy(1016,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed ResolutionErrors.dfy(1019,7): Error: Cycle among type synonyms: A -> B -> A ResolutionErrors.dfy(1024,7): Error: Cycle among type synonyms: A -> B -> A ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x @@ -171,4 +172,4 @@ ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (i ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real) ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int) ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat) -173 resolution/type errors detected in ResolutionErrors.dfy +174 resolution/type errors detected in ResolutionErrors.dfy diff --git a/Test/dafny0/TypeSynonyms.dfy b/Test/dafny0/TypeSynonyms.dfy index 4bec5253..85beb340 100644 --- a/Test/dafny0/TypeSynonyms.dfy +++ b/Test/dafny0/TypeSynonyms.dfy @@ -44,3 +44,10 @@ function Skip(s: Synonym3): Synonym0 case Nil => Nil case Cons(_, tail) => tail } + +type MyMap = map> + +predicate MyMapProperty(m: MyMap, x: int) +{ + x in m && real(x) in m[x] && m[x][real(x)] +} diff --git a/Test/dafny0/TypeSynonyms.dfy.expect b/Test/dafny0/TypeSynonyms.dfy.expect index 4ef2de53..76f19e0d 100644 --- a/Test/dafny0/TypeSynonyms.dfy.expect +++ b/Test/dafny0/TypeSynonyms.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 6 verified, 0 errors +Dafny program verifier finished with 7 verified, 0 errors diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect index 62e41019..5d78fe16 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -25,8 +25,8 @@ TypeTests.dfy(106,3): Error: cannot assign to a range of array elements (try the TypeTests.dfy(107,3): Error: cannot assign to a range of array elements (try the 'forall' statement) TypeTests.dfy(113,6): Error: sorry, cannot instantiate collection type with a subrange type TypeTests.dfy(114,9): Error: sorry, cannot instantiate type parameter with a subrange type -TypeTests.dfy(115,8): Error: sorry, cannot instantiate 'array' type with a subrange type -TypeTests.dfy(116,8): Error: sorry, cannot instantiate 'array' type with a subrange type +TypeTests.dfy(115,8): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(116,8): Error: sorry, cannot instantiate type parameter with a subrange type TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification contexts TypeTests.dfy(138,4): Error: cannot assign to non-ghost variable in a ghost context TypeTests.dfy(139,7): Error: cannot assign to non-ghost variable in a ghost context -- cgit v1.2.3 From a2b04d603976cc54ab40d981b4c2866b58c9945e Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Tue, 5 Aug 2014 11:03:55 +0200 Subject: Tests for non-terminating computations. Already passing. --- Test/dafny0/ComputationsLoop.dfy | 13 +++++++++++++ Test/dafny0/ComputationsLoop.dfy.expect | 9 +++++++++ Test/dafny0/ComputationsLoop2.dfy | 17 +++++++++++++++++ Test/dafny0/ComputationsLoop2.dfy.expect | 13 +++++++++++++ 4 files changed, 52 insertions(+) create mode 100644 Test/dafny0/ComputationsLoop.dfy create mode 100644 Test/dafny0/ComputationsLoop.dfy.expect create mode 100644 Test/dafny0/ComputationsLoop2.dfy create mode 100644 Test/dafny0/ComputationsLoop2.dfy.expect diff --git a/Test/dafny0/ComputationsLoop.dfy b/Test/dafny0/ComputationsLoop.dfy new file mode 100644 index 00000000..b89455a2 --- /dev/null +++ b/Test/dafny0/ComputationsLoop.dfy @@ -0,0 +1,13 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function KeepDoin'It(x: nat): nat + decreases x; +{ + KeepDoin'It(x + 1) +} + +lemma Test(r: nat) +{ + assert KeepDoin'It(20) == r; +} \ No newline at end of file diff --git a/Test/dafny0/ComputationsLoop.dfy.expect b/Test/dafny0/ComputationsLoop.dfy.expect new file mode 100644 index 00000000..d9d48024 --- /dev/null +++ b/Test/dafny0/ComputationsLoop.dfy.expect @@ -0,0 +1,9 @@ +ComputationsLoop.dfy(7,3): Error: failure to decrease termination measure +Execution trace: + (0,0): anon0 + (0,0): anon3_Else +ComputationsLoop.dfy(12,26): Error: assertion violation +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 1 verified, 2 errors diff --git a/Test/dafny0/ComputationsLoop2.dfy b/Test/dafny0/ComputationsLoop2.dfy new file mode 100644 index 00000000..d03d7c79 --- /dev/null +++ b/Test/dafny0/ComputationsLoop2.dfy @@ -0,0 +1,17 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function KeepDoin'It(x: nat): nat +{ + KeepDoin'ItToo(x + 1) +} + +function KeepDoin'ItToo(x: nat): nat +{ + KeepDoin'It(x + 1) +} + +lemma Test(r: nat) +{ + assert KeepDoin'It(20) == r; +} \ No newline at end of file diff --git a/Test/dafny0/ComputationsLoop2.dfy.expect b/Test/dafny0/ComputationsLoop2.dfy.expect new file mode 100644 index 00000000..0a45e6d0 --- /dev/null +++ b/Test/dafny0/ComputationsLoop2.dfy.expect @@ -0,0 +1,13 @@ +ComputationsLoop2.dfy(6,3): Error: cannot prove termination; try supplying a decreases clause +Execution trace: + (0,0): anon0 + (0,0): anon3_Else +ComputationsLoop2.dfy(11,3): Error: cannot prove termination; try supplying a decreases clause +Execution trace: + (0,0): anon0 + (0,0): anon3_Else +ComputationsLoop2.dfy(16,26): Error: assertion violation +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 1 verified, 3 errors -- cgit v1.2.3 From 498bff41addc9ca481926f668fb6b69b17b9deda Mon Sep 17 00:00:00 2001 From: leino Date: Tue, 5 Aug 2014 10:06:39 -0700 Subject: Resolved further merge issues --- Source/Dafny/Cloner.cs | 7 - Source/Dafny/Printer.cs | 3 + Source/Dafny/Resolver.cs | 323 ++++++++++----------- Test/dafny0/ResolutionErrors.dfy | 10 + Test/dafny0/ResolutionErrors.dfy.expect | 3 +- Test/dafny0/Trait/TraitBasix.dfy.expect | 4 +- Test/dafny0/Trait/TraitMultiModule.dfy.expect | 2 +- Test/dafny0/Trait/TraitOverride0.dfy.expect | 2 +- Test/dafny0/Trait/TraitOverride1.dfy.expect | 2 +- .../Trait/TraitUsingParentMembers.dfy.expect | 2 +- 10 files changed, 175 insertions(+), 183 deletions(-) diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index cbd27f74..203dbef4 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -136,19 +136,14 @@ namespace Microsoft.Dafny Contract.Assert(!(member is SpecialField)); // we don't expect a SpecialField to be cloned (or do we?) var f = (Field)member; 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 return field; } else if (member is Function) { var f = (Function)member; - f.Inherited = member.Inherited; Function func = CloneFunction(f); - func.Inherited = member.Inherited; return func; } else { var m = (Method)member; - m.Inherited = member.Inherited; Method method = CloneMethod(m); - method.Inherited = member.Inherited; return method; } } @@ -190,8 +185,6 @@ namespace Microsoft.Dafny public Formal CloneFormal(Formal formal) { Formal f = new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost); - if (f.Type is UserDefinedType && formal.Type is UserDefinedType) - ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(formal.Type)).ResolvedClass; return f; } diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 6e10e7a1..a96efb8b 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -265,6 +265,9 @@ namespace Microsoft.Dafny { Contract.Requires(c != null); Indent(indent); PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs); + if (c.TraitId != null) { + wr.Write(" extends {0}", c.TraitId.val); + } if (c.Members.Count == 0) { wr.WriteLine(" { }"); } else { diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index d1ae1627..d391ab4e 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -136,12 +136,12 @@ namespace Microsoft.Dafny return nm; } } - //Dictionary> allDatatypeCtors; + //Dictionary> allDatatypeCtors; - readonly Dictionary/*!*/>/*!*/ classMembers = new Dictionary/*!*/>(); - readonly Dictionary/*!*/>/*!*/ datatypeMembers = new Dictionary/*!*/>(); - readonly Dictionary/*!*/>/*!*/ datatypeCtors = new Dictionary/*!*/>(); - readonly Graph/*!*/ dependencies = new Graph(); + readonly Dictionary> classMembers = new Dictionary>(); + readonly Dictionary> datatypeMembers = new Dictionary>(); + readonly Dictionary> datatypeCtors = new Dictionary>(); + readonly Graph dependencies = new Graph(); private ModuleSignature systemNameInfo = null; private bool useCompileSignatures = false; private RefinementTransformer refinementTransformer = null; @@ -1457,6 +1457,14 @@ namespace Microsoft.Dafny allTypeParameters.PopMarker(); } + // Now that all traits have been resolved, let classes inherit the trait members + foreach (var d in declarations) { + var cl = d as ClassDecl; + if (cl != null) { + InheritTraitMembers(cl); + } + } + // perform acyclicity test on type synonyms var cycle = typeSynonymDependencies.TryFindCycle(); if (cycle != null) { @@ -1478,7 +1486,7 @@ namespace Microsoft.Dafny Contract.Assert(d != null); if (d is TraitDecl && d.TypeArgs != null && d.TypeArgs.Count > 0) { - Error(d, "a trait can not declare type parameters"); + Error(d, "a trait cannot declare type parameters"); } allTypeParameters.PushMarker(); ResolveTypeParameters(d.TypeArgs, false, d); @@ -2763,13 +2771,33 @@ namespace Microsoft.Dafny /// /// Assumes type parameters have already been pushed /// - void ResolveClassMemberTypes(ClassDecl/*!*/ cl) { + void ResolveClassMemberTypes(ClassDecl cl) { Contract.Requires(cl != null); Contract.Requires(currentClass == null); Contract.Ensures(currentClass == null); currentClass = cl; - RefinementCloner cloner = new RefinementCloner(cl.Module); + + // Resolve names of traits extended + if (cl.TraitId != null) { + var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == cl.TraitId.val); + if (trait == null) { + Error(cl.TraitId, "unresolved identifier: {0}", cl.TraitId.val); + } else if (!(trait is TraitDecl)) { + Error(cl.TraitId, "identifier '{0}' does not denote a trait", cl.TraitId.val); + } else { + //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.TraitId, 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; + } + } + } + foreach (MemberDecl member in cl.Members) { member.EnclosingClass = cl; if (member is Field) { @@ -2814,165 +2842,126 @@ namespace Microsoft.Dafny } } + currentClass = null; + } + + void InheritTraitMembers(ClassDecl cl) { + Contract.Requires(cl != null); + //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)); + if (cl.Trait != null) { + var clMembers = classMembers[cl]; + var traitMembers = classMembers[cl.Trait]; + //merging current class members with the inheriting trait + foreach (KeyValuePair traitMem in traitMembers) { + MemberDecl clMember; + if (clMembers.TryGetValue(traitMem.Key, out clMember)) { + //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; + // TODO: should check that the class member is also a method, and the same kind of method + Method classMethod = (Method)clMember; + //refinementTransformer.CheckMethodsAreRefinements(classMethod, traitMethod); + if (traitMethod.Body != null && !clMembers[classMethod.CompileName].Inherited) //if the existing method in the class is not that inherited one from the parent + Error(classMethod, "a class cannot 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 - { - cl.Trait = (TraitDecl)trait; - var traitMembers = classMembers[trait]; - //merging current class members with the inheriting trait - foreach (KeyValuePair 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); - if (classNewMember is Field) - { - Field f = (Field)classNewMember; - if (f.Type is UserDefinedType) - ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(((Field)(traitMem.Value)).Type)).ResolvedClass; - } - classNewMember.EnclosingClass = cl; - classNewMember.Inherited = true; - classMembers[cl].Add(traitMem.Key, classNewMember); - cl.Members.Add(classNewMember); - } - }//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; - if (traitFunc.Body == null) //we do this check only if trait function body is null + } 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 cannot 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 (!clMembers[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 + // enter the trait member in the symbol table for the class + clMembers.Add(traitMem.Key, 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 cl.Trait.Members.Where(mem => mem is Function || mem is Method)) { + if (traitMember is Function) { + Function traitFunc = (Function)traitMember; + if (traitFunc.Body == null) //we do this check only if trait function body is null { - 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; - if (traitMethod.Body == null) //we do this check only if trait method body is null + 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; + if (traitMethod.Body == null) //we do this check only if trait method body is null { - 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); - } - } - } + 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; } /// @@ -5886,17 +5875,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.NormalizeExpand() is UserDefinedType) { + if (rr.EType.NormalizeExpand() is UserDefinedType) { var udt = (UserDefinedType)rr.EType.NormalizeExpand(); var cl = (ClassDecl)udt.ResolvedClass; // cast is guaranteed by the call to rr.EType.IsRefType above, together with the "rr.EType is UserDefinedType" test - if (cl.HasConstructor) { + if (cl is TraitDecl) { + Error(stmt, "new cannot be applied to a trait"); + } + if (!callsConstructor && cl.HasConstructor) { Error(stmt, "when allocating an object of type '{0}', one of its constructor methods must be called", cl.Name); } } diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index aaf1291c..9f6c948a 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1090,3 +1090,13 @@ module OpaqueTypes1 { assert p != q; // error: types must be the same in order to do compare } } + +// ----- new trait ------------------------------------------- + + +trait J { } +type JJ = J +method TraitSynonym() +{ + var x := new JJ; // error: new cannot be applied to a trait +} diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index d5d12eb9..b11fa9f8 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -172,4 +172,5 @@ ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (i ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real) ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int) ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat) -174 resolution/type errors detected in ResolutionErrors.dfy +ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait +175 resolution/type errors detected in ResolutionErrors.dfy diff --git a/Test/dafny0/Trait/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect index 1d44d0f6..4a908ee7 100644 --- a/Test/dafny0/Trait/TraitBasix.dfy.expect +++ b/Test/dafny0/Trait/TraitBasix.dfy.expect @@ -1,7 +1,7 @@ +TraitBasix.dfy(91,23): Error: unresolved identifier: IX TraitBasix.dfy(77,13): Error: member in the class has been already inherited from its parent trait TraitBasix.dfy(70,7): Error: class: I0Child does not implement trait member: Customizable TraitBasix.dfy(80,7): Error: class: I0Child2 does not implement trait member: F -TraitBasix.dfy(91,7): Error: unresolved identifier: IX TraitBasix.dfy(98,6): Error: a trait is not allowed to declare a constructor -TraitBasix.dfy(117,10): Error: new can not be applied to a trait +TraitBasix.dfy(117,10): Error: new cannot be applied to a trait 6 resolution/type errors detected in TraitBasix.dfy diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy.expect b/Test/dafny0/Trait/TraitMultiModule.dfy.expect index 589fba07..b9031dac 100644 --- a/Test/dafny0/Trait/TraitMultiModule.dfy.expect +++ b/Test/dafny0/Trait/TraitMultiModule.dfy.expect @@ -1,2 +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 +TraitMultiModule.dfy(21,20): 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.expect b/Test/dafny0/Trait/TraitOverride0.dfy.expect index 4020b880..1e7bface 100644 --- a/Test/dafny0/Trait/TraitOverride0.dfy.expect +++ b/Test/dafny0/Trait/TraitOverride0.dfy.expect @@ -1,4 +1,4 @@ -TraitOverride0.dfy(53,20): Error: a class can not override implemented functions +TraitOverride0.dfy(53,20): Error: a class cannot 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 diff --git a/Test/dafny0/Trait/TraitOverride1.dfy.expect b/Test/dafny0/Trait/TraitOverride1.dfy.expect index 0f7b49e3..c90560b0 100644 --- a/Test/dafny0/Trait/TraitOverride1.dfy.expect +++ b/Test/dafny0/Trait/TraitOverride1.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 62 verified, 0 errors +Dafny program verifier finished with 52 verified, 0 errors diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect index 6849499c..b59d7b80 100644 --- a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect +++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect @@ -5,4 +5,4 @@ Execution trace: (0,0): anon2 (0,0): anon6_Then -Dafny program verifier finished with 9 verified, 1 error +Dafny program verifier finished with 7 verified, 1 error -- cgit v1.2.3