Fixed some bugs in override axioms (but still missing support for classes with type parameters).

Resolve ClassDecl.TraitsTyp as types.
Moved declaration of TraitParent and NoTraitAtAll to prelude.

6 files changed, 130 insertions, 209 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 8552e480..3c266a28 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -105,7 +105,7 @@ namespace Microsoft.Dafny
         if (d is DefaultClassDecl) {

           return new DefaultClassDecl(m, mm);

         } else {

-            return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp);

+          return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType));

         }

       } else if (d is ModuleDecl) {

         if (d is LiteralModuleDecl) {

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index e557e509..c3d82d06 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -236,25 +236,24 @@ namespace Microsoft.Dafny {
                       }

                   }

               }

-              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.Write("public class @_Companion_{0}", trait.CompileName);

               wr.WriteLine(" {");

-              CompileClassMembers(cl, indent + IndentAmount);

+              CompileClassMembers(trait, indent + IndentAmount);

               Indent(indent); wr.WriteLine("}");

           }

           else if (d is ClassDecl) {

             var cl = (ClassDecl)d;

             Indent(indent);

-            if (cl.TraitsObj != null && cl.TraitsObj.Count > 0)

-            {

-                wr.WriteLine("public class @{0} : @{1}", cl.CompileName, cl.TraitsStr);

-            }

-            else

-                wr.Write("public class @{0}", cl.CompileName);

+            wr.Write("public class @{0}", cl.CompileName);

             if (cl.TypeArgs.Count != 0) {

               wr.Write("<{0}>", TypeParameters(cl.TypeArgs));

             }

+            string sep = " : ";

+            foreach (var trait in cl.TraitsTyp) {

+              wr.Write("{0}{1}", sep, TypeName(trait));

+              sep = ", ";

+            }

             wr.WriteLine(" {");

             CompileClassMembers(cl, indent+IndentAmount);

             Indent(indent);  wr.WriteLine("}");

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index ed089f10..6c498a59 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1865,12 +1865,14 @@ namespace Microsoft.Dafny {
   public class ClassDecl : TopLevelDecl {

     public override string WhatKind { get { return "class"; } }

     public readonly List<MemberDecl> Members;

-    public List<TraitDecl> TraitsObj;

-    public readonly List<Type> TraitsTyp;

+    public readonly List<Type> TraitsTyp;  // these are the types that are parsed after the keyword 'extends'

+    public readonly List<TraitDecl> TraitsObj = new List<TraitDecl>();  // populated during resolution

     public bool HasConstructor;  // filled in (early) during resolution; true iff there exists a member that is a Constructor

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(Members));

+      Contract.Invariant(TraitsTyp != null);

+      Contract.Invariant(TraitsObj != null);

     }

 

     public ClassDecl(IToken tok, string name, ModuleDefinition module,

@@ -1882,42 +1884,18 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(typeArgs));

       Contract.Requires(cce.NonNullElements(members));

       Members = members;

-      //if (traits != null)

-      TraitsTyp = traits;

+      TraitsTyp = traits ?? new List<Type>();

     }

     public virtual bool IsDefaultClass {

       get {

         return false;

       }

     }

-

-    public string TraitsStr

-    {

-        get

-        {

-            if (TraitsTyp == null || TraitsTyp.Count == 0)

-                return string.Empty;

-            StringBuilder sb = new StringBuilder();

-            foreach (Type ty in TraitsTyp)

-            {

-                if (ty is UserDefinedType)

-                {

-                    sb.Append(((UserDefinedType)(ty)).Name);

-                    sb.Append(",");

-                }

-            }

-            if (sb.Length > 0)

-            {

-                sb.Remove(sb.Length - 1, 1);

-            }

-            return sb.ToString();

-        }

-    }

   }

 

   public class DefaultClassDecl : ClassDecl {

     public DefaultClassDecl(ModuleDefinition module, [Captured] List<MemberDecl> members)

-      : base(Token.NoToken, "_default", module, new List<TypeParameter>(), members, null,null) {

+      : base(Token.NoToken, "_default", module, new List<TypeParameter>(), members, null, null) {

       Contract.Requires(module != null);

       Contract.Requires(cce.NonNullElements(members));

     }

@@ -1934,7 +1912,7 @@ namespace Microsoft.Dafny {
     public ArrayClassDecl(int dims, ModuleDefinition module, Attributes attrs)

     : base(Token.NoToken, BuiltIns.ArrayClassName(dims), module,

       new List<TypeParameter>(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}),

-      new List<MemberDecl>(), attrs,null)

+      new List<MemberDecl>(), attrs, null)

     {

       Contract.Requires(1 <= dims);

       Contract.Requires(module != null);

@@ -2218,7 +2196,7 @@ namespace Microsoft.Dafny {
                         List<MaybeFreeExpression> yieldRequires,

                         List<MaybeFreeExpression> yieldEnsures,

                         BlockStmt body, Attributes attributes, IToken signatureEllipsis)

-      : base(tok, name, module, typeArgs, new List<MemberDecl>(), attributes,null)

+      : base(tok, name, module, typeArgs, new List<MemberDecl>(), attributes, null)

     {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index b8c99b00..5fa232f1 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -319,8 +319,11 @@ namespace Microsoft.Dafny {
       Contract.Requires(c != null);

       Indent(indent);

       PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);

-      if (c.TraitsStr!=string.Empty) {

-          wr.Write(" extends {0}", c.TraitsStr);

+      string sep = " extends ";

+      foreach (var trait in c.TraitsTyp) {

+        wr.Write(sep);

+        PrintType(trait);

+        sep = ", ";

       }

       if (c.Members.Count == 0) {

         wr.WriteLine(" { }");

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 727011e8..0e8e0ec3 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2837,39 +2837,24 @@ namespace Microsoft.Dafny
       currentClass = cl;

 

       // Resolve names of traits extended

-      if (cl.TraitsTyp != null)

-      {

-          cl.TraitsObj = new List<TraitDecl>();

-          foreach (Type traitTyp in cl.TraitsTyp)

-          {

-              if (traitTyp is UserDefinedType)

-              {

-                  var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == ((UserDefinedType)(traitTyp)).FullCompileName);

-                  if (trait == null)

-                  {

-                      Error(((UserDefinedType)(traitTyp)).tok, "unresolved identifier: {0}", ((UserDefinedType)(traitTyp)).tok.val);

-                  }

-                  else if (!(trait is TraitDecl))

-                  {

-                      Error(((UserDefinedType)(traitTyp)).tok, "identifier '{0}' does not denote a trait", ((UserDefinedType)(traitTyp)).tok.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(((UserDefinedType)(traitTyp)).tok, 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.TraitsObj.Add((TraitDecl)trait);

-                      }

-                  }

-              }

+      foreach (var tt in cl.TraitsTyp) {

+        var prevErrorCount = ErrorCount;

+        ResolveType(cl.tok, tt, new NoContext(cl.Module), ResolveTypeOptionEnum.DontInfer, null);

+        if (ErrorCount == prevErrorCount) {

+          var udt = tt as UserDefinedType;

+          if (udt != null && udt.ResolvedClass is TraitDecl) {

+            var trait = (TraitDecl)udt.ResolvedClass;

+            //disallowing inheritance in multi module case

+            if (cl.Module != trait.Module) {

+              Error(udt.tok, "class '{0}' is in a different module than trait '{1}'. A class may only extend a trait in the same module.", cl.Name, trait.FullName);

+            } else {

+              // all is good

+              cl.TraitsObj.Add(trait);

+            }

+          } else {

+            Error(udt != null ? udt.tok : cl.tok, "a class can only extend traits (found '{0}')", tt);

           }

+        }

       }

 

       foreach (MemberDecl member in cl.Members) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index c9c900af..2672258d 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -155,6 +155,7 @@ namespace Microsoft.Dafny {
       public readonly Bpl.Type Ty;

       public readonly Bpl.Type TyTag;

       public readonly Bpl.Expr Null;

+      public readonly Bpl.Expr NoTraitAtAll;

       private readonly Bpl.Constant allocField;

       [ContractInvariantMethod]

       void ObjectInvariant() {

@@ -178,6 +179,7 @@ namespace Microsoft.Dafny {
         Contract.Invariant(Ty != null);

         Contract.Invariant(TyTag != null);

         Contract.Invariant(Null != null);

+        Contract.Invariant(NoTraitAtAll != null);

         Contract.Invariant(allocField != null);

       }

 

@@ -282,6 +284,7 @@ namespace Microsoft.Dafny {
         this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new List<Bpl.Type>());

         this.allocField = allocField;

         this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);

+        this.NoTraitAtAll = new Bpl.IdentifierExpr(Token.NoToken, "NoTraitAtAll", ClassNameType);

       }

     }

 

@@ -537,8 +540,7 @@ namespace Microsoft.Dafny {
         }

       }

 

-      //adding TraitParent function and axioms

-      AddTraitParentFuncAndAxioms();

+      AddTraitParentAxioms();

 

       if (InsertChecksums)

       {

@@ -561,35 +563,24 @@ namespace Microsoft.Dafny {
       return sink;

     }

 

-    //adding TraitParent function and axioms

-    //if a class A extends trait J and B does not extned anything, then this method adds the followings to the sink:

-    //   const unique NoTraitAtAll: ClassName;

-    //   function TraitParent(ClassName): ClassName;

-    //   axiom TraitParent(class.A) == class.J;

-    //   axiom TraitParent(class.B) == NoTraitAtAll;

-    private void AddTraitParentFuncAndAxioms()

+    /// <summary>

+    /// adding TraitParent axioms

+    /// if a class A extends trait J and B does not extend anything, then this method adds the followings to the sink:

+    ///   axiom TraitParent(class.A) == class.J;

+    ///   axiom TraitParent(class.B) == NoTraitAtAll;

+    /// </summary>

+    private void AddTraitParentAxioms()

     {

         foreach (ModuleDefinition m in program.Modules)

         {

-            if (m.TopLevelDecls.Any(d => (d is ClassDecl && ((ClassDecl)d).TraitsObj != null && ((ClassDecl)d).TraitsObj.Count > 0) || (d is TraitDecl)))

+            if (m.TopLevelDecls.Any(d => (d is ClassDecl && ((ClassDecl)d).TraitsObj.Count > 0) || (d is TraitDecl)))

             {

-                //adding const unique NoTraitAtAll: ClassName;

-                Token tNoTrait = new Token();

-                Token tTraitParent = new Token();

-                Bpl.Constant cNoTrait = new Bpl.Constant(tNoTrait, new Bpl.TypedIdent(tNoTrait, "NoTraitAtAll", predef.ClassNameType), true);

-                sink.AddTopLevelDeclaration(cNoTrait);

-                //adding function TraitParent(ClassName): ClassName;

-                var arg_ref = new Bpl.Formal(tTraitParent, new Bpl.TypedIdent(tTraitParent, Bpl.TypedIdent.NoName, predef.ClassNameType), true);

-                var res = new Bpl.Formal(tTraitParent, new Bpl.TypedIdent(tTraitParent, Bpl.TypedIdent.NoName, predef.ClassNameType), false);

-                var fTraitParent = new Bpl.Function(tTraitParent, "TraitParent", new List<Variable> { arg_ref }, res);

-                sink.AddTopLevelDeclaration(fTraitParent);

-

                 foreach (TopLevelDecl d in m.TopLevelDecls)

                 {

                     if (d is ClassDecl)

                     {

                         var c = (ClassDecl)d;

-                        if (c is ClassDecl && c.TraitsObj != null && c.TraitsObj.Count > 0)

+                        if (c.TraitsObj.Count > 0)

                         {

                             foreach (TraitDecl traitObj in c.TraitsObj)

                             {

@@ -598,27 +589,18 @@ namespace Microsoft.Dafny {
                                 Bpl.Constant trait = new Bpl.Constant(traitObj.tok, trait_id, true);

                                 Bpl.Expr traitId_expr = new Bpl.IdentifierExpr(traitObj.tok, trait);

 

-                                var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);

-                                var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), false);

-                                var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "TraitParent", new List<Variable> { args }, ret_value));

-                                var funCallExpr = new Bpl.NAryExpr(c.tok, funCall, new List<Expr> { new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType) });

+                                var id = new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType);

+                                var funCallExpr = FunctionCall(c.tok, BuiltinFunction.TraitParent, null, id);

                                 var traitParentAxiom = new Bpl.Axiom(c.tok, Bpl.Expr.Eq(funCallExpr, traitId_expr));

 

                                 sink.AddTopLevelDeclaration(traitParentAxiom);

                             }

                         }

-                        else if (c is ClassDecl && (c.TraitsObj == null || c.TraitsObj.Count == 0))

+                        else

                         {

-                            //this adds: axiom TraitParent(class.B) == NoTraitAtAll; Where B does not extend any traits

-                            Bpl.TypedIdent noTraitAtAll_id = new Bpl.TypedIdent(c.tok, "NoTraitAtAll", predef.ClassNameType);

-                            Bpl.Constant noTraitAtAll = new Bpl.Constant(c.tok, noTraitAtAll_id, true);

-                            Bpl.Expr noTraitAtAll_expr = new Bpl.IdentifierExpr(c.tok, noTraitAtAll);

-

-                            var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);

-                            var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), false);

-                            var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "TraitParent", new List<Variable> { args }, ret_value));

-                            var funCallExpr = new Bpl.NAryExpr(c.tok, funCall, new List<Expr> { new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType) });

-                            var traitParentAxiom = new Bpl.Axiom(c.tok, Bpl.Expr.Eq(funCallExpr, noTraitAtAll_expr));

+                            var id = new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType);

+                            var funCallExpr = FunctionCall(c.tok, BuiltinFunction.TraitParent, null, id);

+                            var traitParentAxiom = new Bpl.Axiom(c.tok, Bpl.Expr.Eq(funCallExpr, predef.NoTraitAtAll));

 

                             sink.AddTopLevelDeclaration(traitParentAxiom);

                         }

@@ -1365,7 +1347,7 @@ namespace Microsoft.Dafny {
                       {

                           var t = (TraitDecl)c;

                           var dtypeFunc = FunctionCall(o.tok, BuiltinFunction.DynamicType, null, o);

-                          Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.Name, Bpl.Type.Bool, new List<Expr> { dtypeFunc });

+                          Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.FullSanitizedName, Bpl.Type.Bool, new List<Expr> { dtypeFunc });

                           rhs = BplOr(o_null, implementsFunc);

                       }

                       else

@@ -1380,34 +1362,20 @@ namespace Microsoft.Dafny {
           });

       }

 

-      //this adds: function implements$J(ClassName): bool;

-      if (c is TraitDecl)

-      {

-          var arg_ref = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);

-          var res = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);

-          var implement_intr = new Bpl.Function(c.tok, "implements$" + c.Name, new List<Variable> { arg_ref }, res);

-          sink.AddTopLevelDeclaration(implement_intr);

-      }

-      //this adds: axiom implements$J(class.C);

-      else if (c is ClassDecl)

-      {

-          if (c.TraitsObj != null && c.TraitsObj.Count > 0)

-          {

-              //var dtypeFunc = FunctionCall(c.tok, BuiltinFunction.DynamicType, null, o);

-              //Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.Name, Bpl.Type.Bool, new List<Expr> { dtypeFunc });

-              foreach (Type traitType in c.TraitsTyp)

-              {

-                  if (traitType is UserDefinedType)

-                  {

-                      var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);

-                      var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);

-                      var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "implements$" + ((UserDefinedType)(traitType)).tok, new List<Variable> { args }, ret_value));

-                      var expr = new Bpl.NAryExpr(c.tok, funCall, new List<Expr> { new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType) });

-                      var implements_axiom = new Bpl.Axiom(c.tok, expr);

-                      sink.AddTopLevelDeclaration(implements_axiom);

-                  }

-              }

-          }

+      if (c is TraitDecl) {

+        //this adds: function implements$J(Ty): bool;

+        var arg_ref = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.Ty), true);

+        var res = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);

+        var implement_intr = new Bpl.Function(c.tok, "implements$" + c.FullSanitizedName, new List<Variable> { arg_ref }, res);

+        sink.AddTopLevelDeclaration(implement_intr);

+      } else if (c is ClassDecl) {

+        //this adds: axiom implements$J(class.C);

+        foreach (var trait in c.TraitsObj) {

+          var arg = ClassTyCon(c, new List<Expr>());  // TODO: this needs more work if overridingClass has type parameters

+          var expr = FunctionCall(c.tok, "implements$" + trait.FullSanitizedName, Bpl.Type.Bool, arg);

+          var implements_axiom = new Bpl.Axiom(c.tok, expr);

+          sink.AddTopLevelDeclaration(implements_axiom);

+        }

       }

 

       foreach (MemberDecl member in c.Members) {

@@ -1514,7 +1482,7 @@ namespace Microsoft.Dafny {
       AddFrameAxiom(f);

       // add consequence axiom

       sink.AddTopLevelDeclaration(FunctionConsequenceAxiom(f, f.Ens));

-      // add definition axioms, suitably specialized for "match" cases and for literals

+      // add definition axioms, suitably specialized for literals

       if (f.Body != null && !IsOpaqueFunction(f)) {

         AddFunctionAxiom(f, FunctionAxiomVisibility.IntraModuleOnly, f.Body.Resolved);

         AddFunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, f.Body.Resolved);

@@ -2097,10 +2065,11 @@ namespace Microsoft.Dafny {
       }

     }

 

-    Bpl.Axiom FunctionAxiom(Function f, FunctionAxiomVisibility visibility, Expression body, ICollection<Formal> lits) {

+    Bpl.Axiom FunctionAxiom(Function f, FunctionAxiomVisibility visibility, Expression body, ICollection<Formal> lits, TopLevelDecl overridingClass = null) {

       Contract.Requires(f != null);

       Contract.Requires(predef != null);

       Contract.Requires(f.EnclosingClass != null);

+      Contract.Requires(!f.IsStatic || overridingClass == null);

 

       // only if body is null, we will return null:

       Contract.Ensures((Contract.Result<Bpl.Axiom>() == null) == (body == null));

@@ -2114,7 +2083,8 @@ namespace Microsoft.Dafny {
       //   ==>

       //   (forall s, $Heap, formals ::                  // let args := $Heap,formals

       //       { f(Succ(s), args) }                      // (*)

-      //       f#canCall(args) || USE_VIA_CONTEXT

+      //       (f#canCall(args) || USE_VIA_CONTEXT) &&

+      //       dtype(this) == overridingClass            // if "overridingClass" != null

       //       ==>

       //       BODY-can-make-its-calls &&

       //       f(Succ(s), args) == BODY);                // (*)

@@ -2178,6 +2148,7 @@ namespace Microsoft.Dafny {
       // ante:  $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&

       Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);

 

+      Bpl.Expr additionalAntecedent = null;

       if (!f.IsStatic) {

         var bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, etran.This, predef.RefType));

         formals.Add(bvThis);

@@ -2189,6 +2160,10 @@ namespace Microsoft.Dafny {
           Bpl.Expr.Neq(bvThisIdExpr, predef.Null),

           etran.GoodRef(f.tok, bvThisIdExpr, thisType));

         ante = Bpl.Expr.And(ante, wh);

+        if (overridingClass != null) {

+          // additionalAntecednet := dtype(this) == overridingClass

+          additionalAntecedent = DType(bvThisIdExpr, ClassTyCon(overridingClass, new List<Expr>()));  // TODO: this needs more work if overridingClass has type parameters

+        }

       }

 

       var substMap = new Dictionary<IVariable, Expression>();

@@ -2225,11 +2200,13 @@ namespace Microsoft.Dafny {
 

       // Add the precondition function and its axiom (which is equivalent to the ante)

       if (body == null || (visibility == FunctionAxiomVisibility.IntraModuleOnly && lits == null)) {

-        var precondF = new Bpl.Function(f.tok,

-          RequiresName(f), new List<Bpl.TypeVariable>(),

-          formals.ConvertAll(v => (Bpl.Variable)BplFormalVar(null, v.TypedIdent.Type, true)),

-          BplFormalVar(null, Bpl.Type.Bool, false));

-        sink.AddTopLevelDeclaration(precondF);

+        if (overridingClass == null) {

+          var precondF = new Bpl.Function(f.tok,

+            RequiresName(f), new List<Bpl.TypeVariable>(),

+            formals.ConvertAll(v => (Bpl.Variable)BplFormalVar(null, v.TypedIdent.Type, true)),

+            BplFormalVar(null, Bpl.Type.Bool, false));

+          sink.AddTopLevelDeclaration(precondF);

+        }

         var appl = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool,

           formals.ConvertAll(x => (Bpl.Expr)(new Bpl.IdentifierExpr(f.tok, x))));

         sink.AddTopLevelDeclaration(new Axiom(f.tok, BplForall(formals, BplTrigger(appl), Bpl.Expr.Eq(appl, ante))));

@@ -2246,6 +2223,9 @@ namespace Microsoft.Dafny {
 

       // ante := useViaCanCall || (useViaContext && typeAnte && pre)

       ante = Bpl.Expr.Or(useViaCanCall, ante);

+      if (additionalAntecedent != null) {

+        ante = Bpl.Expr.And(ante, additionalAntecedent);

+      }

 

       Bpl.Expr funcAppl;

       {

@@ -2287,7 +2267,11 @@ namespace Microsoft.Dafny {
       Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, kv, tr, Bpl.Expr.Imp(ante, meat));

       var activate = AxiomActivation(f, visibility == FunctionAxiomVisibility.ForeignModuleOnly, visibility == FunctionAxiomVisibility.IntraModuleOnly, etran);

       string comment;

-      comment = "definition axiom for " + f.FullSanitizedName;

+      if (overridingClass == null) {

+        comment = "definition axiom for " + f.FullSanitizedName;

+      } else {

+        comment = "override axiom for " + f.FullSanitizedName + " in class " + overridingClass.FullSanitizedName;

+      }

       if (lits != null) {

         if (lits.Count == f.Formals.Count) {

           comment += " for all literals";

@@ -3056,67 +3040,32 @@ namespace Microsoft.Dafny {
 

     private void AddFunctionOverrideAxiom(Function f)

     {

-        Contract.Requires(f != null);

-        Contract.Requires(sink != null && predef != null);

-        // function override axiom

-        // axiom (forall $heap: HeapType, this: ref, x#0: int ::

-        //     { J.F($heap, this, x#0) }

-        //     this != null && dtype(this) == class.C

-        //     ==>

-        //     J.F($heap, this, x#0) == C.F($heap, this, x#0));

-

-        var formals = new List<Variable>();

-        var argsC = new List<Bpl.Expr>();

-        var argsT = new List<Bpl.Expr>();

-

-        var bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType));

-        var s = new Bpl.IdentifierExpr(f.tok, bv);

-        if (f.IsRecursive)

-        {

-            formals.Add(bv);

-            argsC.Add(FunctionCall(f.tok, BuiltinFunction.LayerSucc, null, s));

-            argsT.Add(FunctionCall(f.tok, BuiltinFunction.LayerSucc, null, s));

-        }

-

-        bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));

-        formals.Add(bv);

-        s = new Bpl.IdentifierExpr(f.tok, bv);

-        argsC.Add(s);

-        argsT.Add(s);

-

-        if (!f.IsStatic)

-        {

-            bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));

-            formals.Add(bv);

-            s = new Bpl.IdentifierExpr(f.tok, bv);

-            argsC.Add(s);

-            argsT.Add(s);

-        }

-        foreach (var p in f.Formals)

-        {

-            bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, f.FullSanitizedName + "_" + p.AssignUniqueName(f.IdGenerator), TrType(p.Type)));

-            formals.Add(bv);

-            s = new Bpl.IdentifierExpr(f.tok, bv);

-            argsC.Add(s);

-        }

-        foreach (var p in f.OverriddenFunction.Formals)

-        {

-            bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, f.OverriddenFunction.FullSanitizedName + "_" + p.AssignUniqueName(f.OverriddenFunction.IdGenerator), TrType(p.Type)));

-            formals.Add(bv);

-            s = new Bpl.IdentifierExpr(f.OverriddenFunction.tok, bv);

-            argsT.Add(s);

-        }

-

-        var funcIdC = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));

-        var funcIdT = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.OverriddenFunction.tok, f.OverriddenFunction.FullSanitizedName, TrType(f.OverriddenFunction.ResultType)));

-        var funcApplC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);

-        var funcApplT = new Bpl.NAryExpr(f.OverriddenFunction.tok, funcIdT, argsT);

-

-        var typeParams = TrTypeParamDecls(f.TypeArgs);

+      Contract.Requires(f != null);

+      Contract.Requires(!f.IsStatic);  // only instance functions can be overridden

+      Contract.Requires(sink != null && predef != null);

 

-        Bpl.Trigger tr = new Bpl.Trigger(f.OverriddenFunction.tok, true, new List<Bpl.Expr> { funcApplT, funcApplC });

-        Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Eq(funcApplC, funcApplT));

-        sink.AddTopLevelDeclaration(new Bpl.Axiom(f.tok, ax, "function override axiom"));

+      // Essentially, the function override axiom looks like:

+      //   axiom (forall $heap: HeapType, this: ref, x#0: int ::

+      //     { J.F($heap, this, x#0) }

+      //     this != null && dtype(this) == class.C

+      //     ==>

+      //     J.F($heap, this, x#0) == C.F($heap, this, x#0));

+      // but it also has the various usual antecedents.  Essentially, the override gives a part of the body of the

+      // trait's function, so we call FunctionAxiom to generate a conditional axiom (that is, we pass in the "overridingClass"

+      // parameter to FunctionAxiom, which will add 'dtype(this) == class.C' as an additional antecedent) for a

+      // body of 'C.F(this, x#0)'.

+      // TODO:  More work needs to be done to support any type parameters that class C might have.  These would

+      // need to be quantified (existentially?) in the axiom.

+      var receiver = new ThisExpr(f.tok);

+      receiver.Type = Resolver.GetReceiverType(f.tok, f);

+      var args = f.OverriddenFunction.Formals.ConvertAll(p => (Expression)new IdentifierExpr(p.tok, p.Name) { Var = p, Type = p.Type });

+      var pseudoBody = new FunctionCallExpr(f.tok, f.Name, new ThisExpr(f.tok), f.tok, args);

+      pseudoBody.Function = f;  // resolve here

+      // TODO: the following two lines (incorrectly) assume there are no type parameters

+      pseudoBody.Type = f.ResultType;  // resolve here

+      pseudoBody.TypeArgumentSubstitutions = new Dictionary<TypeParameter,Type>();  // resolve here

+      sink.AddTopLevelDeclaration(FunctionAxiom(f.OverriddenFunction, FunctionAxiomVisibility.IntraModuleOnly, pseudoBody, null, f.EnclosingClass));

+      sink.AddTopLevelDeclaration(FunctionAxiom(f.OverriddenFunction, FunctionAxiomVisibility.ForeignModuleOnly, pseudoBody, null, f.EnclosingClass));

     }

 

     private void AddFunctionOverrideEnsChk(Function f, StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap, List<Variable> implInParams)

@@ -11718,6 +11667,8 @@ namespace Microsoft.Dafny {
       Is, IsBox,

       IsAlloc, IsAllocBox,

 

+      TraitParent,

+

       SetCard,

       SetEmpty,

       SetUnionOne,

@@ -11895,6 +11846,11 @@ namespace Microsoft.Dafny {
           Contract.Assert(typeInstantiation == null);

           return FunctionCall(tok, "$IsAllocBox", Bpl.Type.Bool, args);

 

+        case BuiltinFunction.TraitParent:

+          Contract.Assert(args.Length == 1);

+          Contract.Assert(typeInstantiation == null);

+          return FunctionCall(tok, "TraitParent", predef.ClassNameType, args);

+

         case BuiltinFunction.SetCard:

           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation == null);