Dafny: datatype constructors can be accessed across module boundaries.

1 files changed, 56 insertions, 38 deletions

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 04350247..05cbc74f 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -3525,44 +3525,9 @@ namespace Microsoft.Dafny {
         } else if (d is AmbiguousTopLevelDecl) {

           Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", dtv.DatatypeName, ((AmbiguousTopLevelDecl)d).ModuleNames());

         } else if (!(d is DatatypeDecl)) {

-          Error(expr.tok, "Expected datatype, found class: {0}", dtv.DatatypeName);

+          Error(expr.tok, "Expected datatype: {0}", dtv.DatatypeName);

         } else {

-          // this resolution is a little special, in that the syntax shows only the base name, not its instantiation (which is inferred)

-          DatatypeDecl dt = (DatatypeDecl)d;

-          List<Type> gt = new List<Type>(dt.TypeArgs.Count);

-          Dictionary<TypeParameter,Type> subst = new Dictionary<TypeParameter,Type>();

-          for (int i = 0; i < dt.TypeArgs.Count; i++) {

-            Type t = new InferredTypeProxy();

-            gt.Add(t);

-            dtv.InferredTypeArgs.Add(t);

-            subst.Add(dt.TypeArgs[i], t);

-          }

-          expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt, null);

-          ResolveType(expr.tok, expr.Type, null, true);

-

-          DatatypeCtor ctor;

-          if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {

-            Error(expr.tok, "undeclared constructor {0} in datatype {1}", dtv.MemberName, dtv.DatatypeName);

-          } else {

-            Contract.Assert(ctor != null);  // follows from postcondition of TryGetValue

-            dtv.Ctor = ctor;

-            if (ctor.Formals.Count != dtv.Arguments.Count) {

-              Error(expr.tok, "wrong number of arguments to datatype constructor {0} (found {1}, expected {2})", dtv.DatatypeName, dtv.Arguments.Count, ctor.Formals.Count);

-            }

-          }

-          int j = 0;

-          foreach (Expression arg in dtv.Arguments) {

-            Formal formal = ctor != null && j < ctor.Formals.Count ? ctor.Formals[j] : null;

-            ResolveExpression(arg, twoState, null);

-            Contract.Assert(arg.Type != null);  // follows from postcondition of ResolveExpression

-            if (formal != null) {

-              Type st = SubstType(formal.Type, subst);

-              if (!UnifyTypes(arg.Type, st)) {

-                Error(arg.tok, "incorrect type of datatype constructor argument (found {0}, expected {1})", arg.Type, st);

-              }

-            }

-            j++;

-          }

+          ResolveDatatypeValue(twoState, dtv, (DatatypeDecl)d);

         }

 

       } else if (expr is DisplayExpression) {

@@ -4193,6 +4158,44 @@ namespace Microsoft.Dafny {
       }

     }

 

+    private void ResolveDatatypeValue(bool twoState, DatatypeValue dtv, DatatypeDecl dt) {

+      // this resolution is a little special, in that the syntax shows only the base name, not its instantiation (which is inferred)

+      List<Type> gt = new List<Type>(dt.TypeArgs.Count);

+      Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();

+      for (int i = 0; i < dt.TypeArgs.Count; i++) {

+        Type t = new InferredTypeProxy();

+        gt.Add(t);

+        dtv.InferredTypeArgs.Add(t);

+        subst.Add(dt.TypeArgs[i], t);

+      }

+      // Construct a resolved type directly, as we know the declaration is dt.

+      dtv.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, dt, gt);

+      

+      DatatypeCtor ctor;

+      if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {

+        Error(dtv.tok, "undeclared constructor {0} in datatype {1}", dtv.MemberName, dtv.DatatypeName);

+      } else {

+        Contract.Assert(ctor != null);  // follows from postcondition of TryGetValue

+        dtv.Ctor = ctor;

+        if (ctor.Formals.Count != dtv.Arguments.Count) {

+          Error(dtv.tok, "wrong number of arguments to datatype constructor {0} (found {1}, expected {2})", dtv.DatatypeName, dtv.Arguments.Count, ctor.Formals.Count);

+        }

+      }

+      int j = 0;

+      foreach (Expression arg in dtv.Arguments) {

+        Formal formal = ctor != null && j < ctor.Formals.Count ? ctor.Formals[j] : null;

+        ResolveExpression(arg, twoState, null);

+        Contract.Assert(arg.Type != null);  // follows from postcondition of ResolveExpression

+        if (formal != null) {

+          Type st = SubstType(formal.Type, subst);

+          if (!UnifyTypes(arg.Type, st)) {

+            Error(arg.tok, "incorrect type of datatype constructor argument (found {0}, expected {1})", arg.Type, st);

+          }

+        }

+        j++;

+      }

+    }

+

     private bool ComparableTypes(Type A, Type B) {

       if (A.IsArrayType && B.IsArrayType) {

         Type a = UserDefinedType.ArrayElementType(A);

@@ -4551,6 +4554,7 @@ namespace Microsoft.Dafny {
 

       TopLevelDecl decl;

       MemberDecl member;

+      Tuple<DatatypeCtor, bool> pair;

       var id = e.Tokens[p];

       if (sig.TopLevels.TryGetValue(id.val, out decl)) {

         if (decl is AmbiguousTopLevelDecl) {

@@ -4571,11 +4575,25 @@ namespace Microsoft.Dafny {
           var dt = (DatatypeDecl)decl;  // otherwise, unexpected TopLevelDecl

           var args = (e.Tokens.Count == p + 2 ? e.Arguments : null) ?? new List<Expression>();

           r = new DatatypeValue(id, id.val, e.Tokens[p + 1].val, args);

-          ResolveExpression(r, twoState);

+          ResolveDatatypeValue(twoState, (DatatypeValue) r, dt);

           if (e.Tokens.Count != p + 2) {

             r = ResolveSuffix(r, e, p + 2, twoState, allowMethodCall, out call);

           }

         }

+      } else if (sig.Ctors.TryGetValue(id.val, out pair)) {

+        // ----- root is a datatype constructor

+        if (pair.Item2) {

+          // there is more than one constructor with this name

+          Error(id, "the name '{0}' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, '{1}.{0}')", id.val, pair.Item1.EnclosingDatatype.Name);

+        } else {

+          var dt = pair.Item1.EnclosingDatatype;

+          var args = (e.Tokens.Count == p+1 ? e.Arguments : null) ?? new List<Expression>();

+          r = new DatatypeValue(id, dt.Name, id.val, args);

+          ResolveDatatypeValue(twoState, (DatatypeValue)r, dt);

+          if (e.Tokens.Count != p+1) {

+            r = ResolveSuffix(r, e, p+1, twoState, allowMethodCall, out call);

+          }

+        }

       } else if (sig.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.

       {

         // ----- function, or method