Refactor: Change ApplyExpr's Receiver to Function

6 files changed, 18 insertions, 18 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 0f21d50c..f4315041 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -307,7 +307,7 @@ namespace Microsoft.Dafny
 

       } else if (expr is ApplyExpr) {

         var e = (ApplyExpr)expr;

-        return new ApplyExpr(Tok(e.tok), Tok(e.OpenParen), CloneExpr(e.Receiver), e.Args.ConvertAll(CloneExpr));

+        return new ApplyExpr(Tok(e.tok), Tok(e.OpenParen), CloneExpr(e.Function), e.Args.ConvertAll(CloneExpr));

 

       } else if (expr is OldExpr) {

         var e = (OldExpr)expr;

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 4c930724..0ea3d4a3 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -2186,9 +2186,9 @@ namespace Microsoft.Dafny {
       } else if (expr is ApplyExpr) {

         var e = expr as ApplyExpr;

         wr.Write("Dafny.Helpers.Id<");

-        wr.Write(TypeName(e.Receiver.Type));

+        wr.Write(TypeName(e.Function.Type));

         wr.Write(">(");

-        TrExpr(e.Receiver);

+        TrExpr(e.Function);

         wr.Write(")");

         TrExprList(e.Args);

 

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 67e8a364..b5a806ec 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -5180,13 +5180,13 @@ namespace Microsoft.Dafny {
     // The idea is that this apply expression does not need a type argument substitution,

     // since lambda functions and anonymous functions are never polymorphic.

     // Make a FunctionCallExpr otherwise, to call a resolvable anonymous function.

-    public readonly Expression Receiver;

+    public readonly Expression Function;

     public readonly List<Expression> Args;

     public readonly IToken OpenParen;

 

     public override IEnumerable<Expression> SubExpressions {

       get {

-        yield return Receiver;

+        yield return Function;

         foreach (var e in Args) {

           yield return e;

         }

@@ -5197,7 +5197,7 @@ namespace Microsoft.Dafny {
       : base(tok)

     {

       OpenParen = openParen;

-      Receiver = receiver;

+      Function = receiver;

       Args = args;

     }

   }

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 349c954a..bfbc9644 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1357,7 +1357,7 @@ namespace Microsoft.Dafny {
 

         if (parensNeeded) { wr.Write("("); }

 

-        PrintExpr(e.Receiver, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);

+        PrintExpr(e.Function, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);

         wr.Write("(");

         PrintExpressionList(e.Args, false);

         wr.Write(")");

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 568fe224..0e1e1010 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -6461,16 +6461,16 @@ namespace Microsoft.Dafny
 

       } else if (expr is ApplyExpr) {

         ApplyExpr e = (ApplyExpr)expr;

-        ResolveExpression(e.Receiver, twoState, codeContext);

+        ResolveExpression(e.Function, twoState, codeContext);

         foreach (var arg in e.Args) {

           ResolveExpression(arg, twoState, codeContext);

         }

         Type tb = new InferredTypeProxy();

         var targs = e.Args.ConvertAll(arg => arg.Type);

         Type tc = new ArrowType(targs, tb);

-        if (!UnifyTypes(e.Receiver.Type, tc)) {

+        if (!UnifyTypes(e.Function.Type, tc)) {

           Error(e.OpenParen, "cannot apply arguments with types {0} to expression with type {1}", 

-            Util.Comma(targs, x => x.ToString()), e.Receiver.Type, ", ");

+            Util.Comma(targs, x => x.ToString()), e.Function.Type, ", ");

         }

         expr.Type = tb;

 

@@ -8531,7 +8531,7 @@ namespace Microsoft.Dafny
         return e.Args.Exists(arg => UsesSpecFeatures(arg));

       } else if (expr is ApplyExpr) {

         ApplyExpr e = (ApplyExpr)expr;

-        return UsesSpecFeatures(e.Receiver) || e.Args.Exists(UsesSpecFeatures);

+        return UsesSpecFeatures(e.Function) || e.Args.Exists(UsesSpecFeatures);

       } else if (expr is OldExpr) {

         OldExpr e = (OldExpr)expr;

         return UsesSpecFeatures(e.E);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index c214fe90..6f3e7ecb 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3952,7 +3952,7 @@ namespace Microsoft.Dafny {
       } else if (expr is ApplyExpr) {

         ApplyExpr e = (ApplyExpr)expr;

         return BplAnd(

-          Cons(CanCallAssumption(e.Receiver, etran), 

+          Cons(CanCallAssumption(e.Function, etran), 

           e.Args.ConvertAll(ee => CanCallAssumption(ee, etran))));

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

@@ -4408,12 +4408,12 @@ namespace Microsoft.Dafny {
       } else if (expr is ApplyExpr) {

         var e = (ApplyExpr)expr;

         int arity = e.Args.Count;

-        var tt = e.Receiver.Type as ArrowType;

+        var tt = e.Function.Type as ArrowType;

         Contract.Assert(tt != null);

         Contract.Assert(tt.Arity == arity);

 

         // check WF of receiver and arguments

-        CheckWellformed(e.Receiver, options, locals, builder, etran);

+        CheckWellformed(e.Function, options, locals, builder, etran);

         foreach (Expression arg in e.Args) {

           CheckWellformed(arg, options, locals, builder, etran);

         }

@@ -4446,7 +4446,7 @@ namespace Microsoft.Dafny {
 

         var args = Concat(

           Map(tt.TypeArgs, TypeToTy),

-          Cons(etran.TrExpr(e.Receiver), 

+          Cons(etran.TrExpr(e.Function), 

           Cons(etran.HeapExpr, 

           e.Args.ConvertAll(arg => TrArg(arg)))));

 

@@ -10078,7 +10078,7 @@ namespace Microsoft.Dafny {
         } else if (expr is ApplyExpr) {

           ApplyExpr e = (ApplyExpr)expr;

           int arity = e.Args.Count;

-          var tt = e.Receiver.Type as ArrowType;

+          var tt = e.Function.Type as ArrowType;

           Contract.Assert(tt != null);

           Contract.Assert(tt.Arity == arity);

 

@@ -10086,7 +10086,7 @@ namespace Microsoft.Dafny {
 

           var applied = translator.FunctionCall(expr.tok, translator.Apply(arity), predef.BoxType, 

             Concat(Map(tt.TypeArgs,translator.TypeToTy),

-            Cons(TrExpr(e.Receiver), Cons(HeapExpr, e.Args.ConvertAll(arg => TrArg(arg))))));

+            Cons(TrExpr(e.Function), Cons(HeapExpr, e.Args.ConvertAll(arg => TrArg(arg))))));

 

           return translator.UnboxIfBoxed(applied, tt.Result);

 

@@ -12533,7 +12533,7 @@ namespace Microsoft.Dafny {
 

         } else if (expr is ApplyExpr) {

           ApplyExpr e = (ApplyExpr)expr;

-          Expression receiver = Substitute(e.Receiver);

+          Expression receiver = Substitute(e.Function);

           List<Expression> args = SubstituteExprList(e.Args);

           newExpr = new ApplyExpr(e.tok, e.OpenParen, receiver, args);