Use a nice warning symbol in some warning messages

This is useful because trigger-related messages can contain quite a bit of
information, especially if they include info about multiple split quantifiers.

4 files changed, 40 insertions, 28 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 66cf639f..245632ad 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -40,6 +40,7 @@ namespace Microsoft.Dafny
       Bpl.CommandLineOptions.Install(options);

     }

 

+    public bool UnicodeOutput = false;

     public bool DisallowSoundnessCheating = false;

     public bool Dafnycc = false;

     public int Induction = 3;

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 828e0e18..cbc212d2 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -132,55 +132,63 @@ namespace Microsoft.Dafny.Triggers {
       //FIXME

     }

 

-    private void CommitOne(QuantifierWithTriggers q, object conjunctId) {

+    private void CommitOne(QuantifierWithTriggers q, bool addHeader) {

       var errorLevel = ErrorLevel.Info;

       var msg = new StringBuilder();

-      var indent = conjunctId != null ? "    " : "  ";

-      var header = conjunctId != null ? String.Format("  For conjunct {0}:{1}", conjunctId, Environment.NewLine) : "";

+      var indent = addHeader ? "   " : " "; //FIXME if multiline messages were properly supported, this indentation wouldn't be needed

 

-      if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: no_trigger is passed down to Boogie

-        msg.Append(indent).AppendLine("Not generating triggers for this quantifier.");

+      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(); 

+        // FIXME This shouldn't be printed for autoReqs. (see autoReq.dfy)

+        // FIXME typeQuantifier?

       } else {

-        foreach (var candidate in q.Candidates) {

-          q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes);

+        if (addHeader) {

+          msg.AppendFormat("  For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine();

         }

 

-        if (q.Candidates.Any()) {

-          msg.Append(indent).AppendLine("Selected triggers:");

-          foreach (var mc in q.Candidates) {

-            msg.Append(indent).Append("  ").AppendLine(mc.ToString());

-          }

+        foreach (var candidate in q.Candidates) { //FIXME make this _trigger instead of trigger

+          q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes);

         }

 

-        if (q.RejectedCandidates.Any()) {

-          msg.Append(indent).AppendLine("Rejected triggers:");

-          foreach (var mc in q.RejectedCandidates) {

-            msg.Append(indent).Append("  ").AppendLine(mc.ToString());

-          }

-        }

+        AddTriggersToMessage("Selected triggers:", q.Candidates, msg, indent);

+        AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true);

 

 #if QUANTIFIER_WARNINGS

+        string WARN = DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "; //FIXME set unicodeoutput in extension

         if (!q.CandidateTerms.Any()) {

           errorLevel = ErrorLevel.Warning;

-          msg.Append(indent).AppendLine("No terms found to trigger on.");

+          msg.Append(indent).Append(WARN).AppendLine("No terms found to trigger on.");

         } else if (!q.Candidates.Any()) {

           errorLevel = ErrorLevel.Warning;

-          msg.Append(indent).AppendLine("No trigger covering all quantified variables found.");

-        } else if (!q.CouldSuppressLoops) {

+          msg.Append(indent).Append(WARN).AppendLine("No trigger covering all quantified variables found.");

+        } else if (!q.CouldSuppressLoops && !q.AllowsLoops) {

           errorLevel = ErrorLevel.Warning;

-          msg.Append(indent).AppendLine("Suppressing loops would leave this quantifier without triggers.");

+          msg.Append(indent).Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers.");

         }

 #endif

       }

-

+      

       if (msg.Length > 0) {

-        reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, header + msg.ToString());

+        reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msg.ToString().TrimEnd("\r\n".ToCharArray()));

+      }

+    }

+

+    private static void AddTriggersToMessage<T>(string header, List<T> triggers, StringBuilder msg, string indent, bool newlines = false) {

+      if (triggers.Any()) {

+        msg.Append(indent).Append(header);

+        if (triggers.Count == 1) {

+          msg.Append(" ");

+        } else if (triggers.Count > 1) {

+          msg.AppendLine().Append(indent).Append("  ");

+        }

+        var separator = newlines && triggers.Count > 1 ? Environment.NewLine + indent + "  " : ", ";

+        msg.AppendLine(String.Join(separator, triggers));

       }

     }

 

     internal void CommitTriggers() {

       foreach (var q in quantifiers) {

-        CommitOne(q, quantifiers.Count > 1 ? q.quantifier : null);

+        CommitOne(q, quantifiers.Count > 1);

       }

     }

   }

diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs
index 74cdd8c2..bdfd66b4 100644
--- a/Source/DafnyServer/Server.cs
+++ b/Source/DafnyServer/Server.cs
@@ -33,11 +33,13 @@ namespace Microsoft.Dafny {
     public Server() {

       this.running = true;

       Console.CancelKeyPress += this.CancelKeyPress;

+      Console.InputEncoding = System.Text.Encoding.UTF8;

+      Console.OutputEncoding = System.Text.Encoding.UTF8;

       ExecutionEngine.printer = new DafnyConsolePrinter();

     }

 

     void CancelKeyPress(object sender, ConsoleCancelEventArgs e) {

-      e.Cancel = true;

+      // e.Cancel = true;

       // FIXME TerminateProver and RunningProverFromCommandLine

       // Cancel the current verification? TerminateProver() ? Or kill entirely?

     }

diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs
index 8fb03b05..4b06e9f5 100644
--- a/Source/DafnyServer/Utilities.cs
+++ b/Source/DafnyServer/Utilities.cs
@@ -45,13 +45,14 @@ namespace Microsoft.Dafny {
 

     internal static void ApplyArgs(string[] args) {

       Dafny.DafnyOptions.Install(new Dafny.DafnyOptions());

+      Dafny.DafnyOptions.O.ProverKillTime = 10;

 

       if (CommandLineOptions.Clo.Parse(args)) {

         // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME

         // Dafny.DafnyOptions.O.ModelViewFile = "-";

-        Dafny.DafnyOptions.O.ProverKillTime = 10;

-        Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1);

+        Dafny.DafnyOptions.O.UnicodeOutput = true;

         Dafny.DafnyOptions.O.VerifySnapshots = 2;

+        Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1);

       } else {

         throw new ServerException("Invalid command line options");

       }