summaryrefslogtreecommitdiff
path: root/Source/ModelViewer/BaseProvider.cs
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2010-11-06 01:20:53 +0000
committerGravatar MichalMoskal <unknown>2010-11-06 01:20:53 +0000
commitb7c15131d88f175dde213522e4509e1e21eeeb41 (patch)
treec060a52ff50329aa1fca12d324c614a4ba4dbff7 /Source/ModelViewer/BaseProvider.cs
parentac7906f4e1f400bbc1514b3576db2a4484021db0 (diff)
Simplify languague-specific interface
Diffstat (limited to 'Source/ModelViewer/BaseProvider.cs')
-rw-r--r--Source/ModelViewer/BaseProvider.cs87
1 files changed, 36 insertions, 51 deletions
diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index c4bae59e..8875cce6 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -15,22 +15,39 @@ namespace Microsoft.Boogie.ModelViewer.Base
return true;
}
- IEnumerable<IDisplayNode> GetStateNodes(Model m)
+ public ILanguageSpecificModel GetLanguageSpecificModel(Model m)
{
- yield return GenericNodes.Functions(m);
- yield return GenericNodes.Constants(m);
- foreach (var s in m.States)
- yield return new StateNode(s);
+ return new GenericModel(m);
+ }
+ }
+
+ public class GenericModel : LanguageModel
+ {
+ Model m;
+
+ public GenericModel(Model m)
+ {
+ this.m = m;
}
- public IEnumerable<IState> GetStates(Model m)
+ public IDisplayNode Function(Model.Func f)
{
- yield return new TopState("TOP", GetStateNodes(m));
+ return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(this, a), f.Apps);
}
- public IEnumerable<string> SortFields(IEnumerable<string> fields)
+ IEnumerable<IDisplayNode> GetStateNodes()
{
- return GlobalNamer.DefaultSortFields(fields);
+ yield return new ContainerNode<Model.Func>("Functions", f => f.Arity == 0 ? null : Function(f), m.Functions);
+ yield return new ContainerNode<Model.Func>("Constants", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.Functions);
+ foreach (var s in m.States)
+ yield return new StateNode(this, s);
+ }
+
+ public override IEnumerable<IState> States
+ {
+ get {
+ yield return new TopState("TOP", GetStateNodes());
+ }
}
}
@@ -38,73 +55,41 @@ namespace Microsoft.Boogie.ModelViewer.Base
{
protected Model.CapturedState state;
- public StateNode(Model.CapturedState s) : base(s.Name)
+ public StateNode(ILanguageSpecificModel p, Model.CapturedState s) : base(p, s.Name, null)
{
state = s;
}
- public override IEnumerable<string> Aliases
+ public override string Value
{
- get { foreach (var v in state.Variables) yield return v; }
+ get {
+ return state.Variables.Concat(", ");
+ }
}
- public override bool Expandable { get { return state.VariableCount != 0; } }
-
- public override IEnumerable<IDisplayNode> Expand()
+ protected override void ComputeChildren()
{
foreach (var v in state.Variables) {
- yield return new ElementNode(v, state.TryGet(v));
+ children.Add(new ElementNode(langModel, v, state.TryGet(v)));
}
}
}
public class ElementNode : DisplayNode
{
- protected Model.Element elt;
-
- public ElementNode(string name, Model.Element elt) : base(name)
- {
- this.elt = elt;
- }
-
- public override IEnumerable<string> Aliases
- {
- get
- {
- if (!(elt is Model.Uninterpreted))
- yield return elt.ToString();
- foreach (var tupl in elt.Names) {
- if (tupl.Func.Arity == 0)
- yield return tupl.Func.Name;
- }
- }
- }
+ public ElementNode(ILanguageSpecificModel p, string name, Model.Element elt) : base(p, name, elt) {}
}
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)
+ public AppNode(ILanguageSpecificModel m, Model.FuncTuple t)
+ : base(m, t.Func.Name, t.Result)
{
tupl = t;
var sb = new StringBuilder();