Fixed resolution of method calls with explicit type parameters.

Finished refactoring of the recent name segments changes.

11 files changed, 273 insertions, 319 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index cb41a75f..ebb291fb 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -440,7 +440,7 @@ namespace Microsoft.Dafny
       }

     }

 

-    public AssignmentRhs CloneRHS(AssignmentRhs rhs) {

+    public virtual AssignmentRhs CloneRHS(AssignmentRhs rhs) {

       AssignmentRhs c;

       if (rhs is ExprRhs) {

         var r = (ExprRhs)rhs;

@@ -454,7 +454,7 @@ namespace Microsoft.Dafny
         } 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 = new TypeRhs(Tok(r.Tok), CloneType(r.EType), r.OptionalNameComponent, r.Arguments.ConvertAll(CloneExpr));

         }

       }

       c.Attributes = CloneAttributes(rhs.Attributes);

@@ -507,10 +507,6 @@ namespace Microsoft.Dafny
         var s = (AssignStmt)stmt;

         r = new AssignStmt(Tok(s.Tok), Tok(s.EndTok), CloneExpr(s.Lhs), CloneRHS(s.Rhs));

 

-      } else if (stmt is CallStmt) {

-        var s = (CallStmt)stmt;

-        r = new CallStmt(Tok(s.Tok), Tok(s.EndTok), s.Lhs.ConvertAll(CloneExpr), CloneExpr(s.Receiver), s.MethodName, s.Args.ConvertAll(CloneExpr));

-

       } else if (stmt is BlockStmt) {

         r = CloneBlockStmt((BlockStmt)stmt);

 

@@ -744,7 +740,7 @@ namespace Microsoft.Dafny
 

   /// <summary>

   /// The task of the CoLemmaBodyCloner is to fill in the implicit _k-1 arguments in corecursive colemma calls.

-  /// The source statement and the given "k" are assumed to have been resolved, and the resulting statement will also be resolved.

+  /// The source statement and the given "k" are assumed to have been resolved.

   /// </summary>

   class CoLemmaBodyCloner : CoCloner

   {

@@ -757,49 +753,33 @@ namespace Microsoft.Dafny
       Contract.Requires(resolver != null);

       this.context = context;

     }

-    public override Statement CloneStmt(Statement stmt) {

-      if (stmt is UpdateStmt) {

-        var s = (UpdateStmt)stmt;

-        if (s.ResolvedStatements.Count == 1 && s.ResolvedStatements[0] is CallStmt) {

-          var call = (CallStmt)s.ResolvedStatements[0];

-          var moduleCaller = context.EnclosingClass.Module;

-          var moduleCallee = call.Method.EnclosingClass.Module;

-          if (call.Method is CoLemma && ModuleDefinition.InSameSCC(context, call.Method)) {

-            // we're looking at a recursive call to a colemma

-            var args = new List<Expression>();

-            args.Add(k);

-            foreach (var arg in call.Args) {

-              args.Add(CloneExpr(arg));

-            }

-            var rhs = new CallRhs(Tok(call.Tok), CloneExpr(call.Receiver), call.MethodName + "#", args);

-            var r = new UpdateStmt(Tok(s.Tok), Tok(s.EndTok), s.Lhss.ConvertAll(CloneExpr), new List<AssignmentRhs>() { rhs }, s.CanMutateKnownState);

-            // don't forget to add labels to the cloned statement

-            AddStmtLabels(r, stmt.Labels);

-            r.Attributes = CloneAttributes(stmt.Attributes);

-            ReportAdditionalInformation(call.Tok, call.MethodName);

-            return r;

-          }

-        }

-      } else if (stmt is CallStmt) {

-        var s = (CallStmt)stmt;

-        if (s.Method is CoLemma) {

-          if (s.Method is CoLemma && ModuleDefinition.InSameSCC(context, s.Method)) {

-            // we're looking at a recursive call to a colemma

-            var args = new List<Expression>();

-            args.Add(k);

-            foreach (var arg in s.Args) {

-              args.Add(CloneExpr(arg));

-            }

-            var r = new CallStmt(Tok(s.Tok), Tok(s.EndTok), s.Lhs.ConvertAll(CloneExpr), CloneExpr(s.Receiver), s.MethodName + "#", args);

-            // don't forget to add labels to the cloned statement

-            AddStmtLabels(r, stmt.Labels);

-            r.Attributes = CloneAttributes(stmt.Attributes);

-            ReportAdditionalInformation(s.Tok, s.MethodName);

-            return r;

+    public override AssignmentRhs CloneRHS(AssignmentRhs rhs) {

+      var r = rhs as ExprRhs;

+      if (r != null && r.Expr is ApplySuffix) {

+        var apply = (ApplySuffix)r.Expr;

+        var mse = apply.Lhs.Resolved as MemberSelectExpr;

+        if (mse != null && mse.Member is CoLemma && ModuleDefinition.InSameSCC(context, (CoLemma)mse.Member)) {

+          // we're looking at a recursive call to a colemma

+          Contract.Assert(apply.Lhs is NameSegment || apply.Lhs is ExprDotName);  // this is the only way a call statement can have been parsed

+          // clone "apply.Lhs", changing the co lemma to the prefix lemma; then clone "apply", adding in the extra argument

+          Expression lhsClone;

+          if (apply.Lhs is NameSegment) {

+            var lhs = (NameSegment)apply.Lhs;

+            lhsClone = new NameSegment(Tok(lhs.tok), lhs.Name + "#", lhs.OptTypeArguments == null ? null : lhs.OptTypeArguments.ConvertAll(CloneType));

+          } else {

+            var lhs = (ExprDotName)apply.Lhs;

+            lhsClone = new ExprDotName(Tok(lhs.tok), CloneExpr(lhs.Lhs), lhs.SuffixName + "#", lhs.OptTypeArguments == null ? null : lhs.OptTypeArguments.ConvertAll(CloneType));

           }

+          var args = new List<Expression>();

+          args.Add(k);

+          apply.Args.ForEach(arg => args.Add(CloneExpr(arg)));

+          var applyClone = new ApplySuffix(Tok(apply.tok), lhsClone, args);

+          var c = new ExprRhs(applyClone);

+          ReportAdditionalInformation(apply.tok, mse.Member.Name);

+          return c;

         }

       }

-      return base.CloneStmt(stmt);

+      return base.CloneRHS(rhs);

     }

   }

 

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index c7ee28ac..e474f3aa 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1428,8 +1428,8 @@ ReturnStmt<out Statement/*!*/ s>
   ( "return"                         (. returnTok = t; .)

   | "yield"                          (. returnTok = t; isYield = true; .)

   )

-  [ Rhs<out r, null>                 (. rhss = new List<AssignmentRhs>(); rhss.Add(r); .)

-    { "," Rhs<out r, null>           (. rhss.Add(r); .)

+  [ Rhs<out r>                       (. rhss = new List<AssignmentRhs>(); rhss.Add(r); .)

+    { "," Rhs<out r>                 (. rhss.Add(r); .)

     }

   ]

   ";"                                (. if (isYield) {

@@ -1443,7 +1443,6 @@ UpdateStmt<out Statement/*!*/ s>
 = (. List<Expression> lhss = new List<Expression>();

      List<AssignmentRhs> rhss = new List<AssignmentRhs>();

      Expression e;  AssignmentRhs r;

-     Expression lhs0;

      IToken x, endTok = Token.NoToken;

      Attributes attrs = null;

      IToken suchThatAssume = null;

@@ -1452,12 +1451,12 @@ UpdateStmt<out Statement/*!*/ s>
   Lhs<out e>                       (. x = e.tok; .)

   ( { Attribute<ref attrs> }

     ";"                            (. endTok = t; rhss.Add(new ExprRhs(e, attrs)); .)

-  |                                (. lhss.Add(e);  lhs0 = e; .)

+  |                                (. lhss.Add(e); .)

     { "," Lhs<out e>               (. lhss.Add(e); .)

     }

     ( ":="                         (. x = t; .)

-      Rhs<out r, lhs0>             (. rhss.Add(r); .)

-      { "," Rhs<out r, lhs0>       (. rhss.Add(r); .)

+      Rhs<out r>                   (. rhss.Add(r); .)

+      { "," Rhs<out r>             (. rhss.Add(r); .)

       }

     | ":|"                         (. x = t; .)

       [ IF(la.kind == _assume)     /* an Expression can also begin with an "assume", so this says to resolve it to pick up any "assume" here */

@@ -1479,7 +1478,7 @@ UpdateStmt<out Statement/*!*/ s>
      }

   .)

   .

-Rhs<out AssignmentRhs r, Expression receiverForInitCall>

+Rhs<out AssignmentRhs r>

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

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

      Type ty = null;

@@ -1504,7 +1503,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
     (. 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);

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

        } else {

          r = new TypeRhs(newToken, ty);

        }

@@ -1517,7 +1516,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
 VarDeclStatement<.out Statement/*!*/ s.>

 = (. IToken x = null, assignTok = null;  bool isGhost = false;

      LocalVariable d;

-     AssignmentRhs r;  IdentifierExpr lhs0;

+     AssignmentRhs r;

      List<LocalVariable> lhss = new List<LocalVariable>();

      List<AssignmentRhs> rhss = new List<AssignmentRhs>();

      IToken suchThatAssume = null;

@@ -1534,11 +1533,9 @@ VarDeclStatement<.out Statement/*!*/ s.>
     { Attribute<ref attrs> }

     LocalIdentTypeOptional<out d, isGhost>  (. lhss.Add(d); d.Attributes = attrs; attrs = null; .)

   }

-  [ ":="                           (. assignTok = t;

-                                      lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);

-                                   .)

-    Rhs<out r, lhs0>               (. rhss.Add(r); .)

-    { "," Rhs<out r, lhs0>         (. rhss.Add(r); .)

+  [ ":="                           (. assignTok = t; .)

+    Rhs<out r>                     (. rhss.Add(r); .)

+    { "," Rhs<out r>               (. rhss.Add(r); .)

     }

   | ":|"                           (. assignTok = t; .)

     [ IF(la.kind == _assume)       /* an Expression can also begin with an "assume", so this says to resolve it to pick up any "assume" here */

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 1593aeb5..0b845c23 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3465,7 +3465,6 @@ namespace Microsoft.Dafny {
     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 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

@@ -3492,7 +3491,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(type != null);

       EType = type;

     }

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

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

       : base(tok)

     {

       Contract.Requires(tok != null);

@@ -3500,7 +3499,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(arguments != null);

       EType = type;

       OptionalNameComponent = optionalNameComponent;  // may be null

-      ReceiverArgumentForInitCall = receiverForInitCall;

       Arguments = arguments;

     }

     public override bool CanAffectPreviouslyKnownExpressions {

@@ -3534,53 +3532,6 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class CallRhs : AssignmentRhs

-  {

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(Receiver != null);

-      Contract.Invariant(MethodName != null);

-      Contract.Invariant(cce.NonNullElements(Args));

-    }

-

-    public readonly Expression Receiver;

-    public readonly string MethodName;

-    public readonly List<Expression> Args;

-    public Method Method;  // filled in by resolution

-

-    public CallRhs(IToken tok, Expression receiver, string methodName, List<Expression> args)

-      : base(tok)

-    {

-      Contract.Requires(tok != null);

-      Contract.Requires(receiver != null);

-      Contract.Requires(methodName != null);

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

-

-      this.Receiver = receiver;

-      this.MethodName = methodName;

-      this.Args = args;

-    }

-    // TODO: Investigate this. For an initialization, this is true. But for existing objects, this is not true.

-    public override bool CanAffectPreviouslyKnownExpressions {

-      get {

-        foreach (var mod in Method.Mod.Expressions) {

-          if (!(mod.E is ThisExpr)) {

-            return true;

-          }

-        }

-        return false;

-      }

-    }

-    public override IEnumerable<Expression> SubExpressions {

-      get {

-        yield return Receiver;

-        foreach (var e in Args) {

-          yield return e;

-        }

-      }

-    }

-  }

-

   public class HavocRhs : AssignmentRhs {

     public HavocRhs(IToken tok)

       : base(tok)

@@ -3886,39 +3837,35 @@ namespace Microsoft.Dafny {
     }

   }

 

+  /// <summary>

+  /// A CallStmt is always resolved.  It is typically produced as a resolved counterpart of the syntactic AST note ApplySuffix.

+  /// </summary>

   public class CallStmt : Statement {

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      //Contract.Invariant(Receiver != null);

-      Contract.Invariant(MethodName != null);

+      Contract.Invariant(MethodSelect.Member is Method);

       Contract.Invariant(cce.NonNullElements(Lhs));

       Contract.Invariant(cce.NonNullElements(Args));

-      Contract.Invariant(TypeArgumentSubstitutions == null ||

-        Contract.ForAll(Method.TypeArgs, tp => TypeArgumentSubstitutions.ContainsKey(tp)));

     }

 

     public readonly List<Expression> Lhs;

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

-    public readonly string MethodName;

+    public readonly MemberSelectExpr MethodSelect;

     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)

-	// That's not going to work! It should never be deleted!

-    public Method Method;  // filled in by resolution

 

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

+    public Expression Receiver { get { return MethodSelect.Obj; } }

+    public Method Method { get { return (Method)MethodSelect.Member; } }

+

+    public CallStmt(IToken tok, IToken endTok, List<Expression> lhs, MemberSelectExpr memSel, List<Expression> args)

       : base(tok, endTok) {

       Contract.Requires(tok != null);

       Contract.Requires(endTok != null);

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

-      Contract.Requires(receiver != null);

-      Contract.Requires(methodName != null);

+      Contract.Requires(memSel != null);

+      Contract.Requires(memSel.Member is Method);

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

 

       this.Lhs = lhs;

-      this.Receiver = receiver;

-      this.MethodName = methodName;

+      this.MethodSelect = memSel;

       this.Args = args;

     }

 

@@ -3928,7 +3875,7 @@ namespace Microsoft.Dafny {
         foreach (var ee in Lhs) {

           yield return ee;

         }

-        yield return Receiver;

+        yield return MethodSelect;

         foreach (var ee in Args) {

           yield return ee;

         }

@@ -5503,13 +5450,33 @@ namespace Microsoft.Dafny {
     public readonly Expression Obj;

     public readonly string MemberName;

     public MemberDecl Member;          // filled in by resolution, will be a Field or Function

-    public List<Type> TypeApplication; // If Member is a Function, then TypeApplication is the list of type arguments used with the enclosing class and the function itself

+    public List<Type> TypeApplication; // If Member is a Function or Method, then TypeApplication is the list of type arguments used with the enclosing class and the function/method itself

+

+    public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions() {

+      Contract.Requires(WasResolved());

+      Contract.Requires(Member is ICallable);

+      Contract.Ensures(Contract.Result<Dictionary<TypeParameter, Type>>() != null);

+      Contract.Ensures(Contract.Result<Dictionary<TypeParameter, Type>>().Count == TypeApplication.Count);

+

+      Contract.Assert(Member.EnclosingClass.TypeArgs.Count + ((ICallable)Member).TypeArgs.Count == TypeApplication.Count);  // a consequence of proper resolution

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

+      var i = 0;

+      foreach (var tp in Member.EnclosingClass.TypeArgs) {

+        subst.Add(tp, TypeApplication[i]);

+        i++;

+      }

+      foreach (var tp in ((ICallable)Member).TypeArgs) {

+        subst.Add(tp, TypeApplication[i]);

+        i++;

+      }

+      return subst;

+    }

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Obj != null);

       Contract.Invariant(MemberName != null);

-      Contract.Invariant((Member is Function) == (TypeApplication != null));

+      Contract.Invariant((Member is Function || Member is Method) == (TypeApplication != null));

     }

 

     public MemberSelectExpr(IToken tok, Expression obj, string memberName)

@@ -5692,8 +5659,7 @@ namespace Microsoft.Dafny {
     public readonly Expression Receiver;

     public readonly IToken OpenParen;  // can be null if Args.Count == 0

     public readonly List<Expression> Args;

-    public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions;

-	// created, initialized, and used by resolution (and also used by translation)

+    public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions;  // created, initialized, and used by resolution (and also used by translation)

     public enum CoCallResolution {

       No,

       Yes,

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 42627024..15137923 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -2104,7 +2104,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Expression> lhss = new List<Expression>();

 		List<AssignmentRhs> rhss = new List<AssignmentRhs>();

 		Expression e;  AssignmentRhs r;

-		Expression lhs0;

 		IToken x, endTok = Token.NoToken;

 		Attributes attrs = null;

 		IToken suchThatAssume = null;

@@ -2119,7 +2118,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(25);

 			endTok = t; rhss.Add(new ExprRhs(e, attrs)); 

 		} else if (la.kind == 20 || la.kind == 89 || la.kind == 91) {

-			lhss.Add(e);  lhs0 = e; 

+			lhss.Add(e); 

 			while (la.kind == 20) {

 				Get();

 				Lhs(out e);

@@ -2128,11 +2127,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (la.kind == 89) {

 				Get();

 				x = t; 

-				Rhs(out r, lhs0);

+				Rhs(out r);

 				rhss.Add(r); 

 				while (la.kind == 20) {

 					Get();

-					Rhs(out r, lhs0);

+					Rhs(out r);

 					rhss.Add(r); 

 				}

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

@@ -2165,7 +2164,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void VarDeclStatement(out Statement/*!*/ s) {

 		IToken x = null, assignTok = null;  bool isGhost = false;

 		LocalVariable d;

-		AssignmentRhs r;  IdentifierExpr lhs0;

+		AssignmentRhs r;

 		List<LocalVariable> lhss = new List<LocalVariable>();

 		List<AssignmentRhs> rhss = new List<AssignmentRhs>();

 		IToken suchThatAssume = null;

@@ -2195,14 +2194,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 89 || la.kind == 91) {

 			if (la.kind == 89) {

 				Get();

-				assignTok = t;

-				lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);

-				

-				Rhs(out r, lhs0);

+				assignTok = t; 

+				Rhs(out r);

 				rhss.Add(r); 

 				while (la.kind == 20) {

 					Get();

-					Rhs(out r, lhs0);

+					Rhs(out r);

 					rhss.Add(r); 

 				}

 			} else {

@@ -2560,11 +2557,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			returnTok = t; isYield = true; 

 		} else SynErr(191);

 		if (StartOf(26)) {

-			Rhs(out r, null);

+			Rhs(out r);

 			rhss = new List<AssignmentRhs>(); rhss.Add(r); 

 			while (la.kind == 20) {

 				Get();

-				Rhs(out r, null);

+				Rhs(out r);

 				rhss.Add(r); 

 			}

 		}

@@ -2612,7 +2609,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		s = new SkeletonStatement(dotdotdot, t, names, exprs); 

 	}

 

-	void Rhs(out AssignmentRhs r, Expression receiverForInitCall) {

+	void Rhs(out AssignmentRhs r) {

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

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

 		Type ty = null;

@@ -2649,7 +2646,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			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);

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

 			} else {

 			 r = new TypeRhs(newToken, ty);

 			}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 9a27c080..794dfe05 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -786,25 +786,6 @@ namespace Microsoft.Dafny {
         PrintRhs(s.Rhs);

         wr.Write(";");

 

-      } else if (stmt is CallStmt) {

-        CallStmt s = (CallStmt)stmt;

-        if (s.Lhs.Count != 0) {

-          string sep = "";

-          foreach (IdentifierExpr v in s.Lhs) {

-            wr.Write(sep);

-            PrintExpression(v, true);

-            sep = ", ";

-          }

-          wr.Write(" := ");

-        }

-        if (!(s.Receiver is ImplicitThisExpr)) {

-          PrintExpr(s.Receiver, 0x70, false, false, true, -1);

-          wr.Write(".");

-        }

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

-        PrintActualArguments(s.Args, s.MethodName);

-        wr.Write(";");

-

       } else if (stmt is BlockStmt) {

         wr.WriteLine("{");

         int ind = indent + IndentAmount;

@@ -1145,14 +1126,6 @@ namespace Microsoft.Dafny {
           PrintExpressionList(t.Arguments, false);

           wr.Write(")");

         }

-      } else if (rhs is CallRhs) {

-        var r = (CallRhs)rhs;

-        if (!(r.Receiver is ImplicitThisExpr)) {

-          PrintExpr(r.Receiver, 0x70, false, false, true, -1);

-          wr.Write(".");

-        }

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

-        PrintActualArguments(r.Args, r.MethodName);

       } else {

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

       }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 483ff08f..f1e0f315 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1878,13 +1878,6 @@ namespace Microsoft.Dafny
         } else if (stmt is ForallStmt) {

           var s = (ForallStmt)stmt;

           s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable"));

-        } else if (stmt is CallStmt) {

-          var s = (CallStmt)stmt;

-          foreach (var p in s.TypeArgumentSubstitutions) {

-            if (!IsDetermined(p.Value.Normalize())) {

-              Error(stmt.Tok, "type variable '{0}' in the method call to '{1}' could not be determined", p.Key.Name, s.MethodName);

-            }

-          }

         }

       }

       protected override void VisitOneExpr(Expression expr) {

@@ -1900,10 +1893,11 @@ namespace Microsoft.Dafny
           }

         } else if (expr is MemberSelectExpr) {

           var e = (MemberSelectExpr)expr;

-          if (e.Member is Function) {

+          var what = e.Member is Function ? "function" : e.Member is Method ? "method" : null;

+          if (what != null) {

             foreach (var p in e.TypeApplication) {

               if (!IsDetermined(p.Normalize())) {

-                Error(e.tok, "type '{0}' to the function '{1}' is not determined", p, e.Member.Name);

+                Error(e.tok, "type '{0}' to the {2} '{1}' is not determined", p, e.Member.Name, what);

               }

             }

           }

@@ -2420,10 +2414,10 @@ namespace Microsoft.Dafny
           return false;

         } else if (stmt is CallStmt) {

           var s = (CallStmt)stmt;

-          Contract.Assert(s.Method.TypeArgs.Count <= s.TypeArgumentSubstitutions.Count);

+          Contract.Assert(s.Method.TypeArgs.Count <= s.MethodSelect.TypeArgumentSubstitutions().Count);

           var i = 0;

           foreach (var formalTypeArg in s.Method.TypeArgs) {

-            var actualTypeArg = s.TypeArgumentSubstitutions[formalTypeArg];

+            var actualTypeArg = s.MethodSelect.TypeArgumentSubstitutions()[formalTypeArg];

             if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) {

               Error(s.Tok, "type parameter {0} ({1}) passed to method {2} must support equality (got {3}){4}", i, formalTypeArg.Name, s.Method.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg));

             }

@@ -2905,7 +2899,7 @@ namespace Microsoft.Dafny
                         else

                         {

                             classFunction.OverriddenFunction = traitFunction;

-                            //adding a call graph edge from the trait method to that of class

+                            //adding a call graph edge from the trait function to that of class

                             cl.Module.CallGraph.AddEdge(traitFunction, classFunction);

 

                             //checking specifications

@@ -4587,7 +4581,6 @@ namespace Microsoft.Dafny
             Contract.Assert(s.rhss.Count > 0);

             // Create a hidden update statement using the out-parameter formals, resolve the RHS, and check that the RHS is good.

             List<Expression> formals = new List<Expression>();

-            int i = 0;

             foreach (Formal f in cmc.Outs) {

               Expression produceLhs;

               if (stmt is ReturnStmt) {

@@ -4603,14 +4596,6 @@ namespace Microsoft.Dafny
                 produceLhs = yieldIdent;

               }

               formals.Add(produceLhs);

-              // link the receiver parameter properly:

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

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

-                if (r.Arguments != null) {

-                  r.ReceiverArgumentForInitCall = produceLhs;

-                }

-              }

-              i++;

             }

             s.hiddenUpdate = new UpdateStmt(s.Tok, s.EndTok, formals, s.rhss, true);

             // resolving the update statement will check for return/yield statement specifics.

@@ -4659,18 +4644,6 @@ namespace Microsoft.Dafny
             lhs.Var = local;

             lhs.Type = local.Type;

           }

-          // there is one more place where a newly declared local may be lurking

-          if (upd.Rhss.Count == 1 && upd.Rhss[0] is TypeRhs) {

-            var rhs = (TypeRhs)upd.Rhss[0];

-            Contract.Assert(s.Locals.Count != 0);  // this is always true of a VarDeclStmt

-            var local = s.Locals[0];

-            if (rhs != null && rhs.ReceiverArgumentForInitCall != null) {

-              var lhs = (IdentifierExpr)rhs.ReceiverArgumentForInitCall;  // as above, we expect this to be an IdentifierExpr, because that's how the parser sets things up

-              Contract.Assert(lhs.Type == null || (upd.Lhss.Count == 1 && upd.Lhss[0] == lhs));  // if it's been resolved before, it's because it's aliased with a Lhss

-              lhs.Var = local;

-              lhs.Type = local.type;

-            }

-          }

           // resolve the whole thing

           ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext);

         }

@@ -5325,7 +5298,7 @@ namespace Microsoft.Dafny
       Contract.Requires(update != null);

       Contract.Requires(codeContext != null);

       IToken firstEffectfulRhs = null;

-      CallRhs callRhs = null;

+      MethodCallInformation methodCallInfo = null;

       foreach (var rhs in update.Rhss) {

         bool isEffectful;

         if (rhs is TypeRhs) {

@@ -5334,17 +5307,13 @@ namespace Microsoft.Dafny
           isEffectful = tr.InitCall != null;

         } else if (rhs is HavocRhs) {

           isEffectful = false;

-        } else if (rhs is CallRhs) {

-          // (a CallRhs is never parsed; we must have got here from an act of cloning)

-          isEffectful = true;

-          callRhs = callRhs ?? (CallRhs)rhs;

         } else {

           var er = (ExprRhs)rhs;

           if (er.Expr is ApplySuffix) {

             var a = (ApplySuffix)er.Expr;

             var cRhs = ResolveApplySuffix(a, new ResolveOpts(codeContext, true), true);

             isEffectful = cRhs != null;

-            callRhs = callRhs ?? cRhs;

+            methodCallInfo = methodCallInfo ?? cRhs;

           } else {

             ResolveExpression(er.Expr, new ResolveOpts(codeContext, true));

             isEffectful = false;

@@ -5375,8 +5344,8 @@ namespace Microsoft.Dafny
           Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");

         } else { // it might be ok, if it is a TypeRhs

           Contract.Assert(update.Rhss.Count == 1);

-          if (callRhs != null) {

-            Error(callRhs.Tok, "cannot have method call in return statement.");

+          if (methodCallInfo != null) {

+            Error(methodCallInfo.Tok, "cannot have method call in return statement.");

           } else {

             // we have a TypeRhs

             Contract.Assert(update.Rhss[0] is TypeRhs);

@@ -5395,7 +5364,7 @@ namespace Microsoft.Dafny
         // if there was an effectful RHS, that must be the only RHS

         if (update.Rhss.Count != 1) {

           Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");

-        } else if (callRhs == null) {

+        } else if (methodCallInfo == null) {

           // must be a single TypeRhs

           if (update.Lhss.Count != 1) {

             Contract.Assert(2 <= update.Lhss.Count);  // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)

@@ -5410,7 +5379,7 @@ namespace Microsoft.Dafny
           foreach (var ll in update.Lhss) {

             resolvedLhss.Add(ll.Resolved);

           }

-          var a = new CallStmt(callRhs.Tok, update.EndTok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);

+          var a = new CallStmt(methodCallInfo.Tok, update.EndTok, resolvedLhss, methodCallInfo.Callee, methodCallInfo.Args);

           update.ResolvedStatements.Add(a);

         }

       }

@@ -5509,30 +5478,14 @@ namespace Microsoft.Dafny
       Contract.Requires(codeContext != null);

       bool isInitCall = receiverType != null;

 

-      // resolve receiver

-      ResolveReceiver(s.Receiver, new ResolveOpts(codeContext, true));

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

-      if (receiverType == null) {

-        receiverType = s.Receiver.Type;

+      var callee = s.Method;

+      Contract.Assert(callee != null);  // follows from the invariant of CallStmt

+      if (!isInitCall && callee is Constructor) {

+        Error(s, "a constructor is allowed to be called only when an object is being allocated");

       }

-      // resolve the method name

-      NonProxyType nptype;

-      MemberDecl member = ResolveMember(s.Tok, receiverType, s.MethodName, out nptype);

-      Method callee = null;

-      if (member == null) {

-        // error has already been reported by ResolveMember

-      } else if (member is Method) {

-        s.Method = (Method)member;

-        callee = s.Method;

-        if (!isInitCall && callee is Constructor) {

-          Error(s, "a constructor is allowed to be called only when an object is being allocated");

-        }

-        s.IsGhost = callee.IsGhost;

-        if (specContextOnly && !callee.IsGhost) {

-          Error(s, "only ghost methods can be called from this context");

-        }

-      } else {

-        Error(s, "member {0} in type {1} does not refer to a method", s.MethodName, nptype);

+      s.IsGhost = callee.IsGhost;

+      if (specContextOnly && !callee.IsGhost) {

+        Error(s, "only ghost methods can be called from this context");

       }

 

       // resolve left-hand sides

@@ -5545,7 +5498,7 @@ namespace Microsoft.Dafny
       }

       int j = 0;

       foreach (Expression e in s.Args) {

-        bool allowGhost = s.IsGhost || callee == null || callee.Ins.Count <= j || callee.Ins[j].IsGhost;

+        bool allowGhost = s.IsGhost || callee.Ins.Count <= j || callee.Ins[j].IsGhost;

         var ec = ErrorCount;

         ResolveExpression(e, new ResolveOpts(codeContext, true));

         if (ec == ErrorCount && !allowGhost) {

@@ -5554,9 +5507,7 @@ namespace Microsoft.Dafny
         j++;

       }

 

-      if (callee == null) {

-        // error has been reported above

-      } else if (callee.Ins.Count != s.Args.Count) {

+      if (callee.Ins.Count != s.Args.Count) {

         Error(s, "wrong number of method arguments (got {0}, expected {1})", s.Args.Count, callee.Ins.Count);

       } else if (callee.Outs.Count != s.Lhs.Count) {

         if (isInitCall) {

@@ -5565,7 +5516,6 @@ namespace Microsoft.Dafny
           Error(s, "wrong number of method result arguments (got {0}, expected {1})", s.Lhs.Count, callee.Outs.Count);

         }

       } else {

-        Contract.Assert(nptype != null);  // follows from postcondition of ResolveMember above

         if (isInitCall) {

           if (callee.IsStatic) {

             Error(s.Tok, "a method called as an initialization method must not be 'static'");

@@ -5580,26 +5530,15 @@ namespace Microsoft.Dafny
             Error(s.Receiver, "call to instance method requires an instance");

           }

         }

-#if !NO_WORK_TO_BE_DONE

-        UserDefinedType ctype = (UserDefinedType)nptype;  // TODO: get rid of this statement, make this code handle any non-proxy type

-#endif

-        // build the type substitution map

-        s.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();

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

-          s.TypeArgumentSubstitutions.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);

-        }

-        foreach (TypeParameter p in callee.TypeArgs) {

-          s.TypeArgumentSubstitutions.Add(p, new ParamTypeProxy(p));

-        }

         // type check the arguments

         for (int i = 0; i < callee.Ins.Count; i++) {

-          Type st = SubstType(callee.Ins[i].Type, s.TypeArgumentSubstitutions);

+          Type st = SubstType(callee.Ins[i].Type, s.MethodSelect.TypeArgumentSubstitutions());

           if (!UnifyTypes(cce.NonNull(s.Args[i].Type), st)) {

             Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);

           }

         }

         for (int i = 0; i < callee.Outs.Count; i++) {

-          Type st = SubstType(callee.Outs[i].Type, s.TypeArgumentSubstitutions);

+          Type st = SubstType(callee.Outs[i].Type, s.MethodSelect.TypeArgumentSubstitutions());

           var lhs = s.Lhs[i];

           if (!UnifyTypes(cce.NonNull(lhs.Type), st)) {

             Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);

@@ -5650,7 +5589,7 @@ namespace Microsoft.Dafny
           }

         }

       }

-      if (callee != null && Contract.Exists(callee.Decreases.Expressions, e => e is WildcardExpr) && !codeContext.AllowsNontermination) {

+      if (Contract.Exists(callee.Decreases.Expressions, e => e is WildcardExpr) && !codeContext.AllowsNontermination) {

         Error(s.Tok, "a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating");

       }

     }

@@ -6038,10 +5977,25 @@ namespace Microsoft.Dafny
             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, stmt.EndTok, new List<Expression>(), rr.ReceiverArgumentForInitCall, rr.OptionalNameComponent, rr.Arguments);

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

-              if (rr.InitCall.Method is Constructor) {

-                callsConstructor = true;

+              var prevErrorCount = ErrorCount;

+

+              // We want to create a MemberSelectExpr for the initializing method.  To do that, we create a throw-away receiver of the appropriate

+              // type, create an dot-suffix expression around this receiver, and then resolve it in the usual way for dot-suffix expressions.

+              var lhs = new ImplicitThisExpr(initCallTok) { Type = rr.EType };

+              var callLhs = new ExprDotName(initCallTok, lhs, rr.OptionalNameComponent, null/*TODO: if the all-but-last components of the original EType above denote a type, then we should use any type arguments of the final EType component here*/);

+              ResolveDotSuffix(callLhs, true, rr.Arguments, new ResolveOpts(codeContext, true, specContextOnly), true);  // we use this call instead of the regular ResolveDotSuffix, since callLhs.Expr has already been resolved

+              if (prevErrorCount == ErrorCount) {

+                Contract.Assert(callLhs.ResolvedExpression is MemberSelectExpr);  // since ResolveApplySuffix succeeded and call.Lhs denotes an expression (not a module or a type)

+                var methodSel = (MemberSelectExpr)callLhs.ResolvedExpression;

+                if (methodSel.Member is Method) {

+                  rr.InitCall = new CallStmt(initCallTok, stmt.EndTok, new List<Expression>(), methodSel, rr.Arguments);

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

+                  if (rr.InitCall.Method is Constructor) {

+                    callsConstructor = true;

+                  }

+                } else {

+                  Error(initCallTok, "object initialization must denote an initializing method or constructor ({0})", rr.OptionalNameComponent);

+                }

               }

             } else {

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

@@ -6092,17 +6046,11 @@ namespace Microsoft.Dafny
       if (ctype != null) {

         var cd = (ClassDecl)ctype.ResolvedClass;  // correctness of cast follows from postcondition of DenotesClass

         Contract.Assert(ctype.TypeArgs.Count == cd.TypeArgs.Count);  // follows from the fact that ctype was resolved

-#if TWO_SEARCHES

-        MemberDecl member = cd.Members.Find(md => md.Name == memberName);

-        if (member == null &&

-          (!classMembers.ContainsKey(cd) || !classMembers[cd].TryGetValue(memberName, out member))) {

-#else

         MemberDecl member;

         if (!classMembers[cd].TryGetValue(memberName, out member)) {

-#endif

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

           if (memberName == "_ctor") {

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

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

           } else {

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

           }

@@ -6148,7 +6096,7 @@ namespace Microsoft.Dafny
     }

 

     /// <summary>

-    /// Returns a resolved MemberSelectExpr.

+    /// Returns a resolved MemberSelectExpr for a field.

     /// </summary>

     public static MemberSelectExpr NewMemberSelectExpr(IToken tok, Expression obj, Field field, Dictionary<TypeParameter, Type> typeSubstMap) {

       Contract.Requires(tok != null);

@@ -6534,7 +6482,7 @@ namespace Microsoft.Dafny
             e.TypeApplication.Add(prox);

           }

           e.Type = new ArrowType(fn.tok, fn.Formals.ConvertAll(f => SubstType(f.Type, subst)), SubstType(fn.ResultType, subst), builtIns.SystemModule);

-          AddCallGraphEdge(e, opts.codeContext, fn);

+          AddCallGraphEdge(opts.codeContext, fn, e);

         } else if (member is Field) {

           var field = (Field)member;

           e.Member = field;

@@ -6678,8 +6626,8 @@ namespace Microsoft.Dafny
         }

 

       } else if (expr is FunctionCallExpr) {

-        FunctionCallExpr e = (FunctionCallExpr)expr;

-        ResolveFunctionCallExpr(e, opts, false);

+        var e = (FunctionCallExpr)expr;

+        ResolveFunctionCallExpr(e, opts);

 

       } else if (expr is ApplyExpr) {

         var e = (ApplyExpr)expr;

@@ -7712,24 +7660,60 @@ namespace Microsoft.Dafny
           subst.Add(fn.TypeArgs[i], ta);

         }

         rr.Type = new ArrowType(fn.tok, fn.Formals.ConvertAll(f => SubstType(f.Type, subst)), SubstType(fn.ResultType, subst), builtIns.SystemModule);

-        AddCallGraphEdge(rr, caller, fn);

+        AddCallGraphEdge(caller, fn, rr);

       } else {

         // the member is a method

-        Contract.Assert(member is Method);

+        var m = (Method)member;

         if (!allowMethodCall) {

           // it's a method and method calls are not allowed in the given context

           Error(tok, "expression is not allowed to invoke a method ({0})", member.Name);

         }

+        int suppliedTypeArguments = optTypeArguments == null ? 0 : optTypeArguments.Count;

+        if (optTypeArguments != null && suppliedTypeArguments != m.TypeArgs.Count) {

+          Error(tok, "method '{0}' expects {1} type arguments (got {2})", member.Name, m.TypeArgs.Count, suppliedTypeArguments);

+        }

+        rr.TypeApplication = new List<Type>();

+        if (udt != null && udt.ResolvedClass != null) {

+          rr.TypeApplication.AddRange(udt.TypeArgs);

+        }

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

+          var ta = i < suppliedTypeArguments ? optTypeArguments[i] : new InferredTypeProxy();

+          rr.TypeApplication.Add(ta);

+        }

         rr.Type = new InferredTypeProxy();  // fill in this field, in order to make "rr" resolved

       }

       return rr;

     }

 

+    class MethodCallInformation

+    {

+      public readonly IToken Tok;

+      public readonly MemberSelectExpr Callee;

+      public readonly List<Expression> Args;

+

+      [ContractInvariantMethod]

+      void ObjectInvariant() {

+        Contract.Invariant(Tok != null);

+        Contract.Invariant(Callee != null);

+        Contract.Invariant(Callee.Member is Method);

+        Contract.Invariant(cce.NonNullElements(Args));

+      }

+

+      public MethodCallInformation(IToken tok, MemberSelectExpr callee, List<Expression> args) {

+        Contract.Requires(tok != null);

+        Contract.Requires(callee != null);

+        Contract.Requires(callee.Member is Method);

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

+        this.Tok = tok;

+        this.Callee = callee;

+        this.Args = args;

+      }

+    }

 

-    CallRhs ResolveApplySuffix(ApplySuffix e, ResolveOpts opts, bool allowMethodCall) {

+    MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolveOpts opts, bool allowMethodCall) {

       Contract.Requires(e != null);

       Contract.Requires(opts != null);

-      Contract.Ensures(Contract.Result<CallRhs>() == null || allowMethodCall);

+      Contract.Ensures(Contract.Result<MethodCallInformation>() == null || allowMethodCall);

       Expression r = null;  // upon success, the expression to which the ApplySuffix resolves

       var errorCount = ErrorCount;

       if (e.Lhs is NameSegment) {

@@ -7774,13 +7758,11 @@ namespace Microsoft.Dafny
           } else {

             if (lhs is MemberSelectExpr && ((MemberSelectExpr)lhs).Member is Method) {

               var mse = (MemberSelectExpr)lhs;

-              var method = (Method)mse.Member;

               if (allowMethodCall) {

-                var cRhs = new CallRhs(e.tok, mse.Obj, method.Name, e.Args);

-                cRhs.Method = method;

+                var cRhs = new MethodCallInformation(e.tok, mse, e.Args);

                 return cRhs;

               } else {

-                Error(e.tok, "method call is not allowed to be used in an expression context ({0})", method.Name);

+                Error(e.tok, "method call is not allowed to be used in an expression context ({0})", mse.Member.Name);

               }

             } else if (lhs != null) {  // if e.Lhs.Resolved is null, then e.Lhs was not successfully resolved and an error has already been reported

               Error(e.tok, "non-function expression (of type {0}) is called with parameters", e.Lhs.Type);

@@ -7802,8 +7784,37 @@ namespace Microsoft.Dafny
               // no nothing else; error has been reported

             } else if (callee != null) {

               // produce a FunctionCallExpr instead of an ApplyExpr(MemberSelectExpr)

-              r = new FunctionCallExpr(e.Lhs.tok, callee.Name, mse.Obj, e.tok, e.Args);

-              ResolveExpression(r, opts);

+              var rr = new FunctionCallExpr(e.Lhs.tok, callee.Name, mse.Obj, e.tok, e.Args);

+              // resolve it here:

+              rr.Function = callee;

+              Contract.Assert(!(mse.Obj is StaticReceiverExpr) || callee.IsStatic);  // this should have been checked already

+              Contract.Assert(callee.Formals.Count == rr.Args.Count);  // this should have been checked already

+              // build the type substitution map

+              rr.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();

+              Contract.Assert(mse.TypeApplication.Count == callee.EnclosingClass.TypeArgs.Count + callee.TypeArgs.Count);

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

+                rr.TypeArgumentSubstitutions.Add(callee.EnclosingClass.TypeArgs[i], mse.TypeApplication[i]);

+              }

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

+                rr.TypeArgumentSubstitutions.Add(callee.TypeArgs[i], mse.TypeApplication[callee.EnclosingClass.TypeArgs.Count + i]);

+              }

+              // type check the arguments

+              for (int i = 0; i < callee.Formals.Count; i++) {

+                Expression farg = rr.Args[i];

+                ResolveExpression(farg, opts);

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

+                Type s = SubstType(callee.Formals[i].Type, rr.TypeArgumentSubstitutions);

+                if (!UnifyTypes(farg.Type, s)) {

+                  Error(rr, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);

+                }

+              }

+              rr.Type = SubstType(callee.ResultType, rr.TypeArgumentSubstitutions);

+              // further bookkeeping

+              if (callee is CoPredicate) {

+                ((CoPredicate)callee).Uses.Add(rr);

+              }

+              AddCallGraphEdge(opts.codeContext, callee, rr);

+              r = rr;

             } else {

               r = new ApplyExpr(e.Lhs.tok, e.Lhs, e.Args);

               r.Type = fnType.Result;

@@ -8053,12 +8064,7 @@ namespace Microsoft.Dafny
       }

     }

 

-    /// <summary>

-    /// If "!allowMethodCall" or if what is being called does not refer to a method, resolves "e" and returns "null".

-    /// Otherwise (that is, if "allowMethodCall" and what is being called refers to a method), resolves the receiver

-    /// of "e" but NOT the arguments, and returns a CallRhs corresponding to the call.

-    /// </summary>

-    public CallRhs ResolveFunctionCallExpr(FunctionCallExpr e, ResolveOpts opts, bool allowMethodCall) {

+    public void ResolveFunctionCallExpr(FunctionCallExpr e, ResolveOpts opts) {

       ResolveReceiver(e.Receiver, opts);

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

       NonProxyType nptype;

@@ -8070,12 +8076,7 @@ namespace Microsoft.Dafny
       if (member == null) {

         // error has already been reported by ResolveMember

       } else if (member is Method) {

-        if (allowMethodCall) {

-          // it's a method

-          return new CallRhs(e.tok, e.Receiver, e.Name, e.Args);

-        } else {

-          Error(e, "member {0} in type {1} refers to a method, but only functions can be used in this context", e.Name, cce.NonNull(ctype).Name);

-        }

+        Error(e, "member {0} in type {1} refers to a method, but only functions can be used in this context", e.Name, cce.NonNull(ctype).Name);

       } else if (!(member is Function)) {

         Error(e, "member {0} in type {1} does not refer to a function", e.Name, cce.NonNull(ctype).Name);

       } else {

@@ -8126,22 +8127,24 @@ namespace Microsoft.Dafny
           e.Type = SubstType(function.ResultType, e.TypeArgumentSubstitutions);

         }

 

-        AddCallGraphEdge(e, opts.codeContext, function);

+        AddCallGraphEdge(opts.codeContext, function, e);

       }

-      return null;

     }

 

-    private static void AddCallGraphEdge(Expression e, ICodeContext codeContext, Function function) {

+    private static void AddCallGraphEdge(ICodeContext callingContext, Function function, Expression e) {

+      Contract.Requires(callingContext != null);

+      Contract.Requires(function != null);

+      Contract.Requires(e != null);

       // Resolution termination check

-      ModuleDefinition callerModule = codeContext.EnclosingModule;

+      ModuleDefinition callerModule = callingContext.EnclosingModule;

       ModuleDefinition calleeModule = function.EnclosingClass.Module;

       if (callerModule == calleeModule) {

         // intra-module call; add edge in module's call graph

-        var caller = codeContext as ICallable;

+        var caller = callingContext as ICallable;

         if (caller == null) {

           // don't add anything to the call graph after all

         } else if (caller is IteratorDecl) {

-          callerModule.CallGraph.AddEdge(((IteratorDecl)codeContext).Member_MoveNext, function);

+          callerModule.CallGraph.AddEdge(((IteratorDecl)callingContext).Member_MoveNext, function);

         } else {

           callerModule.CallGraph.AddEdge(caller, function);

           if (caller is Function) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e836eca1..3decb1f8 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2728,8 +2728,13 @@ namespace Microsoft.Dafny {
                 recursiveCallArgs.Add(ie);

               }

             }

-            var recursiveCall = new CallStmt(m.tok, m.tok, new List<Expression>(), recursiveCallReceiver, m.Name, recursiveCallArgs);

-            recursiveCall.Method = m;  // resolve here

+            var methodSel = new MemberSelectExpr(m.tok, recursiveCallReceiver, m.Name);

+            methodSel.Member = m;  // resolve here

+            methodSel.TypeApplication = new List<Type>();

+            methodSel.TypeApplication.AddRange(recursiveCallReceiver.Type.TypeArgs);

+            m.TypeArgs.ForEach(tp => methodSel.TypeApplication.Add(new UserDefinedType(tp)));

+            methodSel.Type = new InferredTypeProxy();  // this is the last step in resolving 'methodSel'

+            var recursiveCall = new CallStmt(m.tok, m.tok, new List<Expression>(), methodSel, recursiveCallArgs);

             recursiveCall.IsGhost = m.IsGhost;  // resolve here

 

             Expression parRange = new LiteralExpr(m.tok, true);

@@ -7990,14 +7995,14 @@ namespace Microsoft.Dafny {
         var argsSubstMap = new Dictionary<IVariable, Expression>();  // maps formal arguments to actuals

         Contract.Assert(s0.Method.Ins.Count == s0.Args.Count);

         for (int i = 0; i < s0.Method.Ins.Count; i++) {

-          var arg = Substitute(s0.Args[i], null, substMap, s0.TypeArgumentSubstitutions);  // substitute the renamed bound variables for the declared ones

+          var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutions());  // substitute the renamed bound variables for the declared ones

           argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type));

         }

-        var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.TypeArgumentSubstitutions)), s0.Receiver.Type);

+        var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutions())), s0.Receiver.Type);

         var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap);

         Bpl.Expr post = Bpl.Expr.True;

         foreach (var ens in s0.Method.Ens) {

-          var p = Substitute(ens.E, receiver, argsSubstMap, s0.TypeArgumentSubstitutions);  // substitute the call's actuals for the method's formals

+          var p = Substitute(ens.E, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutions());  // substitute the call's actuals for the method's formals

           post = BplAnd(post, callEtran.TrExpr(p));

         }

 

@@ -8393,7 +8398,7 @@ namespace Microsoft.Dafny {
         builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, initHeap, etran.HeapExpr));

       }

       builder.Add(new CommentCmd("TrCallStmt: Before ProcessCallStmt"));

-      ProcessCallStmt(s.Tok, s.TypeArgumentSubstitutions, GetTypeParams(s.Method), s.Receiver, actualReceiver, s.Method, s.Args, bLhss, lhsTypes, builder, locals, etran);

+      ProcessCallStmt(s.Tok, s.MethodSelect.TypeArgumentSubstitutions(), GetTypeParams(s.Method), s.Receiver, actualReceiver, s.Method, s.Args, bLhss, lhsTypes, builder, locals, etran);

       builder.Add(new CommentCmd("TrCallStmt: After ProcessCallStmt"));

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

         var lhs = s.Lhs[i];

@@ -9482,7 +9487,6 @@ namespace Microsoft.Dafny {
                                        Bpl.StmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {

       Contract.Requires(tok != null);

       Contract.Requires(rhs != null);

-      Contract.Requires(!(rhs is CallRhs));  // calls are handled in a different translation method

       Contract.Requires(builder != null);

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

       Contract.Requires(etran != null);

@@ -13466,12 +13470,7 @@ namespace Microsoft.Dafny {
           r = new AssignStmt(s.Tok, s.EndTok, Substitute(s.Lhs), SubstRHS(s.Rhs));

         } else if (stmt is CallStmt) {

           var s = (CallStmt)stmt;

-          var rr = new CallStmt(s.Tok, s.EndTok, s.Lhs.ConvertAll(Substitute), Substitute(s.Receiver), s.MethodName, s.Args.ConvertAll(Substitute));

-          rr.Method = s.Method;

-          rr.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();

-          foreach (var p in s.TypeArgumentSubstitutions) {

-            rr.TypeArgumentSubstitutions[p.Key] = Resolver.SubstType(p.Value, typeMap);

-          }

+          var rr = new CallStmt(s.Tok, s.EndTok, s.Lhs.ConvertAll(Substitute), (MemberSelectExpr)Substitute(s.MethodSelect), s.Args.ConvertAll(Substitute));

           r = rr;

         } else if (stmt is BlockStmt) {

           r = SubstBlockStmt((BlockStmt)stmt);

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 55a4b1e6..f1c5532e 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -14,7 +14,6 @@ ResolutionErrors.dfy(594,14): Error: new allocation not allowed in ghost context
 ResolutionErrors.dfy(604,23): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(611,15): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(611,15): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(611,10): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(620,17): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(622,29): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(624,17): Error: calls to methods with side-effects are not allowed inside a hint

@@ -116,7 +115,7 @@ ResolutionErrors.dfy(412,10): Error: a hint is not allowed to update a variable
 ResolutionErrors.dfy(438,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called

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

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

-ResolutionErrors.dfy(446,9): Error: class Lamb does not have a anonymous constructor

+ResolutionErrors.dfy(446,9): Error: class Lamb does not have an anonymous constructor

 ResolutionErrors.dfy(844,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)

 ResolutionErrors.dfy(848,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

 ResolutionErrors.dfy(851,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

@@ -182,4 +181,4 @@ ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-184 resolution/type errors detected in ResolutionErrors.dfy

+183 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect
index 0a15ad67..e40f2c35 100644
--- a/Test/dafny0/TypeTests.dfy.expect
+++ b/Test/dafny0/TypeTests.dfy.expect
@@ -18,7 +18,7 @@ TypeTests.dfy(72,28): Error: unresolved identifier: z
 TypeTests.dfy(73,29): Error: unresolved identifier: w1

 TypeTests.dfy(73,47): Error: unresolved identifier: w0

 TypeTests.dfy(76,28): Error: unresolved identifier: e

-TypeTests.dfy(91,17): Error: member F in type C does not refer to a method

+TypeTests.dfy(91,17): Error: object initialization must denote an initializing method or constructor (F)

 TypeTests.dfy(92,17): Error: a method called as an initialization method must not have any result arguments

 TypeTests.dfy(101,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

 TypeTests.dfy(102,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

diff --git a/Test/dafny0/UserSpecifiedTypeParameters.dfy b/Test/dafny0/UserSpecifiedTypeParameters.dfy
index 52bff60e..bf059d88 100644
--- a/Test/dafny0/UserSpecifiedTypeParameters.dfy
+++ b/Test/dafny0/UserSpecifiedTypeParameters.dfy
@@ -60,3 +60,41 @@ module M1 {
     }

   }

 }

+

+module M2 {

+  class ClassA {

+    function F<A>(a: A): int

+

+    lemma Lem<Y>() returns (y: Y)

+

+    lemma M<X>(x: X)

+    {

+      var k := Lem<int>();

+    }

+  }

+  class ClassB {

+    lemma LemmaX<A>(y: A)

+    lemma LemmaY<A>(x: int)

+    {

+      LemmaX<A>(x);  // error: The given type instantiation A does not agree with the type of parameter x

+    }

+

+    lemma LemmaR<T>(x: int)

+    lemma LemmaS<A>()

+    {

+      LemmaR<A>(5);

+    }

+

+    function FuncX<A>(y: A): real

+    function FuncY<A>(x: int): real

+    {

+      FuncX<A>(x)  // error: The given type instantiation A does not agree with the type of parameter x

+    }

+

+    function FuncR<T>(x: int): real

+    function FuncS<A>(): real

+    {

+      FuncR<A>(5)

+    }

+  }

+}

diff --git a/Test/dafny0/UserSpecifiedTypeParameters.dfy.expect b/Test/dafny0/UserSpecifiedTypeParameters.dfy.expect
index 12970e85..2504fbfb 100644
--- a/Test/dafny0/UserSpecifiedTypeParameters.dfy.expect
+++ b/Test/dafny0/UserSpecifiedTypeParameters.dfy.expect
@@ -6,4 +6,6 @@ UserSpecifiedTypeParameters.dfy(48,26): Error: Undeclared top-level type or type
 UserSpecifiedTypeParameters.dfy(48,18): Error: variable 'a' does not take any type parameters

 UserSpecifiedTypeParameters.dfy(48,30): Error: non-function expression (of type int) is called with parameters

 UserSpecifiedTypeParameters.dfy(48,16): Error: wrong number of arguments to function application (function 'F' expects 2, got 1)

-8 resolution/type errors detected in UserSpecifiedTypeParameters.dfy

+UserSpecifiedTypeParameters.dfy(79,15): Error: incorrect type of method in-parameter 0 (expected A, got int)

+UserSpecifiedTypeParameters.dfy(91,15): Error: type mismatch for argument 0 (function expects A, got int)

+10 resolution/type errors detected in UserSpecifiedTypeParameters.dfy