Add find find uses and find aliases facilities

4 files changed, 57 insertions, 5 deletions

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index 5fedf732..33211ef3 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -15,6 +15,8 @@ namespace Microsoft.Boogie.ModelViewer
   {

     string CanonicalName(Model.Element elt);

 

+    Model.Element FindElement(string canonicalName);

+

     string PathName(IEnumerable<IDisplayNode> path);

 

     IEnumerable<IState> States { get; }

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index e8a9df36..5bc18fb2 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -27,7 +27,7 @@ namespace Microsoft.Boogie.ModelViewer
     IEnumerable<ILanguageProvider> Providers()

     {

       yield return Vcc.Provider.Instance;

-      //yield return Dafny.Provider.Instance;

+      yield return Dafny.Provider.Instance;

       yield return Base.Provider.Instance;

     }

 

@@ -302,13 +302,43 @@ namespace Microsoft.Boogie.ModelViewer
 

     private void UpdateMatches(bool force)

     {

-      var words = textBox1.Text.Split(' ').Where(s => s != "").Select(s => s.ToLower()).ToArray();

+      var bad = false;

+      Model.Element eltEq = null;

+      var eltRef = new List<Model.Element>();

+      var words = new List<string>();

+

+      foreach (var w in textBox1.Text.Split(' ')) {

+        if (w == "") continue;

+        if (w.StartsWith("eq:")) {

+          if (eltEq != null) bad = true;

+          else {

+            eltEq = langModel.FindElement(w.Substring(3));

+            if (eltEq == null) bad = true;

+          }

+        } else if (w.StartsWith("ref:")) {

+          var e = langModel.FindElement(w.Substring(4));

+          if (e == null) bad = true;

+          else eltRef.Add(e);

+        } else {

+          words.Add(w.ToLower());

+        }

+      }

+

+      textBox1.ForeColor = bad ? Color.Red : Color.Black;

+      

+      var wordsA = words.ToArray();

+      var refsA = eltRef.ToArray();

+

+      if (eltEq == null && wordsA.Length == 0 && refsA.Length == 0)

+        bad = true;

+

       var changed = force;

       var matches = new List<SkeletonItem>();

+

       foreach (var s in allItems) {

         var newMatch = false;

-        if (s.isPrimary[currentState] && words.Length > 0) {

-          newMatch = s.MatchesWords(words, currentState);

+        if (s.isPrimary[currentState] && !bad) {

+          newMatch = s.MatchesWords(wordsA, refsA, eltEq, currentState);

         }

         if (newMatch)

           matches.Add(s);

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index afbcf4ee..8c36de3c 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -9,6 +9,7 @@ namespace Microsoft.Boogie.ModelViewer
   {

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

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

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

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

 

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

@@ -62,9 +63,18 @@ namespace Microsoft.Boogie.ModelViewer
         baseNameUse[baseName] = cnt;

       }

       canonicalName.Add(elt, res);

+      invCanonicalName.Add(res, elt);

       return res;

     }

 

+    public virtual Model.Element FindElement(string canonicalName)

+    {

+      Model.Element res;

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

+        return res;

+      return null;

+    }

+    

     public virtual string PathName(IEnumerable<IDisplayNode> path)

     {

       return path.Select(n => n.Name).Concat(".");

diff --git a/Source/ModelViewer/TreeSkeleton.cs b/Source/ModelViewer/TreeSkeleton.cs
index b7a83dee..00273dd1 100644
--- a/Source/ModelViewer/TreeSkeleton.cs
+++ b/Source/ModelViewer/TreeSkeleton.cs
@@ -149,17 +149,27 @@ namespace Microsoft.Boogie.ModelViewer
       }

     }

 

-    public bool MatchesWords(string[] words, int stateId)

+    public bool MatchesWords(string[] words, Model.Element[] elts, Model.Element eq, int stateId)

     {

       var node = displayNodes[stateId];

       if (node == null)

         return false;

       var s1 = node.Name.ToLower();

       var s2 = node.Value.ToLower();

+

+      if (eq != null && node.Element != eq)

+        return false;

+

       foreach (var w in words) {

         if (!s1.Contains(w) && !s2.Contains(w))

           return false;

       }

+

+      foreach (var e in elts) {

+        if (!node.References.Contains(e))

+          return false;

+      }

+

       return true;

     }

   }