Merged PredicateExpr and CalcExpr into a single StmtExpr

In that process, added a SubstStmt method (and entourage) for substituting into statements

1 files changed, 10 insertions, 8 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index a66286b5..43a06799 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1811,19 +1811,21 @@ EndlessExpression<out Expression e>
   | MatchExpression<out e>

   | QuantifierGuts<out e>

   | ComprehensionExpr<out e>

-  | "assert"                        (. x = t; .)

-    Expression<out e0> ";"

-    Expression<out e1>              (. e = new AssertExpr(x, e0, e1); .)

-  | "assume"                        (. x = t; .)

-    Expression<out e0> ";"

-    Expression<out e1>              (. e = new AssumeExpr(x, e0, e1); .)

-  | CalcStmt<out s>             

-    Expression<out e1>              (. e = new CalcExpr(s.Tok, (CalcStmt)s, e1); .)

+  | StmtInExpr<out s>

+    Expression<out e>               (. e = new StmtExpr(s.Tok, s, e); .)

   | LetExpr<out e>

   | NamedExpr<out e>

   )

   .

 

+StmtInExpr<out Statement s>

+= (. s = dummyStmt; .)

+  ( AssertStmt<out s>

+  | AssumeStmt<out s>

+  | CalcStmt<out s>

+  )

+  .

+

 LetExpr<out Expression e>

 = (. IToken/*!*/ x;

      e = dummyExpr;