From 30f9cf0eed24a72102449c329b6eb2cfed5122d5 Mon Sep 17 00:00:00 2001
From: Michal Moskal <michal@moskal.me>
Date: Tue, 15 Nov 2011 22:24:58 -0600
Subject: VCC: Further data type improvements

---
 Source/ModelViewer/VccProvider.cs | 38 ++++++++++++++++----------------------
 1 file changed, 16 insertions(+), 22 deletions(-)

(limited to 'Source/ModelViewer')

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 27d6422b..6fd068a8 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -48,8 +48,6 @@ 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>();
@@ -1222,27 +1220,29 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       }
 
       if (dataTypeType != null) {
-        if (ctor != null && ctor.Args.Length == 0)
+        if (ctor != null)
           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]);
+        if (ctor != null && ctor.Args.Length > 0) {
+          if (level <= 0) sb.Append("(...)");
+          else {
+            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(")");
           }
-          sb.Append(")");
         }
+      } else  {
+        sb.Append(CanonicalName(elt));
       }
       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);
@@ -1253,14 +1253,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         }
       }
 
-      var useCnt = 0;
-      if (!datatypePrefixUse.TryGetValue(baseName, out useCnt))
-        useCnt = -1;
-      useCnt++;
-      datatypePrefixUse[baseName] = useCnt;
-      res = baseName + "." + useCnt.ToString();
-      datatypeShortName[elt] = res;
-      return res;
+      return baseName;
     }
 
     private string CanonicalBaseNameCore(string name, Model.Element elt, bool doDatatypes, ref NameSeqSuffix suff)
@@ -1297,6 +1290,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         if (dtpName != null) {
           var sb = new StringBuilder();
           string prev = null;
+          datatypeLongName[elt] = "*SELF*"; // in case we recurse (but this shouldn't happen)
           for (int lev = 0; lev < 10; lev++) {
             sb.Length = 0;
             var len = DataTypeToString(sb, lev, elt);
@@ -1305,7 +1299,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           }
 
           datatypeLongName[elt] = prev;
-          suff = NameSeqSuffix.None;
+          suff = NameSeqSuffix.WhenNonZero;
           return prev;
         }
       }
@@ -1334,7 +1328,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         return lit;
       }
       if (datatypeLongName.TryGetValue(elt, out lit)) {
-        suff = NameSeqSuffix.None;
+        suff = NameSeqSuffix.WhenNonZero;
         return lit;
       }
       
-- 
cgit v1.2.3