From 674e30357980e1192ac532f4bd16c529cedc7fdc Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Wed, 19 Aug 2015 10:51:44 -0700
Subject: Draft out a more advanced version of trigger generation

This new version will include a cleaner pipeline, and trigger splitting.
---
 Test/dafny0/SeqFromArray.dfy.expect | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'Test/dafny0')

diff --git a/Test/dafny0/SeqFromArray.dfy.expect b/Test/dafny0/SeqFromArray.dfy.expect
index af845d3e..5395e298 100644
--- a/Test/dafny0/SeqFromArray.dfy.expect
+++ b/Test/dafny0/SeqFromArray.dfy.expect
@@ -1,3 +1,6 @@
+SeqFromArray.dfy(56,13): Warning: (!) No terms found to trigger on.
+SeqFromArray.dfy(76,17): Warning: (!) No terms found to trigger on.
+SeqFromArray.dfy(82,17): Warning: (!) No terms found to trigger on.
 
 Dafny program verifier finished with 10 verified, 0 errors
 Program compiled successfully
-- 
cgit v1.2.3


From b4f926f38536d30b7d12c35cbf8f45fa7ef71c27 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Wed, 19 Aug 2015 10:37:49 -0700
Subject: Cleanup indentation of trigger warnings

---
 Source/Dafny/Triggers/QuantifiersCollection.cs | 12 ++++++------
 Test/dafny0/TriggerInPredicate.dfy             |  2 +-
 Test/dafny0/TriggerInPredicate.dfy.expect      |  2 ++
 3 files changed, 9 insertions(+), 7 deletions(-)

(limited to 'Test/dafny0')

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 01bceeb7..aa008e36 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -138,12 +138,12 @@ namespace Microsoft.Dafny.Triggers {
       var indent = addHeader ? "   " : " "; //FIXME if multiline messages were properly supported, this indentation wouldn't be needed
 
       if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop and autotriggers attributes are passed down to Boogie
-        msg.AppendFormat("  Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); 
+        msg.AppendFormat("Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); 
         // FIXME This shouldn't be printed for autoReqs. (see autoReq.dfy)
         // FIXME typeQuantifier?
       } else {
         if (addHeader) {
-          msg.AppendFormat("  For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine();
+          msg.AppendFormat("For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine();
         }
 
         foreach (var candidate in q.Candidates) { //FIXME make this _trigger instead of trigger
@@ -154,16 +154,16 @@ namespace Microsoft.Dafny.Triggers {
         AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true);
 
 #if QUANTIFIER_WARNINGS
-        string WARN = DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "; //FIXME set unicodeoutput in extension
+        string WARN = (msg.Length > 0 ? indent : "") + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "); //FIXME set unicodeoutput in extension
         if (!q.CandidateTerms.Any()) {
           errorLevel = ErrorLevel.Warning;
-          msg.Append(indent).Append(WARN).AppendLine("No terms found to trigger on.");
+          msg.Append(WARN).AppendLine("No terms found to trigger on.");
         } else if (!q.Candidates.Any()) {
           errorLevel = ErrorLevel.Warning;
-          msg.Append(indent).Append(WARN).AppendLine("No trigger covering all quantified variables found.");
+          msg.Append(WARN).AppendLine("No trigger covering all quantified variables found.");
         } else if (!q.CouldSuppressLoops && !q.AllowsLoops) {
           errorLevel = ErrorLevel.Warning;
-          msg.Append(indent).Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers.");
+          msg.Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers.");
         }
 #endif
       }
diff --git a/Test/dafny0/TriggerInPredicate.dfy b/Test/dafny0/TriggerInPredicate.dfy
index 3f2eac2c..b9c372dc 100644
--- a/Test/dafny0/TriggerInPredicate.dfy
+++ b/Test/dafny0/TriggerInPredicate.dfy
@@ -3,7 +3,7 @@
 
 predicate A(x: bool, y: bool) { x }
 
-predicate B(x: bool, z: bool) { forall y {:trigger A(x, y) } :: A(x, y) && z }
+predicate B(x: bool, z: bool) { forall y {:trigger A(x, y)} :: A(x, y) && z }
 
 // Inlining is disabled here to prevent pollution of the trigger in B
 method C() requires B(true || false, true) {}
diff --git a/Test/dafny0/TriggerInPredicate.dfy.expect b/Test/dafny0/TriggerInPredicate.dfy.expect
index 7f6e0268..1cbd4034 100644
--- a/Test/dafny0/TriggerInPredicate.dfy.expect
+++ b/Test/dafny0/TriggerInPredicate.dfy.expect
@@ -1,3 +1,5 @@
+TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {A(x, y)}.
+TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {z}.
 TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.
 TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.
 
-- 
cgit v1.2.3