Newer
Older
using JsonSubTypes;
using Newtonsoft.Json;
using System.Collections.Generic;
public class Scroll
John Schihada
committed
public string @ref;
public string label;
public string description;
public List<ScrollFact> requiredFacts;
John Schihada
committed
public string scroll;
public List<ScrollAssignment> assignments;
John Schihada
committed
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 abstract String getType();
public abstract String getApplicant();
public class UriReference
{
public string uri;
John Schihada
committed
public UriReference(string uri)
{
this.uri = uri;
}
/**
* Class used for deserializing incoming symbol-declarations from mmt
*/
public class ScrollSymbolFact : ScrollFact
{
public MMTTerm tp;
public MMTTerm df;
public override String getType()
{
if (this.tp is OMS oMS)
return oMS.uri;
else if (this.tp is OMA oMA)
return ((OMS)((OMA) oMA.arguments[0]).applicant).uri;
else
return 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;
if (this.df is OMA && ((OMA)this.df).applicant is OMS)
return ((OMS)((OMA)this.df).applicant).uri;
return null ;// ((OMS)((OMA)((OMA)this.df).arguments[0]).applicant).uri;
}
}
/**
* Class used for deserializing incoming value-declarations from mmt
*/
public class ScrollValueFact : ScrollFact
public MMTTerm lhs;
public MMTTerm valueTp;
public MMTTerm value;
public MMTTerm proof;
public override String getType()
{
if (this.lhs is OMA & (((OMA)this.lhs).applicant is OMS))
return ((OMS)((OMA)this.lhs).applicant).uri;
else
return null;
}
public override String getApplicant()
{
// TODO Test this
if (this.lhs is OMA & (((OMA)this.lhs).applicant is OMS))
return ((OMS)((OMA)this.lhs).applicant).uri;
return null;
}
John Schihada
committed
public class ScrollAssignment
{
public UriReference fact;
public OMS assignment;
John Schihada
committed
}
public class ScrollApplicationInfo
{
public Boolean valid;
public ScrollApplicationCheckingError[] errors;
public List<Scroll.ScrollFact> acquiredFacts;
}
public class ScrollDynamicInfo
{
public Scroll original;
public Scroll rendered;
John Schihada
committed
public List<List<Scroll.ScrollAssignment>> completions;
public Boolean valid;
public ScrollApplicationCheckingError[] errors;
}
public class ScrollApplicationCheckingError
{
public String kind;
public string msg;
public MMTTerm fact;
}