Select Git revision
Endpoints.cs
Endpoints.cs 12.10 KiB
using JsonSubTypes;
using Newtonsoft.Json;
using System.Collections.Generic;
using System.Linq;
using System.Text.RegularExpressions;
using static JSONsavable;
/// <summary>
/// Implements REST/JSON API
/// </summary>
/// <seealso href="https://github.com/UniFormal/MMT/tree/devel/src/frameit-mmt#rest-api"/>
namespace REST_JSON_API
{
public class ScrollApplicationInfo
{
/// <remarks>Invariant: <see cref="valid"/> == <c>false</c> => <see cref="errors"/><c>.Length > 0</c></remarks>
[JsonProperty("valid")]
public bool valid;
[JsonProperty("errors")]
public ScrollApplicationCheckingError[] errors;
[JsonProperty("acquiredFacts")]
public List<MMTFact> acquiredFacts;
}
/// <summary>Response to "POST /scroll/dynamic" using <see cref="ScrollApplication"/></summary>
public class ScrollDynamicInfo : IJSONsavable<ScrollDynamicInfo>
{
/// <summary>Contains the original scroll.</summary>
[JsonProperty("original"), JsonAutoPostProcess]
public Scroll original;
/// <summary>All fact and scroll labels, all fact types, and all fact definitions are subject to being dynamically adapted to the (possibly utterly partial) scroll application.</summary>
/// <remarks>Contains <see cref="Scroll.requiredFacts"/> inferred/forward hints (A,B,C => °ABC)</remarks>
[JsonProperty("rendered"), JsonAutoPostProcess]
public Scroll rendered;
/// <summary>
/// An array of scroll view completion suggestions for the yet missing assignments.
/// For instance, the first element of completions might be a list of some (possibly not all) of the yet missing assignments of the request's scroll view.
/// Analogously for the other elements of completions, if they exist.
/// It might happen that multiple mutually exclusive completions exist, hence the response contains an array of them.
/// </summary>
/// <remarks>Contains backwart hints (°ABC => A,B,C)</remarks>
[JsonProperty("completions")]
public List<List<ScrollAssignment>> backward_completions;
/// <remarks>Invariant: <see cref="valid"/> == <c>false</c> => <see cref="errors"/><c>.Length > 0</c></remarks>
[JsonProperty("valid")]
public bool valid;
[JsonProperty("errors")]
public ScrollApplicationCheckingError[] errors;
public string name { get => throw new System.NotImplementedException(); set => throw new System.NotImplementedException(); }
public string path { get => throw new System.NotImplementedException(); set => throw new System.NotImplementedException(); }
}
public class FactReference
{
/// <summary>MMT URI</summary>
[JsonProperty("uri")]
public string uri;
public FactReference(string uri)
{
this.uri = uri;
}
}
[JsonConverter(typeof(JsonSubtypes), "kind")]
[JsonSubtypes.KnownSubType(typeof(MMTGeneralFact), "general")]
[JsonSubtypes.KnownSubType(typeof(MMTValueFact), "veq")]
public abstract class MMTFact
{
[JsonProperty("kind")]
public abstract string kind { get; }
[JsonProperty("label")]
public string label
{
get => _label ??= Regex.Match(@ref.uri, @".*\?(.*)").Captures[0].Value;
set => _label = value;
}
private string _label;
[JsonProperty("ref")]
public OMS @ref;
public abstract string getType();
public abstract string getApplicant();
public abstract SOMDoc GetDefines();
public abstract MMTFact MapURIs(Dictionary<string, string> old_to_new);
public abstract string[] GetDependentFactIds();
public static bool Equivalent(MMTFact f1, MMTFact f2)
=> f1.Equivalent(f2);
public bool Equivalent(MMTFact f2)
=> this.getType().Equals(f2.getType())
&& EquivalentWrapped(this, f2);
protected abstract bool EquivalentWrapped(MMTFact f1, MMTFact f2);
public abstract SOMDoc GetMMTType();
public new abstract string ToString();
}
/// <summary>Class for facts without values, e.g. Points</summary>
public class MMTGeneralFact : MMTFact
{
public override string kind => "general";
[JsonProperty("tp")]
public SOMDoc type;
[JsonProperty("df")]
public SOMDoc defines;
[JsonConstructor]
private MMTGeneralFact(OMS @ref, string label, SOMDoc type, SOMDoc defines)
{
this.@ref = @ref;
this.label = label;
this.type = type;
this.defines = defines;
}
/// <summary>Constructor used for sending new declarations to mmt</summary>
public MMTGeneralFact(string label, SOMDoc type, SOMDoc defines)
{
this.label = label;
this.type = type;
this.defines = defines; }
public override string getType()
{
if (type is OMS oms)
return oms.uri;
if (type is OMA oma)
{
if (oma.applicant is OMS ded
&& ded.uri == MMTConstants.Ded)
return ((oma.arguments[0] as OMA)
.applicant as OMS).uri;
else
return (oma
.applicant as OMS).uri;
}
if (type is FUNTYPE)
return MMTConstants.FunctionFact;
return null;
}
public override string getApplicant()
{
return defines switch
{
OMA oMA when oMA.applicant is OMS oMS => oMS.uri,
_ => null
};
}
public override MMTFact MapURIs(Dictionary<string, string> old_to_new)
=> new MMTGeneralFact(@ref, label, type.MapURIs(old_to_new), defines.MapURIs(old_to_new));
public override SOMDoc GetDefines() => defines;
public override string[] GetDependentFactIds()
=> type.GetDependentFactIds().ShallowCloneAppend(defines.GetDependentFactIds());
protected override bool EquivalentWrapped(MMTFact f1, MMTFact f2)
{
MMTGeneralFact g1 = (MMTGeneralFact)f1;
MMTGeneralFact g2 = (MMTGeneralFact)f2;
return g1.type.Equivalent(g2.type)
&& g1.defines.Equivalent(g2.defines);
}
public override SOMDoc GetMMTType()
=> type;
public override string ToString()
=> $"[{type}]: {defines}";
}
/// <summary>Class for facts with values, e.g. Distances or Angles</summary>
public class MMTValueFact : MMTFact
{
public override string kind => "veq";
[JsonProperty("lhs")]
public SOMDoc lhs;
[JsonProperty("valueTp")]
public SOMDoc valueType;
[JsonProperty("value")]
public SOMDoc value;
[JsonProperty("proof")]
public SOMDoc proof;
[JsonConstructor]
private MMTValueFact(OMS @ref, string label, SOMDoc lhs, SOMDoc valueType, SOMDoc value, SOMDoc proof = null)
{
this.@ref = @ref;
this.label = label;
this.lhs = lhs;
this.valueType = valueType;
this.value = value;
this.proof = proof;
}
/// <summary>Constructor used for sending new declarations to mmt</summary>
public MMTValueFact(string label, SOMDoc lhs, SOMDoc valueType, SOMDoc value, SOMDoc proof = null)
{
this.label = label;
this.lhs = lhs;
this.valueType = valueType;
this.value = value;
this.proof = proof;
}
public override string getType()
{
return lhs switch
{
OMA oMA when oMA.applicant is OMS oMS => oMS.uri,
_ => null
};
}
public override string getApplicant()
{
return lhs switch
{
OMA oMA when oMA.applicant is OMS oMS => oMS.uri,
_ => null
};
}
public override MMTFact MapURIs(Dictionary<string, string> old_to_new)
=> new MMTValueFact(@ref, label,
lhs.MapURIs(old_to_new),
valueType.MapURIs(old_to_new),
value.MapURIs(old_to_new),
proof.MapURIs(old_to_new)
);
public override SOMDoc GetDefines() => value;
public override string[] GetDependentFactIds()
=> lhs.GetDependentFactIds().ShallowCloneAppend(value.GetDependentFactIds());
protected override bool EquivalentWrapped(MMTFact f1, MMTFact f2)
{
MMTValueFact g1 = (MMTValueFact)f1;
MMTValueFact g2 = (MMTValueFact)f2;
return g1.lhs.Equivalent(g2.lhs)
&& g1.value.Equivalent(g2.value);
}
public override SOMDoc GetMMTType()
{
throw new System.NotImplementedException();
}
public override string ToString()
=> $"<{lhs}> == <{value}>";
}
public class Scroll: IJSONsavable<Scroll>
{
/// <summary>MMT URI to theory declaring the scroll</summary>
[JsonProperty("ref")]
public string ScrollReference;
/// <summary>"some label"</summary>
[JsonProperty("label")]
public string label;
/// <summary>"some description"</summary>
[JsonProperty("description")]
public string description;
/// <summary>array of facts; facts that the scroll required you to give for scroll application</summary>
[JsonProperty("requiredFacts")]
public List<MMTFact> requiredFacts;
/// <summary>array of facts; facts that the scroll gives you upon successful scroll application</summary>
[JsonProperty("acquiredFacts")]
public List<MMTFact> acquiredFacts;
#region IJSONsavable<Scroll>
public string name { get => throw new System.NotImplementedException(); set => throw new System.NotImplementedException(); }
public string path { get => throw new System.NotImplementedException(); set => throw new System.NotImplementedException(); }
Scroll IJSONsavable<Scroll>._IJPostProcess(Scroll payload)
{
// remove already defined facts
payload.requiredFacts = payload.requiredFacts
.Where(f => f.GetDefines() == null)
.ToList();
return payload;
}
#endregion IJSONsavable<Scroll>
}
public class ScrollAssignment
{
[JsonProperty("fact")]
public FactReference fact; // Key
[JsonProperty("assignment")]
public SOMDoc assignment; // Value
[JsonConstructor]
private ScrollAssignment() { }
public ScrollAssignment(string fact_id, string assignment_id)
{
this.fact = new FactReference(fact_id);
this.assignment = new OMS(assignment_id);
}
public ScrollAssignment(string fact_id, SOMDoc assignment)
{
this.fact = new FactReference(fact_id);
this.assignment = assignment;
}
}
public class ScrollApplication
{
/// <summary>MMT URI to theory declaring the scroll</summary>
[JsonProperty("scroll")] public string ScrollReference;
[JsonProperty("assignments")]
public List<ScrollAssignment> assignments;
public ScrollApplication(string scroll, List<ScrollAssignment> assignments)
{
this.ScrollReference = scroll;
this.assignments = assignments;
}
}
public class ScrollApplicationCheckingError
{
/// <summary>"invalidAssignment" | "unknown"</summary>
/// <remarks>above list maybe incomplete</remarks>
[JsonProperty("kind")]
public string kind;
/// <summary>some human-readable message</summary>
[JsonProperty("msg")]
public string msg;
/// <summary>a fact reference to the fact whose assignment was erroneous</summary>
[JsonProperty("fact")]
public FactReference fact;
}
}