using JsonSubTypes; using Newtonsoft.Json; using System; using System.Collections.Generic; using static SOMDocManager; public class Scroll { public string @ref; public string label; public string description; public List<ScrollFact> requiredFacts; public List<ScrollFact> acquiredFacts; public class FilledScroll { public string scroll; public List<ScrollAssignment> assignments; public FilledScroll(string scroll, List<ScrollAssignment> assignments) { this.scroll = scroll; this.assignments = assignments; } } public class ScrollTheoryReference { public string problemTheory; public string solutionTheory; } [JsonConverter(typeof(JsonSubtypes), "kind")] [JsonSubtypes.KnownSubType(typeof(ScrollSymbolFact), "general")] [JsonSubtypes.KnownSubType(typeof(ScrollValueFact), "veq")] public abstract class ScrollFact { public string kind; public UriReference @ref; public string label; public abstract String getType(); public abstract String getApplicant(); } public class UriReference { public string uri; public UriReference(string uri) { this.uri = uri; } } /** * Class used for deserializing incoming symbol-declarations from mmt */ public class ScrollSymbolFact : ScrollFact { public SOMDoc tp; public SOMDoc df; public override String getType() { return tp switch { OMS oMS => oMS.uri, OMA oMA => ((oMA.arguments[0] as OMA).applicant as OMS).uri, _ => null }; } public override String getApplicant() { //Debug.Log(" Check " + this.tp is OMS + " and " + this.tp is OMA + " and " + this.tp is OMSTR + " or " + this.tp is OMF); // return ((OMS)((OMA)((OMA)this.tp).arguments[0]).arguments[0]).uri; return df switch { OMA oMA when oMA.applicant is OMS oMS => oMS.uri, _ => null // ((OMS)((OMA)((OMA)this.df).arguments[0]).applicant).uri; }; } } /** * Class used for deserializing incoming value-declarations from mmt */ public class ScrollValueFact : ScrollFact { public SOMDoc lhs; public SOMDoc valueTp; public SOMDoc value; public SOMDoc proof; public override String getType() { return lhs switch { OMA oMA when oMA.applicant is OMS oMS => oMS.uri, _ => null }; } public override String getApplicant() { // TODO Test this return lhs switch { OMA oMA when oMA.applicant is OMS oMS => oMS.uri, _ => null }; } } public class ScrollAssignment { public UriReference fact; public OMS assignment; } public class ScrollApplicationInfo { public Boolean valid; public ScrollApplicationCheckingError[] errors; public List<Scroll.ScrollFact> acquiredFacts; } public class ScrollDynamicInfo { public Scroll original; public Scroll rendered; public List<List<Scroll.ScrollAssignment>> completions; public Boolean valid; public ScrollApplicationCheckingError[] errors; } public class ScrollApplicationCheckingError { public String kind; public string msg; public SOMDoc fact; } }