Now the parser parses "Type" rather than "IToken" for a trait

9 files changed, 47 insertions, 45 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 0d77ecc6..60e737b1 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), new List<IToken> { dd.TraitId });

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

         }

       } else if (d is ModuleDecl) {

         if (d is LiteralModuleDecl) {

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index a3312c4a..0e8b886b 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -247,9 +247,9 @@ namespace Microsoft.Dafny {
           else if (d is ClassDecl) {

             var cl = (ClassDecl)d;

             Indent(indent);

-            if (cl.Trait != null && cl.Trait is TraitDecl)

+            if (cl.TraitObj != null && cl.TraitObj is TraitDecl)

             {

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

+                wr.WriteLine("public class @{0} : @{1}", cl.CompileName, ((UserDefinedType)cl.TraitTyp).tok);

             }

             else

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

@@ -767,7 +767,7 @@ namespace Microsoft.Dafny {
                   {

                       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.Write("{0} @{1}.@{2}", TypeName(f.Type), c.TraitObj.CompileName, f.CompileName);

                       wr.WriteLine(" {");

                       wr.WriteLine(" get { ");

                       wr.Write("return this.@{0};", f.CompileName);

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 690f8403..5bc8ad5f 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -354,7 +354,7 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
 = (. Contract.Requires(module != null);

      Contract.Ensures(Contract.ValueAtReturn(out c) != null);

      IToken/*!*/ id;

-     List<IToken>/*!*/ traitId=null;

+     Type/*!*/ trait = null;

 	 Attributes attrs = null;

      List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();

      List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

@@ -365,12 +365,12 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
   { Attribute<ref attrs> }

   NoUSIdent<out id>

   [ GenericParameters<typeArgs> ]

-  ["extends" QualifiedName<out traitId>]

-  "{"                                            (. bodyStart = t; .)

+  ["extends" Type<out trait>]         

+  "{"                                            (. bodyStart = t;  .)

   { ClassMemberDecl<members, true>

   }

   "}"

-  (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traitId);

+  (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, trait);

      c.BodyStartTok = bodyStart;

      c.BodyEndTok = t;

   .)

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 7fa8df76..58666c6a 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1688,8 +1688,8 @@ namespace Microsoft.Dafny {
 

   public class ClassDecl : TopLevelDecl {

     public readonly List<MemberDecl> Members;

-    public TraitDecl Trait;

-    public readonly IToken TraitId;

+    public TraitDecl TraitObj;

+    public readonly Type TraitTyp;

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

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -1697,7 +1697,7 @@ namespace Microsoft.Dafny {
     }

 

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

-      List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes, List<IToken> traitId)

+      List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes, Type trait)

       : base(tok, name, module, typeArgs, attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -1705,8 +1705,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

+      if (trait != null)

+          TraitTyp = trait; //there are at most one inheriting trait at the moment

     }

     public virtual bool IsDefaultClass {

       get {

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index f990f9ff..dd1ff730 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -465,7 +465,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		Contract.Requires(module != null);

 		Contract.Ensures(Contract.ValueAtReturn(out c) != null);

 		IToken/*!*/ id;

-		List<IToken>/*!*/ traitId=null;

+		Type/*!*/ trait = null;

 		Attributes attrs = null;

 		List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();

 		List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

@@ -482,15 +482,15 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		}

 		if (la.kind == 31) {

 			Get();

-			QualifiedName(out traitId);

+			Type(out trait);

 		}

 		Expect(15);

-		bodyStart = t; 

+		bodyStart = t;  

 		while (StartOf(2)) {

 			ClassMemberDecl(members, true);

 		}

 		Expect(16);

-		c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traitId);

+		c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, trait);

 		c.BodyStartTok = bodyStart;

 		c.BodyEndTok = t;

 		

@@ -837,6 +837,11 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		Expect(47);

 	}

 

+	void Type(out Type ty) {

+		Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; 

+		TypeAndToken(out tok, out ty);

+	}

+

 	void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {

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

 		Attributes attrs = null;

@@ -1164,11 +1169,6 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		}

 	}

 

-	void Type(out Type ty) {

-		Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; 

-		TypeAndToken(out tok, out ty);

-	}

-

 	void Expression(out Expression e, bool allowSemi, bool allowLambda) {

 		Expression e0; IToken endTok; 

 		EquivExpression(out e, allowSemi, allowLambda);

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 9e569ef1..36eeb554 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -298,8 +298,8 @@ 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.TraitTyp != null) {

+          wr.Write(" extends {0}", ((UserDefinedType)(c.TraitTyp)).tok);

       }

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

         wr.WriteLine(" { }");

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 99045b01..b6b0ab0b 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2657,21 +2657,22 @@ namespace Microsoft.Dafny
       currentClass = cl;

 

       // Resolve names of traits extended

-      if (cl.TraitId != null) {

-        var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == cl.TraitId.val);

+      if (cl.TraitTyp != null && cl.TraitTyp is UserDefinedType)

+      {

+          var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == ((UserDefinedType)(cl.TraitTyp)).FullCompileName);

         if (trait == null) {

-          Error(cl.TraitId, "unresolved identifier: {0}", cl.TraitId.val);

+            Error(((UserDefinedType)(cl.TraitTyp)).tok, "unresolved identifier: {0}", ((UserDefinedType)(cl.TraitTyp)).tok.val);

         } else if (!(trait is TraitDecl)) {

-          Error(cl.TraitId, "identifier '{0}' does not denote a trait", cl.TraitId.val);

+            Error(((UserDefinedType)(cl.TraitTyp)).tok, "identifier '{0}' does not denote a trait", ((UserDefinedType)(cl.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(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",

+              Error(((UserDefinedType)(cl.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.Trait = (TraitDecl)trait;

+            cl.TraitObj = (TraitDecl)trait;

           }

         }

       }

@@ -2730,9 +2731,9 @@ namespace Microsoft.Dafny
       Contract.Requires(cl != null);

 

       //merging class members with parent members if any

-      if (cl.Trait != null) {

+      if (cl.TraitObj != null) {

         var clMembers = classMembers[cl];

-        var traitMembers = classMembers[cl.Trait];

+        var traitMembers = classMembers[cl.TraitObj];

         //merging current class members with the inheriting trait

         foreach (KeyValuePair<string, MemberDecl> traitMem in traitMembers) {

           MemberDecl clMember;

@@ -2815,7 +2816,7 @@ namespace Microsoft.Dafny
         //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)) {

+        foreach (MemberDecl traitMember in cl.TraitObj.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

@@ -4021,9 +4022,9 @@ namespace Microsoft.Dafny
           }

           return successSoFar;

         } else if ((bb.ResolvedClass is ClassDecl) && (aa.ResolvedClass is TraitDecl)) {

-          return ((ClassDecl)bb.ResolvedClass).Trait.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName;

+          return ((ClassDecl)bb.ResolvedClass).TraitObj.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName;

         } else if ((aa.ResolvedClass is ClassDecl) && (bb.ResolvedClass is TraitDecl)) {

-          return ((ClassDecl)aa.ResolvedClass).Trait.FullCompileName == ((TraitDecl)bb.ResolvedClass).FullCompileName;

+          return ((ClassDecl)aa.ResolvedClass).TraitObj.FullCompileName == ((TraitDecl)bb.ResolvedClass).FullCompileName;

         } else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) {

           // type parameters

           if (aa.TypeArgs.Count != bb.TypeArgs.Count) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 72a9e752..cdf9eb86 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -509,7 +509,7 @@ namespace Microsoft.Dafny {
     {

         foreach (ModuleDefinition m in program.Modules)

         {

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

+            if (m.TopLevelDecls.Any(d => (d is ClassDecl && ((ClassDecl)d).TraitObj != null) || (d is TraitDecl)))

             {

                 //adding const unique NoTraitAtAll: ClassName;

                 Token tNoTrait = new Token();

@@ -527,12 +527,12 @@ namespace Microsoft.Dafny {
                     if (d is ClassDecl)

                     {

                         var c = (ClassDecl)d;

-                        if (c is ClassDecl && c.Trait != null)

+                        if (c is ClassDecl && c.TraitObj != null)

                         {

                             //this adds: axiom TraitParent(class.A) == class.J; Where A extends J

-                            Bpl.TypedIdent trait_id = new Bpl.TypedIdent(c.Trait.tok, string.Format("class.{0}", c.Trait.FullSanitizedName), predef.ClassNameType);

-                            Bpl.Constant trait = new Bpl.Constant(c.Trait.tok, trait_id, true);

-                            Bpl.Expr traitId_expr = new Bpl.IdentifierExpr(c.Trait.tok, trait);

+                            Bpl.TypedIdent trait_id = new Bpl.TypedIdent(c.TraitObj.tok, string.Format("class.{0}", c.TraitObj.FullSanitizedName), predef.ClassNameType);

+                            Bpl.Constant trait = new Bpl.Constant(c.TraitObj.tok, trait_id, true);

+                            Bpl.Expr traitId_expr = new Bpl.IdentifierExpr(c.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);

@@ -542,7 +542,7 @@ namespace Microsoft.Dafny {
 

                             sink.AddTopLevelDeclaration(traitParentAxiom);

                         }

-                        else if (c is ClassDecl && c.Trait == null)

+                        else if (c is ClassDecl && c.TraitObj == null)

                         {

                             //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);

@@ -1325,14 +1325,14 @@ namespace Microsoft.Dafny {
       //this adds: axiom implements$J(class.C);

       else if (c is ClassDecl)

       {

-          if (c.Trait != null)

+          if (c.TraitObj != null)

           {

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

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

 

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

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

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

+              var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "implements$" + ((UserDefinedType)(c.TraitTyp)).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);

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 2bda7cf0..16349ccc 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -39,7 +39,7 @@ namespace Microsoft.Dafny
     public static int ThreadMain(string[] args)

     {

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

-

+         

       printer = new DafnyConsolePrinter();

       ExecutionEngine.printer = printer;

 

@@ -51,7 +51,7 @@ namespace Microsoft.Dafny
         exitValue = ExitValue.PREPROCESSING_ERROR;

         goto END;

       }

-      //CommandLineOptions.Clo.Files = new List<string> { @"C:\dafny\Test\dafny0\Trait\TraitOverride1.dfy" };

+      //CommandLineOptions.Clo.Files = new List<string> { @"C:\dafny\Test\dafny0\Trait\TraitExtend.dfy" };

 

       if (CommandLineOptions.Clo.Files.Count == 0)

       {

@@ -109,6 +109,7 @@ namespace Microsoft.Dafny
           // TODO(wuestholz): We should probably add a separate flag for this. This is currently only used by the new testing infrastructure.

           return 0;

         }

+        //Console.ReadKey();

         return (int)exitValue;

     }