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.

1 files changed, 8 insertions, 0 deletions

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;