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 ++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 80 insertions(+), 2 deletions(-)

(limited to 'Source/ModelViewer/DataModel.cs')

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();
+    }
+  }
+
 }
-- 
cgit v1.2.3