1 files changed, 240 insertions, 0 deletions
diff --git a/Source/VCExpr/VCExprASTPrinter.ssc b/Source/VCExpr/VCExprASTPrinter.ssc
new file mode 100644
index 00000000..1c143516
--- /dev/null
+++ b/Source/VCExpr/VCExprASTPrinter.ssc
@@ -0,0 +1,240 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using Microsoft.Contracts;
+using Microsoft.Basetypes;
+
+// A simple visitor for turning a VCExpr into a human-readable string
+// (S-expr syntax)
+
+namespace Microsoft.Boogie.VCExprAST
+{
+
+  public class VCExprPrinter : IVCExprVisitor<bool, TextWriter!> {
+    private VCExprOpPrinter OpPrinterVar = null;
+    private VCExprOpPrinter! OpPrinter { get {
+      if (OpPrinterVar == null)
+        OpPrinterVar = new VCExprOpPrinter(this);
+      return OpPrinterVar;
+    } }
+
+    public void Print(VCExpr! expr, TextWriter! wr) {
+      expr.Accept<bool, TextWriter!>(this, wr);
+    }
+
+    public bool Visit(VCExprLiteral! node, TextWriter! wr) {
+      if (node == VCExpressionGenerator.True)
+        wr.Write("true");
+      else if (node == VCExpressionGenerator.False)
+        wr.Write("false");
+      else if (node is VCExprIntLit) {
+        wr.Write(((VCExprIntLit)node).Val);
+      } else
+        assert false;
+      return true;
+    }
+    public bool Visit(VCExprNAry! node, TextWriter! wr) {
+      VCExprOp! op = node.Op;
+
+      if (op.Equals(VCExpressionGenerator.AndOp) ||
+          op.Equals(VCExpressionGenerator.OrOp)) {
+        // handle these operators without recursion
+
+        wr.Write("({0}",
+                 op.Equals(VCExpressionGenerator.AndOp) ? "And" : "Or");
+        IEnumerator! enumerator = new VCExprNAryUniformOpEnumerator (node);
+        while (enumerator.MoveNext()) {
+          VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
+          if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+            wr.Write(" ");
+            Print((VCExpr!)enumerator.Current, wr);
+          }
+        }
+
+        wr.Write(")");
+
+        return true;
+      }
+
+      return node.Accept<bool, TextWriter!>(OpPrinter, wr);
+    }
+    public bool Visit(VCExprVar! node, TextWriter! wr) {
+      wr.Write(node.Name);
+      return true;
+    }
+    public bool Visit(VCExprQuantifier! node, TextWriter! wr) {
+      string! quan = node.Quan == Quantifier.ALL ? "Forall" : "Exists";
+
+      wr.Write("({0} ", quan);
+
+      if (node.TypeParameters.Count > 0) {
+        wr.Write("<");
+        string! sep = "";
+        foreach (TypeVariable! v in node.TypeParameters) {
+          wr.Write(sep);
+          sep = ", ";
+          wr.Write("{0}", v.Name);
+        }
+        wr.Write("> ");
+      }
+
+      if (node.BoundVars.Count > 0) {
+        string! sep = "";
+        foreach (VCExprVar! v in node.BoundVars) {
+          wr.Write(sep);
+          sep = ", ";
+          Print(v, wr);
+        }
+        wr.Write(" ");
+      }
+      
+      wr.Write(":: ");
+
+      if (node.Triggers.Count > 0) {
+        wr.Write("{0} ", "{");
+        string! sep = "";
+        foreach (VCTrigger! t in node.Triggers) {
+          wr.Write(sep);
+          sep = ", ";
+          string! sep2 = "";
+          foreach (VCExpr! e in t.Exprs) {
+            wr.Write(sep2);
+            sep2 = "+";
+            Print(e, wr);
+          }
+        }
+        wr.Write(" {0} ", "}");
+      }
+
+      Print(node.Body, wr);
+      wr.Write(")");
+      return true;
+    }
+    public bool Visit(VCExprLet! node, TextWriter! wr) {
+      wr.Write("(Let ");
+
+      string! sep = "";
+      foreach (VCExprLetBinding! b in node) {
+        wr.Write(sep);
+        sep = ", ";
+        Print(b.V, wr);
+        wr.Write(" = ");
+        Print(b.E, wr);
+      }
+      wr.Write(" ");
+
+      Print(node.Body, wr);
+      wr.Write(")");
+      return true;
+    }
+  }
+
+  public class VCExprOpPrinter : IVCExprOpVisitor<bool, TextWriter!> {
+    private VCExprPrinter! ExprPrinter;
+
+    public VCExprOpPrinter(VCExprPrinter! exprPrinter) {
+      this.ExprPrinter = exprPrinter;
+    }
+
+    private bool PrintNAry(string! op, VCExprNAry! node, TextWriter! wr) {
+      wr.Write("({0}", op);
+      foreach (VCExpr! arg in node) {
+        wr.Write(" ");
+        ExprPrinter.Print(arg, wr);
+      }
+      wr.Write(")");
+      return true;
+    }
+
+    public bool VisitNotOp      (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("!", node, wr);
+    }
+    public bool VisitEqOp       (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("==", node, wr);
+    }
+    public bool VisitNeqOp      (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("!=", node, wr);
+    }
+    public bool VisitAndOp      (VCExprNAry! node, TextWriter! wr) {
+      assert false;
+    }
+    public bool VisitOrOp       (VCExprNAry! node, TextWriter! wr) {
+      assert false;
+    }
+    public bool VisitImpliesOp  (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("Implies", node, wr);
+    }
+    public bool VisitDistinctOp (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("Distinct", node, wr);
+    }
+    public bool VisitLabelOp    (VCExprNAry! node, TextWriter! wr) {
+      VCExprLabelOp! op = (VCExprLabelOp)node.Op;
+      return PrintNAry("Label " + op.label, node, wr);
+    }
+    public bool VisitSelectOp   (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("Select", node, wr);
+    }
+    public bool VisitStoreOp    (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("Store", node, wr);
+    }
+    public bool VisitBvOp       (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("Bv", node, wr);
+    }
+    public bool VisitBvExtractOp(VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("BvExtract", node, wr);
+    }
+    public bool VisitBvConcatOp (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("BvConcat", node, wr);
+    }
+    public bool VisitAddOp            (VCExprNAry! node, TextWriter! wr) {
+      if (CommandLineOptions.Clo.ReflectAdd) {
+        return PrintNAry("Reflect$Add", node, wr);
+      } else {
+        return PrintNAry("+", node, wr);
+      }
+    }
+    public bool VisitSubOp            (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("-", node, wr);
+    }
+    public bool VisitMulOp            (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("*", node, wr);
+    }
+    public bool VisitDivOp            (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("/", node, wr);
+    }
+    public bool VisitModOp            (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("%", node, wr);
+    }
+    public bool VisitLtOp             (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("<", node, wr);
+    }
+    public bool VisitLeOp             (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("<=", node, wr);
+    }
+    public bool VisitGtOp             (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry(">", node, wr);
+    }
+    public bool VisitGeOp             (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry(">=", node, wr);
+    }
+    public bool VisitSubtypeOp        (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("<:", node, wr);
+    }
+    public bool VisitSubtype3Op       (VCExprNAry! node, TextWriter! wr) {
+      return PrintNAry("<::", node, wr);
+    }
+    public bool VisitBoogieFunctionOp (VCExprNAry! node, TextWriter! wr) {
+      VCExprBoogieFunctionOp! op = (VCExprBoogieFunctionOp)node.Op;
+      return PrintNAry(op.Func.Name, node, wr);
+    }
+  }
+
+
+}
+\ No newline at end of file