using System; using System.Collections.Generic; using System.Linq; using System.Text; namespace Microsoft.Boogie.ModelViewer { public class ViewOptions { // 0 - Normal // 1 - Expert // 2 - Everything // 3 - Include the kitchen sink public int ViewLevel = 1; public bool DebugMode; } // sync with Main.categoryBrushes! public enum NodeCategory { Local, PhysField, SpecField, MethodologyProperty, UserFunction, Maplet } public interface ILanguageProvider { bool IsMyModel(Model m); ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts); } public interface ILanguageSpecificModel { string CanonicalName(Model.Element elt); Model.Element FindElement(string canonicalName); string PathName(IEnumerable path); IEnumerable States { get; } // This function is given IDisplayNode possibly from different states. IEnumerable SortFields(IEnumerable fields); } public class SourceViewState { public string Header; public string RichTextContent; public int Location; } public interface IState { string Name { get; } SourceViewState ShowSource(); IEnumerable Nodes { get; } } public interface IDisplayNode { /// /// Used for indexing the state tree. /// string Name { get; } NodeCategory Category { get; } string Value { get; } string ToolTip { get; } int ViewLevel { get; } /// /// Used to determine aliasing. Can be null. /// Model.Element Element { get; } IEnumerable References { get; } IEnumerable Children { get; } object ViewSync { get; set; } } public class TopState : IState { protected IDisplayNode[] children; protected string name; public TopState(string name, IEnumerable nodes) { this.name = name; children = nodes.ToArray(); } public string Name { get { return name; } } public IEnumerable Nodes { get { return children; } } public SourceViewState ShowSource() { return null; } } public abstract class DisplayNode : IDisplayNode { protected EdgeName name; protected Model.Element element; protected ILanguageSpecificModel langModel; protected List children; public DisplayNode(ILanguageSpecificModel model, string n, Model.Element elt) : this(model, new EdgeName(n), elt) {} public DisplayNode(ILanguageSpecificModel model, EdgeName n, Model.Element elt) { langModel = model; name = n; element = elt; } public virtual string ToolTip { get { return null; } } public virtual int ViewLevel { get; set; } public virtual NodeCategory Category { get; set; } public virtual IEnumerable Children { get { if (children == null) { children = new List(); ComputeChildren(); } return children; } } protected virtual void ComputeChildren() { } public object ViewSync { get; set; } public virtual string Name { get { return name.ToString(); } } public virtual Model.Element Element { get { return element; } } public virtual string Value { get { if (element == null) return ""; return langModel.CanonicalName(element); } } public virtual IEnumerable References { get { foreach (var r in name.Dependencies) yield return r; if (element != null) yield return element; } } } public class ContainerNode : DisplayNode { protected Func convert; protected IEnumerable data; public ContainerNode(EdgeName name, Func convert, IEnumerable data) : base(null, name, null) { this.convert = convert; this.data = data; } public ContainerNode(string name, Func convert, IEnumerable data) : this(new EdgeName(name), convert, data) { } protected override void ComputeChildren() { foreach (var f in data) { var res = convert(f); if (res != null) children.Add(res); } } } public static class Util { public static void Assert(bool cond) { if (!cond) throw new System.Exception("assertion violation"); } public static string Concat(this IEnumerable strs, string sep) { var res = new StringBuilder(); foreach (var e in strs) res.Append(e).Append(sep); if (res.Length > 0) res.Length -= sep.Length; return res.ToString(); } public static IEnumerable Empty() { yield break; } public static IEnumerable Singleton(T e) { yield return e; } public static IEnumerable Concat1(this IEnumerable s, T e) { return s.Concat(Singleton(e)); } public static IEnumerable Map(this IEnumerable inp, Func conv) { foreach (var s in inp) yield return conv(s); } public static void Iter(this IEnumerable inp, Action fn) { foreach (var s in inp) fn(s); } public static void AddRange(this HashSet st, IEnumerable elts) { foreach (var e in elts) st.Add(e); } public static T OrElse(T a, T b) where T : class { if (a != null) return a; return b; } public static S GetWithDefault(this Dictionary dict, T key, S defl) { S r; if (dict.TryGetValue(key, out r)) return r; return defl; } } }