Skip to content
Snippets Groups Projects
Commit d2767df8 authored by MaZiFAU's avatar MaZiFAU
Browse files

Refactored parseFact I

parent fbffc500
No related branches found
No related tags found
No related merge requests found
Showing
with 5271 additions and 5373 deletions
...@@ -15,11 +15,11 @@ public class FactObject : MonoBehaviour, ISerializationCallbackReceiver ...@@ -15,11 +15,11 @@ public class FactObject : MonoBehaviour, ISerializationCallbackReceiver
public string URI; public string URI;
/// <summary> /// <summary>
/// Shorthand and Cache for <see cref="Fact.TryGetGlobalFact(string, out Fact)"/>. /// Shorthand and Cache for <see cref="FactOrganizer.AllFacts.TryGetValue(string, out Fact)"/>.
/// </summary> /// </summary>
public Fact Fact { public Fact Fact {
get { get {
if (_Fact == null) Fact.TryGetGlobalFact(URI, out _Fact); if (_Fact == null) FactOrganizer.AllFacts.TryGetValue(URI, out _Fact);
return _Fact; return _Fact;
} }
set { _Fact = value; URI = value.Id; } set { _Fact = value; URI = value.Id; }
......
using System.Collections.Generic; using System.Collections.Generic;
using System.Reflection;
using System.IO;
using Newtonsoft.Json; using Newtonsoft.Json;
using System.Collections;
using UnityEngine; using UnityEngine;
using System.Linq; using System.Linq;
using System; using System;
using static CommunicationEvents;
using UnityEditor.Experimental.GraphView;
using UnityEngine.InputSystem.Utilities; using UnityEngine.InputSystem.Utilities;
using UnityEngine.Rendering.VirtualTexturing; using static CommunicationEvents;
using System.Collections.ObjectModel;
using System.Xml.Linq;
//TODO: MMT: move some functionality there //TODO: MMT: move some functionality there
//TODO: consequent!= samestep != dependent //TODO: consequent!= samestep != dependent
......
...@@ -166,7 +166,6 @@ public void SpawnCircle(CircleFact circleFact, Transform parent = null) ...@@ -166,7 +166,6 @@ public void SpawnCircle(CircleFact circleFact, Transform parent = null)
circle.transform.localScale = Vector3.Scale(circle.transform.localScale, circleFact.LocalScale); circle.transform.localScale = Vector3.Scale(circle.transform.localScale, circleFact.LocalScale);
} }
public void DeleteObject(Fact fact) public void DeleteObject(Fact fact)
=> GameObject.Destroy(fact.Representation); => GameObject.Destroy(fact.Representation);
......
...@@ -173,21 +173,21 @@ protected override MMTDeclaration MakeMMTDeclaration() ...@@ -173,21 +173,21 @@ protected override MMTDeclaration MakeMMTDeclaration()
if (fact is not MMTValueDeclaration value_fact) //If angle is a 90Degree-Angle if (fact is not MMTValueDeclaration value_fact) //If angle is a 90Degree-Angle
throw new ArgumentException("Angle 90 degrees parsed. This shouldn't happen anymore"); throw new ArgumentException("Angle 90 degrees parsed. This shouldn't happen anymore");
if (value_fact.lhs is not OMA df) if (value_fact.lhs is not OMA lhs)
return null; return null;
float angle = value_fact.value == null float angle = value_fact.value == null
? 0f ? 0f
: ((OMF)value_fact.value).f; : ((OMF)value_fact.value).@float;
string pointAUri = ((OMS)df.arguments[0]).uri; string pointAUri = ((OMS)lhs.arguments[0]).uri;
string pointBUri = ((OMS)df.arguments[1]).uri; string pointBUri = ((OMS)lhs.arguments[1]).uri;
string pointCUri = ((OMS)df.arguments[2]).uri; string pointCUri = ((OMS)lhs.arguments[2]).uri;
if (!StageStatic.stage.factState.ContainsKey(pointAUri) if (!FactOrganizer.AllFacts.ContainsKey(pointAUri)
|| !StageStatic.stage.factState.ContainsKey(pointBUri) || !FactOrganizer.AllFacts.ContainsKey(pointBUri)
|| !StageStatic.stage.factState.ContainsKey(pointCUri)) || !FactOrganizer.AllFacts.ContainsKey(pointCUri))
return null; //If dependent facts do not exist return null return null;
return new AngleFact(pointAUri, pointBUri, pointCUri, angle, fact.@ref.uri, StageStatic.stage.factState); return new AngleFact(pointAUri, pointBUri, pointCUri, angle, fact.@ref.uri, StageStatic.stage.factState);
} }
...@@ -274,7 +274,7 @@ protected override MMTDeclaration MakeMMTDeclaration() ...@@ -274,7 +274,7 @@ protected override MMTDeclaration MakeMMTDeclaration()
/// \copydoc Fact.parseFact(ScrollFact) /// \copydoc Fact.parseFact(ScrollFact)
public new static RightAngleFact parseFact(MMTDeclaration fact) public new static RightAngleFact parseFact(MMTDeclaration fact)
{ {
if (((MMTSymbolDeclaration)fact).tp if (((MMTSymbolDeclaration)fact).type
is not OMA proof_OMA // proof DED is not OMA proof_OMA // proof DED
|| proof_OMA.arguments[0] || proof_OMA.arguments[0]
is not OMA rightAngleOMA // rightAngle OMA is not OMA rightAngleOMA // rightAngle OMA
...@@ -287,10 +287,10 @@ is not OMS // rightAngle Arg0 ...@@ -287,10 +287,10 @@ is not OMS // rightAngle Arg0
string Point2Uri = ((OMS)rightAngleOMA.arguments[1]).uri; string Point2Uri = ((OMS)rightAngleOMA.arguments[1]).uri;
string Point3Uri = ((OMS)rightAngleOMA.arguments[2]).uri; string Point3Uri = ((OMS)rightAngleOMA.arguments[2]).uri;
if (!StageStatic.stage.factState.ContainsKey(Point1Uri) if (!FactOrganizer.AllFacts.ContainsKey(Point1Uri)
|| !StageStatic.stage.factState.ContainsKey(Point2Uri) || !FactOrganizer.AllFacts.ContainsKey(Point2Uri)
|| !StageStatic.stage.factState.ContainsKey(Point3Uri)) || !FactOrganizer.AllFacts.ContainsKey(Point3Uri))
return null; //If dependent facts do not exist return null return null;
return new RightAngleFact(Point1Uri, Point2Uri, Point3Uri, fact.@ref.uri, StageStatic.stage.factState); return new RightAngleFact(Point1Uri, Point2Uri, Point3Uri, fact.@ref.uri, StageStatic.stage.factState);
} }
......
...@@ -130,7 +130,7 @@ public class LineFact : AbstractLineFactWrappedCRTP<LineFact> ...@@ -130,7 +130,7 @@ public class LineFact : AbstractLineFactWrappedCRTP<LineFact>
public LineFact() : base() { } public LineFact() : base() { }
/// <summary> \copydoc AbstractLineFact.AbstractLineFact(string, string, string, FactOrganizer) </summary> /// <summary> \copydoc AbstractLineFact.AbstractLineFact(string, string, string, FactOrganizer) </summary>
public LineFact(string pid1, string pid2, string backendURI, FactOrganizer organizer) : base(pid1, pid2, backendURI, organizer) public LineFact(string pid1, string pid2, string backendURI, FactOrganizer organizer) : base(pid1, pid2, backendURI, organizer)
=> _ = this.Label; => _ = this.Label;
/// <summary> \copydoc AbstractLineFact.AbstractLineFact(string, string, FactOrganizer) </summary> /// <summary> \copydoc AbstractLineFact.AbstractLineFact(string, string, FactOrganizer) </summary>
...@@ -159,16 +159,14 @@ protected override MMTDeclaration MakeMMTDeclaration() ...@@ -159,16 +159,14 @@ protected override MMTDeclaration MakeMMTDeclaration()
/// \copydoc Fact.parseFact(ScrollFact) /// \copydoc Fact.parseFact(ScrollFact)
public new static LineFact parseFact(MMTDeclaration fact) public new static LineFact parseFact(MMTDeclaration fact)
{ {
string uri = fact.@ref.uri;
string pointAUri = ((OMS)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).uri; string pointAUri = ((OMS)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).uri;
string pointBUri = ((OMS)((OMA)((MMTValueDeclaration)fact).lhs).arguments[1]).uri; string pointBUri = ((OMS)((OMA)((MMTValueDeclaration)fact).lhs).arguments[1]).uri;
if (StageStatic.stage.factState.ContainsKey(pointAUri) if (!FactOrganizer.AllFacts.ContainsKey(pointAUri)
&& StageStatic.stage.factState.ContainsKey(pointBUri)) || !FactOrganizer.AllFacts.ContainsKey(pointBUri))
return new LineFact(pointAUri, pointBUri, uri, StageStatic.stage.factState); return null;
//If dependent facts do not exist return null return new LineFact(pointAUri, pointBUri, fact.@ref.uri, StageStatic.stage.factState);
else return null;
} }
/// \copydoc Fact.generateLabel /// \copydoc Fact.generateLabel
...@@ -206,7 +204,7 @@ public class RayFact : AbstractLineFactWrappedCRTP<RayFact> ...@@ -206,7 +204,7 @@ public class RayFact : AbstractLineFactWrappedCRTP<RayFact>
public RayFact() : base() { } public RayFact() : base() { }
/// <summary> \copydoc AbstractLineFact.AbstractLineFact(string, string, string, FactOrganizer) </summary> /// <summary> \copydoc AbstractLineFact.AbstractLineFact(string, string, string, FactOrganizer) </summary>
public RayFact(string pid1, string pid2, string backendURI, FactOrganizer organizer) : base(pid1, pid2, backendURI, organizer) public RayFact(string pid1, string pid2, string backendURI, FactOrganizer organizer) : base(pid1, pid2, backendURI, organizer)
=> _ = this.Label; => _ = this.Label;
/// <summary> \copydoc AbstractLineFact.AbstractLineFact(string, string, FactOrganizer) </summary> /// <summary> \copydoc AbstractLineFact.AbstractLineFact(string, string, FactOrganizer) </summary>
...@@ -237,20 +235,17 @@ protected override void RecalculateTransform() ...@@ -237,20 +235,17 @@ protected override void RecalculateTransform()
/// \copydoc Fact.parseFact(ScrollFact) /// \copydoc Fact.parseFact(ScrollFact)
public new static RayFact parseFact(MMTDeclaration fact) public new static RayFact parseFact(MMTDeclaration fact)
{ {
string uri = fact.@ref.uri; if (((MMTSymbolDeclaration)fact).defines is not OMA defines)
if ((OMA)((MMTSymbolDeclaration)fact).df == null)
return null; return null;
string pointAUri = ((OMS)((OMA)((MMTSymbolDeclaration)fact).df).arguments[0]).uri; string pointAUri = ((OMS)defines.arguments[0]).uri;
string pointBUri = ((OMS)((OMA)((MMTSymbolDeclaration)fact).df).arguments[1]).uri; string pointBUri = ((OMS)defines.arguments[1]).uri;
if (StageStatic.stage.factState.ContainsKey(pointAUri) if (!FactOrganizer.AllFacts.ContainsKey(pointAUri)
&& StageStatic.stage.factState.ContainsKey(pointBUri)) || !FactOrganizer.AllFacts.ContainsKey(pointBUri))
return new RayFact(pointAUri, pointBUri, uri, StageStatic.stage.factState); return null;
//If dependent facts do not exist return null return new RayFact(pointAUri, pointBUri, fact.@ref.uri, StageStatic.stage.factState);
else return null;
} }
/// \copydoc Fact.generateLabel /// \copydoc Fact.generateLabel
......
...@@ -151,7 +151,7 @@ protected override void RecalculateTransform() { } ...@@ -151,7 +151,7 @@ protected override void RecalculateTransform() { }
public new static FunctionFact parseFact(MMTDeclaration fact) public new static FunctionFact parseFact(MMTDeclaration fact)
{// TODO Correctness {// TODO Correctness
string uri = fact.@ref.uri; string uri = fact.@ref.uri;
OMA df = (OMA)((MMTSymbolDeclaration)fact).df; OMA df = (OMA)((MMTSymbolDeclaration)fact).defines;
if (df == null) if (df == null)
return null; return null;
...@@ -204,12 +204,11 @@ public class AttachedPositionFunction : FactWrappedCRTP<AttachedPositionFunction ...@@ -204,12 +204,11 @@ public class AttachedPositionFunction : FactWrappedCRTP<AttachedPositionFunction
public string[] func_call_ids; public string[] func_call_ids;
[JsonIgnore] [JsonIgnore]
public Fact Fact { get => FactOrganizer.AllFacts[fid]; } public Fact Fact => FactOrganizer.AllFacts[fid];
[JsonIgnore] [JsonIgnore]
public FunctionCallFact[] FunctionFacts public FunctionCallFact[] FunctionFacts
{ => func_call_ids.Select(f => FactOrganizer.AllFacts[f] as FunctionCallFact).ToArray();
get => func_call_ids.Select(f => FactOrganizer.AllFacts[f] as FunctionCallFact).ToArray();
}
/// <summary>\copydoc Fact.Fact()</summary> /// <summary>\copydoc Fact.Fact()</summary>
public AttachedPositionFunction() : base() { } public AttachedPositionFunction() : base() { }
...@@ -225,10 +224,7 @@ public AttachedPositionFunction(string fid, string[] funcids, FactOrganizer orga ...@@ -225,10 +224,7 @@ public AttachedPositionFunction(string fid, string[] funcids, FactOrganizer orga
private void init(string fid, string[] funcids) private void init(string fid, string[] funcids)
{ {
this.fid = fid; this.fid = fid;
this.func_call_ids = funcids;
this.func_call_ids = new string[funcids.Length];
funcids.CopyTo(this.func_call_ids, 0);
} }
protected AttachedPositionFunction(string fid, string[] funcids, string uri, FactOrganizer organizer) : base(organizer) protected AttachedPositionFunction(string fid, string[] funcids, string uri, FactOrganizer organizer) : base(organizer)
...@@ -241,7 +237,7 @@ protected AttachedPositionFunction(string fid, string[] funcids, string uri, Fac ...@@ -241,7 +237,7 @@ protected AttachedPositionFunction(string fid, string[] funcids, string uri, Fac
public new static AttachedPositionFunction parseFact(MMTDeclaration fact) public new static AttachedPositionFunction parseFact(MMTDeclaration fact)
{// TODO Correctness {// TODO Correctness
string uri = fact.@ref.uri; string uri = fact.@ref.uri;
OMA df = (OMA)((MMTSymbolDeclaration)fact).df; OMA df = (OMA)((MMTSymbolDeclaration)fact).defines;
if (df == null) if (df == null)
return null; return null;
......
...@@ -14,13 +14,12 @@ public override void _Hit(RaycastHit[] hit) ...@@ -14,13 +14,12 @@ public override void _Hit(RaycastHit[] hit)
{ {
// It's probably better to keep this only on the first hit and not multiple hits // It's probably better to keep this only on the first hit and not multiple hits
string hid = hit[0].transform.GetComponent<FactObject>()?.URI; string hid = hit[0].transform.GetComponent<FactObject>()?.URI;
if (hid == null) return; if (hid == null)
return;
Workflow.Add(hid); Workflow.Add(hid);
StageStatic.stage.factState.Remove(Workflow[0], samestep: false, gadget: this); StageStatic.stage.factState.Remove(Workflow[0], samestep: false, gadget: this);
ResetGadget(); ResetGadget();
} }
} }
...@@ -252,7 +252,7 @@ public void animateHint(GameObject scrollParameter, string scrollParameterUri) ...@@ -252,7 +252,7 @@ public void animateHint(GameObject scrollParameter, string scrollParameterUri)
if (suitableCompletion != null) if (suitableCompletion != null)
{ {
if (StageStatic.stage.factState.ContainsKey(suitableCompletion.assignment.uri)) if (FactOrganizer.AllFacts.ContainsKey(suitableCompletion.assignment.uri))
{ {
fact = FactOrganizer.AllFacts[suitableCompletion.assignment.uri]; fact = FactOrganizer.AllFacts[suitableCompletion.assignment.uri];
//Animate ScrollParameter //Animate ScrollParameter
...@@ -267,7 +267,7 @@ public void animateHint(GameObject scrollParameter, string scrollParameterUri) ...@@ -267,7 +267,7 @@ public void animateHint(GameObject scrollParameter, string scrollParameterUri)
var factId = fact.Id; var factId = fact.Id;
//If there is an equal existing fact -> Animate that fact AND ScrollParameter //If there is an equal existing fact -> Animate that fact AND ScrollParameter
if (StageStatic.stage.factState.ContainsKey(factId)) if (FactOrganizer.AllFacts.ContainsKey(factId))
{ {
Fact existingFact = FactOrganizer.AllFacts[factId]; Fact existingFact = FactOrganizer.AllFacts[factId];
......
...@@ -61,7 +61,7 @@ public static class MMT_OMS_URI ...@@ -61,7 +61,7 @@ public static class MMT_OMS_URI
public static readonly string Multiply = "Multiply"; public static readonly string Multiply = "Multiply";
public static readonly string Subtract = "Subtract"; public static readonly string Subtract = "Subtract";
public static readonly string SquareRoot = "SquareRoot"; public static readonly string SquareRoot = "SquareRoot";
public static readonly string MakeUnityEngineVector3 = "UnityEngine.Vector3"; //public static readonly string MakeUnityEngineVector3 = "UnityEngine.Vector3";
public static readonly string MakeObjectArray = "MakeObjectArray"; public static readonly string MakeObjectArray = "MakeObjectArray";
} }
...@@ -80,7 +80,7 @@ public static class SOMDoctoLambdaExpression<T> ...@@ -80,7 +80,7 @@ public static class SOMDoctoLambdaExpression<T>
MakeCos}, MakeCos},
{ MMT_OMS_URI.SquareRoot, { MMT_OMS_URI.SquareRoot,
MakeCos}, MakeCos},
{ MMT_OMS_URI.MakeUnityEngineVector3, { MMT_OMS_URI.Tuple,
MakeUnityEngineVector3}, MakeUnityEngineVector3},
{ MMT_OMS_URI.MakeObjectArray, { MMT_OMS_URI.MakeObjectArray,
MakeArray}, MakeArray},
...@@ -198,6 +198,7 @@ public static class SOMDoctoLambdaExpression<T> ...@@ -198,6 +198,7 @@ public static class SOMDoctoLambdaExpression<T>
#endregion ExpressionDictionaries #endregion ExpressionDictionaries
//TODO: case ((f->x)->y) instead of assumed (f->(x->y))
public static LambdaExpression MakeLambdaExpression(string URI, LambdaExpression[] lambda_args, ParameterExpression[] bound_params) public static LambdaExpression MakeLambdaExpression(string URI, LambdaExpression[] lambda_args, ParameterExpression[] bound_params)
{ {
void ThrowArgumentException(ExpressionType expression_cast, int expected) void ThrowArgumentException(ExpressionType expression_cast, int expected)
...@@ -208,25 +209,34 @@ void ThrowArgumentException(ExpressionType expression_cast, int expected) ...@@ -208,25 +209,34 @@ void ThrowArgumentException(ExpressionType expression_cast, int expected)
)); ));
} }
ParameterExpression[] lambda_params =
lambda_args
.SelectMany(l => l.Parameters)
.ToArray(); //PERF: .ToList().Sort() => .BinarySearch;
ParameterExpression[] found_bound_params =
bound_params
.Where(p => lambda_params.Contains(p))
.ToArray();
if (MMTtoUnaryExpressionType.TryGetValue(URI, out var unnary_type)) if (MMTtoUnaryExpressionType.TryGetValue(URI, out var unnary_type))
{ {
if (bound_params.Count() < 1) if (found_bound_params.Count() < 1)
ThrowArgumentException(unnary_type, 1); ThrowArgumentException(unnary_type, 1);
Type UnarySecondArgument = bound_params.Count() < 2 ? null : bound_params[1].Type; Type UnarySecondArgument = found_bound_params.Count() < 2 ? null : found_bound_params[1].Type;
return Expression.Lambda(Expression.MakeUnary(unnary_type, lambda_args[0].Body, UnarySecondArgument), bound_params); return Expression.Lambda(Expression.MakeUnary(unnary_type, lambda_args[0].Body, UnarySecondArgument), found_bound_params);
} }
else if (MMTtoBinaryExpressionType.TryGetValue(URI, out var binary_type)) else if (MMTtoBinaryExpressionType.TryGetValue(URI, out var binary_type))
{ {
if (lambda_args.Count() != 2) if (lambda_args.Count() != 2)
ThrowArgumentException(binary_type, 2); ThrowArgumentException(binary_type, 2);
return Expression.Lambda(Expression.MakeBinary(binary_type, lambda_args[0].Body, lambda_args[1].Body), bound_params); return Expression.Lambda(Expression.MakeBinary(binary_type, lambda_args[0].Body, lambda_args[1].Body), found_bound_params);
} }
else if (MMTtoLambdaMaker.TryGetValue(URI, out var lamda_maker)) else if (MMTtoLambdaMaker.TryGetValue(URI, out var lamda_maker))
{ {
return lamda_maker(lambda_args, bound_params); return lamda_maker(lambda_args, found_bound_params);
} }
throw new NotImplementedException("Could not map URI: \"" + URI + "\""); throw new NotImplementedException("Could not map URI: \"" + URI + "\"");
...@@ -302,6 +312,8 @@ abstract public class SOMDoc ...@@ -302,6 +312,8 @@ abstract public class SOMDoc
typeof(double)}, typeof(double)},
{typeof(string).ToString(), {typeof(string).ToString(),
typeof(string)}, typeof(string)},
{MMT_OMS_URI.Tuple,
typeof(UnityEngine.Vector3)},
{typeof(UnityEngine.Vector3).ToString(), {typeof(UnityEngine.Vector3).ToString(),
typeof(UnityEngine.Vector3)}, typeof(UnityEngine.Vector3)},
}; };
...@@ -384,7 +396,7 @@ public LambdaExpression GetLambdaExpression() ...@@ -384,7 +396,7 @@ public LambdaExpression GetLambdaExpression()
public static SOMDoc MakeUnityEngineVector3(Vector3 vec) public static SOMDoc MakeUnityEngineVector3(Vector3 vec)
=> new OMA( => new OMA(
new OMS(MMT_OMS_URI.MakeUnityEngineVector3), new OMS(MMT_OMS_URI.Tuple),
new() { new() {
new OMF(vec.x), new OMF(vec.x),
new OMF(vec.y), new OMF(vec.y),
...@@ -563,22 +575,22 @@ public class OMF : SOMDocCRTP<OMF> ...@@ -563,22 +575,22 @@ public class OMF : SOMDocCRTP<OMF>
public new string kind = "OMF"; public new string kind = "OMF";
[JsonProperty("float")] [JsonProperty("float")]
public float f; public float @float;
[JsonConstructor] [JsonConstructor]
public OMF(float f) : base() public OMF(float f) : base()
{ {
this.f = f; this.@float = f;
} }
protected override bool EquivalentWrapped(OMF sd2) protected override bool EquivalentWrapped(OMF sd2)
=> this.f.IsApproximatelyEqual(sd2.f); => this.@float.IsApproximatelyEqual(sd2.@float);
protected internal override LambdaExpression GetLambdaExpression(LambdaExpression[] lambda_args, ParameterExpression[] bound_params) protected internal override LambdaExpression GetLambdaExpression(LambdaExpression[] lambda_args, ParameterExpression[] bound_params)
=> Expression.Lambda(Expression.Constant(f, typeof(float)), null); => Expression.Lambda(Expression.Constant(@float, typeof(float)), null);
public override string ToString() public override string ToString()
=> f.ToString(); => @float.ToString();
public override OMF MapURIsWrapped(Dictionary<string, string> old_to_new) public override OMF MapURIsWrapped(Dictionary<string, string> old_to_new)
=> (OMF)this.MemberwiseClone(); => (OMF)this.MemberwiseClone();
...@@ -682,23 +694,25 @@ public class MMTSymbolDeclaration : MMTDeclaration ...@@ -682,23 +694,25 @@ public class MMTSymbolDeclaration : MMTDeclaration
{ {
public new string kind = "general"; public new string kind = "general";
public SOMDoc tp; [JsonProperty("tp")]
public SOMDoc df; public SOMDoc type;
[JsonProperty("df")]
public SOMDoc defines;
[JsonConstructor] [JsonConstructor]
private MMTSymbolDeclaration() { } private MMTSymbolDeclaration() { }
/// <summary>Constructor used for sending new declarations to mmt</summary> /// <summary>Constructor used for sending new declarations to mmt</summary>
public MMTSymbolDeclaration(string label, SOMDoc tp, SOMDoc df) public MMTSymbolDeclaration(string label, SOMDoc type, SOMDoc defines)
{ {
this.label = label; this.label = label;
this.tp = tp; this.type = type;
this.df = df; this.defines = defines;
} }
public override string getType() public override string getType()
{ {
return tp switch return type switch
{ {
OMS oMS => oMS.uri, OMS oMS => oMS.uri,
OMA oMA => ((oMA.arguments[0] as OMA).applicant as OMS).uri, OMA oMA => ((oMA.arguments[0] as OMA).applicant as OMS).uri,
...@@ -708,7 +722,7 @@ public override string getType() ...@@ -708,7 +722,7 @@ public override string getType()
public override string getApplicant() public override string getApplicant()
{ {
return df switch return defines switch
{ {
OMA oMA when oMA.applicant is OMS oMS => oMS.uri, OMA oMA when oMA.applicant is OMS oMS => oMS.uri,
_ => null _ => null
...@@ -722,7 +736,8 @@ public class MMTValueDeclaration : MMTDeclaration ...@@ -722,7 +736,8 @@ public class MMTValueDeclaration : MMTDeclaration
public new string kind = "veq"; public new string kind = "veq";
public SOMDoc lhs; public SOMDoc lhs;
public SOMDoc valueTp; [JsonProperty("valueTp")]
public SOMDoc valueType;
public SOMDoc value; public SOMDoc value;
public SOMDoc proof; public SOMDoc proof;
...@@ -730,11 +745,11 @@ public class MMTValueDeclaration : MMTDeclaration ...@@ -730,11 +745,11 @@ public class MMTValueDeclaration : MMTDeclaration
private MMTValueDeclaration() { } private MMTValueDeclaration() { }
/// <summary>Constructor used for sending new declarations to mmt</summary> /// <summary>Constructor used for sending new declarations to mmt</summary>
public MMTValueDeclaration(string label, SOMDoc lhs, SOMDoc valueTp, SOMDoc value, SOMDoc proof = null) public MMTValueDeclaration(string label, SOMDoc lhs, SOMDoc valueType, SOMDoc value, SOMDoc proof = null)
{ {
this.label = label; this.label = label;
this.lhs = lhs; this.lhs = lhs;
this.valueTp = valueTp; this.valueType = valueType;
this.value = value; this.value = value;
this.proof = proof; this.proof = proof;
} }
......
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment