Newer
Older
using JsonSubTypes;
using Newtonsoft.Json;
using System.Collections.Generic;
MaZiFAU
committed
using System.Runtime.Serialization;
using System.Text.RegularExpressions;
using static Unity.Burst.Intrinsics.X86;
/// <summary>
/// Implements REST/JSON API
/// </summary>
/// <seealso href="https://github.com/UniFormal/MMT/tree/devel/src/frameit-mmt#rest-api"/>
namespace REST_JSON_API
/// <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
/// <summary>Contains the original scroll.</summary>
[JsonProperty("original")]
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")]
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;
/// <summary>MMT URI</summary>
[JsonProperty("uri")]
John Schihada
committed
John Schihada
committed
{
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")]
MaZiFAU
committed
public string label
MaZiFAU
committed
get => _label ??= Regex.Match(@ref.uri, @".*\?(.*)").Captures[0].Value;
set => _label = value;
MaZiFAU
committed
private string _label;
MaZiFAU
committed
[JsonProperty("ref")]
public FactReference @ref;
public abstract string getType();
public abstract string getApplicant();
}
/// <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;
MaZiFAU
committed
[JsonConstructor]
private MMTGeneralFact() { }
/// <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()
{
MaZiFAU
committed
if (type is OMS oms)
return oms.uri;
if (type is OMA oma)
MaZiFAU
committed
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;
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
}
public override string getApplicant()
{
return defines switch
{
OMA oMA when oMA.applicant is OMS oMS => oMS.uri,
_ => null
};
}
}
/// <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() { }
/// <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 class 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;
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.assignment = new OMS(assignment_id);
John Schihada
committed
public ScrollAssignment(string fact_id, SOMDoc assignment)
{
this.fact = new FactReference(fact_id);
this.assignment = assignment;
}
/// <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")]
/// <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;