From 9a032278736765e35ac825647a994cd66d9be668 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Tue, 12 Oct 2010 01:19:07 +0000
Subject: Add function and constant view

---
 Source/ModelViewer/DataModel.cs | 82 ++++++++++++++++++++++++++++++++++++++++-
 Source/ModelViewer/Main.cs      | 41 ++++++++++++++-------
 2 files changed, 107 insertions(+), 16 deletions(-)

(limited to 'Source/ModelViewer')

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) {
-- 
cgit v1.2.3