Review preceding commit with Rustan

5 files changed, 15 insertions, 28 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 961d4d14..e89a385f 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -374,18 +374,13 @@ namespace Microsoft.Dafny
         if (e is QuantifierExpr) {

           var q = (QuantifierExpr)e;

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

-          QuantifierExpr cloned;

           if (e is ForallExpr) {

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

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

           } else if (e is ExistsExpr) {

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

+            return 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 d19d2bed..c969ac1f 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -2817,10 +2817,7 @@ 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;

-        }

+        // Compilation does not check whether a quantifier was split.

         

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

         var n = e.BoundVars.Count;

@@ -2864,7 +2861,7 @@ namespace Microsoft.Dafny {
           wr.Write("{0}, ", expr is ForallExpr ? "true" : "false");

           wr.Write("@{0} => ", bv.CompileName);

         }

-        TrExpr(e.LogicalBody());

+        TrExpr(e.LogicalBody(true));

         for (int i = 0; i < n; i++) {

           wr.Write(")");

         }

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 05548f38..a902a18c 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1552,11 +1552,6 @@ namespace Microsoft.Dafny {
       set {

         Contract.Requires(Parent == null);  // set it only once

         Contract.Requires(value != null);

-        // 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 && ((QuantifierExpr)value).SplitQuantifier == null));

-        //modifies parent;

         parent = value;

       }

     }

@@ -6816,8 +6811,7 @@ namespace Microsoft.Dafny {
       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;

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

       }

       return accumulator;

     }

@@ -6835,7 +6829,11 @@ namespace Microsoft.Dafny {
 

     internal Expression SplitQuantifierExpression { get; private set; }

 

-    public abstract Expression LogicalBody();

+    public virtual Expression LogicalBody(bool bypassSplitQuantifier = false) {

+      // Don't call this on a quantifier with a Split clause: it's not a real quantifier. The only exception is the Compiler.

+      Contract.Requires(bypassSplitQuantifier || SplitQuantifier == null);

+      throw new cce.UnreachableException(); // This body is just here for the "Requires" clause

+    }

 

     public override IEnumerable<Expression> SubExpressions {

       get {

@@ -6847,9 +6845,8 @@ namespace Microsoft.Dafny {
       }

     }

   }

-

+  

   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)

@@ -6864,8 +6861,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

       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

+    public override Expression LogicalBody(bool bypassSplitQuantifier = false) {

       if (Range == null) {

         return Term;

       }

@@ -6877,7 +6873,6 @@ 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)

@@ -6892,7 +6887,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

       Contract.Requires(term != null);

     }

-    public override Expression LogicalBody() {

+    public override Expression LogicalBody(bool bypassSplitQuantifier = false) {

       if (Range == null) {

         return Term;

       }

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 43b69bbb..7c684fde 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1730,8 +1730,7 @@ 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?

+        if (DafnyOptions.O.DafnyPrintResolvedFile != null && e.SplitQuantifier != null) {

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

           return;

         }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index f0b7f276..df816b6d 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5306,6 +5306,7 @@ namespace Microsoft.Dafny {
 

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

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

+          return;

         }

 

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