Refactor the Namer into two classes

1 files changed, 39 insertions, 38 deletions

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 9832bff1..8eb9f331 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -23,15 +23,13 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         vm.states.Add(sn);

       }

       foreach (var s in vm.states) s.ComputeNames();

-      for (int i = 0; i < 1; i++) {

-        Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer));

-      }

+      vm.gn.ComputeCanonicalNames();

       return vm.states;

     }

 

     public IEnumerable<string> SortFields(IEnumerable<string> fields)

     {

-      return Namer.DefaultSortFields(fields);

+      return GlobalNamer.DefaultSortFields(fields);

     }

 

   }

@@ -44,8 +42,9 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     Map

   }

 

-  class VccModel

+  class VccModel : INamerCallbacks

   {

+    public readonly GlobalNamer gn;

     public readonly Model model;

     public readonly Model.Func f_ptr_to, f_phys_ptr_cast, f_spec_ptr_cast, f_mathint, f_local_value_is, f_spec_ptr_to, f_heap, f_select_field,

                                f_select_value, f_field, f_field_type, f_int_to_ptr, f_ptr_to_int, f_ptr, f_map_t;

@@ -54,6 +53,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

     public VccModel(Model m)

     {

+      gn = new GlobalNamer(this);

       model = m;

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

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

@@ -272,21 +272,52 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

       return result;

     }

+

+    public string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)

+    {

+      var vm = this;

+      var name = GlobalNamer.DefaultCanonicalBaseName(elt, edgeName, stateIdx);

+

+      if (name.Contains("[") || name.Contains("'") || name.Contains("-"))

+        name = "";

+

+      if (name != "")

+        return name;

+

+      foreach (var tpl in elt.References) {

+        var fn = tpl.Func;

+        if (fn.Name.StartsWith("$select.$map_t") && fn.Arity == 2 && tpl.Args[0] == elt)

+          return "map";

+        if (fn.Name.StartsWith("$int_to_map_t") && tpl.Result == elt)

+          return "map";

+      }

+

+      var fld = vm.f_field.TryEval(elt);

+      if (fld != null) {

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

+        if (tp != null) {

+          return vm.TypeName(tp);

+        }

+      }

+

+      // return elt.ToString(); // for debugging

+      return "";

+    }

   }

 

-  class StateNode : IState, INamerCallbacks

+  class StateNode : IState

   {

     internal Model.CapturedState state;

     string name;

     internal VccModel vm;

     internal List<VariableNode> vars;

-    internal Namer namer;

+    internal StateNamer namer;

     internal int index;

     

     public StateNode(int i, VccModel parent, Model.CapturedState s)

     {

-      this.namer = new Namer(this);

       this.vm = parent;

+      this.namer = new StateNamer(vm.gn);

       state = s;

       index = i;

 

@@ -308,36 +339,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       SetupVars();

     }

 

-    public string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)

-    {

-      var name = Namer.DefaultCanonicalBaseName(elt, edgeName, stateIdx);

-

-      if (name.Contains("[") || name.Contains("'") || name.Contains("-"))

-        name = "";

-

-      if (name != "")

-        return name;

-

-      foreach (var tpl in elt.References) {

-        var fn = tpl.Func;

-        if (fn.Name.StartsWith("$select.$map_t") && fn.Arity == 2 && tpl.Args[0] == elt)

-          return "map";

-        if (fn.Name.StartsWith("$int_to_map_t") && tpl.Result == elt)

-          return "map";

-      }

-

-      var fld = vm.f_field.TryEval(elt);

-      if (fld != null) {

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

-        if (tp != null) {

-          return vm.TypeName(tp);

-        }

-      }

-

-      // return elt.ToString(); // for debugging

-      return "";

-    }

-

     void SetupVars()

     {

       if (vars != null) return;