Dafny: finished refinement cloning transformations

1 files changed, 75 insertions, 302 deletions

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 8b46c897..a25d1eb8 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -235,8 +235,9 @@ namespace Microsoft.Dafny {
     }

 

     Expression CloneExpr(Expression expr) {

-#if SOON

-      if (expr is LiteralExpr) {

+      if (expr == null) {

+        return null;

+      } else if (expr is LiteralExpr) {

         var e = (LiteralExpr)expr;

         if (e.Value == null) {

           return new LiteralExpr(Tok(e.tok));

@@ -247,360 +248,131 @@ namespace Microsoft.Dafny {
         }

 

       } else if (expr is ThisExpr) {

-        wr.Write("this");

+        if (expr is ImplicitThisExpr) {

+          return new ImplicitThisExpr(Tok(expr.tok));

+        } else {

+          return new ThisExpr(Tok(expr.tok));

+        }

 

       } else if (expr is IdentifierExpr) {

-        wr.Write(((IdentifierExpr)expr).Name);

+        var e = (IdentifierExpr)expr;

+        return new IdentifierExpr(Tok(e.tok), e.Name);

 

       } else if (expr is DatatypeValue) {

-        DatatypeValue dtv = (DatatypeValue)expr;

-        wr.Write("#{0}.{1}", dtv.DatatypeName, dtv.MemberName);

-        if (dtv.Arguments.Count != 0) {

-          wr.Write("(");

-          PrintExpressionList(dtv.Arguments);

-          wr.Write(")");

-        }

+        var e = (DatatypeValue)expr;

+        return new DatatypeValue(Tok(e.tok), e.DatatypeName, e.MemberName, e.Arguments.ConvertAll(CloneExpr));

 

       } else if (expr is DisplayExpression) {

         DisplayExpression e = (DisplayExpression)expr;

-        if (e is MultiSetDisplayExpr) wr.Write("multiset");

-        wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "{" : "[");

-        PrintExpressionList(e.Elements);

-        wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "}" : "]");

+        if (expr is SetDisplayExpr) {

+          return new SetDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr));

+        } else if (expr is MultiSetDisplayExpr) {

+          return new MultiSetDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr));

+        } else {

+          Contract.Assert(expr is SeqDisplayExpr);

+          return new SeqDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr));

+        }

 

       } else if (expr is FieldSelectExpr) {

-        FieldSelectExpr e = (FieldSelectExpr)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x70;

-        bool parensNeeded = !(e.Obj is ImplicitThisExpr) &&

-          opBindingStrength < contextBindingStrength ||

-          (fragileContext && opBindingStrength == contextBindingStrength);

-

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

-        if (!(e.Obj is ImplicitThisExpr)) {

-          PrintExpr(e.Obj, opBindingStrength, false, false, -1);

-          wr.Write(".");

-        }

-        wr.Write(e.FieldName);

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

+        var e = (FieldSelectExpr)expr;

+        return new FieldSelectExpr(Tok(e.tok), CloneExpr(e.Obj), e.FieldName);

 

       } else if (expr is SeqSelectExpr) {

-        SeqSelectExpr e = (SeqSelectExpr)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x70;

-        bool parensNeeded = opBindingStrength < contextBindingStrength ||

-          (fragileContext && opBindingStrength == contextBindingStrength);

-

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

-        PrintExpr(e.Seq, 0x00, false, false, indent);  // BOGUS: fix me

-        wr.Write("[");

-        if (e.SelectOne) {

-          Contract.Assert( e.E0 != null);

-          PrintExpression(e.E0);

-        } else {

-          if (e.E0 != null) {

-            PrintExpression(e.E0);

-          }

-          wr.Write(e.E0 != null && e.E1 != null ? " .. " : "..");

-          if (e.E1 != null) {

-            PrintExpression(e.E1);

-          }

-        }

-        wr.Write("]");

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

+        var e = (SeqSelectExpr)expr;

+        return new SeqSelectExpr(Tok(e.tok), e.SelectOne, CloneExpr(e.Seq), CloneExpr(e.E0), CloneExpr(e.E1));

 

       } else if (expr is MultiSelectExpr) {

-        MultiSelectExpr e = (MultiSelectExpr)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x70;

-        bool parensNeeded = opBindingStrength < contextBindingStrength ||

-          (fragileContext && opBindingStrength == contextBindingStrength);

-

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

-        PrintExpr(e.Array, 0x00, false, false, indent);  // BOGUS: fix me

-        string prefix = "[";

-        foreach (Expression idx in e.Indices) {

-          Contract.Assert(idx != null);

-          wr.Write(prefix);

-          PrintExpression(idx);

-          prefix = ", ";

-        }

-        wr.Write("]");

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

+        var e = (MultiSelectExpr)expr;

+        return new MultiSelectExpr(Tok(e.tok), CloneExpr(e.Array), e.Indices.ConvertAll(CloneExpr));

 

       } else if (expr is SeqUpdateExpr) {

-        SeqUpdateExpr e = (SeqUpdateExpr)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x70;

-        bool parensNeeded = opBindingStrength < contextBindingStrength ||

-          (fragileContext && opBindingStrength == contextBindingStrength);

-

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

-        PrintExpr(e.Seq, 00, false, false, indent);  // BOGUS: fix me

-        wr.Write("[");

-        PrintExpression(e.Index);

-        wr.Write(" := ");

-        PrintExpression(e.Value);

-        wr.Write("]");

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

+        var e = (SeqUpdateExpr)expr;

+        return new SeqUpdateExpr(Tok(e.tok), CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value));

 

       } else if (expr is FunctionCallExpr) {

-        FunctionCallExpr e = (FunctionCallExpr)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x70;

-        bool parensNeeded = !(e.Receiver is ImplicitThisExpr) &&

-          opBindingStrength < contextBindingStrength ||

-          (fragileContext && opBindingStrength == contextBindingStrength);

-

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

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

-          PrintExpr(e.Receiver, opBindingStrength, false, false, -1);

-          wr.Write(".");

-        }

-        wr.Write(e.Name);

-        wr.Write("(");

-        PrintExpressionList(e.Args);

-        wr.Write(")");

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

+        var e = (FunctionCallExpr)expr;

+        return new FunctionCallExpr(Tok(e.tok), e.Name, CloneExpr(e.Receiver), e.Args.ConvertAll(CloneExpr));

 

       } else if (expr is OldExpr) {

-        wr.Write("old(");

-        PrintExpression(((OldExpr)expr).E);

-        wr.Write(")");

+        var e = (OldExpr)expr;

+        return new OldExpr(Tok(e.tok), CloneExpr(e.E));

 

       } else if (expr is MultiSetFormingExpr) {

-        wr.Write("multiset(");

-        PrintExpression(((MultiSetFormingExpr)expr).E);

-        wr.Write(")");

+        var e = (MultiSetFormingExpr)expr;

+        return new MultiSetFormingExpr(Tok(e.tok), CloneExpr(e.E));

 

       } else if (expr is FreshExpr) {

-        wr.Write("fresh(");

-        PrintExpression(((FreshExpr)expr).E);

-        wr.Write(")");

+        var e = (FreshExpr)expr;

+        return new FreshExpr(Tok(e.tok), CloneExpr(e.E));

 

       } else if (expr is AllocatedExpr) {

-        wr.Write("allocated(");

-        PrintExpression(((AllocatedExpr)expr).E);

-        wr.Write(")");

+        var e = (AllocatedExpr)expr;

+        return new AllocatedExpr(Tok(e.tok), CloneExpr(e.E));

 

       } else if (expr is UnaryExpr) {

-        UnaryExpr e = (UnaryExpr)expr;

-        if (e.Op == UnaryExpr.Opcode.SeqLength) {

-          wr.Write("|");

-          PrintExpression(e.E);

-          wr.Write("|");

-        } else {

-          // Prefix operator.

-          // determine if parens are needed

-          string op;

-          int opBindingStrength;

-          switch (e.Op) {

-            case UnaryExpr.Opcode.SetChoose:

-              op = "choose ";  opBindingStrength = 0;  break;

-            case UnaryExpr.Opcode.Not:

-              op = "!";  opBindingStrength = 0x60;  break;

-            default:

-              Contract.Assert(false); throw new cce.UnreachableException();  // unexpected unary opcode

-          }

-          bool parensNeeded = opBindingStrength < contextBindingStrength ||

-            (fragileContext && opBindingStrength == contextBindingStrength);

-

-          bool containsNestedNot = e.E is ParensExpression &&

-                                ((ParensExpression)e.E).E is UnaryExpr &&

-                                ((UnaryExpr)((ParensExpression)e.E).E).Op == UnaryExpr.Opcode.Not;

-

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

-          wr.Write(op);

-          PrintExpr(e.E, opBindingStrength, containsNestedNot, parensNeeded || isRightmost, -1);

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

-        }

+        var e = (UnaryExpr)expr;

+        return new UnaryExpr(Tok(e.tok), e.Op, CloneExpr(e.E));

 

       } else if (expr is BinaryExpr) {

-        BinaryExpr e = (BinaryExpr)expr;

-        // determine if parens are needed

-        int opBindingStrength;

-        bool fragileLeftContext = false;  // false means "allow same binding power on left without parens"

-        bool fragileRightContext = false;  // false means "allow same binding power on right without parens"

-        switch (e.Op)

-        {

-          case BinaryExpr.Opcode.Add:

-            opBindingStrength = 0x40; break;

-          case BinaryExpr.Opcode.Sub:

-            opBindingStrength = 0x40; fragileRightContext = true; break;

-          case BinaryExpr.Opcode.Mul:

-            opBindingStrength = 0x50; break;

-          case BinaryExpr.Opcode.Div:

-          case BinaryExpr.Opcode.Mod:

-            opBindingStrength = 0x50; fragileRightContext = true; break;

-          case BinaryExpr.Opcode.Eq:

-          case BinaryExpr.Opcode.Neq:

-          case BinaryExpr.Opcode.Gt:

-          case BinaryExpr.Opcode.Ge:

-          case BinaryExpr.Opcode.Lt:

-          case BinaryExpr.Opcode.Le:

-          case BinaryExpr.Opcode.Disjoint:

-          case BinaryExpr.Opcode.In:

-          case BinaryExpr.Opcode.NotIn:

-            opBindingStrength = 0x30; fragileLeftContext = fragileRightContext = true; break;

-          case BinaryExpr.Opcode.And:

-            opBindingStrength = 0x20; break;

-          case BinaryExpr.Opcode.Or:

-            opBindingStrength = 0x21; break;

-          case BinaryExpr.Opcode.Imp:

-            opBindingStrength = 0x10; fragileLeftContext = true; break;

-          case BinaryExpr.Opcode.Iff:

-            opBindingStrength = 0x08; break;

-          default:

-            Contract.Assert(false); throw new cce.UnreachableException();  // unexpected binary operator

-        }

-        int opBS = opBindingStrength & 0xF8;

-        int ctxtBS = contextBindingStrength & 0xF8;

-        bool parensNeeded = opBS < ctxtBS ||

-          (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));

-

-        string op = BinaryExpr.OpcodeString(e.Op);

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

-        if (0 <= indent && e.Op == BinaryExpr.Opcode.And) {

-          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, indent);

-          wr.WriteLine(" {0}", op);

-          Indent(indent);

-          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, indent);

-        } else if (0 <= indent && e.Op == BinaryExpr.Opcode.Imp) {

-          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, indent);

-          wr.WriteLine(" {0}", op);

-          int ind = indent + IndentAmount;

-          Indent(ind);

-          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, ind);

-        } else {

-          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, -1);

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

-          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, -1);

-        }

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

+        var e = (BinaryExpr)expr;

+        return new BinaryExpr(Tok(e.tok), e.Op, CloneExpr(e.E0), CloneExpr(e.E1));

 

       } else if (expr is ChainingExpression) {

         var e = (ChainingExpression)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x30;

-        int opBS = opBindingStrength & 0xF8;

-        int ctxtBS = contextBindingStrength & 0xF8;

-        bool parensNeeded = opBS < ctxtBS ||

-          (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));

-

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

-        PrintExpr(e.Operands[0], opBindingStrength, true, false, -1);

-        for (int i = 0; i < e.Operators.Count; i++) {

-          string op = BinaryExpr.OpcodeString(e.Operators[i]);

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

-          PrintExpr(e.Operands[i+1], opBindingStrength, true, i == e.Operators.Count - 1 && (parensNeeded || isRightmost), -1);

-        }

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

+        return CloneExpr(e.E);  // just clone the desugaring, since it's already available

 

       } else if (expr is LetExpr) {

         var e = (LetExpr)expr;

-        bool parensNeeded = !isRightmost;

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

-        string sep = "";

-        foreach (var v in e.Vars) {

-          wr.Write("{0}{1}", sep, v.Name);

-          PrintType(": ", v.Type);

-          sep = ", ";

-        }

-        wr.Write(" := ");

-        PrintExpressionList(e.RHSs);

-        wr.Write("; ");

-        PrintExpression(e.Body);

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

-

-

-      } else if (expr is QuantifierExpr) {

-        QuantifierExpr e = (QuantifierExpr)expr;

-        bool parensNeeded = !isRightmost;

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

-        wr.Write(e is ForallExpr ? "forall " : "exists ");

-        PrintQuantifierDomain(e.BoundVars, e.Attributes, e.Range);

-        wr.Write(" :: ");

-        if (0 <= indent) {

-          int ind = indent + IndentAmount;

-          wr.WriteLine();

-          Indent(ind);

-          PrintExpression(e.Term, ind);

+        return new LetExpr(Tok(e.tok), e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body));

+

+      } else if (expr is ComprehensionExpr) {

+        var e = (ComprehensionExpr)expr;

+        var tk = Tok(e.tok);

+        var bvs = e.BoundVars.ConvertAll(CloneBoundVar);

+        var range = CloneExpr(e.Range);

+        var term = CloneExpr(e.Term);

+        if (e is ForallExpr) {

+          return new ForallExpr(tk, bvs, range, term, null);

+        } else if (e is ExistsExpr) {

+          return new ExistsExpr(tk, bvs, range, term, null);

         } else {

-          PrintExpression(e.Term);

+          Contract.Assert(e is SetComprehension);

+          return new SetComprehension(tk, bvs, range, term);

         }

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

-

-      } else if (expr is SetComprehension) {

-        var e = (SetComprehension)expr;

-        bool parensNeeded = !isRightmost;

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

-        wr.Write("set ");

-        string sep = "";

-        foreach (BoundVar bv in e.BoundVars) {

-          wr.Write("{0}{1}", sep, bv.Name);

-          sep = ", ";

-          PrintType(": ", bv.Type);

-        }

-        PrintAttributes(e.Attributes);

-        wr.Write(" | ");

-        PrintExpression(e.Range);

-        if (!e.TermIsImplicit) {

-          wr.Write(" :: ");

-          PrintExpression(e.Term);

-        }

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

 

       } else if (expr is WildcardExpr) {

-        wr.Write("*");

+        return new WildcardExpr(Tok(expr.tok));

 

       } else if (expr is PredicateExpr) {

         var e = (PredicateExpr)expr;

-        bool parensNeeded = !isRightmost;

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

-        wr.Write("{0} ", e.Kind);

-        PrintExpression(e.Guard);

-        wr.Write("; ");

-        PrintExpression(e.Body);

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

+        if (e is AssertExpr) {

+          return new AssertExpr(Tok(e.tok), CloneExpr(e.Guard), CloneExpr(e.Body));

+        } else {

+          Contract.Assert(e is AssumeExpr);

+          return new AssumeExpr(Tok(e.tok), CloneExpr(e.Guard), CloneExpr(e.Body));

+        }

 

       } else if (expr is ITEExpr) {

-        ITEExpr ite = (ITEExpr)expr;

-        bool parensNeeded = !isRightmost;

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

-        wr.Write("if ");

-        PrintExpression(ite.Test);

-        wr.Write(" then ");

-        PrintExpression(ite.Thn);

-        wr.Write(" else ");

-        PrintExpression(ite.Els);

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

+        var e = (ITEExpr)expr;

+        return new ITEExpr(Tok(e.tok), CloneExpr(e.Test), CloneExpr(e.Thn), CloneExpr(e.Els));

 

       } else if (expr is ParensExpression) {

         var e = (ParensExpression)expr;

-        // printing of parentheses is done optimally, not according to the parentheses in the given program

-        PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, indent);

+        return CloneExpr(e.E);  // skip the parentheses in the clone

 

       } else if (expr is IdentifierSequence) {

         var e = (IdentifierSequence)expr;

-        string sep = "";

-        foreach (var id in e.Tokens) {

-          wr.Write("{0}{1}", sep, id.val);

-          sep = ".";

-        }

-        if (e.Arguments != null) {

-          wr.Write("(");

-          PrintExpressionList(e.Arguments);

-          wr.Write(")");

-        }

+        var aa = e.Arguments == null ? null : e.Arguments.ConvertAll(CloneExpr);

+        return new IdentifierSequence(e.Tokens.ConvertAll(tk => Tok(tk)), Tok(e.OpenParen), aa);

 

       } else if (expr is MatchExpr) {

-        Contract.Assert(false); throw new cce.UnreachableException();  // MatchExpr is an extended expression and should be printed only using PrintExtendedExpr

+        var e = (MatchExpr)expr;

+        return new MatchExpr(Tok(e.tok), CloneExpr(e.Source),

+          e.Cases.ConvertAll(c => new MatchCaseExpr(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))));

+

       } else {

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

       }

-#else

-      return expr;  // TODO

-#endif

     }

 

     AssignmentRhs CloneRHS(AssignmentRhs rhs) {

@@ -696,7 +468,8 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

-        r = new MatchStmt(Tok(s.Tok), CloneExpr(s.Source), s.Cases.ConvertAll(c => new MatchCaseStmt(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), c.Body.ConvertAll(CloneStmt))));

+        r = new MatchStmt(Tok(s.Tok), CloneExpr(s.Source),

+          s.Cases.ConvertAll(c => new MatchCaseStmt(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), c.Body.ConvertAll(CloneStmt))));

 

       } else if (stmt is UpdateStmt) {

         var s = (UpdateStmt)stmt;