diff options
| author |  MichalMoskal <unknown> | 2010-10-12 01:19:07 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2010-10-12 01:19:07 +0000 |
| commit | 9a032278736765e35ac825647a994cd66d9be668 (patch) | |
| tree | cf7591880ed8ae12ed9099389140726708b1d2b0 /Source/ModelViewer/DataModel.cs | |
| parent | 15e2fa869e98fdd7900a422aa78bb034d39bfe37 (diff) | |
Add function and constant view
Diffstat (limited to 'Source/ModelViewer/DataModel.cs')
| -rw-r--r-- | Source/ModelViewer/DataModel.cs | 82 |
1 files changed, 80 insertions, 2 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();
+ }
+ }
+
}
|