Allow array-type parameters to be filled in automatically.

Enhanced filling in of datatype parameters:  allow places that need only a prefix of the parameters of the datatype

9 files changed, 90 insertions, 54 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 5b8f8cc5..9b6d12c0 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -64,18 +64,13 @@ namespace Microsoft.Dafny
           body, CloneAttributes(dd.Attributes), dd.SignatureEllipsis);

         return iter;

       } else if (d is ClassDecl) {

+        var dd = (ClassDecl)d;

+        var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

+        var mm = dd.Members.ConvertAll(CloneMember);

         if (d is DefaultClassDecl) {

-          var dd = (ClassDecl)d;

-          var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

-          var mm = dd.Members.ConvertAll(CloneMember);

-          var cl = new DefaultClassDecl(m, mm);

-          return cl;

+          return new DefaultClassDecl(m, mm);

         } else {

-          var dd = (ClassDecl)d;

-          var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

-          var mm = dd.Members.ConvertAll(CloneMember);

-          var cl = new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes));

-          return cl;

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

         }

       } else if (d is ModuleDecl) {

         if (d is LiteralModuleDecl) {

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 5c1148c6..c8f410c9 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -795,21 +795,15 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
 ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>

 = (. Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);

      tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

-     List<Type/*!*/>/*!*/ gt;

+     List<Type> gt;

      List<IToken> path;

   .)

   ( "object"                        (. tok = t;  ty = new ObjectType(); .)

-  | arrayToken                      (. tok = t;  gt = new List<Type/*!*/>(); .)

-    GenericInstantiation<gt>        (. if (gt.Count != 1) {

-                                         SemErr("array type expects exactly one type argument");

-                                       }

-                                       int dims = 1;

-                                       if (tok.val.Length != 5) {

-                                         dims = int.Parse(tok.val.Substring(5));

-                                       }

-                                       ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);

+  | arrayToken                      (. tok = t;  gt = new List<Type>(); .)

+    [ GenericInstantiation<gt> ]    (. int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));

+                                       ty = theBuiltIns.ArrayType(tok, dims, gt, true);

                                     .)

-  | Ident<out tok>                  (. gt = new List<Type/*!*/>();

+  | Ident<out tok>                  (. gt = new List<Type>();

                                        path = new List<IToken>(); .)

     {                               (. path.Add(tok); .)

       "." Ident<out tok>

@@ -1135,7 +1129,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
     [ "["                              (. ee = new List<Expression>(); .)

       Expressions<ee>

       "]"                              (. // make sure an array class with this dimensionality exists

-                                          UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);

+                                          var tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);

                                        .)

     |                                  (. x = null; args = new List<Expression/*!*/>(); .)

       [ "." Ident<out x> ]

@@ -2205,7 +2199,7 @@ Suffix<ref Expression e>
       (. if (multipleIndices != null) {

            e = new MultiSelectExpr(x, e, multipleIndices);

            // make sure an array class with this dimensionality exists

-           UserDefinedType tmp = theBuiltIns.ArrayType(x, multipleIndices.Count, new IntType(), true);

+           var tmp = theBuiltIns.ArrayType(multipleIndices.Count, new IntType(), true);

          } else {

            if (!anyDots && e0 == null) {

              /* a parsing error occurred */

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 55dc973f..d72db478 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -99,7 +99,7 @@ namespace Microsoft.Dafny {
       SystemModule.TopLevelDecls.Add(ObjectDecl);

       // add one-dimensional arrays, since they may arise during type checking

       // Arrays of other dimensions may be added during parsing as the parser detects the need for these

-      UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true);

+      UserDefinedType tmp = ArrayType(1, Type.Int, true);

       // add real number functions

       Function RealToInt = new Function(Token.NoToken, "RealToInt", true, true, new List<TypeParameter>(), Token.NoToken,

         new List<Formal> { new Formal(Token.NoToken, "x", Type.Real, true, true) }, Type.Int, new List<Expression>(),

@@ -125,17 +125,17 @@ namespace Microsoft.Dafny {
       return new Attributes("compile", new List<Attributes.Argument>() { flse }, null);

     }

 

-    public UserDefinedType ArrayType(int dims, Type arg) {

-      return ArrayType(Token.NoToken, dims, arg, false);

+    public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass = false) {

+      Contract.Requires(1 <= dims);

+      Contract.Requires(arg != null);

+      return ArrayType(Token.NoToken, dims, new List<Type>() { arg }, allowCreationOfNewClass);

     }

-    public UserDefinedType ArrayType(IToken tok, int dims, Type arg, bool allowCreationOfNewClass) {

+    public UserDefinedType ArrayType(IToken tok, int dims, List<Type> typeArgs, bool allowCreationOfNewClass) {

       Contract.Requires(tok != null);

       Contract.Requires(1 <= dims);

-      Contract.Requires(arg != null);

+      Contract.Requires(typeArgs != null);

       Contract.Ensures(Contract.Result<UserDefinedType>() != null);

 

-      List<Type> typeArgs = new List<Type>();

-      typeArgs.Add(arg);

       UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs, null);

       if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {

         ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule, DontCompile());

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index a7f058db..750c04d0 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1472,7 +1472,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {

 		Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);

 		tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

-		List<Type/*!*/>/*!*/ gt;

+		List<Type> gt;

 		List<IToken> path;

 		

 		if (la.kind == 60) {

@@ -1480,20 +1480,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			tok = t;  ty = new ObjectType(); 

 		} else if (la.kind == 5) {

 			Get();

-			tok = t;  gt = new List<Type/*!*/>(); 

-			GenericInstantiation(gt);

-			if (gt.Count != 1) {

-			 SemErr("array type expects exactly one type argument");

-			}

-			int dims = 1;

-			if (tok.val.Length != 5) {

-			 dims = int.Parse(tok.val.Substring(5));

+			tok = t;  gt = new List<Type>(); 

+			if (la.kind == 38) {

+				GenericInstantiation(gt);

 			}

-			ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);

+			int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));

+			ty = theBuiltIns.ArrayType(tok, dims, gt, true);

 			

 		} else if (la.kind == 1) {

 			Ident(out tok);

-			gt = new List<Type/*!*/>();

+			gt = new List<Type>();

 			path = new List<IToken>(); 

 			while (la.kind == 61) {

 				path.Add(tok); 

@@ -2262,7 +2258,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					ee = new List<Expression>(); 

 					Expressions(ee);

 					Expect(75);

-					UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);

+					var tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);

 					

 				} else {

 					x = null; args = new List<Expression/*!*/>(); 

@@ -3192,7 +3188,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			 // make sure an array class with this dimensionality exists

-			 UserDefinedType tmp = theBuiltIns.ArrayType(x, multipleIndices.Count, new IntType(), true);

+			 var tmp = theBuiltIns.ArrayType(multipleIndices.Count, new IntType(), true);

 			} else {

 			 if (!anyDots && e0 == null) {

 			   /* a parsing error occurred */

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 73925aef..af4cad41 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3252,8 +3252,9 @@ namespace Microsoft.Dafny
     void ResolveCtorSignature(DatatypeCtor ctor, List<TypeParameter> dtTypeArguments) {

       Contract.Requires(ctor != null);

       Contract.Requires(dtTypeArguments != null);

+      var option = dtTypeArguments.Count == 0 ? ResolveTypeOption.AllowPrefixExtend : ResolveTypeOption.AllowPrefix;

       foreach (Formal p in ctor.Formals) {

-        ResolveType(p.tok, p.Type, ResolveTypeOption.AllowExact, dtTypeArguments);

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

       }

     }

 

@@ -3515,10 +3516,6 @@ namespace Microsoft.Dafny
       /// </summary>

       InferTypeProxies,

       /// <summary>

-      /// if exactly defaultTypeArguments.Count type arguments are needed, use defaultTypeArguments

-      /// </summary>

-      AllowExact,

-      /// <summary>

       /// if at most defaultTypeArguments.Count type arguments are needed, use a prefix of defaultTypeArguments

       /// </summary>

       AllowPrefix,

@@ -3635,7 +3632,7 @@ namespace Microsoft.Dafny
           } else {

             Error(t.tok, "Type parameter expects no type arguments: {0}", t.Name);

           }

-        } else if (t.ResolvedClass == null) {  // this test is because 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string')

+        } else {

           TopLevelDecl d = null;

 

           int j;

@@ -3715,8 +3712,6 @@ namespace Microsoft.Dafny
         for (int i = 0; i < n; i++) {

           typeArgs.Add(new InferredTypeProxy());

         }

-      } else if (option == ResolveTypeOption.AllowExact && defaultTypeArguments.Count != n) {

-        // the number of default arguments is not exactly what we need, so don't add anything

       } else if (option == ResolveTypeOption.AllowPrefix && defaultTypeArguments.Count < n) {

         // there aren't enough default arguments, so don't do anything

       } else {

@@ -7030,7 +7025,7 @@ namespace Microsoft.Dafny
         // ----- root is a local variable, parameter, or bound variable

         r = new IdentifierExpr(id, id.val);

         ResolveExpression(r, twoState, codeContext);

-        r = ResolveSuffix(r, e, 1, twoState, codeContext,  allowMethodCall, out call);

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

 

       } else if (moduleInfo.TopLevels.TryGetValue(id.val, out decl)) {

         if (decl is AmbiguousTopLevelDecl) {

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 35c17112..74405fa5 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -943,3 +943,25 @@ method TupleResolution(x: int, y: int, r: real)
   var pp: (int) := x;

   var qq: int := pp;

 }

+

+// --- filling in type arguments and checking that there aren't too many ---

+

+module TypeArgumentCount {

+  class C<T> {

+    var f: T;

+  }

+

+  method R0(a: array3, c: C)

+

+  method R1()

+  {

+    var a: array3;

+    var c: C;

+  }

+

+  method R2<T>()

+  {

+    var a: array3<T,int>;  // error: too many type arguments

+    var c: C<T,int>;  // error: too many type arguments

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 22f3274e..74f4ab50 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -53,6 +53,8 @@ ResolutionErrors.dfy(898,9): Error: cannot assign to a range of array elements (
 ResolutionErrors.dfy(899,9): Error: cannot assign to a range of array elements (try the 'forall' statement)

 ResolutionErrors.dfy(900,5): Error: cannot assign to a range of array elements (try the 'forall' statement)

 ResolutionErrors.dfy(901,5): Error: cannot assign to a range of array elements (try the 'forall' statement)

+ResolutionErrors.dfy(964,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: array3

+ResolutionErrors.dfy(965,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: C

 ResolutionErrors.dfy(429,2): Error: More than one default constructor

 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

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

@@ -139,4 +141,4 @@ ResolutionErrors.dfy(931,9): Error: condition is expected to be of type bool, bu
 ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3

 ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2

 ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int))

-141 resolution/type errors detected in ResolutionErrors.dfy

+143 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index 963916f0..900b6110 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -321,3 +321,35 @@ method IdentityMap(s: set<Pair>) returns (m: map)
     m, s := m[p.0 := p.1], s - {p};

   }

 }

+

+// -------------- auto filled-in type arguments for array types ------

+

+module ArrayTypeMagic {

+  method M(a: array2)

+  {

+  }

+

+  method F(b: array) returns (s: seq)

+    requires b != null;

+  {

+    return b[..];

+  }

+

+  datatype ArrayCubeTree = Leaf(array3) | Node(ArrayCubeTree, ArrayCubeTree)

+  datatype AnotherACT<T> = Leaf(array3) | Node(AnotherACT, AnotherACT)

+  datatype OneMoreACT<T,U> = Leaf(array3) | Node(OneMoreACT, OneMoreACT)

+

+  function G(t: ArrayCubeTree): array3

+  {

+    match t

+    case Leaf(d) => d

+    case Node(l, _) => G(l)

+  }

+

+  datatype Nat = Zero | Succ(Nat)

+

+  datatype List<T> = Nil | Cons(T, List)

+

+  datatype Cell<T> = Mk(T)

+  datatype DList<T,U> = Nil(Cell) | Cons(T, U, DList)

+}

diff --git a/Test/dafny0/TypeParameters.dfy.expect b/Test/dafny0/TypeParameters.dfy.expect
index 00efc26f..3d00e89a 100644
--- a/Test/dafny0/TypeParameters.dfy.expect
+++ b/Test/dafny0/TypeParameters.dfy.expect
@@ -49,4 +49,4 @@ Execution trace:
     TypeParameters.dfy(177,3): anon21_Else

     TypeParameters.dfy(177,3): anon23_Else

 

-Dafny program verifier finished with 58 verified, 8 errors

+Dafny program verifier finished with 63 verified, 8 errors