Fix issue 101. Instead of swapping operands for Exp opcode in BinaryExpr,

swap them when the expr is first created in parser or for calcstmt. This
avoids problems of operands being swapped again when the expr is copied.

1 files changed, 5 insertions, 2 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 5fa1085d..ff3b75a3 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -2175,10 +2175,13 @@ ImpliesExpliesExpression<out Expression e0, bool allowSemi, bool allowLambda>
     ( ImpliesOp                                               (. x = t; .)

       ImpliesExpression<out e1, allowSemi, allowLambda>       (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)

     | ExpliesOp                                               (. x = t; .)

-      LogicalExpression<out e1, allowSemi, allowLambda>       (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)

+      LogicalExpression<out e1, allowSemi, allowLambda>       (. // The order of operands is reversed so that it can be turned into implication during resolution 

+			                                                           e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); .)

       { IF(IsExpliesOp())  /* read a reverse implication as far as possible */

         ExpliesOp                                             (. x = t; .)

-        LogicalExpression<out e1, allowSemi, allowLambda>     (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)

+        LogicalExpression<out e1, allowSemi, allowLambda>     (. //The order of operands is reversed so that it can be turned into implication during resolution

+				                                                         e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); 

+																															.)

       }

     )

   ]