Rework the namer interface a bit

4 files changed, 75 insertions, 36 deletions

diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index b4ed0977..80d2e3c9 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -17,7 +17,7 @@ namespace Microsoft.Boogie.ModelViewer.Base
 

     public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts)

     {

-      return new GenericModel(m);

+      return new GenericModel(m, opts);

     }

   }

 

@@ -26,7 +26,8 @@ namespace Microsoft.Boogie.ModelViewer.Base
     internal Model m;

     List<BaseState> states = new List<BaseState>();

 

-    public GenericModel(Model m)

+    public GenericModel(Model m, ViewOptions opts)

+        : base(opts)

     {

       this.m = m;

       foreach (var s in m.States)

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index ccec9f5e..859ce211 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -19,7 +19,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
 

     public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts)

     {

-      var dm = new DafnyModel(m);

+      var dm = new DafnyModel(m, opts);

       foreach (var s in m.States) {

         var sn = new StateNode(dm.states.Count, dm, s);

         dm.states.Add(sn);

@@ -37,7 +37,8 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
     Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();

     public List<StateNode> states = new List<StateNode>();

 

-    public DafnyModel(Model m)

+    public DafnyModel(Model m, ViewOptions opts)

+      : base(opts)

     {

       model = m;

       f_heap_select = m.MkFunc("[3]", 3);

@@ -100,22 +101,25 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       return null;

     }

 

-    public override string CanonicalName(Model.Element elt) {

+    protected override string CanonicalBaseName(Model.Element elt, out NameSeqSuffix suff)

+    {

       Model.FuncTuple fnTuple;

+      suff = NameSeqSuffix.WhenNonZero;

       if (DatatypeValues.TryGetValue(elt, out fnTuple)) {

         // elt is s a datatype value, make its name be the name of the datatype constructor

         string nm = fnTuple.Func.Name;

         if (fnTuple.Func.Arity == 0)

           return nm;

         else

-          return nm + "(...)" + base.CanonicalName(elt);

+          return nm + "(...)";

       }

       var seqLen = f_seq_length.AppWithArg(0, elt);

       if (seqLen != null) {

         // elt is a sequence

-        return string.Format("[Length {0}]{1}", seqLen.Result.AsInt(), base.CanonicalName(elt));

+        return string.Format("[Length {0}]", seqLen.Result.AsInt());

       }

-      return base.CanonicalName(elt);

+      

+      return base.CanonicalBaseName(elt, out suff);

     }

 

     public IEnumerable<ElementNode> GetExpansion(StateNode state, Model.Element elt)

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index ee1d82fd..fb6a9372 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -5,6 +5,13 @@ using System.Text;
 

 namespace Microsoft.Boogie.ModelViewer

 {

+  public enum NameSeqSuffix

+  {

+    None,

+    WhenNonZero,

+    Always

+  }

+

   public abstract class LanguageModel : ILanguageSpecificModel

   {

     protected Dictionary<string, int> baseNameUse = new Dictionary<string, int>();

@@ -12,6 +19,12 @@ namespace Microsoft.Boogie.ModelViewer
     protected Dictionary<string, Model.Element> invCanonicalName = new Dictionary<string, Model.Element>();

     protected Dictionary<Model.Element, string> localValue = new Dictionary<Model.Element, string>();

 

+    public readonly ViewOptions viewOpts;

+    public LanguageModel(ViewOptions opts)

+    {

+      viewOpts = opts;

+    }

+    

     // Elements (other than integers and Booleans) get canonical names of the form 

     // "<base>'<idx>", where <base> is returned by this function, and <idx> is given 

     // starting with 0, and incrementing when there are conflicts between bases.

@@ -22,9 +35,17 @@ namespace Microsoft.Boogie.ModelViewer
     // A reasonable strategy is to check if it's a name of the local, and if so return it,

     // and otherwise use the type of element (e.g., return "seq" for elements representing

     // sequences). It is also possible to return "" in such cases.

-    protected virtual string CanonicalBaseName(Model.Element elt)

+    //

+    // The suff output parameter specifies whether the number sequence suffix should be 

+    // always added, only when it's non-zero, or never.

+    protected virtual string CanonicalBaseName(Model.Element elt, out NameSeqSuffix suff)

     {

       string res;

+      if (elt is Model.Integer || elt is Model.Boolean) {

+       suff = NameSeqSuffix.None;

+       return elt.ToString();

+      }

+      suff = NameSeqSuffix.Always;

       if (localValue.TryGetValue(elt, out res))

         return res;

       return "";

@@ -38,39 +59,45 @@ namespace Microsoft.Boogie.ModelViewer
       localValue[elt] = name;

     }

 

-    protected virtual string LiteralName(Model.Element elt)

+    protected virtual string AppendSuffix(string baseName, int id)

     {

-      if (elt is Model.Integer)

-        return elt.ToString();

-      if (elt is Model.Boolean)

-        return elt.ToString();

-      return null;

+      return baseName + "'" + id.ToString();

     }

 

     public virtual string CanonicalName(Model.Element elt)

     {

       string res;

       if (canonicalName.TryGetValue(elt, out res)) return res;

-      res = LiteralName(elt);

-      if (res == null) {

-        var baseName = CanonicalBaseName(elt);

-        int cnt;

-        if (!baseNameUse.TryGetValue(baseName, out cnt)) {

-          cnt = -1;

-        }

-        cnt++;

-        res = baseName + "'" + cnt;

-        baseNameUse[baseName] = cnt;

+      NameSeqSuffix suff;

+      var baseName = CanonicalBaseName(elt, out suff);

+      if (baseName == "")

+        suff = NameSeqSuffix.Always;

+

+      if (viewOpts.DebugMode && !(elt is Model.Boolean) && !(elt is Model.Number)) {

+        baseName += string.Format("({0})", elt);

+        suff = NameSeqSuffix.WhenNonZero;

       }

+      

+      int cnt;

+      if (!baseNameUse.TryGetValue(baseName, out cnt))

+        cnt = -1;

+      cnt++;

+

+      if (suff == NameSeqSuffix.Always || (cnt > 0 && suff == NameSeqSuffix.WhenNonZero))

+        res = AppendSuffix(baseName, cnt);

+      else

+        res = baseName;

+ 

+      baseNameUse[baseName] = cnt;

       canonicalName.Add(elt, res);

-      invCanonicalName.Add(res, elt);

+      invCanonicalName[res.Replace(" ", "")] = elt;

       return res;

     }

 

     public virtual Model.Element FindElement(string canonicalName)

     {

       Model.Element res;

-      if (invCanonicalName.TryGetValue(canonicalName, out res))

+      if (invCanonicalName.TryGetValue(canonicalName.Replace(" ", ""), out res))

         return res;

       return null;

     }

@@ -92,6 +119,7 @@ namespace Microsoft.Boogie.ModelViewer
 

       Action<IEnumerable<IDisplayNode>> addList = (IEnumerable<IDisplayNode> nodes) =>

       {

+        var tmp = nodes.Select(x => x.Name).ToArray();

         var ch = nodes.ToDictionary(x => x.Name);

         foreach (var k in SortFields(nodes))

           workList.Enqueue(ch[k]);

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 0a8430f0..9f1449d2 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -44,13 +44,12 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();

     Dictionary<Model.Element, string> literalName = new Dictionary<Model.Element, string>();

     public List<StateNode> states = new List<StateNode>();

-    public readonly ViewOptions viewOpts;

 

     Dictionary<int, string> fileNameMapping = new Dictionary<int, string>();

 

     public VccModel(Model m, ViewOptions opts)

+      : base(opts)

     {

-      viewOpts = opts;

       model = m;

       f_ptr_to = m.MkFunc("$ptr_to", 1);

       f_spec_ptr_to = m.MkFunc("$spec_ptr_to", 1);

@@ -250,7 +249,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       return null;

     }

 

-    protected override string LiteralName(Model.Element elt)

+    private string LiteralName(Model.Element elt)

     {

       string r;

 

@@ -263,7 +262,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         return r;

       }

 

-      return base.LiteralName(elt);

+      return null;

     }

 

     public Model.Element LocalType(string localName)

@@ -668,19 +667,26 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       if (fld != null) {

         var tp = vm.f_field_type.TryEval(fld);

         if (tp != null) {

-          return vm.TypeName(tp);

+          var n = vm.TryTypeName(tp);

+          if (n != null)

+            return n;

         }

       }

 

       return "";

     }

 

-    protected override string CanonicalBaseName(Model.Element elt)

+    protected override string CanonicalBaseName(Model.Element elt, out NameSeqSuffix suff)

     {

-      var name = base.CanonicalBaseName(elt);

+      var lit = this.LiteralName(elt);

+      if (lit != null) {

+        suff = NameSeqSuffix.None;

+        return lit;

+      }

+      

+      var name = base.CanonicalBaseName(elt, out suff);

       name = CanonicalBaseNameCore(name, elt);

-      if (viewOpts.DebugMode)

-        name += string.Format("({0})", elt);

+     

       return name;

     }