Add a check for SplitQuantifiers that had been incorrectly left out from the merge

1 files changed, 43 insertions, 45 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 23c0c3f6..8146d2cf 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -11526,56 +11526,60 @@ namespace Microsoft.Dafny {
           return TrExpr(((NamedExpr)expr).Body);

         } else if (expr is QuantifierExpr) {

           QuantifierExpr e = (QuantifierExpr)expr;

-          List<Variable> tyvars = translator.MkTyParamBinders(e.TypeArgs);

-          List<Variable> bvars = new List<Variable>();

 

-          var initEtran = this;

-          var bodyEtran = this;

-          bool _scratch = true;

+          if (e.SplitQuantifier != null) {

+            return TrExpr(e.SplitQuantifierExpression);

+          } else {

+            List<Variable> tyvars = translator.MkTyParamBinders(e.TypeArgs);

+            List<Variable> bvars = new List<Variable>();

 

-          Bpl.Expr antecedent = Bpl.Expr.True;

+            var initEtran = this;

+            var bodyEtran = this;

+            bool _scratch = true;

 

-          if (Attributes.ContainsBool(e.Attributes, "layerQuantifier", ref _scratch)) {

-            // If this is a layer quantifier, quantify over layers here, and use $LS(ly) layers in the translation of the body

-            var ly = BplBoundVar(e.Refresh("q$ly#", translator.CurrentIdGenerator), predef.LayerType, bvars);

-            bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, new FuelSetting(translator, 1, ly), new FuelSetting(translator, 1, ly), modifiesFrame, stripLits);

-          }

-          if (Attributes.ContainsBool(e.Attributes, "heapQuantifier", ref _scratch)) {

-            var h = BplBoundVar(e.Refresh("q$heap#", translator.CurrentIdGenerator), predef.HeapType, bvars);

-            bodyEtran = new ExpressionTranslator(bodyEtran, h);

-            antecedent = BplAnd(new List<Bpl.Expr> {

+            Bpl.Expr antecedent = Bpl.Expr.True;

+

+            if (Attributes.ContainsBool(e.Attributes, "layerQuantifier", ref _scratch)) {

+              // If this is a layer quantifier, quantify over layers here, and use $LS(ly) layers in the translation of the body

+              var ly = BplBoundVar(e.Refresh("q$ly#", translator.CurrentIdGenerator), predef.LayerType, bvars);

+              bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, new FuelSetting(translator, 1, ly), new FuelSetting(translator, 1, ly), modifiesFrame, stripLits);

+            }

+            if (Attributes.ContainsBool(e.Attributes, "heapQuantifier", ref _scratch)) {

+              var h = BplBoundVar(e.Refresh("q$heap#", translator.CurrentIdGenerator), predef.HeapType, bvars);

+              bodyEtran = new ExpressionTranslator(bodyEtran, h);

+              antecedent = BplAnd(new List<Bpl.Expr> {

               antecedent,

               translator.FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, h),

               translator.HeapSameOrSucc(initEtran.HeapExpr, h)

             });

-          }

+            }

 

-          antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars));

+            antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars));

 

-          Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger");

-          Bpl.Trigger tr = null;

-          var argsEtran = bodyEtran.WithNoLits();

-          foreach (var aa in e.Attributes.AsEnumerable()) {

-            if (aa.Name == "trigger") {

-              List<Bpl.Expr> tt = new List<Bpl.Expr>();

-              foreach (var arg in aa.Args) {

-                tt.Add(argsEtran.TrExpr(arg));

+            Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger");

+            Bpl.Trigger tr = null;

+            var argsEtran = bodyEtran.WithNoLits();

+            foreach (var aa in e.Attributes.AsEnumerable()) {

+              if (aa.Name == "trigger") {

+                List<Bpl.Expr> tt = new List<Bpl.Expr>();

+                foreach (var arg in aa.Args) {

+                  tt.Add(argsEtran.TrExpr(arg));

+                }

+                tr = new Bpl.Trigger(expr.tok, true, tt, tr);

               }

-              tr = new Bpl.Trigger(expr.tok, true, tt, tr);

             }

-          }

-          if (e.Range != null) {

-            antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range));

-          }

-          Bpl.Expr body = bodyEtran.TrExpr(e.Term);

-          

-          if (e is ForallExpr) {

-            return new Bpl.ForallExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.Imp(antecedent, body));

-          } else {

-            Contract.Assert(e is ExistsExpr);

-            return new Bpl.ExistsExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.And(antecedent, body));

-          }

+            if (e.Range != null) {

+              antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range));

+            }

+            Bpl.Expr body = bodyEtran.TrExpr(e.Term);

 

+            if (e is ForallExpr) {

+              return new Bpl.ForallExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.Imp(antecedent, body));

+            } else {

+              Contract.Assert(e is ExistsExpr);

+              return new Bpl.ExistsExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.And(antecedent, body));

+            }

+          }

         } else if (expr is SetComprehension) {

           var e = (SetComprehension)expr;

           // Translate "set xs | R :: T" into "lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T))".

@@ -13092,13 +13096,7 @@ namespace Microsoft.Dafny {
 

     private bool CanSafelyInline(FunctionCallExpr fexp, Function f) {

       var visitor = new TriggersExplorer();

-

-      visitor.Visit(f.Body);

-      foreach (var expr in f.Ens) { visitor.Visit(expr); }

-      foreach (var expr in f.Req) { visitor.Visit(expr); }

-      foreach (var expr in f.Reads) { visitor.Visit(expr); }

-      foreach (var expr in f.Decreases.Expressions) { visitor.Visit(expr); }

-

+      visitor.Visit(f);

       return f.Formals.Zip(fexp.Args).All(formal_concrete => CanSafelySubstitute(visitor.TriggerVariables, formal_concrete.Item1, formal_concrete.Item2));

     }