Scroll.cs

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;
    }

}