Dafny: allow various forms of leaving off type arguments in declarations

5 files changed, 194 insertions, 26 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 116ca201..624ca3a4 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -419,7 +419,7 @@ namespace Microsoft.Dafny {
       foreach (MemberDecl member in cl.Members) {

         member.EnclosingClass = cl;

         if (member is Field) {

-          ResolveType(member.tok, ((Field)member).Type);

+          ResolveType(member.tok, ((Field)member).Type, null, false);

 

         } else if (member is Function) {

           Function f = (Function)member;

@@ -490,7 +490,7 @@ namespace Microsoft.Dafny {
         ctor.EnclosingDatatype = dt;

 

         allTypeParameters.PushMarker();

-        ResolveCtorSignature(ctor);

+        ResolveCtorSignature(ctor, dt.TypeArgs);

         allTypeParameters.PopMarker();

 

         foreach (Formal p in ctor.Formals) {

@@ -623,13 +623,14 @@ namespace Microsoft.Dafny {
     void ResolveFunctionSignature(Function f) {

       Contract.Requires(f != null);

       scope.PushMarker();

+      var defaultTypeArguments = f.TypeArgs.Count == 0 ? f.TypeArgs : null;

       foreach (Formal p in f.Formals) {

         if (!scope.Push(p.Name, p)) {

           Error(p, "Duplicate parameter name: {0}", p.Name);

         }

-        ResolveType(p.tok, p.Type);

+        ResolveType(p.tok, p.Type, defaultTypeArguments, true);

       }

-      ResolveType(f.tok, f.ResultType);

+      ResolveType(f.tok, f.ResultType, defaultTypeArguments, true);

       scope.PopMarker();

     }

 

@@ -726,19 +727,20 @@ namespace Microsoft.Dafny {
     void ResolveMethodSignature(Method m) {

       Contract.Requires(m != null);

       scope.PushMarker();

+      var defaultTypeArguments = m.TypeArgs.Count == 0 ? m.TypeArgs : null;

       // resolve in-parameters

       foreach (Formal p in m.Ins) {

         if (!scope.Push(p.Name, p)) {

           Error(p, "Duplicate parameter name: {0}", p.Name);

         }

-        ResolveType(p.tok, p.Type);

+        ResolveType(p.tok, p.Type, defaultTypeArguments, true);

       }

       // resolve out-parameters

       foreach (Formal p in m.Outs) {

         if (!scope.Push(p.Name, p)) {

           Error(p, "Duplicate parameter name: {0}", p.Name);

         }

-        ResolveType(p.tok, p.Type);

+        ResolveType(p.tok, p.Type, defaultTypeArguments, true);

       }

       scope.PopMarker();

     }

@@ -806,28 +808,40 @@ namespace Microsoft.Dafny {
       scope.PopMarker();  // for the in-parameters

     }

 

-    void ResolveCtorSignature(DatatypeCtor ctor) {

+    void ResolveCtorSignature(DatatypeCtor ctor, List<TypeParameter> dtTypeArguments) {

       Contract.Requires(ctor != null);

+      Contract.Requires(dtTypeArguments != null);

       foreach (Formal p in ctor.Formals) {

-        ResolveType(p.tok, p.Type);

+        ResolveType(p.tok, p.Type, dtTypeArguments, false);

       }

     }

 

-    public void ResolveType(IToken tok, Type type) {

+    /// <summary>

+    /// If ResolveType encounters a type "T" that takes type arguments but wasn't given any, then:

+    /// * If "defaultTypeArguments" is non-null and "defaultTypeArgument.Count" equals the number

+    ///   of type arguments that "T" expects, then use these default type arguments as "T"'s arguments.

+    /// * If "allowAutoTypeArguments" is true, then infer "T"'s arguments.

+    /// * If "defaultTypeArguments" is non-null AND "allowAutoTypeArguments" is true, then enough

+    ///   type parameters will be added to "defaultTypeArguments" to have at least as many type

+    ///   parameters as "T" expects, and then a prefix of the "defaultTypeArguments" will be supplied

+    ///   as arguments to "T".

+    /// </summary>

+    public void ResolveType(IToken tok, Type type, List<TypeParameter> defaultTypeArguments, bool allowAutoTypeArguments) {

+      Contract.Requires(tok != null);

       Contract.Requires(type != null);

       if (type is BasicType) {

         // nothing to resolve

       } else if (type is CollectionType) {

         var t = (CollectionType)type;

         var argType = t.Arg;

-        ResolveType(tok, argType);

+        ResolveType(tok, argType, defaultTypeArguments, allowAutoTypeArguments);

         if (argType.IsSubrangeType) {

           Error(tok, "sorry, cannot instantiate collection type with a subrange type");

         }

       } else if (type is UserDefinedType) {

         UserDefinedType t = (UserDefinedType)type;

         foreach (Type tt in t.TypeArgs) {

-          ResolveType(t.tok, tt);

+          ResolveType(t.tok, tt, defaultTypeArguments, allowAutoTypeArguments);

           if (tt.IsSubrangeType) {

             Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type");

           }

@@ -845,19 +859,47 @@ namespace Microsoft.Dafny {
             Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget a module import?)", t.Name);

           } else if (d is AmbiguousTopLevelDecl) {

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

-          } else if (d.TypeArgs.Count != t.TypeArgs.Count) {

-            Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name);

           } else if (d is ArbitraryTypeDecl) {

-            t.ResolvedParam = ((ArbitraryTypeDecl)d).TheType;  // resolve as type parameter

+            t.ResolvedParam = ((ArbitraryTypeDecl)d).TheType;  // resolve like a type parameter

           } else {

+            // d is a class or datatype, and it may have type parameters

             t.ResolvedClass = d;

+            if (d.TypeArgs.Count != t.TypeArgs.Count && t.TypeArgs.Count == 0) {

+              if (allowAutoTypeArguments && defaultTypeArguments == null) {

+                // add type arguments that will be inferred

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

+                  t.TypeArgs.Add(new InferredTypeProxy());

+                }

+              } else if (defaultTypeArguments != null) {

+                // add specific type arguments, drawn from defaultTypeArguments (which may have to be extended)

+                if (allowAutoTypeArguments) {

+                  // add to defaultTypeArguments the necessary number of arguments

+                  for (int i = defaultTypeArguments.Count; i < d.TypeArgs.Count; i++) {

+                    defaultTypeArguments.Add(new TypeParameter(t.tok, "T$" + i));

+                  }

+                }

+                if (allowAutoTypeArguments || d.TypeArgs.Count == defaultTypeArguments.Count) {

+                  Contract.Assert(d.TypeArgs.Count <= defaultTypeArguments.Count);

+                  // automatically supply a prefix of the arguments from defaultTypeArguments

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

+                    var typeArg = new UserDefinedType(t.tok, defaultTypeArguments[i].Name, new List<Type>());

+                    typeArg.ResolvedParam = defaultTypeArguments[i];  // resolve "typeArg" here

+                    t.TypeArgs.Add(typeArg);

+                  }

+                }

+              }

+            }

+            // defaults and auto have been applied; check if we now have the right number of arguments

+            if (d.TypeArgs.Count != t.TypeArgs.Count) {

+              Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name);

+            }

           }

         }

 

       } else if (type is TypeProxy) {

         TypeProxy t = (TypeProxy)type;

         if (t.T != null) {

-          ResolveType(tok, t.T);

+          ResolveType(tok, t.T, defaultTypeArguments, allowAutoTypeArguments);

         }

 

       } else {

@@ -1382,7 +1424,7 @@ namespace Microsoft.Dafny {
       } else if (stmt is VarDecl) {

         VarDecl s = (VarDecl)stmt;

         if (s.OptionalType != null) {

-          ResolveType(stmt.Tok, s.OptionalType);

+          ResolveType(stmt.Tok, s.OptionalType, null, true);

           s.type = s.OptionalType;

         }

         // now that the declaration has been processed, add the name to the scope

@@ -1506,7 +1548,7 @@ namespace Microsoft.Dafny {
           if (!scope.Push(v.Name, v)) {

             Error(v, "Duplicate bound-variable name: {0}", v.Name);

           }

-          ResolveType(v.tok, v.Type);

+          ResolveType(v.tok, v.Type, null, true);

         }

         ResolveExpression(s.Range, true);

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

@@ -1631,7 +1673,7 @@ namespace Microsoft.Dafny {
             if (!scope.Push(v.Name, v)) {

               Error(v, "Duplicate parameter name: {0}", v.Name);

             }

-            ResolveType(v.tok, v.Type);

+            ResolveType(v.tok, v.Type, null, true);

             if (ctor != null && i < ctor.Formals.Count) {

               Formal formal = ctor.Formals[i];

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

@@ -2155,7 +2197,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<Type>() != null);

 

       if (rr.Type == null) {

-        ResolveType(stmt.Tok, rr.EType);

+        ResolveType(stmt.Tok, rr.EType, null, true);

         if (rr.ArrayDimensions == null) {

           if (!rr.EType.IsRefType) {

             Error(stmt, "new can be applied only to reference types (got {0})", rr.EType);

@@ -2423,7 +2465,7 @@ namespace Microsoft.Dafny {
             subst.Add(dt.TypeArgs[i], t);

           }

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

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

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

 

           DatatypeCtor ctor;

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

@@ -2771,7 +2813,7 @@ namespace Microsoft.Dafny {
           if (!scope.Push(v.Name, v)) {

             Error(v, "Duplicate let-variable name: {0}", v.Name);

           }

-          ResolveType(v.tok, v.Type);

+          ResolveType(v.tok, v.Type, null, true);

           if (i < e.RHSs.Count && !UnifyTypes(v.Type, e.RHSs[i].Type)) {

             Error(e.RHSs[i].tok, "type of RHS ({0}) does not match type of bound variable ({1})", e.RHSs[i].Type, v.Type);

           }

@@ -2789,7 +2831,7 @@ namespace Microsoft.Dafny {
           if (!scope.Push(v.Name, v)) {

             Error(v, "Duplicate bound-variable name: {0}", v.Name);

           }

-          ResolveType(v.tok, v.Type);

+          ResolveType(v.tok, v.Type, null, true);

         }

         if (e.Range != null) {

           ResolveExpression(e.Range, twoState);

@@ -2825,7 +2867,7 @@ namespace Microsoft.Dafny {
           if (!scope.Push(v.Name, v)) {

             Error(v, "Duplicate bound-variable name: {0}", v.Name);

           }

-          ResolveType(v.tok, v.Type);

+          ResolveType(v.tok, v.Type, null, true);

         }

         ResolveExpression(e.Range, twoState);

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

@@ -2949,7 +2991,7 @@ namespace Microsoft.Dafny {
             if (!scope.Push(v.Name, v)) {

               Error(v, "Duplicate parameter name: {0}", v.Name);

             }

-            ResolveType(v.tok, v.Type);

+            ResolveType(v.tok, v.Type, null, true);

             if (ctor != null && i < ctor.Formals.Count) {

               Formal formal = ctor.Formals[i];

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

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 6f160a66..6c6b54eb 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -498,7 +498,9 @@ ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_
 ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)

 ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts

 ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts

-46 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)

+ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<T$0>, expected GList<int>)

+48 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -1250,6 +1252,10 @@ Execution trace:
 

 Dafny program verifier finished with 12 verified, 3 errors

 

+-------------------- NoTypeArgs.dfy --------------------

+

+Dafny program verifier finished with 12 verified, 0 errors

+

 -------------------- SplitExpr.dfy --------------------

 

 Dafny program verifier finished with 5 verified, 0 errors

diff --git a/Test/dafny0/NoTypeArgs.dfy b/Test/dafny0/NoTypeArgs.dfy
new file mode 100644
index 00000000..c41c7990
--- /dev/null
+++ b/Test/dafny0/NoTypeArgs.dfy
@@ -0,0 +1,82 @@
+datatype List<T> = Nil | Cons(hd: T, tl: List);

+

+method M0() {

+  var l: List;

+  l := Cons(5, Nil);

+  assert l.hd == 5;

+

+  var k: MyClass<bool>;

+  k := new MyClass;

+  k.data := false;

+

+  var h := new MyClass;

+  h.data := false;

+

+  var y := new MyClass.Init(120);

+  var z: int := y.data;

+}

+

+method M1() {  // same thing as above, but with types filled in explicitly

+  var l: List<int>;

+  l := Cons(5, Nil);

+  assert l.hd == 5;

+

+  var k: MyClass<bool>;

+  k := new MyClass<bool>;

+  k.data := false;

+

+  var h := new MyClass<bool>;

+  h.data := false;

+

+  var y := new MyClass<int>.Init(120);

+  var z: int := y.data;

+}

+

+class MyClass<G> {

+  var data: G;

+  method Init(g: G)

+    modifies this;

+  {

+    data := g;

+  }

+}

+

+// ---------------------------------------------------

+

+// The followinng functions and methods are oblivious of the fact that

+// List takes a type parameter.

+

+function concat(xs: List, ys: List): List

+{

+  match xs

+  case Nil => ys

+  case Cons(x, tail) => Cons(x, concat(tail, ys))

+}

+

+function reverse(xs: List): List

+{

+  match xs

+  case Nil => Nil

+  case Cons(t, rest) => concat(reverse(rest), Cons(t, Nil))

+}

+

+ghost method Theorem(xs: List)

+  ensures reverse(reverse(xs)) == xs;

+{

+  match (xs) {

+    case Nil =>

+    case Cons(t, rest) =>

+      Lemma(reverse(rest), Cons(t, Nil));

+  }

+}

+

+ghost method Lemma(xs: List, ys: List)

+  ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));

+{

+  match (xs) {

+    case Nil =>

+      assert forall ws :: concat(ws, Nil) == ws;

+    case Cons(t, rest) =>

+      assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 34cfc762..274cc95a 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -317,3 +317,40 @@ method PrintOnlyNonGhosts(a: int, ghost b: int)
   print "a: ", a, "\n";

   print "b: ", b, "\n";  // error: print statement cannot take ghosts

 }

+

+// ------------------- auto-added type arguments ------------------------------

+

+class GenericClass<T> { var data: T; }

+

+method MG0(a: GenericClass, b: GenericClass)

+  requires a != null && b != null;

+  modifies a;

+{

+  a.data := b.data;  // allowed, since both a and b get the same auto type argument

+}

+

+method G_Caller()

+{

+  var x := new GenericClass;

+  MG0(x, x);  // fine

+  var y := new GenericClass;

+  MG0(x, y);  // also fine (and now y's type argument is constrained to be that of x's)

+  var z := new GenericClass<int>;

+  y.data := z.data;  // this will have the effect of unifying all type args so far to be 'int'

+  assert x.data == 5;  // this is type correct

+

+  var w := new GenericClass<bool>;

+  MG0(x, w);  // error: types don't match up

+}

+

+datatype GList<T> = GNil | GCons(hd: T, tl: GList);

+

+method MG1(l: GList, n: nat)

+{

+  if (n != 0) {

+    MG1(l, n-1);

+    MG1(GCons(12, GCons(20, GNil)), n-1);

+  }

+  var t := GCons(100, GNil);

+  t := GCons(120, l);  // error: types don't match up (List<T$0> versus List<int>)

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index d09e1cc2..b1402e83 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -17,7 +17,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             ModulesCycle.dfy Modules0.dfy Modules1.dfy BadFunction.dfy

             Comprehensions.dfy Basics.dfy ControlStructures.dfy

             Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy

-            TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

+            TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy NoTypeArgs.dfy

+            SplitExpr.dfy

             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy