Add function and constant view

3 files changed, 108 insertions, 16 deletions

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index f2250e0f..7ccf5d54 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -25,12 +25,12 @@ namespace Microsoft.Boogie.ModelViewer
 

     public virtual string Name

     {

-      get { return "State"; }

+      get { return state.Name; }

     }

 

     public virtual IEnumerable<string> Values

     {

-      get { yield return state.Name; }

+      get { foreach (var v in state.Variables) yield return v; }

     }

 

     public virtual bool Expandable { get { return state.VariableCount != 0; } }

@@ -79,4 +79,82 @@ namespace Microsoft.Boogie.ModelViewer
 

     public object ViewSync { get; set; }

   }

+

+

+  public class ContainerNode<T> : IDisplayNode

+  {

+    protected string name;

+    protected Func<T, IDisplayNode> convert;

+    protected IEnumerable<T> data;

+

+    public ContainerNode(string name, Func<T, IDisplayNode> convert, IEnumerable<T> data)

+    {

+      this.name = name;

+      this.convert = convert;

+      this.data = data;

+    }

+

+    public virtual string Name

+    {

+      get { return name; }

+    }

+

+    public virtual IEnumerable<string> Values

+    {

+      get { yield break; }

+    }

+

+    public virtual bool Expandable { get { return true; } }

+

+    public virtual IEnumerable<IDisplayNode> Expand()

+    {

+      foreach (var f in data) {

+        var res = convert(f);

+        if (res != null)

+          yield return res;

+      }

+    }

+

+    public object ViewSync { get; set; }

+  }

+

+  public static class GenericNodes

+  {

+    public static IDisplayNode Function(Model.Func f)

+    {

+      return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(a), f.Apps);

+    }

+

+    public static IDisplayNode Functions(Model m)

+    {

+      return new ContainerNode<Model.Func>("Functions", f => f.Arity == 0 ? null : Function(f), m.Functions);

+    }

+

+    public static IDisplayNode Constants(Model m)

+    {

+      return new ContainerNode<Model.Func>("Constants", f => f.Arity != 0 ? null : new AppNode(f.Apps.First()), m.Functions);

+    }

+  }

+

+  public class AppNode : ElementNode

+  {

+    protected Model.FuncTuple tupl;

+

+    public AppNode(Model.FuncTuple t)

+      : base(t.Func.Name, t.Result)

+    {

+      tupl = t;

+      var sb = new StringBuilder();

+      sb.Append(t.Func.Name);

+      if (t.Args.Length > 0) {

+        sb.Append("(");

+        foreach (var a in t.Args)

+          sb.Append(a.ToString()).Append(", ");

+        sb.Length -= 2;

+        sb.Append(")");

+      }

+      name = sb.ToString();

+    }

+  }

+

 }

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 8d06a9a0..6a19b357 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -30,6 +30,8 @@ namespace Microsoft.Boogie.ModelViewer
       }

 

       var items = new List<ListViewItem>();

+      items.Add(new DisplayItem(GenericNodes.Functions(m)));

+      items.Add(new DisplayItem(GenericNodes.Constants(m)));

       foreach (var s in m.States)

         items.Add(new DisplayItem(new StateNode(s)));

       listView1.Items.AddRange(items.ToArray());

@@ -48,7 +50,9 @@ namespace Microsoft.Boogie.ModelViewer
     }

 

     const int levelMult = 10;

-    const int plusWidth = 17;

+    const int plusWidth = 16;

+

+    static StringFormat center = new StringFormat() { Alignment = StringAlignment.Center };

     

     private void listView1_DrawItem(object sender, DrawListViewItemEventArgs e)

     {

@@ -70,22 +74,31 @@ namespace Microsoft.Boogie.ModelViewer
       var plusRect = rect;

       plusRect.Width = plusWidth;

       plusRect.X += off;

-      e.Graphics.FillRectangle(Brushes.Gray, plusRect);

+      var plusBorder = plusRect;

+      plusBorder.Height -= 4;

+      plusBorder.Width -= 4;

+      plusBorder.X += 2;

+      plusBorder.Y += 2;

+      e.Graphics.FillRectangle(Brushes.BlueViolet, plusBorder);

       // TODO these should be icons

-      e.Graphics.DrawString(item.expanded ? "[-]" : "[+]", listView1.Font, Brushes.Black, plusRect); // , StringFormat.GenericDefault);

+      if (item.displayNode.Expandable)

+        e.Graphics.DrawString(item.expanded ? "-" : "+", listView1.Font, Brushes.Black, plusRect, center);

 

       off += plusWidth + 3;

-      var valRect = rect;

-      valRect.Width = listView1.Columns[0].Width - 1 - off;

-      if (valRect.Width > 10) {

-        valRect.X += off;

-        e.Graphics.DrawString(item.displayNode.Name, listView1.Font, textBrush, valRect); // , StringFormat.GenericDefault);

-      }

-

       var nameRect = rect;

-      nameRect.Width = listView1.Columns[1].Width - 1;

-      nameRect.X += listView1.Columns[0].Width + 1;

-      e.Graphics.DrawString(item.SubItems[1].Text, listView1.Font, textBrush, nameRect); // , StringFormat.GenericDefault);

+      var font = listView1.Font;

+

+      var sz = e.Graphics.MeasureString(item.displayNode.Name, font);

+      nameRect.Width = listView1.Columns[0].Width - 1 - off;

+      if (nameRect.Width < sz.Width + 2)

+        nameRect.Width = (int)sz.Width + 20;

+      nameRect.X += off;

+      e.Graphics.DrawString(item.displayNode.Name, font, textBrush, nameRect);

+      

+      var valRect = rect;

+      valRect.X = nameRect.X + nameRect.Width + 4;

+      valRect.Width = listView1.Width - valRect.X;

+      e.Graphics.DrawString(item.SubItems[1].Text, font, textBrush, valRect); // , StringFormat.GenericDefault);

     }

 

     private void listView1_DrawSubItem(object sender, DrawListViewSubItemEventArgs e)

@@ -110,7 +123,7 @@ namespace Microsoft.Boogie.ModelViewer
         clickedItem.Focused = true;

 

         int plusLoc = clickedItem.level * levelMult;

-        if (e.X >= plusLoc && e.X <= plusLoc + plusWidth) {

+        if (clickedItem.displayNode.Expandable && e.X >= plusLoc && e.X <= plusLoc + plusWidth) {

           clickedItem.expanded = !clickedItem.expanded;

 

           if (clickedItem.expanded) {

diff --git a/Source/VCGeneration/Model.cs b/Source/VCGeneration/Model.cs
index d2d9cc24..5e4a0a0f 100644
--- a/Source/VCGeneration/Model.cs
+++ b/Source/VCGeneration/Model.cs
@@ -99,6 +99,7 @@ namespace Microsoft.Boogie
       public readonly int Arity;

       internal readonly List<FuncTuple> apps = new List<FuncTuple>();

       public IEnumerable<FuncTuple> Apps { get { return apps; } }

+      public int AppCount { get { return apps.Count; } }

 

       internal Func(Model p, string n, int a) { Model = p;  Name = n; Arity = a; }