Start committing split quantifiers

This requires rewriting the parts of the AST that contain these quantifiers. We
unfortunately don't have facilities to do such rewrites at the moment (and there
are loops in the AST, so it would be hard to write such a facility). As a
workaround, this commit introduces a field in quantifier expressions,
SplitQuantifiers. Code that manipulate triggers is expected to look for this
field, and ignore the other fields if that one is found.

12 files changed, 203 insertions, 69 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 323abc70..961d4d14 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -4,6 +4,7 @@ using System.Collections.Generic;
 using System.Numerics;

 using System.Diagnostics.Contracts;

 using IToken = Microsoft.Boogie.IToken;

+using System.Linq;

 

 namespace Microsoft.Dafny

 {

@@ -373,13 +374,18 @@ namespace Microsoft.Dafny
         if (e is QuantifierExpr) {

           var q = (QuantifierExpr)e;

           var tvs = q.TypeArgs.ConvertAll(CloneTypeParam);

+          QuantifierExpr cloned;

           if (e is ForallExpr) {

-            return new ForallExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes));

+            cloned = new ForallExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes));

           } else if (e is ExistsExpr) {

-            return new ExistsExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes));

+            cloned = new ExistsExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes));

           } else {

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

           }

+          if (q.SplitQuantifier != null) { //TODO CLEMENT TRIGGERS: Should we clone the quantifier as a quantifier in this case? Or should we just replace entirely?

+            cloned.SplitQuantifier = q.SplitQuantifier.Select(CloneExpr).ToList();

+          }

+          return cloned;

         } else if (e is MapComprehension) {

           return new MapComprehension(tk, ((MapComprehension)e).Finite, bvs, range, term, CloneAttributes(e.Attributes));

         } else if (e is LambdaExpr) {

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 4fdd34f6..d19d2bed 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -2816,6 +2816,12 @@ namespace Microsoft.Dafny {
 

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

+

+        if (e.SplitQuantifier != null) { //TODO CLEMENT TRIGGERS: Do we compile a split quantifier in its original form, or in its split form?

+          TrExpr(e.SplitQuantifierExpression);

+          return;

+        }

+        

         Contract.Assert(e.Bounds != null);  // for non-ghost quantifiers, the resolver would have insisted on finding bounds

         var n = e.BoundVars.Count;

         Contract.Assert(e.Bounds.Count == n);

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index efe94c66..05548f38 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1555,7 +1555,7 @@ namespace Microsoft.Dafny {
         // BUGBUG:  The following line is a workaround to tell the verifier that 'value' is not of an Immutable type.

         // A proper solution would be to be able to express that in the program (in a specification or attribute) or

         // to be able to declare 'parent' as [PeerOrImmutable].

-        Contract.Requires(value is TopLevelDecl || value is Function || value is Method || value is DatatypeCtor || value is QuantifierExpr);

+        Contract.Requires(value is TopLevelDecl || value is Function || value is Method || value is DatatypeCtor || (value is QuantifierExpr && ((QuantifierExpr)value).SplitQuantifier == null));

         //modifies parent;

         parent = value;

       }

@@ -6552,6 +6552,15 @@ namespace Microsoft.Dafny {
       }

     }

 

+    /// <summary>

+    /// Returns a resolved binary expression

+    /// </summary>

+    public BinaryExpr(Boogie.IToken tok, BinaryExpr.ResolvedOpcode rop, Expression e0, Expression e1)

+    : this(tok, BinaryExpr.ResolvedOp2SyntacticOp(rop), e0, e1) {

+      ResolvedOp = rop;

+      Type = Type.Bool;

+    }

+

     public override IEnumerable<Expression> SubExpressions {

       get {

         yield return E0;

@@ -6770,6 +6779,8 @@ namespace Microsoft.Dafny {
     public List<TypeParameter> TypeArgs;

     private static int currentQuantId = -1;

 

+    protected abstract BinaryExpr.ResolvedOpcode SplitResolvedOp { get; }

+

     static int FreshQuantId() {

       return System.Threading.Interlocked.Increment(ref currentQuantId);

     }

@@ -6800,10 +6811,47 @@ namespace Microsoft.Dafny {
       this.TypeArgs = tvars;

       this.UniqueId = FreshQuantId();

     }

+

+    private Expression SplitQuantifierToExpression() {

+      Contract.Requires(SplitQuantifier != null && SplitQuantifier.Any());

+      Expression accumulator = SplitQuantifier[0];

+      for (int tid = 1; tid < SplitQuantifier.Count; tid++) {

+        var newAcc = new BinaryExpr(Term.tok, SplitResolvedOp, accumulator, SplitQuantifier[tid]);

+        accumulator = newAcc;

+      }

+      return accumulator;

+    }

+

+    private List<Expression> _SplitQuantifier;

+    public List<Expression> SplitQuantifier {

+      get {

+        return _SplitQuantifier;

+      }

+      set {

+        _SplitQuantifier = value;

+        SplitQuantifierExpression = SplitQuantifierToExpression();

+      }

+    }

+

+    internal Expression SplitQuantifierExpression { get; private set; }

+

     public abstract Expression LogicalBody();

+

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        if (SplitQuantifier == null) {

+          return base.SubExpressions;

+        } else {

+          return SplitQuantifier;

+        }

+      }

+    }

   }

 

   public class ForallExpr : QuantifierExpr {

+    protected override BinaryExpr.Opcode SplitOp { get { return BinaryExpr.Opcode.And; } }

+    protected override BinaryExpr.ResolvedOpcode SplitResolvedOp { get { return BinaryExpr.ResolvedOpcode.And; } }

+

     public ForallExpr(IToken tok, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)

       : this(tok, new List<TypeParameter>(), bvars, range, term, attrs) {

       Contract.Requires(cce.NonNullElements(bvars));

@@ -6817,6 +6865,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(term != null);

     }

     public override Expression LogicalBody() {

+      Contract.Assert(SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier

       if (Range == null) {

         return Term;

       }

@@ -6828,6 +6877,9 @@ namespace Microsoft.Dafny {
   }

 

   public class ExistsExpr : QuantifierExpr {

+    protected override BinaryExpr.Opcode SplitOp { get { return BinaryExpr.Opcode.Or; } }

+    protected override BinaryExpr.ResolvedOpcode SplitResolvedOp { get { return BinaryExpr.ResolvedOpcode.Or; } }

+

     public ExistsExpr(IToken tok, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)

       : this(tok, new List<TypeParameter>(), bvars, range, term, attrs) {

       Contract.Requires(cce.NonNullElements(bvars));

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 1c7508eb..43b69bbb 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1729,6 +1729,13 @@ namespace Microsoft.Dafny {
 

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

+

+        if (e.SplitQuantifier != null) {

+          // CLEMENT TODO TRIGGERS: Should (do) we have a setting to print the original forms instead of rewritten forms?

+          PrintExpr(e.SplitQuantifierExpression, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, resolv_count);

+          return;

+        }

+

         bool parensNeeded = !isRightmost;

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

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

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 7bf085f9..e1c3c63b 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -305,7 +305,7 @@ namespace Microsoft.Dafny
             Contract.Assert(!useCompileSignatures);

             useCompileSignatures = true;  // set Resolver-global flag to indicate that Signatures should be followed to their CompiledSignature

             var oldErrorsOnly = reporter.ErrorsOnly;

-            reporter.ErrorsOnly = true; // turn off warning reporting for the clone

+            reporter.ErrorsOnly = true; // turn off warning reporter for the clone

             var nw = new Cloner().CloneModuleDefinition(m, m.CompileName + "_Compile");

             var compileSig = RegisterTopLevelDecls(nw, true);

             compileSig.Refines = refinementTransformer.RefinedSig;

@@ -338,7 +338,7 @@ namespace Microsoft.Dafny
                   if (refinementTransformer.CheckIsRefinement(compileSig, p)) {

                     abs.Signature.CompileSignature = compileSig;

                   } else {

-                    reporter.Error(MessageSource.Resolver,

+                    reporter.Error(MessageSource.Resolver, 

                       abs.CompilePath[0],

                       "module " + Util.Comma(".", abs.CompilePath, x => x.val) + " must be a refinement of "

                       + Util.Comma(".", abs.Path, x => x.val));

@@ -2438,6 +2438,7 @@ namespace Microsoft.Dafny
           return false;

         } else if (expr is QuantifierExpr) {

           var e = (QuantifierExpr)expr;

+          Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution

           var cpos = IsCoContext ? cp : Invert(cp);

           if ((cpos == CallingPosition.Positive && e is ExistsExpr) || (cpos == CallingPosition.Negative && e is ForallExpr)) {

             if (e.MissingBounds != null && e.MissingBounds.Count != 0) {

@@ -6962,7 +6963,7 @@ namespace Microsoft.Dafny
           reporter.Error(MessageSource.Resolver, expr, "'this' is not allowed in a 'static' context");

         }

         if (currentClass != null) {

-          expr.Type = GetThisType(expr.tok, currentClass);  // do this regardless of scope.AllowInstance, for better error reporting

+          expr.Type = GetThisType(expr.tok, currentClass);  // do this regardless of scope.AllowInstance, for better error reporter

         }

 

       } else if (expr is IdentifierExpr) {

@@ -7605,6 +7606,7 @@ namespace Microsoft.Dafny
         e.Type = e.Body.Type;

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

+        Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution

         int prevErrorCount = reporter.Count(ErrorLevel.Error);

         bool _val = true;

         bool typeQuantifier = Attributes.ContainsBool(e.Attributes, "typeQuantifier", ref _val) && _val;

@@ -9177,6 +9179,7 @@ namespace Microsoft.Dafny
         return;

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

+        Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution

         if (e.MissingBounds != null) {

           foreach (var bv in e.MissingBounds) {

             reporter.Error(MessageSource.Resolver, expr, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);

@@ -9774,10 +9777,13 @@ namespace Microsoft.Dafny
 

       if (expr is IdentifierExpr) {

         var e = (IdentifierExpr)expr;

+

         return new HashSet<IVariable>() { e.Var };

 

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

+        Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution

+

         var s = FreeVariables(e.LogicalBody());

         foreach (var bv in e.BoundVars) {

           s.Remove(bv);

@@ -10139,7 +10145,9 @@ namespace Microsoft.Dafny
       } else if (expr is NamedExpr) {

         return moduleInfo.IsGhost ? false : UsesSpecFeatures(((NamedExpr)expr).Body);

       } else if (expr is ComprehensionExpr) {

-        if (expr is QuantifierExpr && ((QuantifierExpr)expr).Bounds == null) {

+        var q = expr as QuantifierExpr;

+        Contract.Assert(q == null || q.SplitQuantifier == null); // No split quantifiers during resolution

+        if (q != null && q.Bounds == null) {

           return true;  // the quantifier cannot be compiled if the resolver found no bounds

         }

         return Contract.Exists(expr.SubExpressions, se => UsesSpecFeatures(se));

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 0798510a..2c00e203 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -43,9 +43,9 @@ namespace Microsoft.Dafny
       Contract.Requires(reporter != null);

     }

 

-    internal override void PostResolve(ModuleDefinition m) {

+    internal override void PostCyclicityResolve(ModuleDefinition m) {

       var finder = new Triggers.QuantifierCollectionsFinder(reporter);

-

+        

       foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {

         if (decl is Function) {

           var function = (Function)decl;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 14fca463..f0b7f276 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4465,6 +4465,11 @@ namespace Microsoft.Dafny {
         var e = (ComprehensionExpr)expr;

         var canCall = CanCallAssumption(e.Term, etran);

         var q = e as QuantifierExpr;

+

+        if (q != null && q.SplitQuantifier != null) {

+          return CanCallAssumption(q.SplitQuantifierExpression, etran);

+        }

+

         var tyvars = MkTyParamBinders(q != null ? q.TypeArgs : new List<TypeParameter>());

         if (e.Range != null) {

           canCall = BplAnd(CanCallAssumption(e.Range, etran), BplImp(etran.TrExpr(e.Range), canCall));

@@ -4758,6 +4763,12 @@ namespace Microsoft.Dafny {
         // If the quantifier is universal, then continue as:

         //   assume (\forall x :: body(x));

         // Create local variables corresponding to the type arguments:

+

+        if (e.SplitQuantifier != null) {

+          CheckWellformedAndAssume(e.SplitQuantifierExpression, options, locals, builder, etran);

+          return;

+        }

+

         var typeArgumentCopies = Map(e.TypeArgs, tp => e.Refresh(tp, CurrentIdGenerator));

         var typeMap = Util.Dict(e.TypeArgs, Map(typeArgumentCopies, tp => (Type)new UserDefinedType(tp)));

         var newLocals = Map(typeArgumentCopies, tp => new Bpl.LocalVariable(tp.tok, new TypedIdent(tp.tok, nameTypeParam(tp), predef.Ty)));

@@ -5293,6 +5304,10 @@ namespace Microsoft.Dafny {
         var q = e as QuantifierExpr;

         var lam = e as LambdaExpr;

 

+        if (q != null && q.SplitQuantifier != null) {

+          CheckWellformedWithResult(q.SplitQuantifierExpression, options, result, resultType, locals, builder, etran);

+        }

+

         var typeMap = new Dictionary<TypeParameter, Type>();

         var copies = new List<TypeParameter>();

         if (q != null) {

@@ -11534,56 +11549,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;

 

-          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)

-            });

-          }

+          if (e.SplitQuantifier != null) {

+            return TrExpr(e.SplitQuantifierExpression);

+          } else {

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

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

+

+            var initEtran = this;

+            var bodyEtran = this;

+            bool _scratch = true;

+

+            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.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 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))".

@@ -12966,9 +12985,11 @@ namespace Microsoft.Dafny {
           }

         }

 

+      } else if (expr is QuantifierExpr && ((QuantifierExpr)expr).SplitQuantifier != null) {

+        return TrSplitExpr(((QuantifierExpr)expr).SplitQuantifierExpression, splits, position, heightLimit, apply_induction, etran);

       } else if (((position && expr is ForallExpr) || (!position && expr is ExistsExpr))

-          /* NB: only for type arg less quantifiers for now: */

-             && ((QuantifierExpr)expr).TypeArgs.Count == 0) {

+        /* NB: only for type arg less quantifiers for now: */

+            && ((QuantifierExpr)expr).TypeArgs.Count == 0) {

         var e = (QuantifierExpr)expr;

         var inductionVariables = ApplyInduction(e);

         if (apply_induction && 2 <= DafnyOptions.O.Induction && inductionVariables.Count != 0) {

@@ -13138,8 +13159,11 @@ namespace Microsoft.Dafny {
 

       protected override void VisitOneExpr(Expression expr) {

         if (expr is QuantifierExpr) {

-          foreach (var trigger in (expr as QuantifierExpr).Attributes.AsEnumerable().Where(a => a.Name == "trigger").SelectMany(a => a.Args)) {

-            collector.Visit(trigger);

+          var e = (QuantifierExpr)expr;

+          if (e.SplitQuantifier == null) {

+            foreach (var trigger in (expr as QuantifierExpr).Attributes.AsEnumerable().Where(a => a.Name == "trigger").SelectMany(a => a.Args)) {

+              collector.Visit(trigger);

+            }

           }

         }

       }

@@ -13173,6 +13197,7 @@ namespace Microsoft.Dafny {
     }

 

     List<BoundVar> ApplyInduction(QuantifierExpr e) {

+      Contract.Requires(e.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier

       Contract.Requires(e.TypeArgs.Count == 0);

       return ApplyInduction(e.BoundVars, e.Attributes, new List<Expression>() { e.LogicalBody() },

         delegate(System.IO.TextWriter wr) { new Printer(wr).PrintExpression(e, true); });

@@ -13946,6 +13971,12 @@ namespace Microsoft.Dafny {
           var e = (ComprehensionExpr)expr;

           // For quantifiers and setComprehesion we want to make sure that we don't introduce name clashes with

           // the enclosing scopes.

+

+          var q = e as QuantifierExpr;

+          if (q != null && q.SplitQuantifier != null) {

+            return Substitute(q.SplitQuantifierExpression);

+          }

+

           var newBoundVars = CreateBoundVarSubstitutions(e.BoundVars, expr is ForallExpr || expr is ExistsExpr || expr is SetComprehension);

           Expression newRange = e.Range == null ? null : Substitute(e.Range);

           Expression newTerm = Substitute(e.Term);

diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs
index 33be0da2..80381f0a 100644
--- a/Source/Dafny/Triggers/QuantifierSplitter.cs
+++ b/Source/Dafny/Triggers/QuantifierSplitter.cs
@@ -21,30 +21,37 @@ namespace Microsoft.Dafny.Triggers {
     // Unfortunately, this would cause ill-behaved quantifiers to produce

     // exponentially many smaller quantifiers.

 

+    private static UnaryOpExpr Not(Expression expr) {

+      var not = new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type };

+      return not;

+    }

+

     internal static IEnumerable<Expression> SplitExpr(Expression expr, BinaryExpr.Opcode separator) {

       expr = expr.Resolved;

       var unary = expr as UnaryOpExpr;

       var binary = expr as BinaryExpr;

 

       if (unary != null && unary.Op == UnaryOpExpr.Opcode.Not) {

-        foreach (var e in SplitExpr(unary.E, FlipOpcode(separator))) { yield return new UnaryOpExpr(unary.tok, UnaryOpExpr.Opcode.Not, e); }

+        foreach (var e in SplitExpr(unary.E, FlipOpcode(separator))) { yield return Not(e); }

       } else if (binary != null && binary.Op == separator) {

         foreach (var e in SplitExpr(binary.E0, separator)) { yield return e; }

         foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; }

       } else if (binary != null && binary.Op == BinaryExpr.Opcode.Imp && separator == BinaryExpr.Opcode.Or) {

-        foreach (var e in SplitExpr(new UnaryOpExpr(unary.tok, UnaryOpExpr.Opcode.Not, binary.E0), separator)) { yield return e; }

+        foreach (var e in SplitExpr(Not(binary.E0), separator)) { yield return e; }

         foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; }

+      } else {

+        yield return expr;

       }

     }

 

     internal static IEnumerable<Expression> SplitAndStich(BinaryExpr pair, BinaryExpr.Opcode separator) {

-      foreach (var e1 in SplitExpr(pair.E1, separator)) { 

-        yield return new BinaryExpr(pair.tok, pair.Op, pair.E0, e1);

+      foreach (var e1 in SplitExpr(pair.E1, separator)) {

+        yield return new BinaryExpr(pair.tok, pair.Op, pair.E0, e1) { ResolvedOp = pair.ResolvedOp, Type = pair.Type };

       }

     }

 

     internal static IEnumerable<Expression> SplitQuantifier(QuantifierExpr quantifier) {

-      var body = quantifier.LogicalBody();

+      var body = quantifier.Term;

       var binary = body as BinaryExpr;

 

       if (quantifier is ForallExpr) {

@@ -55,7 +62,7 @@ namespace Microsoft.Dafny.Triggers {
           stream = SplitExpr(body, BinaryExpr.Opcode.And);

         }

         foreach (var e in stream) {

-          yield return new ForallExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, quantifier.Term, quantifier.Attributes);

+          yield return new ForallExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type };

         }

       } else if (quantifier is ExistsExpr) {

         IEnumerable<Expression> stream;

@@ -65,17 +72,18 @@ namespace Microsoft.Dafny.Triggers {
           stream = SplitExpr(body, BinaryExpr.Opcode.Or);

         }

         foreach (var e in stream) {

-          yield return new ExistsExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, quantifier.Term, quantifier.Attributes);

+          yield return new ExistsExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type };

         }

       } else {

         yield return quantifier;

       }

     }

         

-    protected override void VisitOneExpr(Expression expr) { //FIXME: This doesn't save the rewritten quantifier

+    protected override void VisitOneExpr(Expression expr) {

       var quantifier = expr as QuantifierExpr;

       if (quantifier != null) {

-        var rew = SplitQuantifier(quantifier);

+        var split = SplitQuantifier(quantifier).ToList();

+        quantifier.SplitQuantifier = split;

         //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| "));

       }

     }

diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs
index da43abcc..9fbc8a8a 100644
--- a/Source/Dafny/Triggers/TriggerExtensions.cs
+++ b/Source/Dafny/Triggers/TriggerExtensions.cs
@@ -272,6 +272,14 @@ namespace Microsoft.Dafny.Triggers {
     }

 

     private static bool ShallowEq(QuantifierExpr expr1, QuantifierExpr expr2) { //FIXME are these TypeArgs still useful?

+      if (!TriggerUtils.SameNullity(expr1.SplitQuantifier, expr2.SplitQuantifier)) {

+        return false;

+      }

+

+      if (expr1.SplitQuantifier != null && expr2.SplitQuantifier != null) {

+        return ShallowEq_Top(expr1.SplitQuantifierExpression, expr2.SplitQuantifierExpression);

+      }

+

       if (expr1.TypeArgs.Count != expr2.TypeArgs.Count ||

           !TriggerUtils.SameNullity(expr1.Range, expr2.Range)) {

         return false;

diff --git a/Source/Dafny/Triggers/TriggerGenerator.cs b/Source/Dafny/Triggers/TriggerGenerator.cs
index de4b212b..e218ad7b 100644
--- a/Source/Dafny/Triggers/TriggerGenerator.cs
+++ b/Source/Dafny/Triggers/TriggerGenerator.cs
@@ -19,9 +19,13 @@ namespace Microsoft.Dafny.Triggers { //FIXME rename this file
     protected override bool VisitOneExpr(Expression expr, ref object st) {

       var quantifier = expr as QuantifierExpr;

       if (quantifier != null) {

-        quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter));

-      } //FIXME handle the case of groups of quantifiers resulting from a split

-

+        if (quantifier.SplitQuantifier != null) {

+          var collection = quantifier.SplitQuantifier.Select(q => q as QuantifierExpr).Where(q => q != null);

+          quantifierCollections.Add(new QuantifiersCollection(collection, reporter));

+        } else {

+          quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter));

+        }

+      }

       return true;

     }

   }

diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index dedbcbb1..6c6eede2 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -101,6 +101,7 @@ namespace Microsoft.Dafny.Triggers {
     }

 

     internal static bool NeedsAutoTriggers(QuantifierExpr quantifier) {

+      Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier

       return quantifier.Attributes.AsEnumerable().All(aa => aa.Name != "trigger" && aa.Name != "no_trigger");

     }

   }

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index e1f8a013..9f721d9a 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -44,11 +44,13 @@ namespace Microsoft.Dafny.Triggers {
     }

 

     internal IEnumerable<TriggerMatch> LoopingSubterms(QuantifierExpr quantifier) {

+      Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier

       var matchingSubterms = MatchingSubterms(quantifier);

       return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms));

     }

 

     internal List<TriggerMatch> MatchingSubterms(QuantifierExpr quantifier) {

+      Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier

       //FIXME this will miss rewritten expressions (CleanupExpr). Should introduce an OriginalExpr to compare against.

       return Terms.SelectMany(term => quantifier.SubexpressionsMatchingTrigger(term.Expr)).Deduplicate(TriggerMatch.Eq);

     }

@@ -139,7 +141,7 @@ namespace Microsoft.Dafny.Triggers {
           (expr is UnaryOpExpr && (((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Cardinality)) || // FIXME || ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh doesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944

           (expr is BinaryExpr && (((BinaryExpr)expr).Op == BinaryExpr.Opcode.NotIn || ((BinaryExpr)expr).Op == BinaryExpr.Opcode.In))) {

         annotation = AnnotatePotentialCandidate(expr);

-      } else if (expr is QuantifierExpr) {

+      } else if (expr is QuantifierExpr && ((QuantifierExpr)expr).SplitQuantifier == null) {

         annotation = AnnotateQuantifier((QuantifierExpr)expr);

       } else if (expr is LetExpr) {

         annotation = AnnotateLetExpr((LetExpr)expr);

@@ -259,6 +261,7 @@ namespace Microsoft.Dafny.Triggers {
 

     // FIXME document that this will contain duplicates

     internal List<TriggerTerm> CollectTriggers(QuantifierExpr quantifier) {

+      Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier

       // TODO could check for existing triggers and return that instead, but that require a bit of work to extract the expressions

       return Annotate(quantifier).PrivateTerms;

     }