Add some pretty-printing, on by default. Turn off with the flag "/pretty:0"

When running boogie form the command line, this should be on by default.
On the other hand, the TokenTextWriter constructors and PrintBplFile now have an
argument for this, but by default it is off.

8 files changed, 144 insertions, 15 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 0026a3fe..82c5cc59 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1862,8 +1862,10 @@ namespace Microsoft.Boogie {
       Contract.Requires(stream != null);

       Type.EmitOptionalTypeParams(stream, TypeParameters);

       stream.Write("(");

+      stream.push();

       InParams.Emit(stream, true);

       stream.Write(")");

+      stream.sep();

 

       if (shortRet) {

         Contract.Assert(OutParams.Count == 1);

@@ -1874,6 +1876,7 @@ namespace Microsoft.Boogie {
         OutParams.Emit(stream, true);

         stream.Write(")");

       }

+      stream.pop();

     }

 

     // Register all type parameters at the resolution context

@@ -3293,14 +3296,17 @@ namespace Microsoft.Boogie {
     public void Emit(TokenTextWriter stream) {

       Contract.Requires(stream != null);

       stream.SetToken(this);

+      stream.push();

       if (this.Name != NoName) {

         stream.Write("{0}: ", TokenTextWriter.SanitizeIdentifier(this.Name));

       }

       this.Type.Emit(stream);

       if (this.WhereExpr != null) {

+        stream.sep();

         stream.Write(" where ");

         this.WhereExpr.Emit(stream);

       }

+      stream.pop();

     }

     public override void Resolve(ResolutionContext rc) {

       //Contract.Requires(rc != null);

@@ -3374,12 +3380,15 @@ namespace Microsoft.Boogie {
     public static void Emit(this List<Expr> ts, TokenTextWriter stream) {

       Contract.Requires(stream != null);

       string sep = "";

+      stream.push();

       foreach (Expr/*!*/ e in ts) {

         Contract.Assert(e != null);

         stream.Write(sep);

         sep = ", ";

+        stream.sep();

         e.Emit(stream);

       }

+      stream.pop();

     }

 

     public static void Emit(this List<IdentifierExpr> ids, TokenTextWriter stream, bool printWhereComments) {

@@ -3402,12 +3411,15 @@ namespace Microsoft.Boogie {
     public static void Emit(this List<Variable> vs, TokenTextWriter stream, bool emitAttributes) {

       Contract.Requires(stream != null);

       string sep = "";

+      stream.push();

       foreach (Variable/*!*/ v in vs) {

         Contract.Assert(v != null);

         stream.Write(sep);

         sep = ", ";

+        stream.sep();

         v.EmitVitals(stream, 0, emitAttributes);

       }

+      stream.pop();

     }

 

     public static void Emit(this List<Type> tys, TokenTextWriter stream, string separator) {

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 70b445b1..d6dd17c9 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1418,15 +1418,18 @@ namespace Microsoft.Boogie {
       bool parensNeeded = opBS < ctxtBS ||

         (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));

 

+      var pop = stream.push(FunctionName);

       if (parensNeeded) {

         stream.Write("(");

       }

       cce.NonNull(args[0]).Emit(stream, opBindingStrength, fragileLeftContext);

+      stream.sep();

       stream.Write(" {0} ", FunctionName);

       cce.NonNull(args[1]).Emit(stream, opBindingStrength, fragileRightContext);

       if (parensNeeded) {

         stream.Write(")");

       }

+      stream.pop(pop);

     }

     public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {

       //Contract.Requires(subjectForErrorReporting != null);

@@ -2521,13 +2524,17 @@ namespace Microsoft.Boogie {
       //Contract.Requires(args != null);

       stream.SetToken(ref this.tok);

       Contract.Assert(args.Count == 3);

-      stream.Write("(if ");

+      stream.push();

+      stream.Write("(if ");     

       cce.NonNull(args[0]).Emit(stream, 0x00, false);

+      stream.sep();

       stream.Write(" then ");

       cce.NonNull(args[1]).Emit(stream, 0x00, false);

+      stream.sep();

       stream.Write(" else ");

       cce.NonNull(args[2]).Emit(stream, 0x00, false);

       stream.Write(")");

+      stream.pop();

     }

 

     public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 397d8eba..c9e8f210 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -113,20 +113,24 @@ namespace Microsoft.Boogie {
 

     public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

       //Contract.Requires(stream != null);

+      stream.push();

       stream.Write(this, "({0}", Kind.ToString().ToLower());

       this.EmitTypeHint(stream);

       Type.EmitOptionalTypeParams(stream, TypeParameters);

       stream.Write(this, " ");

       this.Dummies.Emit(stream, true);

       stream.Write(" :: ");

+      stream.sep();

       for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {

         kv.Emit(stream);

         stream.Write(" ");

       }

       this.EmitTriggers(stream);

+      stream.sep();

 

       this.Body.Emit(stream);

       stream.Write(")");

+      stream.pop();

     }

 

     protected virtual void ResolveTriggers(ResolutionContext rc) {

@@ -542,10 +546,13 @@ namespace Microsoft.Boogie {
 

     protected override void EmitTriggers(TokenTextWriter stream) {

       //Contract.Requires(stream != null);

+      stream.push();

       for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {

         tr.Emit(stream);

         stream.Write(" ");

+        stream.sep();

       }

+      stream.pop();

     }

 

     // if the user says ( forall x :: forall y ::  ... ) and specifies *no* triggers, we transform it to

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4f9488a3..65554a1e 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -421,6 +421,8 @@ namespace Microsoft.Boogie {
     public string CVC4ExecutablePath = null;

     public int KInductionDepth = -1;

 

+    public bool PrettyPrint = true;

+

     public enum ProverWarnings {

       None,

       Stdout,

@@ -741,6 +743,13 @@ namespace Microsoft.Boogie {
           }

           return true;

 

+        case "pretty":

+          int val = 1;

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

+            PrettyPrint = val == 1;

+          } 

+          return true;

+

         case "OwickiGries":

           if (ps.ConfirmArgumentCount(1)) {

               OwickiGriesDesugaredOutputFile = args[ps.i];

@@ -1657,6 +1666,9 @@ namespace Microsoft.Boogie {
 

   /print:<file>  : print Boogie program after parsing it

                    (use - as <file> to print to console)

+  /pretty:<n>

+                0 - print each Boogie statement on one line (faster).

+                1 (default) - pretty-print with some line breaks.

   /printWithUniqueIds : print augmented information that uniquely

                    identifies variables

   /printUnstructured : with /print option, desugars all structured statements

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index c14cb82e..66eefd8c 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -127,6 +127,90 @@ namespace Microsoft.Boogie {
                 "while",

         };

 

+    // "Pretty" printing: not very efficient, and not necessarily very pretty, but helps a bit 

+    private readonly bool pretty;

+    

+    // The stack of writers in a current separator-block.

+    // The string is an optional identifier that allows you

+    // to not start a new indentation for e.g. "&&" in "a && b && c".

+    // When the pretty printing is finished, this should be empty.

+    Stack<KeyValuePair<string, List<TextWriter>>> wstk;

+

+    // The original writer: where everything should finally end up.

+    TextWriter actual_writer;

+

+    public bool push(string type = null) {

+      if (pretty) {

+        if (wstk == null) {

+          wstk = new Stack<KeyValuePair<string, List<TextWriter>>>();

+          actual_writer = writer;

+        }

+        if (wstk.Count > 0 && wstk.Peek().Key == type && type != null) {

+          sep();

+          return false; // don't actually pop this thing (send this bool to pop)

+        } else {

+          wstk.Push(new KeyValuePair<string, List<TextWriter>>(type, new List<TextWriter> { }));

+          sep();

+          return true;  // this needs to be popped

+        }

+      } else {

+        return false;

+      }

+    }

+

+    public void pop(bool do_it = true) {

+      if (pretty) {

+        if (do_it) {

+          List<TextWriter> ws = wstk.Pop().Value;

+          // try to figure out if you should insert line breaks between

+          // them or print them on one single line

+          // this breaks down when there are newlines inserted

+          List<String> ss = new List<String>();

+          int len = 0;

+          foreach (TextWriter w in ws) {

+            foreach (String s in w.ToString().Split(new String[] { "\r\n", "\n" }, StringSplitOptions.None)) {

+              if (s.Length > 0) {

+                ss.Add(s);

+                len += s.Length;

+                // len = Math.Max(len, s.Length);

+              }

+            }

+          }

+          // figure out which is the next writer to use

+          List<TextWriter> tw = wstk.Count > 0 ? wstk.Peek().Value : null;

+          if (tw == null) {

+            writer = actual_writer;

+          } else {

+            writer = tw.Last();

+          }

+          // write the strings (we would like to know WHERE we are in the document here)

+          if (len > 80 /* - wstk.Count * 2 */) {

+            for (int i = 0; i < ss.Count; i++) {

+              if (i != ss.Count - 1) {

+                writer.WriteLine(ss[i]);

+                writer.Write("  ");

+              } else {

+                writer.Write(ss[i]);

+              }

+            }

+          } else {

+            foreach (String s in ss) {

+              writer.Write(s);

+            }

+          }

+        }

+      }

+    }

+

+    public void sep() {

+      if (pretty) {

+        List<TextWriter> ws = wstk.Peek().Value;

+

+        writer = new StringWriter();

+        wstk.Peek().Value.Add(writer);

+      }

+    }

+

     private IToken/*!*/ CurrentToken {

       get {

         Contract.Ensures(Contract.Result<IToken>() != null);

@@ -160,46 +244,53 @@ namespace Microsoft.Boogie {
       } else if (name.Length > 2 && name[0] == 'b' && name[1] == 'v') {

         int dummy;

         return int.TryParse(name.Substring(2), out dummy) ? "\\" + name : name;

+      } else if (name.Contains('@')) {

+        return SanitizeIdentifier(name.Replace("@", "#AT#"));

       } else {

         return name;

       }

     }

 

-    public TokenTextWriter(string filename)

+    public TokenTextWriter(string filename, bool pretty = false)

       : base() {

       Contract.Requires(filename != null);

+      this.pretty = pretty;

       this.filename = filename;

       this.writer = new StreamWriter(filename);

     }

 

-    public TokenTextWriter(string filename, bool setTokens)

+    public TokenTextWriter(string filename, bool setTokens, bool pretty = false)

       : base() {

       Contract.Requires(filename != null);

+      this.pretty = pretty;

       this.filename = filename;

       this.writer = new StreamWriter(filename);

       this.setTokens = setTokens;

     }

 

-    public TokenTextWriter(string filename, TextWriter writer, bool setTokens)

+    public TokenTextWriter(string filename, TextWriter writer, bool setTokens, bool pretty = false)

       : base() {

       Contract.Requires(writer != null);

       Contract.Requires(filename != null);

+      this.pretty = pretty;

       this.filename = filename;

       this.writer = writer;

       this.setTokens = setTokens;

     }

 

-    public TokenTextWriter(string filename, TextWriter writer)

+    public TokenTextWriter(string filename, TextWriter writer, bool pretty = false)

       : base() {

       Contract.Requires(writer != null);

       Contract.Requires(filename != null);

+      this.pretty = pretty;

       this.filename = filename;

       this.writer = writer;

     }

 

-    public TokenTextWriter(TextWriter writer)

+    public TokenTextWriter(TextWriter writer, bool pretty = false)

       : base() {

       Contract.Requires(writer != null);

+      this.pretty = pretty;

       this.filename = "<no file>";

       this.writer = writer;

     }

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 925b414b..cac56c4b 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -476,7 +476,7 @@ namespace Microsoft.Boogie
           return;

         if (CommandLineOptions.Clo.PrintFile != null)

         {

-          PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);

+          PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false, true, CommandLineOptions.Clo.PrettyPrint);

         }

 

         LinearTypeChecker linearTypeChecker;

@@ -511,7 +511,7 @@ namespace Microsoft.Boogie
           {

               int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;

               CommandLineOptions.Clo.PrintUnstructured = 1;

-              PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false);

+              PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false, CommandLineOptions.Clo.PrettyPrint);

               CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;

           }

         }

@@ -559,7 +559,7 @@ namespace Microsoft.Boogie
     }

 

 

-    public static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring, bool setTokens = true)

+    public static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring, bool setTokens = true, bool pretty = false)

     {

       Contract.Requires(program != null);

       Contract.Requires(filename != null);

@@ -569,8 +569,8 @@ namespace Microsoft.Boogie
         CommandLineOptions.Clo.PrintDesugarings = false;

       }

       using (TokenTextWriter writer = filename == "-" ?

-                                      new TokenTextWriter("<console>", Console.Out, setTokens) :

-                                      new TokenTextWriter(filename, setTokens))

+                                      new TokenTextWriter("<console>", Console.Out, setTokens, pretty) :

+                                      new TokenTextWriter(filename, setTokens, pretty))

       {

         if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never)

         {

@@ -729,7 +729,7 @@ namespace Microsoft.Boogie
       if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings)

       {

         // if PrintDesugaring option is engaged, print the file here, after resolution and type checking

-        PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true);

+        PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true, true, CommandLineOptions.Clo.PrettyPrint);

       }

 

       return PipelineOutcome.ResolvedAndTypeChecked;

@@ -838,7 +838,7 @@ namespace Microsoft.Boogie
 

       if (CommandLineOptions.Clo.PrintInstrumented)

       {

-        program.Emit(new TokenTextWriter(Console.Out));

+        program.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo.PrettyPrint));

       }

       #endregion

 

diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl
index 8aa25d33..c79eff80 100644
--- a/Test/test0/PrettyPrint.bpl
+++ b/Test/test0/PrettyPrint.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -noVerify -printInstrumented "%s" > "%t"

+// RUN: %boogie -pretty:0 -noVerify -printInstrumented "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 const x: int;

 const y: int;

diff --git a/Test/test20/TypeSynonyms2.bpl b/Test/test20/TypeSynonyms2.bpl
index 472b1e96..1cb6e781 100644
--- a/Test/test20/TypeSynonyms2.bpl
+++ b/Test/test20/TypeSynonyms2.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

-// RUN: %boogie -noVerify -print:- -env:0 -printDesugared "%s" > "%t"

+// RUN: %boogie -noVerify -print:- -pretty:0 -env:0 -printDesugared "%s" > "%t"

 // RUN: %diff "%s.print.expect" "%t"