Add /printTooltips and /autoTriggers to the CLI

2 files changed, 39 insertions, 4 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 125ab11e..b2593705 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -56,6 +56,8 @@ namespace Microsoft.Dafny
     public bool AllowGlobals = false;

     public bool CountVerificationErrors = true;

     public bool Optimize = false;

+    public bool AutoTriggers = true;

+    public bool PrintTooltips = false;

 

     protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

       var args = ps.args;  // convenient synonym

@@ -181,6 +183,18 @@ namespace Microsoft.Dafny
           return true;

         }

 

+        case "printTooltips":

+          PrintTooltips = true;

+          return true;

+

+        case "autoTriggers": {

+            int autoTriggers = 1; // defaults to reporting verification errors

+            if (ps.GetNumericArgument(ref autoTriggers, 2)) {

+              AutoTriggers = autoTriggers == 1;

+            }

+            return true;

+          }

+

         case "optimize": {

             Optimize = true;

             return true;

@@ -276,12 +290,19 @@ namespace Microsoft.Dafny
                     of verification errors.

                 1 (default) - If preprocessing succeeds, set exit code to the number of

                               verification errors.

+  /autoTriggers:<n>

+                0 - Do not generate {:trigger} annotations for user-level quantifiers.

+                1 (default) - Add a {:trigger} to each user-level quantifier. Existing

+                              annotations are preserved.

   /optimize     Produce optimized C# code, meaning:

                   - selects optimized C# prelude by passing 

                     /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires 

                     System.Collections.Immutable.dll in the source directory to successfully 

                     compile).

                   - passes /optimize flag to csc.exe.

+  /printTooltips    

+                Dump additional positional information (displayed as mouse-over tooltips by 

+                the VS plugin) to stdout as 'Info' messages.

 ");

       base.Usage();  // also print the Boogie options

     }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index c5535808..300d4985 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -25,7 +25,7 @@ namespace Microsoft.Dafny
       ConsoleColor col = Console.ForegroundColor;

       Console.ForegroundColor = ConsoleColor.Red;

       Console.WriteLine("{0}({1},{2}): Error: {3}",

-          DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col - 1,

+          DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col,

           string.Format(msg, args));

       Console.ForegroundColor = col;

       ErrorCount++;

@@ -254,6 +254,10 @@ namespace Microsoft.Dafny
       // Populate the members of the basic types

       var trunc = new SpecialField(Token.NoToken, "Trunc", "ToBigInteger()", "", "", false, false, false, Type.Int, null);

       basicTypeMembers[(int)BasicTypeVariety.Real].Add(trunc.Name, trunc);

+

+      if (DafnyOptions.O.PrintTooltips) {

+        AdditionalInformationReporter = DefaultInformationReporter;

+      }

     }

 

     [ContractInvariantMethod]

@@ -264,6 +268,12 @@ namespace Microsoft.Dafny
       Contract.Invariant(cce.NonNullDictionaryAndValues(datatypeCtors) && Contract.ForAll(datatypeCtors.Values, v => cce.NonNullDictionaryAndValues(v)));

     }

 

+    public void DefaultInformationReporter(AdditionalInformation info) {

+      Console.WriteLine("{0}({1},{2}): Info: {3}",

+                        DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(info.Token.filename) : info.Token.filename,

+                        info.Token.line, info.Token.col, info.Text);

+    }

+

     public void ResolveProgram(Program prog) {

       Contract.Requires(prog != null);

       var origErrorCount = ErrorCount;

@@ -303,6 +313,10 @@ namespace Microsoft.Dafny
       rewriters.Add(opaqueRewriter);

       rewriters.Add(new TimeLimitRewriter());

 

+      if (DafnyOptions.O.AutoTriggers) {

+        rewriters.Add(new TriggersRewriter(this));

+      }

+

       systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false);

       prog.CompileModules.Add(prog.BuiltIns.SystemModule);

       foreach (var decl in sortedDecls) {

@@ -2048,7 +2062,7 @@ namespace Microsoft.Dafny
           foreach (var p in e.TypeArgumentSubstitutions) {

             if (!IsDetermined(p.Value.Normalize())) {

               Error(e.tok, "type variable '{0}' in the function call to '{1}' could not be determined{2}", p.Key.Name, e.Name,

-                (e.Name.Contains("reveal_") || e.Name.Contains("_FULL"))

+                (e.Name.Contains("reveal_") || e.Name.Contains("_FULL")) //CLEMENT should this be StartsWith and EndsWith?

                 ? ". If you are making an opaque function, make sure that the function can be called."

                 : ""

               );

@@ -8135,7 +8149,7 @@ namespace Microsoft.Dafny
       Contract.Requires(!expr.WasResolved());

       Contract.Requires(opts != null);

       Contract.Ensures(Contract.Result<Expression>() == null || args != null);

-

+      

       if (expr.OptTypeArguments != null) {

         foreach (var ty in expr.OptTypeArguments) {

           ResolveType(expr.tok, ty, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);

@@ -8175,7 +8189,7 @@ namespace Microsoft.Dafny
           receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass, true);

         } else {

           if (!scope.AllowInstance) {

-            Error(expr.tok, "'this' is not allowed in a 'static' context");

+            Error(expr.tok, "'this' is not allowed in a 'static' context"); //FIXME: Rephrase this

             // nevertheless, set "receiver" to a value so we can continue resolution

           }

           receiver = new ImplicitThisExpr(expr.tok);