Dafny: changed iterators to become special cases of classes

4 files changed, 61 insertions, 115 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 71e48fdf..dd190b6c 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -287,16 +287,6 @@ namespace Microsoft.Dafny {
         return IsCoDatatype;  // TODO: should really check structure of the type recursively

       }

     }

-    public IteratorDecl AsIteratorType {

-      get {

-        UserDefinedType udt = this as UserDefinedType;

-        if (udt == null) {

-          return null;

-        } else {

-          return udt.ResolvedClass as IteratorDecl;

-        }

-      }

-    }

     public bool IsTypeParameter {

       get {

         return AsTypeParameter != null;

@@ -587,8 +577,6 @@ namespace Microsoft.Dafny {
             i++;

           }

           return true;

-        } else if (ResolvedClass is IteratorDecl) {

-          return false;

         } else if (ResolvedParam != null) {

           return ResolvedParam.MustSupportEquality;

         }

@@ -1168,7 +1156,7 @@ namespace Microsoft.Dafny {
     ModuleDefinition EnclosingModule { get; }  // to be called only after signature-resolution is complete

   }

 

-  public class IteratorDecl : TopLevelDecl, ICodeContext

+  public class IteratorDecl : ClassDecl, ICodeContext

   {

     public readonly List<Formal> Ins;

     public readonly List<Formal> Outs;

@@ -1182,7 +1170,6 @@ namespace Microsoft.Dafny {
     public readonly List<MaybeFreeExpression> YieldEnsures;

     public readonly BlockStmt Body;

     public readonly bool SignatureIsOmitted;

-    public Dictionary<string, MemberDecl> ImplicitlyDefinedMembers;  // filled in during resolution

     public IteratorDecl(IToken tok, string name, ModuleDefinition module, List<TypeParameter> typeArgs,

                         List<Formal> ins, List<Formal> outs,

                         Specification<FrameExpression> reads, Specification<FrameExpression> mod, Specification<Expression> decreases,

@@ -1191,7 +1178,7 @@ namespace Microsoft.Dafny {
                         List<MaybeFreeExpression> yieldRequires,

                         List<MaybeFreeExpression> yieldEnsures,

                         BlockStmt body, Attributes attributes, bool signatureIsOmitted)

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

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

     {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -3021,27 +3008,15 @@ namespace Microsoft.Dafny {
   public class StaticReceiverExpr : LiteralExpr

   {

     public StaticReceiverExpr(IToken tok, ClassDecl cl)

-      : this(cl, tok)  // constructs a LiteralExpr representing the 'null' literal

-    {

-      Contract.Requires(tok != null);

-      Contract.Requires(cl != null);

-    }

-    public StaticReceiverExpr(IToken tok, IteratorDecl iter)

-      : this(iter, tok)  // constructs a LiteralExpr representing the 'null' literal

-    {

-      Contract.Requires(tok != null);

-      Contract.Requires(iter != null);

-    }

-    private StaticReceiverExpr(TopLevelDecl decl, IToken tok)  // switch the order of the parameters, just to disambiguate calls

       : base(tok)  // constructs a LiteralExpr representing the 'null' literal

     {

       Contract.Requires(tok != null);

-      Contract.Requires(decl != null);

+      Contract.Requires(cl != null);

       var typeArgs = new List<Type>();

-      foreach (var ta in decl.TypeArgs) {

+      foreach (var ta in cl.TypeArgs) {

         typeArgs.Add(new InferredTypeProxy());

       }

-      Type = new UserDefinedType(tok, decl.Name, decl, typeArgs);

+      Type = new UserDefinedType(tok, cl.Name, cl, typeArgs);

     }

   }

 

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 5c5c95b5..1e2424ed 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -53,17 +53,6 @@ namespace Microsoft.Dafny {
         } else if (d is DatatypeDecl) {

           if (i++ != 0) { wr.WriteLine(); }

           PrintDatatype((DatatypeDecl)d, indent);

-        } else if (d is ClassDecl) {

-          ClassDecl cl = (ClassDecl)d;

-          if (!cl.IsDefaultClass) {

-            if (i++ != 0) { wr.WriteLine(); }

-            PrintClass(cl, indent);

-          } else if (cl.Members.Count == 0) {

-            // print nothing

-          } else {

-            if (i++ != 0) { wr.WriteLine(); }

-            PrintMembers(cl.Members, indent);

-          }

         } else if (d is IteratorDecl) {

           var iter = (IteratorDecl)d;

           Indent(indent);

@@ -106,19 +95,27 @@ namespace Microsoft.Dafny {
 

           if (DafnyOptions.O.DafnyPrintResolvedFile != null) {

             // also print the members that were created as part of the interpretation of the iterator

-            Contract.Assert(iter.ImplicitlyDefinedMembers != null);  // filled in during resolution

-            var members = new List<MemberDecl>();

-            foreach (var m in iter.ImplicitlyDefinedMembers.Values) {

-              members.Add(m);

-            }

+            Contract.Assert(iter.Members.Count != 0);  // filled in during resolution

             wr.WriteLine("/*---------- iterator members ----------");

             PrintClassMethodHelper("class", null, iter.Name, iter.TypeArgs);

             wr.WriteLine(" {");

-            PrintMembers(members, indent + IndentAmount);

+            PrintMembers(iter.Members, indent + IndentAmount);

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

             wr.WriteLine("---------- iterator members ----------*/");

           }

 

+        } else if (d is ClassDecl) {

+          ClassDecl cl = (ClassDecl)d;

+          if (!cl.IsDefaultClass) {

+            if (i++ != 0) { wr.WriteLine(); }

+            PrintClass(cl, indent);

+          } else if (cl.Members.Count == 0) {

+            // print nothing

+          } else {

+            if (i++ != 0) { wr.WriteLine(); }

+            PrintMembers(cl.Members, indent);

+          }

+

         } else if (d is ModuleDecl) {

           wr.WriteLine();

           Indent(indent);

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index f2a386f4..03f8faad 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -131,8 +131,6 @@ namespace Microsoft.Dafny
                   if (nw.TypeArgs.Count != d.TypeArgs.Count) {

                     reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters", nw.Name);

                   }

-                } else if (nw is IteratorDecl) {

-                  reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by an iterator");

                 } else if (nw is CoDatatypeDecl) {

                   reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by a codatatype");

                 } else {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 7b11a932..d568ab0e 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -496,39 +496,12 @@ namespace Microsoft.Dafny
         } else if (d is ArbitraryTypeDecl) {

           // nothing more to register

 

-        } else if (d is ClassDecl) {

-          ClassDecl cl = (ClassDecl)d;

-

-          // register the names of the class members

-          Dictionary<string, MemberDecl> members = new Dictionary<string, MemberDecl>();

-          classMembers.Add(cl, members);

-

-          bool hasConstructor = false;

-          foreach (MemberDecl m in cl.Members) {

-            if (members.ContainsKey(m.Name)) {

-              Error(m, "Duplicate member name: {0}", m.Name);

-            } else {

-              members.Add(m.Name, m);

-            }

-            if (m is Constructor) {

-              hasConstructor = true;

-            }

-          }

-          cl.HasConstructor = hasConstructor;

-          if (cl.IsDefaultClass) {

-            foreach (MemberDecl m in cl.Members) {

-              if (m.IsStatic && (m is Function || m is Method)) {

-                sig.StaticMembers[m.Name] = m;

-              }

-            }

-          }

-

         } else if (d is IteratorDecl) {

           var iter = (IteratorDecl)d;

 

           // register the names of the implicit members

           var members = new Dictionary<string, MemberDecl>();

-          iter.ImplicitlyDefinedMembers = members;

+          classMembers.Add(iter, members);

 

           // First, register the iterator's in- and out-parameters as readonly fields

           foreach (var p in iter.Ins) {

@@ -538,6 +511,7 @@ namespace Microsoft.Dafny
               var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, false, p.Type, null);

               field.EnclosingClass = iter;  // resolve here

               members.Add(p.Name, field);

+              iter.Members.Add(field);

             }

           }

           foreach (var p in iter.Outs) {

@@ -547,6 +521,7 @@ namespace Microsoft.Dafny
               var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, false, p.Type, null);

               field.EnclosingClass = iter;  // resolve here

               members.Add(p.Name, field);

+              iter.Members.Add(field);

             }

           }

           var yieldHistoryVariables = new List<MemberDecl>();

@@ -559,17 +534,17 @@ namespace Microsoft.Dafny
               yieldHistoryVariables.Add(field);  // just record this field for now (until all parameters have been added as members)

             }

           }

-          yieldHistoryVariables.ForEach(f => members.Add(f.Name, f));  // now that already-used 'xs' names have been checked for, add these yield-history variables

+          // now that already-used 'xs' names have been checked for, add these yield-history variables

+          yieldHistoryVariables.ForEach(f => {

+            members.Add(f.Name, f);

+            iter.Members.Add(f);

+          });

 

-          var iterTypeArgs = new List<Type>();

-          iter.TypeArgs.ForEach(tp => iterTypeArgs.Add(new UserDefinedType(tp.tok, tp.Name, tp)));

-          var iterType = new UserDefinedType(iter.tok, iter.Name, iter, iterTypeArgs);

           // Note, the typeArgs parameter to the following Method/Predicate constructors is passed in as the empty list.  What that is

           // saying is that the Method/Predicate does not take any type parameters over and beyond what the enclosing type (namely, the

           // iterator type) does.

           // Also add "Valid" and "MoveNext"

-          var init = new Method(iter.tok, iter.Name, true, false, new List<TypeParameter>(),

-            iter.Ins, new List<Formal>() { new Formal(iter.tok, "iter", iterType, false, false) },

+          var init = new Constructor(iter.tok, iter.Name, new List<TypeParameter>(), iter.Ins,

             /* TODO: Fill in the spec here */

             new List<MaybeFreeExpression>(), new Specification<FrameExpression>(null, null), new List<MaybeFreeExpression>(), new Specification<Expression>(null, null),

             null, null, false);

@@ -584,11 +559,13 @@ namespace Microsoft.Dafny
           init.EnclosingClass = iter;

           valid.EnclosingClass = iter;

           moveNext.EnclosingClass = iter;

+          iter.HasConstructor = true;

           MemberDecl member;

           if (members.TryGetValue(init.Name, out member)) {

             Error(member.tok, "member name '{0}' is already predefined for this iterator", init.Name);

           } else {

             members.Add(init.Name, init);

+            iter.Members.Add(init);

           }

           // If the name of the iterator is "Valid" or "MoveNext", one of the following will produce an error message.  That

           // error message may not be as clear as it could be, but the situation also seems unlikely to ever occur in practice.

@@ -596,11 +573,40 @@ namespace Microsoft.Dafny
             Error(member.tok, "member name 'Valid' is already predefined for iterators");

           } else {

             members.Add(valid.Name, valid);

+            iter.Members.Add(valid);

           }

           if (members.TryGetValue("MoveNext", out member)) {

             Error(member.tok, "member name 'MoveNext' is already predefined for iterators");

           } else {

             members.Add(moveNext.Name, moveNext);

+            iter.Members.Add(moveNext);

+          }

+

+        } else if (d is ClassDecl) {

+          ClassDecl cl = (ClassDecl)d;

+

+          // register the names of the class members

+          var members = new Dictionary<string, MemberDecl>();

+          classMembers.Add(cl, members);

+

+          bool hasConstructor = false;

+          foreach (MemberDecl m in cl.Members) {

+            if (members.ContainsKey(m.Name)) {

+              Error(m, "Duplicate member name: {0}", m.Name);

+            } else {

+              members.Add(m.Name, m);

+            }

+            if (m is Constructor) {

+              hasConstructor = true;

+            }

+          }

+          cl.HasConstructor = hasConstructor;

+          if (cl.IsDefaultClass) {

+            foreach (MemberDecl m in cl.Members) {

+              if (m.IsStatic && (m is Function || m is Method)) {

+                sig.StaticMembers[m.Name] = m;

+              }

+            }

           }

 

         } else {

@@ -4045,11 +4051,11 @@ namespace Microsoft.Dafny
 

       UserDefinedType ctype = UserDefinedType.DenotesClass(receiverType);

       if (ctype != null) {

-        ClassDecl cd = (ClassDecl)ctype.ResolvedClass;  // correctness of cast follows from postcondition of DenotesClass

+        var cd = (ClassDecl)ctype.ResolvedClass;  // correctness of cast follows from postcondition of DenotesClass

         Contract.Assert(ctype.TypeArgs.Count == cd.TypeArgs.Count);  // follows from the fact that ctype was resolved

         MemberDecl member;

         if (!classMembers[cd].TryGetValue(memberName, out member)) {

-          Error(tok, "member {0} does not exist in class {1}", memberName, ctype.Name);

+          Error(tok, "member {0} does not exist in {2} {1}", memberName, ctype.Name, cd is IteratorDecl ? "iterator" : "class");

           return null;

         } else {

           nptype = ctype;

@@ -4069,18 +4075,6 @@ namespace Microsoft.Dafny
         }

       }

 

-      IteratorDecl iter = receiverType.AsIteratorType;

-      if (iter != null) {

-        MemberDecl member;  

-        if (!iter.ImplicitlyDefinedMembers.TryGetValue(memberName, out member)) {

-          Error(tok, "member {0} does not exist in iterator {1}", memberName, iter.Name);

-          return null;

-        } else {

-          nptype = (UserDefinedType)receiverType;

-          return member;

-        }

-      }

-

       Error(tok, "type {0} does not have a member {1}", receiverType, memberName);

       return null;

     }

@@ -5198,14 +5192,6 @@ namespace Microsoft.Dafny
       } else if (moduleInfo.TopLevels.TryGetValue(id.val, out decl)) {

         if (decl is AmbiguousTopLevelDecl) {

           Error(id, "The name {0} ambiguously refers to a type in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames());

-        } else if (decl is IteratorDecl) {

-          // ----- root is an iterator

-          if (e.Tokens.Count != 1 || e.Arguments == null) {

-            Error(id, "name of iterator ('{0}') is used as a variable", id.val);

-          } else {

-            r = new StaticReceiverExpr(id, (IteratorDecl)decl);

-            call = new CallRhs(e.tok, r, id.val, e.Arguments);

-          }

         } else if (e.Tokens.Count == 1 && e.Arguments == null) {

           Error(id, "name of type ('{0}') is used as a variable", id.val);

         } else if (e.Tokens.Count == 1 && e.Arguments != null) {

@@ -5319,14 +5305,6 @@ namespace Microsoft.Dafny
             Error(e.tok, "module {0} cannot be used here", ((ModuleDecl)decl).Name);

           }

           call = ResolveIdentifierSequenceModuleScope(e, p + 1, ((ModuleDecl)decl).Signature, twoState, allowMethodCall);

-        } else if (decl is IteratorDecl) {

-          // ----- root is an iterator

-          if (p + 1 == e.Tokens.Count || e.Arguments == null) {

-            Error(id, "name of iterator ('{0}') is used as a variable", id.val);

-          } else {

-            r = new StaticReceiverExpr(id, (IteratorDecl)decl);

-            call = new CallRhs(e.tok, r, id.val, e.Arguments);

-          }

         } else {

           // ----- root is a datatype

           var dt = (DatatypeDecl)decl;  // otherwise, unexpected TopLevelDecl

@@ -5418,8 +5396,6 @@ namespace Microsoft.Dafny
             Dictionary<string, MemberDecl> members;

             if (udt.ResolvedClass is ClassDecl) {

               classMembers.TryGetValue((ClassDecl)udt.ResolvedClass, out members);

-            } else if (udt.ResolvedClass is IteratorDecl) {

-              members = ((IteratorDecl)udt.ResolvedClass).ImplicitlyDefinedMembers;

             } else {

               members = null;

             }