From 51bec918c61f056eb343faccceaa73d885549dde Mon Sep 17 00:00:00 2001
From: Michal Moskal <michal@moskal.me>
Date: Tue, 15 Nov 2011 22:12:29 -0600
Subject: VCC: Better display of data type values

---
 Source/ModelViewer/VccProvider.cs | 91 +++++++++++++++++++++++++++++++++------
 1 file changed, 78 insertions(+), 13 deletions(-)

(limited to 'Source/ModelViewer')

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 4354ddc3..27d6422b 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -48,9 +48,14 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     public List<StateNode> states = new List<StateNode>();
     public Dictionary<string, string> localVariableNames = new Dictionary<string, string>();
 
+    Dictionary<string, int> datatypePrefixUse = new Dictionary<string, int>();
+    Dictionary<Model.Element, string> datatypeShortName = new Dictionary<Model.Element, string>();
+    Dictionary<Model.Element, string> datatypeLongName = new Dictionary<Model.Element, string>();
+
     Dictionary<int, string> fileNameMapping = new Dictionary<int, string>();
 
     public const string selfMarker = "\\self";
+    public const int maxDatatypeNameLength = 5;
 
     public VccModel(Model m, ViewOptions opts)
       : base(m, opts)
@@ -1202,7 +1207,63 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       }
     }
 
-    private string CanonicalBaseNameCore(string name, Model.Element elt)
+    private int DataTypeToString(StringBuilder sb, int level, Model.Element elt)
+    {
+      Model.FuncTuple ctor = null;
+      int len = 1;
+      string dataTypeType = null;
+      foreach (var app in elt.References) {
+        var n = app.Func.Name;
+        if (app.Result == elt && n.StartsWith("DF#")) {
+          ctor = app;
+        }
+        var tmp = DataTypeName(elt, app);
+        if (tmp != null) dataTypeType = tmp;
+      }
+
+      if (dataTypeType != null) {
+        if (ctor != null && ctor.Args.Length == 0)
+          sb.Append(ctor.Func.Name.Substring(3));
+        else
+          sb.Append(DataTypeShortName(elt, dataTypeType));
+        if (level > 0 && ctor != null && ctor.Args.Length > 0) {
+          sb.Append("(");
+          for (int i = 0; i < ctor.Args.Length; ++i) {
+            if (i != 0) sb.Append(", ");
+            len += DataTypeToString(sb, level - 1, ctor.Args[i]);
+          }
+          sb.Append(")");
+        }
+      }
+      return len;
+    }
+
+    private string DataTypeShortName(Model.Element elt, string tp)
+    {
+      string res;
+      if (datatypeShortName.TryGetValue(elt, out res)) return res;
+
+      var baseName = tp;
+
+      var hd = model.MkFunc("DGH#" + tp, 1).TryEval(elt);
+      if (hd != null) {
+        foreach (var nm in hd.References) {
+          if (nm.Func.Arity == 0 && nm.Func.Name.StartsWith("DH#"))
+            baseName = nm.Func.Name.Substring(3);
+        }
+      }
+
+      var useCnt = 0;
+      if (!datatypePrefixUse.TryGetValue(baseName, out useCnt))
+        useCnt = -1;
+      useCnt++;
+      datatypePrefixUse[baseName] = useCnt;
+      res = baseName + "." + useCnt.ToString();
+      datatypeShortName[elt] = res;
+      return res;
+    }
+
+    private string CanonicalBaseNameCore(string name, Model.Element elt, bool doDatatypes, ref NameSeqSuffix suff)
     {
       var vm = this;
 
@@ -1234,18 +1295,18 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 
         var dtpName = DataTypeName(elt, tpl);
         if (dtpName != null) {
-          var dgh = model.TryGetFunc("DGH#" + dtpName);
-          if (dgh != null) {
-            var hd = dgh.TryEval(elt);
-            if (hd != null) {
-              foreach (var nm in hd.References) {
-                if (nm.Func.Arity == 0 && nm.Func.Name.StartsWith("DH#"))
-                  return nm.Func.Name.Substring(3);
-              }
-
-            }
+          var sb = new StringBuilder();
+          string prev = null;
+          for (int lev = 0; lev < 10; lev++) {
+            sb.Length = 0;
+            var len = DataTypeToString(sb, lev, elt);
+            if (prev == null || len <= maxDatatypeNameLength)
+              prev = sb.ToString();
           }
-          return dtpName;
+
+          datatypeLongName[elt] = prev;
+          suff = NameSeqSuffix.None;
+          return prev;
         }
       }
 
@@ -1272,9 +1333,13 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         suff = NameSeqSuffix.None;
         return lit;
       }
+      if (datatypeLongName.TryGetValue(elt, out lit)) {
+        suff = NameSeqSuffix.None;
+        return lit;
+      }
       
       var name = base.CanonicalBaseName(elt, out suff);
-      name = CanonicalBaseNameCore(name, elt);
+      name = CanonicalBaseNameCore(name, elt, true, ref suff);
      
       return name;
     }
-- 
cgit v1.2.3