Merge

4 files changed, 169 insertions, 87 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 99de2757..70ea9ae8 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -745,28 +745,32 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
   | "int"                           (. tok = t;  ty = new IntType(); .)

   | "real"                          (. tok = t;  ty = new RealType(); .)

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

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

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

+    [ GenericInstantiation<gt> ]    (. if (gt.Count > 1) {

+                                         SemErr("set type expects only one type argument");

                                        }

-                                       ty = new SetType(gt[0]);

+                                       ty = new SetType(gt.Count == 1 ? gt[0] : null);

                                     .)

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

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

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

+    [ GenericInstantiation<gt> ]    (. if (gt.Count > 1) {

+                                         SemErr("multiset type expects only one type argument");

                                        }

-                                       ty = new MultiSetType(gt[0]);

+                                       ty = new MultiSetType(gt.Count == 1 ? gt[0] : null);

                                     .)

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

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

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

+    [ GenericInstantiation<gt> ]    (. if (gt.Count > 1) {

+                                         SemErr("seq type expects only one type argument");

                                        }

-                                       ty = new SeqType(gt[0]);

+                                       ty = new SeqType(gt.Count == 1 ? gt[0] : null);

                                     .)

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

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

-                                         SemErr("map type expects exactly two type arguments");

+    [ GenericInstantiation<gt> ]    (. if (gt.Count == 0) {

+                                         ty = new MapType(null, null);

+                                       } else if (gt.Count != 2) {

+                                         SemErr("map type expects two type arguments");

+                                         ty = new MapType(gt[0], gt.Count == 1 ? new InferredTypeProxy() : gt[1]);

+                                       } else {

+                                         ty = new MapType(gt[0], gt[1]);

                                        }

-                                       else { ty = new MapType(gt[0], gt[1]); }

                                     .)

   | ReferenceType<out tok, out ty>

   )

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 600c8d3d..a7fc7122 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -447,14 +447,36 @@ namespace Microsoft.Dafny {
 

   public abstract class CollectionType : NonProxyType

   {

-    public readonly Type Arg;  // denotes the Domain type for a Map

+    public abstract string CollectionTypeName { get; }

+    public override string TypeName(ModuleDefinition context) {

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

+      var targs = HasTypeArg() ? "<" + Arg.TypeName(context) + ">" : "";

+      return CollectionTypeName + targs;

+    }

+    public Type Arg {

+      get {

+        Contract.Ensures(Contract.Result<Type>() != null);  // this is true only after "arg" has really been set (i.e., it follows from the precondition)

+        Contract.Assume(arg != null);  // This is really a precondition.  Don't call Arg until "arg" has been set.

+        return arg;

+      }

+    }  // denotes the Domain type for a Map

+    private Type arg;

+    // The following two methods, HasTypeArg and SetTypeArg, are to be called during resolution to make sure that "arg" becomes set.

+    public bool HasTypeArg() {

+      return arg != null;

+    }

+    public void SetTypeArg(Type arg) {

+      Contract.Requires(arg != null);

+      Contract.Assume(this.arg == null);  // Can only set it once.  This is really a precondition.

+      this.arg = arg;

+    }

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(Arg != null);

+      // After resolution, the following is invariant:  Contract.Invariant(Arg != null);

+      // However, it may not be true until then.

     }

     public CollectionType(Type arg) {

-      Contract.Requires(arg != null);

-      this.Arg = arg;

+      this.arg = arg;

     }

     public override bool SupportsEquality {

       get {

@@ -465,13 +487,9 @@ namespace Microsoft.Dafny {
 

   public class SetType : CollectionType {

     public SetType(Type arg) : base(arg) {

-      Contract.Requires(arg != null);

     }

+    public override string CollectionTypeName { get { return "set"; } }

     [Pure]

-    public override string TypeName(ModuleDefinition context) {

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

-      return "set<" + base.Arg.TypeName(context) + ">";

-    }

     public override bool Equals(Type that) {

       var t = that.Normalize() as SetType;

       return t != null && Arg.Equals(t.Arg);

@@ -481,13 +499,8 @@ namespace Microsoft.Dafny {
   public class MultiSetType : CollectionType

   {

     public MultiSetType(Type arg) : base(arg) {

-      Contract.Requires(arg != null);

-    }

-    [Pure]

-    public override string TypeName(ModuleDefinition context) {

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

-      return "multiset<" + base.Arg.TypeName(context) + ">";

     }

+    public override string CollectionTypeName { get { return "multiset"; } }

     public override bool Equals(Type that) {

       var t = that.Normalize() as MultiSetType;

       return t != null && Arg.Equals(t.Arg);

@@ -496,14 +509,8 @@ namespace Microsoft.Dafny {
 

   public class SeqType : CollectionType {

     public SeqType(Type arg) : base(arg) {

-      Contract.Requires(arg != null);

-

-    }

-    [Pure]

-    public override string TypeName(ModuleDefinition context) {

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

-      return "seq<" + base.Arg.TypeName(context) + ">";

     }

+    public override string CollectionTypeName { get { return "seq"; } }

     public override bool Equals(Type that) {

       var t = that.Normalize() as SeqType;

       return t != null && Arg.Equals(t.Arg);

@@ -511,22 +518,30 @@ namespace Microsoft.Dafny {
   }

   public class MapType : CollectionType

   {

-    public Type Range;

+    public Type Range { get { return range; } }

+    private Type range;

+    public void SetRangetype(Type range) {

+      Contract.Requires(range != null);

+      Contract.Assume(this.range == null);  // Can only set once.  This is really a precondition.

+      this.range = range;

+    }

     public MapType(Type domain, Type range) : base(domain) {

-      Contract.Requires(domain != null && range != null);

-      Range = range;

+      Contract.Requires((domain == null && range == null) || (domain != null && range != null));

+      this.range = range;

     }

     public Type Domain {

       get { return Arg; }

     }

+    public override string CollectionTypeName { get { return "map"; } }

     [Pure]

     public override string TypeName(ModuleDefinition context) {

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

-      return "map<" + Domain.TypeName(context) + ", " + Range.TypeName(context) + ">";

+      var targs = HasTypeArg() ? "<" + Domain.TypeName(context) + ", " + Range.TypeName(context) + ">" : "";

+      return CollectionTypeName + targs;

     }

     public override bool Equals(Type that) {

       var t = that.Normalize() as MapType;

-      return t != null && Arg.Equals(t.Arg);

+      return t != null && Arg.Equals(t.Arg) && Range.Equals(t.Range);

     }

   }

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index d78c35a6..24d7d25d 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1147,44 +1147,56 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 		case 56: {

 			Get();

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

-			GenericInstantiation(gt);

-			if (gt.Count != 1) {

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

+			if (la.kind == 38) {

+				GenericInstantiation(gt);

+			}

+			if (gt.Count > 1) {

+			 SemErr("set type expects only one type argument");

 			}

-			ty = new SetType(gt[0]);

+			ty = new SetType(gt.Count == 1 ? gt[0] : null);

 			

 			break;

 		}

 		case 57: {

 			Get();

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

-			GenericInstantiation(gt);

-			if (gt.Count != 1) {

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

+			if (la.kind == 38) {

+				GenericInstantiation(gt);

+			}

+			if (gt.Count > 1) {

+			 SemErr("multiset type expects only one type argument");

 			}

-			ty = new MultiSetType(gt[0]);

+			ty = new MultiSetType(gt.Count == 1 ? gt[0] : null);

 			

 			break;

 		}

 		case 58: {

 			Get();

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

-			GenericInstantiation(gt);

-			if (gt.Count != 1) {

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

+			if (la.kind == 38) {

+				GenericInstantiation(gt);

+			}

+			if (gt.Count > 1) {

+			 SemErr("seq type expects only one type argument");

 			}

-			ty = new SeqType(gt[0]);

+			ty = new SeqType(gt.Count == 1 ? gt[0] : null);

 			

 			break;

 		}

 		case 59: {

 			Get();

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

-			GenericInstantiation(gt);

-			if (gt.Count != 2) {

-			 SemErr("map type expects exactly two type arguments");

+			if (la.kind == 38) {

+				GenericInstantiation(gt);

+			}

+			if (gt.Count == 0) {

+			 ty = new MapType(null, null);

+			} else if (gt.Count != 2) {

+			 SemErr("map type expects two type arguments");

+			 ty = new MapType(gt[0], gt.Count == 1 ? new InferredTypeProxy() : gt[1]);

+			} else {

+			 ty = new MapType(gt[0], gt[1]);

 			}

-			else { ty = new MapType(gt[0], gt[1]); }

 			

 			break;

 		}

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index a409f39e..3b19b11c 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3521,21 +3521,62 @@ namespace Microsoft.Dafny
       if (type is BasicType) {

         // nothing to resolve

       } else if (type is MapType) {

-        MapType mt = (MapType)type;

-        ResolveType(tok, mt.Domain, option, defaultTypeArguments);

-        ResolveType(tok, mt.Range, option, defaultTypeArguments);

+        var mt = (MapType)type;

+        int typeArgumentCount = 0;

+        if (mt.HasTypeArg()) {

+          ResolveType(tok, mt.Domain, option, defaultTypeArguments);

+          ResolveType(tok, mt.Range, option, defaultTypeArguments);

+          typeArgumentCount = 2;

+        } else if (option != ResolveTypeOption.DontInfer) {

+          var inferredTypeArgs = new List<Type>();

+          FillInTypeArguments(tok, 2, inferredTypeArgs, defaultTypeArguments, option);

+          Contract.Assert(inferredTypeArgs.Count <= 2);

+          if (inferredTypeArgs.Count != 0) {

+            mt.SetTypeArg(inferredTypeArgs[0]);

+            typeArgumentCount++;

+          }

+          if (inferredTypeArgs.Count == 2) {

+            mt.SetRangetype(inferredTypeArgs[1]);

+            typeArgumentCount++;

+          }

+        }

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

+        if (2 != typeArgumentCount) {

+          Error(tok, "Wrong number of type arguments ({0} instead of 2) passed to type: {1}", typeArgumentCount, mt.CollectionTypeName);

+          // add proxy types, to make sure that MapType will have have a non-null Arg/Domain and Range

+          if (typeArgumentCount == 0) {

+            mt.SetTypeArg(new InferredTypeProxy());

+          }

+          mt.SetRangetype(new InferredTypeProxy());

+        }

+

         if (mt.Domain.IsSubrangeType || mt.Range.IsSubrangeType) {

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

         }

       } else if (type is CollectionType) {

         var t = (CollectionType)type;

-        var argType = t.Arg;

-        ResolveType(tok, argType, option, defaultTypeArguments);

-        if (argType.IsSubrangeType) {

+        if (t.HasTypeArg()) {

+          ResolveType(tok, t.Arg, option, defaultTypeArguments);

+        } else if (option != ResolveTypeOption.DontInfer) {

+          var inferredTypeArgs = new List<Type>();

+          FillInTypeArguments(tok, 1, inferredTypeArgs, defaultTypeArguments, option);

+          if (inferredTypeArgs.Count != 0) {

+            Contract.Assert(inferredTypeArgs.Count == 1);

+            t.SetTypeArg(inferredTypeArgs[0]);

+          }

+        }

+        if (!t.HasTypeArg()) {

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

+          Error(tok, "Wrong number of type arguments (0 instead of 1) passed to type: {0}", t.CollectionTypeName);

+          // add a proxy type, to make sure that CollectionType will have have a non-null Arg

+          t.SetTypeArg(new InferredTypeProxy());

+        }

+

+        if (t.Arg.IsSubrangeType) {

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

         }

       } else if (type is UserDefinedType) {

-        UserDefinedType t = (UserDefinedType)type;

+        var t = (UserDefinedType)type;

         foreach (Type tt in t.TypeArgs) {

           ResolveType(t.tok, tt, option, defaultTypeArguments);

           if (tt.IsSubrangeType) {

@@ -3596,31 +3637,7 @@ namespace Microsoft.Dafny
             if (option == ResolveTypeOption.DontInfer) {

               // don't add anything

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

-              if (option == ResolveTypeOption.InferTypeProxies) {

-                // add type arguments that will be inferred

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

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

-                }

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

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

-              } else if (option == ResolveTypeOption.AllowPrefix && defaultTypeArguments.Count < d.TypeArgs.Count) {

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

-              } else {

-                // we'll add arguments

-                if (option == ResolveTypeOption.AllowPrefixExtend) {

-                  // extend defaultTypeArguments, if needed

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

-                    defaultTypeArguments.Add(new TypeParameter(t.tok, "_T" + i));

-                  }

-                }

-                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>(), null);

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

-                  t.TypeArgs.Add(typeArg);

-                }

-              }

+              FillInTypeArguments(t.tok, d.TypeArgs.Count, t.TypeArgs, defaultTypeArguments, option);

             }

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

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

@@ -3641,6 +3658,40 @@ namespace Microsoft.Dafny
       return null;

     }

 

+    /// <summary>

+    /// Adds to "typeArgs" a list of "n" type arguments, possibly extending "defaultTypeArguments".

+    /// </summary>

+    static void FillInTypeArguments(IToken tok, int n, List<Type> typeArgs, List<TypeParameter> defaultTypeArguments, ResolveTypeOption option) {

+      Contract.Requires(tok != null);

+      Contract.Requires(0 <= n);

+      Contract.Requires(typeArgs != null && typeArgs.Count == 0);

+      if (option == ResolveTypeOption.InferTypeProxies) {

+        // add type arguments that will be inferred

+        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 {

+        // we'll add arguments

+        if (option == ResolveTypeOption.AllowPrefixExtend) {

+          // extend defaultTypeArguments, if needed

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

+            defaultTypeArguments.Add(new TypeParameter(tok, "_T" + i));

+          }

+        }

+        Contract.Assert(n <= defaultTypeArguments.Count);

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

+        for (int i = 0; i < n; i++) {

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

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

+          typeArgs.Add(typeArg);

+        }

+      }

+    }

+

     public bool UnifyTypes(Type a, Type b) {

       Contract.Requires(a != null);

       Contract.Requires(b != null);