Support default (which, here, means nameless) class-instance constructors

11 files changed, 320 insertions, 161 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 38c793c5..340683f6 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -357,10 +357,10 @@ namespace Microsoft.Dafny
         var r = (TypeRhs)rhs;

         if (r.ArrayDimensions != null) {

           c = new TypeRhs(Tok(r.Tok), CloneType(r.EType), r.ArrayDimensions.ConvertAll(CloneExpr));

-        } else if (r.InitCall != null) {

-          c = new TypeRhs(Tok(r.Tok), CloneType(r.EType), (CallStmt)CloneStmt(r.InitCall));

-        } else {

+        } else if (r.Arguments == null) {

           c = new TypeRhs(Tok(r.Tok), CloneType(r.EType));

+        } else {

+          c = new TypeRhs(Tok(r.Tok), CloneType(r.EType), r.OptionalNameComponent, CloneExpr(r.ReceiverArgumentForInitCall), r.Arguments.ConvertAll(CloneExpr));

         }

       }

       c.Attributes = CloneAttributes(rhs.Attributes);

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 4c425497..fa8cd9b2 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -465,7 +465,8 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
 /*------------------------------------------------------------------------*/

 MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>

 = (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);

-     IToken/*!*/ id;

+     IToken/*!*/ id = Token.NoToken;

+     bool hasName = false;  IToken keywordToken;

      Attributes attrs = null;

      List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();

      IToken openParen;

@@ -491,7 +492,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
                                          SemErr(t, "constructors are only allowed in classes");

                                        }

                                     .)

-  )

+  )                                 (. keywordToken = t; .)

   (. if (isConstructor) {

        if (mmod.IsGhost) {

          SemErr(t, "constructors cannot be declared 'ghost'");

@@ -502,7 +503,15 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
      }

   .)

   { Attribute<ref attrs> }

-  NoUSIdent<out id>

+  [ NoUSIdent<out id>               (. hasName = true; .)

+  ]

+  (. if (!hasName) {

+       id = keywordToken;

+       if (!isConstructor) {

+         SemErr(la, "a method must be given a name (expecting identifier)");

+       }

+     }

+  .)

   (

     [ GenericParameters<typeArgs> ]

     Formals<true, !mmod.IsGhost, ins, out openParen>

@@ -515,7 +524,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
   [ BlockStmt<out body, out bodyStart, out bodyEnd>

   ]

   (. if (isConstructor) {

-       m = new Constructor(id, id.val, typeArgs, ins,

+       m = new Constructor(id, hasName ? id.val : "_ctor", typeArgs, ins,

                            req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);

      } else {

        m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,

@@ -966,10 +975,9 @@ UpdateStmt<out Statement/*!*/ s>
 Rhs<out AssignmentRhs r, Expression receiverForInitCall>

 = (. Contract.Ensures(Contract.ValueAtReturn<AssignmentRhs>(out r) != null);

      IToken/*!*/ x, newToken;  Expression/*!*/ e;

-     List<Expression> ee = null;

      Type ty = null;

-     CallStmt initCall = null;

-     List<Expression> args;

+     List<Expression> ee = null;

+     List<Expression> args = null;

      r = dummyRhs;  // to please compiler

      Attributes attrs = null;

   .)

@@ -980,33 +988,18 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
       "]"                              (. // make sure an array class with this dimensionality exists

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

                                        .)

-    | "." Ident<out x>                 

-      "("                              (. // This case happens when we have type<typeargs>.Constructor(args)

-                                          // There is no ambiguity about where the constructor is or whether one exists.

-                                          args = new List<Expression/*!*/>(); .)

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

+      [ "." Ident<out x> ]

+      "("

         [ Expressions<args> ]

-      ")"                              (. initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args); .)

-    | "("                              (. var udf = ty as UserDefinedType;

-                                          if (udf != null && 0 < udf.Path.Count && udf.TypeArgs.Count == 0) {

-                                            // The parsed name had the form "A.B.Ctr", so treat "A.B" as the name of the type and "Ctr" as

-                                            // the name of the constructor that's being invoked.

-                                            x = udf.tok;

-                                            ty = new UserDefinedType(udf.Path[0], udf.Path[udf.Path.Count-1].val, new List<Type>(), udf.Path.GetRange(0,udf.Path.Count-1));

-                                          } else {

-                                            SemErr(t, "expected '.'");

-                                            x = null;

-                                          }

-                                          args = new List<Expression/*!*/>(); .)

-        [ Expressions<args> ]

-      ")"                              (. if (x != null) {

-                                            initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);

-                                          }

-                                       .)

+      ")"

     ]

     (. if (ee != null) {

          r = new TypeRhs(newToken, ty, ee);

+       } else if (args != null) {

+         r = new TypeRhs(newToken, ty, x == null ? null : x.val, receiverForInitCall, args);

        } else {

-         r = new TypeRhs(newToken, ty, initCall);

+         r = new TypeRhs(newToken, ty);

        }

     .)

   /* One day, the choose expression should be treated just as a special case of a method call. */

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 345fc6fa..3550ddb2 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1786,6 +1786,12 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(ens));

       Contract.Requires(decreases != null);

     }

+

+    public bool HasName {

+      get {

+        return Name != "_ctor";

+      }

+    }

   }

 

   // ------------------------------------------------------------------------------------------------------

@@ -2077,39 +2083,81 @@ namespace Microsoft.Dafny {
     }

   }

 

+  /// <summary>

+  /// A TypeRhs represents one of three things, each having to do with allocating something in the heap:

+  ///  * new T[EE]

+  ///    This allocates an array of objects of type T (where EE is a list of expression)

+  ///  * new C

+  ///    This allocates an object of type C

+  ///  * new C.Init(EE)

+  ///    This allocates an object of type C and then invokes the method/constructor Init on it

+  /// There are four ways to construct a TypeRhs syntactically:

+  ///  * TypeRhs(T, EE)

+  ///      -- represents new T[EE]

+  ///  * TypeRhs(C)

+  ///      -- represents new C

+  ///  * TypeRhs(Path, null, EE)

+  ///    Here, Path may either be of the form C.Init

+  ///      -- represents new C.Init(EE)

+  ///    or all of Path denotes a type

+  ///      -- represents new C._ctor(EE), where _ctor is the default constructor for class C

+  ///  * TypeRhs(Path, s, EE)

+  ///    Here, Path must denote a type and s is a string that denotes the method/constructor Init

+  ///      -- represents new Path.s(EE)

+  /// </summary>

   public class TypeRhs : AssignmentRhs

   {

-    public readonly Type EType;

+    /// <summary>

+    /// If ArrayDimensions != null, then the TypeRhs represents "new EType[ArrayDimensions]"

+    ///     and Arguments, OptionalNameComponent, and InitCall are all null.

+    /// If Arguments == null, then the TypeRhs represents "new C"

+    ///     and ArrayDimensions, OptionalNameComponent, and InitCall are all null.

+    /// If OptionalNameComponent != null, then the TypeRhs represents "new EType.OptionalNameComponents(Arguments)"

+    ///     and InitCall is filled in by resolution, and ArrayDimensions == null and Arguments != null.

+    /// If OptionalNameComponent == null and Arguments != null, then the TypeRHS has not been resolved yet;

+    ///   resolution will either produce an error or will chop off the last part of "EType" and move it to

+    ///   OptionalNameComponent, after which the case above applies.

+    /// </summary>

+    public Type EType;  // almost readonly, except that resolution can split a given EType into a new EType plus a non-null OptionalNameComponent

     public readonly List<Expression> ArrayDimensions;

-    public CallStmt InitCall;  // may be null (and is definitely null for arrays)

+    public readonly List<Expression> Arguments;

+    public Expression ReceiverArgumentForInitCall;  // may be filled during resolution (and, if so, had better be done before InitCall is filled)

+    public string OptionalNameComponent;

+    public CallStmt InitCall;  // may be null (and is definitely null for arrays), may be filled in during resolution

     public Type Type;  // filled in during resolution

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(EType != null);

+      Contract.Invariant(ArrayDimensions == null || (Arguments == null && OptionalNameComponent == null && InitCall == null));

       Contract.Invariant(ArrayDimensions == null || 1 <= ArrayDimensions.Count);

-      Contract.Invariant(ArrayDimensions == null || InitCall == null);

+      Contract.Invariant(OptionalNameComponent == null || (Arguments != null && ArrayDimensions == null));

     }

 

-    public TypeRhs(IToken tok, Type type)

-      : base(tok)

-    {

+    public TypeRhs(IToken tok, Type type, List<Expression> arrayDimensions)

+      : base(tok) {

+      Contract.Requires(tok != null);

       Contract.Requires(type != null);

+      Contract.Requires(arrayDimensions != null && 1 <= arrayDimensions.Count);

       EType = type;

+      ArrayDimensions = arrayDimensions;

     }

-    public TypeRhs(IToken tok, Type type, CallStmt initCall)

+    public TypeRhs(IToken tok, Type type)

       : base(tok)

     {

+      Contract.Requires(tok != null);

       Contract.Requires(type != null);

       EType = type;

-      InitCall = initCall;

     }

-    public TypeRhs(IToken tok, Type type, List<Expression> arrayDimensions)

+    public TypeRhs(IToken tok, Type type, string optionalNameComponent, Expression receiverForInitCall, List<Expression> arguments)

       : base(tok)

     {

+      Contract.Requires(tok != null);

       Contract.Requires(type != null);

-      Contract.Requires(arrayDimensions != null && 1 <= arrayDimensions.Count);

+      Contract.Requires(arguments != null);

       EType = type;

-      ArrayDimensions = arrayDimensions;

+      OptionalNameComponent = optionalNameComponent;  // may be null

+      ReceiverArgumentForInitCall = receiverForInitCall;

+      Arguments = arguments;

     }

     public override bool CanAffectPreviouslyKnownExpressions {

       get {

@@ -2448,17 +2496,17 @@ namespace Microsoft.Dafny {
     }

 

     public readonly List<Expression/*!*/>/*!*/ Lhs;

-    public Expression/*!*/ Receiver;

+    public Expression Receiver;  // non-null after resolution

     public readonly string/*!*/ MethodName;

     public readonly List<Expression/*!*/>/*!*/ Args;

     public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions;  // create, initialized, and used by resolution (could be deleted once all of resolution is done)

     public Method Method;  // filled in by resolution

 

-    public CallStmt(IToken tok, List<Expression/*!*/>/*!*/ lhs, Expression/*!*/ receiver,

-      string/*!*/ methodName, List<Expression/*!*/>/*!*/ args)

+    public CallStmt(IToken tok, List<Expression> lhs, Expression receiver, string methodName, List<Expression> args)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(lhs));

+      Contract.Requires(receiver != null);

       Contract.Requires(methodName != null);

       Contract.Requires(cce.NonNullElements(args));

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 032b8a10..1217ae48 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -744,7 +744,8 @@ bool IsAttribute() {
 

 	void MethodDecl(MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m) {

 		Contract.Ensures(Contract.ValueAtReturn(out m) !=null);

-		IToken/*!*/ id;

+		IToken/*!*/ id = Token.NoToken;

+		bool hasName = false;  IToken keywordToken;

 		Attributes attrs = null;

 		List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();

 		IToken openParen;

@@ -774,6 +775,7 @@ bool IsAttribute() {
 			}

 			

 		} else SynErr(135);

+		keywordToken = t; 

 		if (isConstructor) {

 		 if (mmod.IsGhost) {

 		   SemErr(t, "constructors cannot be declared 'ghost'");

@@ -786,7 +788,17 @@ bool IsAttribute() {
 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

-		NoUSIdent(out id);

+		if (la.kind == 1) {

+			NoUSIdent(out id);

+			hasName = true; 

+		}

+		if (!hasName) {

+		 id = keywordToken;

+		 if (!isConstructor) {

+		   SemErr(la, "a method must be given a name (expecting identifier)");

+		 }

+		}

+		

 		if (la.kind == 26 || la.kind == 32) {

 			if (la.kind == 32) {

 				GenericParameters(typeArgs);

@@ -808,7 +820,7 @@ bool IsAttribute() {
 			BlockStmt(out body, out bodyStart, out bodyEnd);

 		}

 		if (isConstructor) {

-		 m = new Constructor(id, id.val, typeArgs, ins,

+		 m = new Constructor(id, hasName ? id.val : "_ctor", typeArgs, ins,

 		                     req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);

 		} else {

 		 m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,

@@ -1919,10 +1931,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void Rhs(out AssignmentRhs r, Expression receiverForInitCall) {

 		Contract.Ensures(Contract.ValueAtReturn<AssignmentRhs>(out r) != null);

 		IToken/*!*/ x, newToken;  Expression/*!*/ e;

-		List<Expression> ee = null;

 		Type ty = null;

-		CallStmt initCall = null;

-		List<Expression> args;

+		List<Expression> ee = null;

+		List<Expression> args = null;

 		r = dummyRhs;  // to please compiler

 		Attributes attrs = null;

 		

@@ -1938,43 +1949,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Expect(66);

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

 					

-				} else if (la.kind == 17) {

-					Get();

-					Ident(out x);

-					Expect(26);

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

-					if (StartOf(13)) {

-						Expressions(args);

-					}

-					Expect(28);

-					initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args); 

 				} else {

-					Get();

-					var udf = ty as UserDefinedType;

-					if (udf != null && 0 < udf.Path.Count && udf.TypeArgs.Count == 0) {

-					 // The parsed name had the form "A.B.Ctr", so treat "A.B" as the name of the type and "Ctr" as

-					 // the name of the constructor that's being invoked.

-					 x = udf.tok;

-					 ty = new UserDefinedType(udf.Path[0], udf.Path[udf.Path.Count-1].val, new List<Type>(), udf.Path.GetRange(0,udf.Path.Count-1));

-					} else {

-					 SemErr(t, "expected '.'");

-					 x = null;

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

+					if (la.kind == 17) {

+						Get();

+						Ident(out x);

 					}

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

+					Expect(26);

 					if (StartOf(13)) {

 						Expressions(args);

 					}

 					Expect(28);

-					if (x != null) {

-					 initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);

-					}

-					

 				}

 			}

 			if (ee != null) {

 			 r = new TypeRhs(newToken, ty, ee);

+			} else if (args != null) {

+			 r = new TypeRhs(newToken, ty, x == null ? null : x.val, receiverForInitCall, args);

 			} else {

-			 r = new TypeRhs(newToken, ty, initCall);

+			 r = new TypeRhs(newToken, ty);

 			}

 			

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

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 7b5c1d42..e85c5e20 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -338,7 +338,8 @@ namespace Microsoft.Dafny {
       string k = method is Constructor ? "constructor" : "method";

       if (method.IsStatic) { k = "static " + k; }

       if (method.IsGhost) { k = "ghost " + k; }

-      PrintClassMethodHelper(k, method.Attributes, method.Name, method.TypeArgs);

+      string nm = method is Constructor && !((Constructor)method).HasName ? "" : method.Name;

+      PrintClassMethodHelper(k, method.Attributes, nm, method.TypeArgs);

       if (method.SignatureIsOmitted) {

         wr.WriteLine(" ...");

       } else {

@@ -840,9 +841,14 @@ namespace Microsoft.Dafny {
             s = ", ";

           }

           wr.Write("]");

-        } else if (t.InitCall != null) {

-          wr.Write(".{0}(", t.InitCall.MethodName);

-          PrintExpressionList(t.InitCall.Args);

+        } else if (t.Arguments == null) {

+          // nothing else to print

+        } else {

+          if (t.OptionalNameComponent != null) {

+            wr.Write(".{0}", t.OptionalNameComponent);

+          }

+          wr.Write("(");

+          PrintExpressionList(t.Arguments);

           wr.Write(")");

         }

       } else {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index a876864e..11acfb2d 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -576,7 +576,7 @@ namespace Microsoft.Dafny
           // saying is that the Method/Predicate does not take any type parameters over and beyond what the enclosing type (namely, the

           // iterator type) does.

           // --- here comes the constructor

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

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

             new List<MaybeFreeExpression>(),

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

             new List<MaybeFreeExpression>(),

@@ -637,10 +637,12 @@ namespace Microsoft.Dafny
 

           bool hasConstructor = false;

           foreach (MemberDecl m in cl.Members) {

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

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

-            } else {

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

               members.Add(m.Name, m);

+            } else if (m is Constructor && !((Constructor)m).HasName) {

+              Error(m, "More than one default constructor");

+            } else {

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

             }

             if (m is Constructor) {

               hasConstructor = true;

@@ -2757,6 +2759,28 @@ namespace Microsoft.Dafny
     }

 

     /// <summary>

+    /// This method calls ResolveTypeLenient with allowShortenedPath=false.

+    /// </summary>

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

+      var r = ResolveTypeLenient(tok, type, defaultTypeArguments, allowAutoTypeArguments, false);

+      Contract.Assert(r == null);

+    }

+

+    public class ResolveTypeReturn

+    {

+      public readonly Type ReplacementType;

+      public readonly string LastName;

+      public readonly IToken LastToken;

+      public ResolveTypeReturn(Type replacementType, string lastName, IToken lastToken) {

+        Contract.Requires(replacementType != null);

+        Contract.Requires(lastName != null);

+        Contract.Requires(lastToken != null);

+        ReplacementType = replacementType;

+        LastName = lastName;

+        LastToken = lastToken;

+      }

+    }

+    /// <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.

@@ -2765,8 +2789,12 @@ namespace Microsoft.Dafny
     ///   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".

+    /// One more thing:  if "allowShortenedPath" is true, then if the resolution would have produced

+    ///   an error message that could have been avoided if "type" denoted an identifier sequence one

+    ///   shorter, then return an unresolved replacement type where the identifier sequence is one

+    ///   shorter.  (In all other cases, the method returns null.)

     /// </summary>

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

+    public ResolveTypeReturn ResolveTypeLenient(IToken tok, Type type, List<TypeParameter> defaultTypeArguments, bool allowAutoTypeArguments, bool allowShortenedPath) {

       Contract.Requires(tok != null);

       Contract.Requires(type != null);

       if (type is BasicType) {

@@ -2803,14 +2831,24 @@ namespace Microsoft.Dafny
         } 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')

           TopLevelDecl d = null;

 

-          int j = 0;

+          int j;

           var sig = moduleInfo;

-          while (j < t.Path.Count) {

-            if (sig.FindSubmodule(t.Path[j].val, out sig)) {

-              j++;

-              sig = GetSignature(sig);

+          for (j = 0; j < t.Path.Count; j++) {

+            ModuleSignature submodule;

+            if (sig.FindSubmodule(t.Path[j].val, out submodule)) {

+              sig = GetSignature(submodule);

             } else {

-              Error(t.Path[j], ModuleNotFoundErrorMessage(j, t.Path));

+              // maybe the last component of t.Path is actually the type name

+              if (allowShortenedPath && t.TypeArgs.Count == 0 && j == t.Path.Count - 1 && sig.TopLevels.TryGetValue(t.Path[j].val, out d)) {

+                // move the last component of t.Path to t.tok/t.name, tell the caller about this, and continue

+                var reducedPath = new List<IToken>();

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

+                  reducedPath.Add(t.Path[i]);

+                }

+                return new ResolveTypeReturn(new UserDefinedType(t.Path[j], t.Path[j].val, t.TypeArgs, reducedPath), t.Name, t.tok);

+              } else {

+                Error(t.Path[j], ModuleNotFoundErrorMessage(j, t.Path));

+              }

               break;

             }

           }

@@ -2875,6 +2913,7 @@ namespace Microsoft.Dafny
       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

       }

+      return null;

     }

 

     public bool UnifyTypes(Type a, Type b) {

@@ -3227,8 +3266,8 @@ namespace Microsoft.Dafny
               // link the receiver parameter properly:

               if (s.rhss[i] is TypeRhs) {

                 var r = (TypeRhs)s.rhss[i];

-                if (r.InitCall != null) {

-                  r.InitCall.Receiver = ident;

+                if (r.Arguments != null) {

+                  r.ReceiverArgumentForInitCall = ident;

                 }

               }

               i++;

@@ -4230,17 +4269,61 @@ namespace Microsoft.Dafny
       Contract.Ensures(Contract.Result<Type>() != null);

 

       if (rr.Type == null) {

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

-        if (rr.ArrayDimensions == null) {

+        if (rr.ArrayDimensions != null) {

+          // ---------- new T[EE]

+          Contract.Assert(rr.Arguments == null && rr.OptionalNameComponent == null && rr.InitCall == null);

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

+          int i = 0;

+          if (rr.EType.IsSubrangeType) {

+            Error(stmt, "sorry, cannot instantiate 'array' type with a subrange type");

+          }

+          foreach (Expression dim in rr.ArrayDimensions) {

+            Contract.Assert(dim != null);

+            ResolveExpression(dim, true);

+            if (!UnifyTypes(dim.Type, Type.Int)) {

+              Error(stmt, "new must use an integer expression for the array size (got {0} for index {1})", dim.Type, i);

+            }

+            i++;

+          }

+          rr.Type = builtIns.ArrayType(rr.ArrayDimensions.Count, rr.EType);

+        } else {

+          var initCallTok = rr.Tok;

+          if (rr.OptionalNameComponent == null && rr.Arguments != null) {

+            // Resolve rr.EType and do one of three things:

+            // * If rr.EType denotes a type, then set rr.OptionalNameComponent to "_ctor", which sets up a call to the default constructor.

+            // * If the all-but-last components of rr.EType denote a type, then do EType,OptionalNameComponent := allButLast(EType),last(EType)

+            // * Otherwise, report an error

+            var ret = ResolveTypeLenient(stmt.Tok, rr.EType, null, true, true);

+            if (ret != null) {

+              // While rr.EType does not denote a type, no error has been reported yet and the all-but-last components of rr.EType may

+              // denote a type, so shift the last component to OptionalNameComponent and retry with the suggested type.

+              rr.OptionalNameComponent = ret.LastName;

+              rr.EType = ret.ReplacementType;

+              initCallTok = ret.LastToken;

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

+            } else {

+              // Either rr.EType resolved correctly as a type or there was no way to drop a last component to make it into something that looked

+              // like a type.  In either case, set OptionalNameComponent to "_ctor" and continue.

+              rr.OptionalNameComponent = "_ctor";

+            }

+          } else {

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

+          }

           if (!rr.EType.IsRefType) {

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

           } else {

             bool callsConstructor = false;

-            if (rr.InitCall != null) {

+            if (rr.Arguments != null) {

+              // ---------- new C.Init(EE)

+              Contract.Assert(rr.OptionalNameComponent != null);  // if it wasn't non-null from the beginning, the code above would have set it to a non-null value

+              rr.InitCall = new CallStmt(initCallTok, new List<Expression>(), rr.ReceiverArgumentForInitCall, rr.OptionalNameComponent, rr.Arguments);

               ResolveCallStmt(rr.InitCall, specContextOnly, codeContext, rr.EType);

               if (rr.InitCall.Method is Constructor) {

                 callsConstructor = true;

               }

+            } else {

+              // ---------- new C

+              Contract.Assert(rr.ArrayDimensions == null && rr.OptionalNameComponent == null && rr.InitCall == null);

             }

             if (!callsConstructor && rr.EType is UserDefinedType) {

               var udt = (UserDefinedType)rr.EType;

@@ -4251,20 +4334,6 @@ namespace Microsoft.Dafny
             }

           }

           rr.Type = rr.EType;

-        } else {

-          int i = 0;

-          if (rr.EType.IsSubrangeType) {

-            Error(stmt, "sorry, cannot instantiate 'array' type with a subrange type");

-          }

-          foreach (Expression dim in rr.ArrayDimensions) {

-            Contract.Assert(dim != null);

-            ResolveExpression(dim, true);

-            if (!UnifyTypes(dim.Type, Type.Int)) {

-              Error(stmt, "new must use an integer expression for the array size (got {0} for index {1})", dim.Type, i);

-            }

-            i++;

-          }

-          rr.Type = builtIns.ArrayType(rr.ArrayDimensions.Count, rr.EType);

         }

       }

       return rr.Type;

@@ -4290,7 +4359,12 @@ namespace Microsoft.Dafny
         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 {2} {1}", memberName, ctype.Name, cd is IteratorDecl ? "iterator" : "class");

+          var kind = cd is IteratorDecl ? "iterator" : "class";

+          if (memberName == "_ctor") {

+            Error(tok, "{0} {1} does not have a default constructor", kind, ctype.Name);

+          } else {

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

+          }

           return null;

         } else {

           nptype = ctype;

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 63b4ffce..370e3c38 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -494,6 +494,7 @@ Execution trace:
 Dafny program verifier finished with 3 verified, 4 errors

 

 -------------------- ResolutionErrors.dfy --------------------

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

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

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

 ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

@@ -511,6 +512,10 @@ ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowe
 ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops

 ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

 ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)

+ResolutionErrors.dfy(402,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called

+ResolutionErrors.dfy(407,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

+ResolutionErrors.dfy(408,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

+ResolutionErrors.dfy(410,9): Error: class Lamb does not have a default constructor

 ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)

 ResolutionErrors.dfy(23,12): Error: sequence/array/map selection requires a sequence, array or map (got array3<T>)

@@ -542,16 +547,16 @@ ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specificat
 ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts

 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<_T0>, expected GList<int>)

-ResolutionErrors.dfy(363,4): Error: arguments to + must be int or a collection type (instead got bool)

-ResolutionErrors.dfy(368,4): Error: all lines in a calculation must have the same type (got int after bool)

-ResolutionErrors.dfy(371,4): Error: first argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(371,4): Error: second argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(372,8): Error: first argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(372,8): Error: second argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(377,8): Error: first argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(377,8): Error: second argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(382,4): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-57 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(363,6): Error: arguments to + must be int or a collection type (instead got bool)

+ResolutionErrors.dfy(368,6): Error: all lines in a calculation must have the same type (got int after bool)

+ResolutionErrors.dfy(371,6): Error: first argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(371,6): Error: second argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(372,10): Error: first argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(372,10): Error: second argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(377,10): Error: first argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(377,10): Error: second argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(382,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+62 resolution/type errors detected in ResolutionErrors.dfy

 

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

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

diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy
index 60b1bc7e..004bc85e 100644
--- a/Test/dafny0/IteratorResolution.dfy
+++ b/Test/dafny0/IteratorResolution.dfy
@@ -13,7 +13,7 @@ module Mx {
   }

 

   method IteratorUser() {

-    var iter := new ExampleIterator.ExampleIterator(15);

+    var iter := new ExampleIterator(15);

     iter.k := 12;  // error: not allowed to assign to iterator's in-parameters

     iter.x := 12;  // allowed (but this destroys the validity of 'iter'

     iter.xs := [];  // error: not allowed to assign to iterator's yield-history variables

@@ -41,7 +41,7 @@ module Mx {
   class Client {

     method M() {

       var m := StaticM(5);

-      var it := new ExampleIterator.ExampleIterator(100);

+      var it := new ExampleIterator(100);

       var a, b := Worker(it);

     }

     method Worker(xi: ExampleIterator) returns (k: int, m: int) {

@@ -58,17 +58,17 @@ module Mx {
     {

       g0.t := true;  // error: not allowed to assign to .t

       g0.u := true;  // allowed (but this destroys the validity of 'iter'

-      var g1 := new GenericIterator.GenericIterator(20);

+      var g1 := new GenericIterator(20);

       assert g1.u < 200;  // .u is an integer

 

       assert g2.u == 200;  // error: the type parameter of g2 is unknown

 

-      var h0 := new GenericIteratorResult.GenericIteratorResult();

+      var h0 := new GenericIteratorResult._ctor();

       // so far, the instantiated type of h0 is unknown

       var k := h0.t;

       assert k < 87;

 

-      var h1 := new GenericIteratorResult.GenericIteratorResult();

+      var h1 := new GenericIteratorResult();

       // so far, the instantiated type of h1 is unknown

       if (*) {

         var b: bool := h1.t;  // this determines h1 to be of type GenericIteratorResult<bool>

@@ -78,7 +78,7 @@ module Mx {
 

       var h2 := new GenericIteratorResult;  // error: constructor is not mentioned

 

-      var h3 := new GenericIterator.GenericIterator(30);

+      var h3 := new GenericIterator._ctor(30);

       if (h3.t == h3.u) {

         assert !h3.t;  // error: type mismatch

       }

diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy
index c6a0488b..43ef4e69 100644
--- a/Test/dafny0/Iterators.dfy
+++ b/Test/dafny0/Iterators.dfy
@@ -24,7 +24,7 @@ iterator Naturals(u: int) yields (n: nat)
 }

 

 method Main() {

-  var m := new MyIter.MyIter(12);

+  var m := new MyIter(12);

   assert m.ys == m.xs == [];

   var a := m.x;

   if (a <= 13) {

@@ -37,7 +37,7 @@ method Main() {
     mer := m.MoveNext();  // error

   }

 

-  var n := new MyIntIter.MyIntIter();

+  var n := new MyIntIter();

   var patience := 10;

   while (patience != 0)

     invariant n.Valid() && fresh(n._new);

@@ -48,7 +48,7 @@ method Main() {
     patience := patience - 1;

   }

 

-  var o := new Naturals.Naturals(18);

+  var o := new Naturals(18);

   var remaining := 100;

   while (remaining != 0)

     invariant o.Valid() && fresh(o._new);

@@ -80,7 +80,7 @@ iterator IterA(c: Cell)
 method TestIterA()

 {

   var c := new Cell;

-  var iter := new IterA.IterA(c);

+  var iter := new IterA(c);

   var tmp := c.data;

   var more := iter.MoveNext();

   assert tmp == c.data;  // error

@@ -107,7 +107,7 @@ iterator IterB(c: Cell)
 method TestIterB()

 {

   var c := new Cell;

-  var iter := new IterB.IterB(c);

+  var iter := new IterB(c);

   var tmp := c.data;

   var more := iter.MoveNext();

   if (more) {

@@ -138,7 +138,7 @@ iterator IterC(c: Cell)
 method TestIterC()

 {

   var c := new Cell;

-  var iter := new IterC.IterC(c);

+  var iter := new IterC(c);

   var tmp := c.data;

   var more := iter.MoveNext();

   if (more) {

@@ -147,7 +147,7 @@ method TestIterC()
     assert tmp == c.data;  // error: the postcondition says nothing about this

   }

 

-  iter := new IterC.IterC(c);

+  iter := new IterC(c);

   c.data := 17;

   more := iter.MoveNext();  // error: iter.Valid() may not hold

 }

@@ -217,7 +217,7 @@ iterator DoleOutReferences(u: Cell) yields (r: Cell, c: Cell)
 

 method ClientOfNewReferences()

 {

-  var m := new DoleOutReferences.DoleOutReferences(null);

+  var m := new DoleOutReferences(null);

   var i := 86;

   while (i != 0)

     invariant m.Valid() && fresh(m._new);

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index c615c5ec..7c919b2a 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -359,27 +359,67 @@ method MG1(l: GList, n: nat)
 

 method TestCalc(m: int, n: int, a: bool, b: bool)

 {

-	calc {

-		a + b; // error: invalid line

-		n + m;

-	}

-	calc {

-		a && b;

-		n + m; // error: all lines must have the same type

-	}

-	calc ==> {

-		n + m; // error: ==> operator requires boolean lines

-		n + m + 1;

-		n + m + 2;

-	}		

-	calc {

-		n + m;

-		n + m + 1;

-		==> n + m + 2; // error: ==> operator requires boolean lines

-	}

-	calc {

-		n + m;

-		{ print n + m; } // error: non-ghost statements are not allowed in hints

-		m + n;

-	}			

+  calc {

+    a + b; // error: invalid line

+    n + m;

+  }

+  calc {

+    a && b;

+    n + m; // error: all lines must have the same type

+  }

+  calc ==> {

+    n + m; // error: ==> operator requires boolean lines

+    n + m + 1;

+    n + m + 2;

+  }    

+  calc {

+    n + m;

+    n + m + 1;

+    ==> n + m + 2; // error: ==> operator requires boolean lines

+  }

+  calc {

+    n + m;

+    { print n + m; } // error: non-ghost statements are not allowed in hints

+    m + n;

+  }

+}

+

+// ------------------- nameless constructors ------------------------------

+

+class YHWH {

+  var data: int;

+  constructor (x: int)

+    modifies this;

+  {

+    data := x;

+  }

+  constructor (y: bool)  // error: duplicate constructor name

+  {

+  }

+  method Test() {

+    var IAmWhoIAm := new YHWH(5);

+    IAmWhoIAm := new YHWH._ctor(7);  // but, in fact, it is also possible to use the underlying name

+    IAmWhoIAm := new YHWH;  // error: the class has a constructor, so one must be used

+    var s := new Lucifer.Init(5);

+    s := new Lucifer.FromArray(null);

+    s := new Lucifer(false);

+    s := new Lucifer._ctor(false);

+    s := new Lucifer.M();  // error: there is a constructor, so one must be called

+    s := new Lucifer;  // error: there is a constructor, so one must be called

+    var l := new Lamb;

+    l := new Lamb();  // error: there is no default constructor

+    l := new Lamb.Gwen();

+  }

+}

+

+class Lucifer {

+  constructor Init(y: int) { }

+  constructor (nameless: bool) { }

+  constructor FromArray(a: array<int>) { }

+  method M() { }

+}

+

+class Lamb {

+  method Jesus() { }

+  method Gwen() { }

 }

diff --git a/Test/dafny3/Iter.dfy b/Test/dafny3/Iter.dfy
index 543a889a..3af868ca 100644
--- a/Test/dafny3/Iter.dfy
+++ b/Test/dafny3/Iter.dfy
@@ -73,7 +73,7 @@ method Client<T(==)>(l: List, stop: T) returns (s: seq<T>)
   requires l != null && l.Valid();

 {

   var c := new Cell;

-  var iter := new M.M(l, c);

+  var iter := new M(l, c);

   s := [];

   while (true)

     invariant iter.Valid() && fresh(iter._new);