Select Git revision
BrowserTab.cs
-
Björn Eßwein authoredBjörn Eßwein authored
SOMDocManager.cs 39.38 KiB
using System.Collections.Generic;
using Newtonsoft.Json;
using JsonSubTypes;
using System.Linq.Expressions;
using System;
using System.Linq;
using MoreLinq;
using UnityEngine;
using REST_JSON_API;
public static class SOMDocManager
{
public static class MMT_OMS_URI
{
public static readonly string Point = "http://mathhub.info/MitM/core/geometry?3DGeometry?point";
public static readonly string Tuple = "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Tuple";
public static readonly string LineType = "http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type";
public static readonly string LineOf = "http://mathhub.info/MitM/core/geometry?Geometry/Common?lineOf";
public static readonly string OnLine = "http://mathhub.info/MitM/core/geometry?Geometry/Common?onLine";
public static readonly string Ded = "http://mathhub.info/MitM/Foundation?Logic?ded";
public static readonly string Eq = "http://mathhub.info/MitM/Foundation?Logic?eq";
public static readonly string Metric = "http://mathhub.info/MitM/core/geometry?Geometry/Common?metric";
public static readonly string Angle = "http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between";
public static readonly string Sketch = "http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch";
public static readonly string RealLit = "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit";
public static readonly string ParallelLine = "http://mathhub.info/MitM/core/geometry?Geometry/Common?parallelLine";
//public static readonly string RectangleFact = "http://mathhub.info/FrameIT/frameworld?FrameITRectangles?rectangleType";
//public static readonly string RectangleFactmk = "http://mathhub.info/FrameIT/frameworld?FrameITRectangles?mkRectangle";
public static readonly string CircleType3d = "http://mathhub.info/FrameIT/frameworld?FrameITCircle?circleType3D";
public static readonly string MkCircle3d = "http://mathhub.info/FrameIT/frameworld?FrameITCircle?circle3D";
public static readonly string TriangleMiddlePoint = "http://mathhub.info/FrameIT/frameworld?FrameITTriangles?triangleMidPointWrapper";
public static readonly string RadiusCircleMetric = "http://mathhub.info/FrameIT/frameworld?FrameITCircle?circleRadius";
public static readonly string AreaCircle = "http://mathhub.info/FrameIT/frameworld?FrameITCircle?areaCircle";
public static readonly string VolumeCone = "http://mathhub.info/FrameIT/frameworld?FrameITCone?volumeCone";
public static readonly string ConeOfCircleApex = "http://mathhub.info/FrameIT/frameworld?FrameITCone?circleConeOf";
public static readonly string ParametrizedPlane = "http://mathhub.info/MitM/core/geometry?Planes?ParametrizedPlane";
public static readonly string pointNormalPlane = "http://mathhub.info/MitM/core/geometry?Planes?pointNormalPlane";
public static readonly string OnCircle = "http://mathhub.info/FrameIT/frameworld?FrameITCircle?pointOnCircle";
public static readonly string AnglePlaneLine = "http://mathhub.info/FrameIT/frameworld?FrameITCircle?angleCircleLine";
public static readonly string OrthoCircleLine = "http://mathhub.info/FrameIT/frameworld?FrameITCircle?orthogonalCircleLine";
public static readonly string TruncatedVolumeCone = "http://mathhub.info/FrameIT/frameworld?FrameITCone?truncatedConeVolume";
public static readonly string CylinderVolume = "http://mathhub.info/FrameIT/frameworld?FrameITCylinder?cylinderVolume";
public static readonly string EqualityCircles = "http://mathhub.info/FrameIT/frameworld?FrameITCircle?equalityCircles";
public static readonly string UnEqualityCircles = "http://mathhub.info/FrameIT/frameworld?FrameITCircle?unequalityCircles";
public static readonly string ParallelCircles = "http://mathhub.info/FrameIT/frameworld?FrameITCone?parallelCircles";
public static readonly string RightAngle = "http://mathhub.info/FrameIT/frameworld?FrameITBasics?rightAngle";
public static readonly string AttachedPositionFunction = "0SET_IN_SOMDocManager!";
public static readonly string FunctionCallFact = "1SET_IN_SOMDocManager!";
public static readonly string FunctionFact = "2SET_IN_SOMDocManager!";
public static readonly string TestType = "http://mathhub.info/FrameIT/frameworld?FrameITCircle?xcircleType3D";
public static readonly string ListType = "http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?ListType";
public static readonly string ListLiteral = "http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?cons";
public static readonly string ListEnd = "http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?nil_constant";
public static readonly string Sin = "Sin";
public static readonly string Cos = "Cos";
public static readonly string Add = "Add";
public static readonly string Divide = "Divide";
public static readonly string Multiply = "Multiply";
public static readonly string Subtract = "Subtract";
public static readonly string SquareRoot = "SquareRoot";
//public static readonly string MakeUnityEngineVector3 = "UnityEngine.Vector3";
public static readonly string MakeObjectArray = "MakeObjectArray";
public const string ScrollOppositeLen = "http://mathhub.info/FrameIT/frameworld?OppositeLen";
public const string ScrollSupplementaryAngles = "http://mathhub.info/FrameIT/frameworld?SupplementaryAngles";
public const string ScrollAngleSum = "http://mathhub.info/FrameIT/frameworld?AngleSum";
public const string ScrollPythagoras = "http://mathhub.info/FrameIT/frameworld?Pythagoras";
public const string ScrollCylinderVolumeScroll = "http://mathhub.info/FrameIT/frameworld?CylinderVolumeScroll";
public const string ScrollCircleLineAngleToAngleScroll = "http://mathhub.info/FrameIT/frameworld?CircleLineAngleToAngleScroll";
public const string ScrollMidpoint = "http://mathhub.info/FrameIT/frameworld?Midpoint";
public const string ScrollCircleScroll = "http://mathhub.info/FrameIT/frameworld?CircleScroll";
public const string ScrollCircleLineAngleScroll = "http://mathhub.info/FrameIT/frameworld?CircleLineAngleScroll";
public const string ScrollCircleAreaScroll = "http://mathhub.info/FrameIT/frameworld?CircleAreaScroll";
public const string ScrollConeVolumeScroll = "http://mathhub.info/FrameIT/frameworld?ConeVolumeScroll";
public const string ScrollTruncatedConeVolumeScroll = "http://mathhub.info/FrameIT/frameworld?TruncatedConeVolumeScroll";
public const string ScrollCannonBall = "CannonBall";
public static readonly IReadOnlyDictionary<Type, string> TYPE_TO_OMS;
public static readonly IReadOnlyDictionary<string, Type> OMS_TO_TYPE = new Dictionary<string, Type>()
{
{ Point,
typeof(PointFact) },
{ Metric,
typeof(LineFact) },
{ Angle,
typeof(AngleFact) },
{ Eq,
typeof(AngleFact) },
{ RightAngle,
typeof(RightAngleFact) },
{ LineType,
typeof(RayFact) },
{ LineOf,
typeof(RayFact) },
{ OnLine,
typeof(OnLineFact) },
{ ParallelLine,
typeof(ParallelLineFact) },
{ CircleType3d,
typeof(CircleFact) },
{ OnCircle,
typeof(OnCircleFact) },
{ AnglePlaneLine,
typeof(AngleCircleLineFact) },
{ RadiusCircleMetric,
typeof(RadiusFact) },
{ AreaCircle,
typeof(AreaCircleFact) },
{ OrthoCircleLine,
typeof(OrthogonalCircleLineFact) },
{ VolumeCone,
typeof(ConeVolumeFact) },
{ TruncatedVolumeCone,
typeof(TruncatedConeVolumeFact) },
{ CylinderVolume,
typeof(CylinderVolumeFact) },
{ TestType,
typeof(TestFact) },
{ EqualityCircles,
typeof(EqualCirclesFact) },
{ UnEqualityCircles,
typeof(UnEqualCirclesFact) },
{ FunctionFact,
typeof(FunctionFact) },
{ FunctionCallFact,
typeof(FunctionCallFact) },
{ AttachedPositionFunction,
typeof(AttachedPositionFunction) },
{ RealLit,
typeof(float) },
{ Tuple,
typeof(TupelFact) },
{ ListType,
typeof(List<>) },
{ MkCircle3d, null }, //typeof(CircleFact) },
{ ConeOfCircleApex, null }, //typeof(ConeVolumeFact) },
{ Ded, null },
{ Sketch, null },
{ TriangleMiddlePoint, null },
{ ParametrizedPlane, null },
{ pointNormalPlane, null },
{ ParallelCircles, null },
{ "R",
typeof(float) },
{ typeof(float).ToString(),
typeof(float) },
{ typeof(double).ToString(),
typeof(double) },
{ typeof(string).ToString(),
typeof(string) },
{ typeof(Vector3).ToString(),
typeof(Vector3) }
};
static MMT_OMS_URI()
{
Dictionary<Type, string> _TYPE_TO_OMS = new() {
// **Overrides**
//{ typeof(Vector3),
// Tuple },
};
foreach (KeyValuePair<string, Type> KeyVal in OMS_TO_TYPE)
if (KeyVal.Value != null)
_TYPE_TO_OMS.TryAdd(KeyVal.Value, KeyVal.Key);
TYPE_TO_OMS = _TYPE_TO_OMS;
}
}
public static class SOMDoctoLambdaExpression<T>
{
// TODO: Populate Dictionaries
#region ExpressionDictionaries
delegate LambdaExpression CustomFunction(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params);
private static readonly Dictionary<string, CustomFunction> MMTtoLambdaMaker = new()
{
{ MMT_OMS_URI.Sin,
MakeSin },
{ MMT_OMS_URI.Cos,
MakeCos },
{ MMT_OMS_URI.SquareRoot,
MakeCos },
{ MMT_OMS_URI.Tuple,
MakeTupel },
{ MMT_OMS_URI.MakeObjectArray,
MakeObjArray },
{ "InstantList",
MakeInstantList },
{ MMT_OMS_URI.ListEnd,
MakeListEnd },
{ MMT_OMS_URI.ListLiteral,
InsertFrontListLiteral },
{ MMT_OMS_URI.ListType,
Identity0 },
};
private static readonly Dictionary<string, ExpressionType> MMTtoBinaryExpressionType = new()
{
{ MMT_OMS_URI.Add,
ExpressionType.Add},
{ "AddAssign",
ExpressionType.AddAssign},
{ "AddAssignChecked",
ExpressionType.AddAssignChecked},
{ "AddChecked",
ExpressionType.AddChecked},
{ "And",
ExpressionType.And},
{ "AndAlso",
ExpressionType.AndAlso},
{ "AndAssign",
ExpressionType.AndAssign},
{ "Assign",
ExpressionType.Assign},
{ MMT_OMS_URI.Divide,
ExpressionType.Divide},
{ "DivideAssign",
ExpressionType.DivideAssign},
{ "Equal",
ExpressionType.Equal},
{ "ExclusiveOr",
ExpressionType.ExclusiveOr},
{ "ExclusiveOrAssign",
ExpressionType.ExclusiveOrAssign},
{ "GreaterThan",
ExpressionType.GreaterThan},
{ "GreaterThanOrEqual",
ExpressionType.GreaterThanOrEqual},
{ "LeftShift",
ExpressionType.LeftShift},
{ "LeftShiftAssign",
ExpressionType.LeftShiftAssign},
{ "LessThan",
ExpressionType.LessThan},
{ "LessThanOrEqual",
ExpressionType.LessThanOrEqual},
{ "Modulo",
ExpressionType.Modulo},
{ "ModuloAssign",
ExpressionType.ModuloAssign},
{ MMT_OMS_URI.Multiply,
ExpressionType.Multiply},
{ "MultiplyAssign",
ExpressionType.MultiplyAssign},
{ "MultiplyAssignChecked",
ExpressionType.MultiplyAssignChecked},
{ "MultiplyChecked",
ExpressionType.MultiplyChecked},
{ "NotEqual",
ExpressionType.NotEqual},
{ "Or",
ExpressionType.Or},
{ "OrAssign",
ExpressionType.OrAssign},
{ "OrElse",
ExpressionType.OrElse},
{ "Power",
ExpressionType.Power},
{ "PowerAssign",
ExpressionType.PowerAssign},
{ "RightShift",
ExpressionType.RightShift},
{ "RightShiftAssign",
ExpressionType.RightShiftAssign},
{ MMT_OMS_URI.Subtract,
ExpressionType.Subtract},
{ "SubtractAssign",
ExpressionType.SubtractAssign},
{ "SubtractAssignChecked",
ExpressionType.SubtractAssignChecked},
{ "SubtractChecked",
ExpressionType.SubtractChecked},
};
private static readonly Dictionary<string, ExpressionType> MMTtoUnaryExpressionType = new()
{
//{ "Constant", // Not Unary
// ExpressionType.Constant},
{ "Convert",
ExpressionType.Convert},
{ "ConvertChecked",
ExpressionType.ConvertChecked},
{ "Decrement",
ExpressionType.Decrement},
{ "Increment",
ExpressionType.Increment},
{ "Negate",
ExpressionType.Negate},
{ "NegateChecked",
ExpressionType.NegateChecked},
{ "Not",
ExpressionType.Not},
{ "OnesComplement",
ExpressionType.OnesComplement},
{ "PostDecrementAssign",
ExpressionType.PostDecrementAssign},
{ "PostIncrementAssign",
ExpressionType.PostIncrementAssign},
{ "PreDecrementAssign",
ExpressionType.PreDecrementAssign},
{ "PreIncrementAssign",
ExpressionType.PreIncrementAssign},
{ "UnaryPlus",
ExpressionType.UnaryPlus},
};
#endregion ExpressionDictionaries
//TODO: case ((f->x)->y) instead of assumed (f->(x->y))
public static LambdaExpression MakeLambdaExpression(string URI, LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
{
void ThrowArgumentException(ExpressionType expression_cast, int expected)
{
throw new ArgumentException(string.Format(
"\"Wrong number of Arguments. Required: {2}. Supplied: {3}.\\n\\tFor URI:\\\"{0}\\\"\\n\\tmapped to:\\\"{1}\\\"\"",
URI, expression_cast, expected, lambda_applicant.Count()
));
}
ParameterExpression[] lambda_params =
lambda_applicant
.SelectMany(l => l.Parameters)
.ToArray(); //PERF: .ToList().Sort() => .BinarySearch; //Too much overhead?
ParameterExpression[] found_bound_params =
bound_params
.Where(p => lambda_params.Contains(p))
.ToArray();
if (MMTtoUnaryExpressionType.TryGetValue(URI, out var unnary_type))
{
if (found_bound_params.Count() < 1)
ThrowArgumentException(unnary_type, 1);
Type UnarySecondArgument = found_bound_params.Count() < 2 ? null : found_bound_params[1].Type;
return Expression.Lambda(Expression.MakeUnary(unnary_type, lambda_applicant[0].Body, UnarySecondArgument), found_bound_params);
}
else
if (MMTtoBinaryExpressionType.TryGetValue(URI, out var binary_type))
{
if (lambda_applicant.Count() != 2)
ThrowArgumentException(binary_type, 2);
return Expression.Lambda(Expression.MakeBinary(binary_type, lambda_applicant[0].Body, lambda_applicant[1].Body), found_bound_params);
}
else
if (MMTtoLambdaMaker.TryGetValue(URI, out var lamda_maker))
{
return lamda_maker(lambda_applicant, lambda_arguments, found_bound_params);
}
else
if (MMT_OMS_URI.OMS_TO_TYPE.TryGetValue(URI, out Type type))
{
return Expression.Lambda(Expression.Default(type), null);
}
throw new NotImplementedException("Could not map URI: \"" + URI + "\"");
}
private static LambdaExpression ExpresionFuncToLambda(LambdaExpression func, string name, LambdaExpression[] args_lamda, ParameterExpression[] bound_params, uint nTargs_fallback)
=> Expression.Lambda(Expression.Invoke(func, args_lamda.Select(l => l.Body)), name, bound_params);
private static LambdaExpression ParseFuncUUToExpression<U>(Func<U, U> func)
=> (Expression<Func<U, U>>)((U x) => func(x));
private static LambdaExpression MakeSin(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
=> ExpresionFuncToLambda(
lambda_applicant[0].ReturnType == typeof(float) ? ParseFuncUUToExpression<float>(MathF.Sin)
: lambda_applicant[0].ReturnType == typeof(double) ? ParseFuncUUToExpression<double>(Math.Sin)
: throw new NotImplementedException("Sinus for " + lambda_applicant[0].ReturnType),
"Sin", lambda_arguments.Length > 0 ? lambda_arguments : lambda_applicant, bound_params, 1
);
private static LambdaExpression MakeCos(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
=> ExpresionFuncToLambda(
lambda_applicant[0].ReturnType == typeof(float) ? ParseFuncUUToExpression<float>(MathF.Cos)
: lambda_applicant[0].ReturnType == typeof(double) ? ParseFuncUUToExpression<double>(Math.Cos)
: throw new NotImplementedException("Cosinus for " + lambda_applicant[0].ReturnType),
"Cos", lambda_arguments.Length > 0 ? lambda_arguments : lambda_applicant, bound_params, 1
);
private static LambdaExpression MakeTupel(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
{
if (lambda_applicant.Length == 3
&& lambda_applicant.All(l => l.ReturnType == typeof(float)))
return ExpresionFuncToLambda(
(Expression<Func<float, float, float, Vector3>>)((x, y, z) => new Vector3(x, y, z)),
"UnityEngineVector3", lambda_applicant, bound_params, 3
);
return MakeObjArray(lambda_applicant, lambda_arguments, bound_params);
}
private static LambdaExpression MakeObjArray(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
=> Expression.Lambda(
Expression.NewArrayInit(
typeof(object),
lambda_applicant.Select(l => Expression.Convert(l.Body, typeof(object)))
),
bound_params
);
private static LambdaExpression MakeInstantList(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
=> Expression.Lambda(
Expression.ListInit(
Expression.New(typeof(List<>).MakeGenericType(lambda_applicant[0].ReturnType)),
lambda_arguments.Select(l => l.Body) // Expression.Convert(l.Body, lambda_applicant[0].ReturnType))
),
bound_params
);
private static LambdaExpression InsertFrontListLiteral(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
=> Expression.Lambda(
Expression.Call(
lambda_applicant[0].Body,
lambda_applicant[0].ReturnType.GetMethod("Insert"),
Expression.Constant(0, typeof(int)),
lambda_applicant[1].Body
),
bound_params
);
private static LambdaExpression MakeListEnd(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
=> Expression.Lambda(
Expression.New(typeof(List<>).MakeGenericType(lambda_applicant[0].ReturnType)),
null
);
private static LambdaExpression Identity0(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
=> lambda_applicant[0];
}
[JsonConverter(typeof(JsonSubtypes), "kind")]
[JsonSubtypes.KnownSubType(typeof(OMA), "OMA")]
[JsonSubtypes.KnownSubType(typeof(OMBINDC), "OMBINDC")]
[JsonSubtypes.KnownSubType(typeof(OMS), "OMS")]
[JsonSubtypes.KnownSubType(typeof(OMSTR), "OMSTR")]
[JsonSubtypes.KnownSubType(typeof(OMF), "OMF")]
[JsonSubtypes.KnownSubType(typeof(OMV), "OMV")]
[JsonSubtypes.KnownSubType(typeof(RAW), "RAW")]
//[JsonSubtypes.KnownSubType(typeof(OMC<T>), "OMC<" + typeof(T) + ">")]
[JsonSubtypes.KnownSubType(typeof(OMC<Vector3>), "OMC<UnityEngine.Vector3>")]
[JsonSubtypes.KnownSubType(typeof(OMC<float>), "OMC<System.Single>")]
[JsonSubtypes.KnownSubType(typeof(OMC<double>), "OMC<System.Double>")]
abstract public class SOMDoc
{
public string kind;
protected SOMDoc() { kind = this.GetType().Name; }
public static bool Equivalent(SOMDoc sd1, SOMDoc sd2)
=> sd1 == null && sd2 == null
|| sd1.Equivalent(sd2);
public abstract bool Equivalent(SOMDoc sd2);
public LambdaExpression PartialInvokeCastingLambdaExpression(out Type[] signature_args, object[] callArgs = null, bool[] useArgs = null)
{
LambdaExpression lambda_orig = GetLambdaExpression();
signature_args = new Type[lambda_orig.Parameters.Count + 1];
ParameterExpression object_arr = Expression.Parameter(typeof(object[]), "PARAMS_Arr");
Expression[] cast_new_to_signature = new Expression[lambda_orig.Parameters.Count];
int n_params = 0;
for (int i = 0; i < lambda_orig.Parameters.Count; i++)
{
if (callArgs != null && callArgs.Length < i
&& (useArgs == null || (useArgs.Length < i && useArgs[i])))
{
cast_new_to_signature[i] =
Expression.Constant(callArgs[i], lambda_orig.Parameters[i].Type);
continue;
}
signature_args[n_params++] = lambda_orig.Parameters[i].Type;
cast_new_to_signature[i] =
Expression.Convert(
Expression.ArrayIndex(
object_arr,
Expression.Constant(i)
),
lambda_orig.Parameters[i].Type
);
}
signature_args[n_params] = lambda_orig.ReturnType;
signature_args = signature_args.Slice(0, n_params + 1).ToArray();
return Expression.Lambda(
typeof(Array).IsAssignableFrom(lambda_orig.ReturnType)
? Expression.Convert(
Expression.Invoke(lambda_orig, cast_new_to_signature),
typeof(object[]))
: Expression.NewArrayInit(
typeof(object),
new Expression[] { Expression.Convert(Expression.Invoke(lambda_orig, cast_new_to_signature), typeof(object)) }),
object_arr
);
}
public LambdaExpression GetLambdaExpression()
=> GetLambdaExpression(new LambdaExpression[0], new LambdaExpression[0], new ParameterExpression[0]);
protected internal abstract LambdaExpression GetLambdaExpression(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params);
public abstract override string ToString();
public abstract SOMDoc MapURIs(Dictionary<string, string> old_to_new);
#region MakeMMT_OMS_URItoSOMDoc
public static OMA MakeTupel(Vector3 vec)
=> MakeTupel(new[] {
new OMF(vec.x),
new OMF(vec.y),
new OMF(vec.z),
});
public static OMA MakeTupel(SOMDoc[] args)
=> new(
new OMS(MMT_OMS_URI.Tuple),
args
);
public static OMA MakeList(string[] lids, Type type)
=> MakeList(lids, MMT_OMS_URI.TYPE_TO_OMS[type]);
public static OMA MakeList(string[] lids, string typeURI)
{
SOMDoc[] end_of_list = new SOMDoc[] {
new OMA(
new OMS(MMT_OMS_URI.ListEnd),
new[] {
new OMS(typeURI),
}
),
lids.Length == 0
? null
: new OMS(lids[^1])
};
if (lids.Length == 0)
end_of_list = end_of_list[..^1];
SOMDoc defines = new OMA(
new OMS(MMT_OMS_URI.ListLiteral),
end_of_list
);
for (int i = lids.Length - 2; i >= 0; i--)
{
defines = new OMA(
new OMS(MMT_OMS_URI.ListLiteral),
new[] {
defines,
new OMS(lids[i]),
});
}
SOMDoc type = new OMA(
new OMS(MMT_OMS_URI.ListType),
new[] { new OMS(typeURI), }
);
return new OMA(type, new[] { defines });
}
#endregion MakeMMT_OMS_URItoSOMDoc
}
public abstract class SOMDocCRTP<T> : SOMDoc where T : SOMDocCRTP<T>
{
protected SOMDocCRTP() : base() { }
public override bool Equivalent(SOMDoc sd2)
=> this.GetType() == sd2.GetType() && (this as T).EquivalentWrapped(sd2 as T);
protected abstract bool EquivalentWrapped(T sd2);
public override SOMDoc MapURIs(Dictionary<string, string> old_to_new)
=> MapURIsWrapped(old_to_new);
public abstract T MapURIsWrapped(Dictionary<string, string> old_to_new);
}
public class OMBINDC : SOMDocCRTP<OMBINDC>
{
public new string kind = "OMBINDC";
public string name;
public SOMDoc lambdabody;
/// <summary>@Type of this variable</summary>
[JsonIgnore]
public Type type;
/// <summary>Enables (especially <see cref="JsonConverter"/>) to read and set <see cref="type"/> by its <c>string</c> representation.</summary>
public string typeString
{
get => MMT_OMS_URI.TYPE_TO_OMS[type];
set => type = MMT_OMS_URI.OMS_TO_TYPE[value];
}
[JsonConstructor]
public OMBINDC(string name, string typeString, SOMDoc lambdabody) : base()
{
this.name = name;
this.typeString = typeString;
this.lambdabody = lambdabody;
}
public OMBINDC(string name, Type type, SOMDoc lambdabody) : base()
{
this.name = name;
this.type = type;
this.lambdabody = lambdabody;
}
protected override bool EquivalentWrapped(OMBINDC sd2)
=> this.type == sd2.type
&& this.name.Equals(sd2.name)
&& this.lambdabody.Equivalent(sd2.lambdabody);
protected internal override LambdaExpression GetLambdaExpression(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
{
ParameterExpression[] bind_me = bound_params.ShallowCloneAppend(
new[] { Expression.Parameter(type, name) }
);
return lambdabody.GetLambdaExpression(lambda_applicant, lambda_arguments, bind_me);
}
public override string ToString()
=> "OMBINDC(" + name + ", " + typeString + ")->";
public override OMBINDC MapURIsWrapped(Dictionary<string, string> old_to_new)
=> new(name, type, lambdabody.MapURIs(old_to_new));
}
public class OMA : SOMDocCRTP<OMA>
{
public new string kind = "OMA";
public SOMDoc applicant;
public SOMDoc[] arguments;
[JsonConstructor]
public OMA(SOMDoc applicant, SOMDoc[] arguments) : base()
{
this.applicant = applicant;
this.arguments = arguments;
}
protected override bool EquivalentWrapped(OMA sd2)
=> Equivalent(this.applicant, sd2.applicant)
&& this.arguments
.Zip(sd2.arguments, (arg1, arg2) => Equivalent(arg1, arg2))
.All(b => b);
protected internal override LambdaExpression GetLambdaExpression(LambdaExpression[] lambda_applicant_paps, LambdaExpression[] lambda_applicant_grands, ParameterExpression[] bound_params)
=> applicant.GetLambdaExpression(
arguments.Select(arg => arg.GetLambdaExpression(new LambdaExpression[0], new LambdaExpression[0], bound_params)).ToArray(),
lambda_applicant_paps,
bound_params
);
public override string ToString()
=> applicant.ToString() + "(" + string.Join(", ", arguments.Select(a => a.ToString())) + ")";
public override OMA MapURIsWrapped(Dictionary<string, string> old_to_new)
=> new OMA(
applicant.MapURIs(old_to_new),
arguments.Select(arg => arg.MapURIs(old_to_new)).ToArray()
);
}
public class OMS : SOMDocCRTP<OMS>
{
public new string kind = "OMS";
public string uri;
[JsonConstructor]
public OMS(string uri) : base()
{
this.uri = uri;
}
protected override bool EquivalentWrapped(OMS sd2)
=> this.uri == sd2.uri;
protected internal override LambdaExpression GetLambdaExpression(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
=> SOMDoctoLambdaExpression<float>.MakeLambdaExpression(uri, lambda_applicant, lambda_arguments, bound_params);
public override string ToString()
=> uri;
public override OMS MapURIsWrapped(Dictionary<string, string> old_to_new)
{
if (!old_to_new.TryGetValue(uri, out string new_uri))
new_uri = uri;
return new OMS(new_uri);
}
}
public class OMSTR : SOMDocCRTP<OMSTR>
{
public new string kind = "OMSTR";
[JsonProperty("float")]
public string s;
[JsonConstructor]
public OMSTR(string s) : base()
{
this.s = s;
}
protected override bool EquivalentWrapped(OMSTR sd2)
=> this.s == sd2.s;
protected internal override LambdaExpression GetLambdaExpression(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
=> Expression.Lambda(Expression.Constant(s, typeof(string)), null);
public override string ToString()
=> s;
public override OMSTR MapURIsWrapped(Dictionary<string, string> old_to_new)
=> (OMSTR)this.MemberwiseClone();
}
public class OMF : SOMDocCRTP<OMF>
{
public new string kind = "OMF";
[JsonProperty("float")]
public float @float;
[JsonConstructor]
public OMF(float f) : base()
{
this.@float = f;
}
protected override bool EquivalentWrapped(OMF sd2)
=> Mathf.Approximately(@float, sd2.@float);
protected internal override LambdaExpression GetLambdaExpression(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
=> Expression.Lambda(Expression.Constant(@float, typeof(float)), null);
public override string ToString()
=> @float.ToString();
public override OMF MapURIsWrapped(Dictionary<string, string> old_to_new)
=> (OMF)this.MemberwiseClone();
}
public class OMC<T> : SOMDocCRTP<OMC<T>>
{
public new string kind = "OMC<" + typeof(T) + ">";
public T value;
[JsonConstructor]
public OMC(T value) : base()
{
this.value = value;
}
protected override bool EquivalentWrapped(OMC<T> sd2)
{
Debug.LogWarning("Cannot check Equivalency for " + this.GetType() + "; only whether it's exact!");
return this.value.Equals(value);
}
protected internal override LambdaExpression GetLambdaExpression(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
=> Expression.Lambda(Expression.Constant(value, typeof(T)), null);
public override string ToString()
=> "C_" + typeof(T) + "(" + value.ToString() + ")";
public override OMC<T> MapURIsWrapped(Dictionary<string, string> old_to_new)
=> (OMC<T>)this.MemberwiseClone();
}
public class OMV : SOMDocCRTP<OMV>
{
public new string kind = "OMV";
public string name;
[JsonConstructor]
public OMV(string name) : base()
{
this.name = name;
}
protected override bool EquivalentWrapped(OMV sd2)
=> this.name == sd2.name;
protected internal override LambdaExpression GetLambdaExpression(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
{
ParameterExpression v = bound_params.FirstOrDefault(param => param.Name.Equals(name));
if (v == null)
{
Debug.LogErrorFormat("Unable to find {0} for {1} with name: {2}", nameof(OMBINDC), nameof(OMV), name);
return Expression.Lambda(Expression.Empty(), null);
}
else
return Expression.Lambda(v, new[] { v });
}
public override string ToString()
=> "Variable_" + "(" + name + ")";
public override OMV MapURIsWrapped(Dictionary<string, string> old_to_new)
=> (OMV)this.MemberwiseClone();
}
public class RAW : SOMDocCRTP<RAW>
{
public new string kind = "RAW";
public string xml;
[JsonConstructor]
public RAW(string xml) : base()
{
this.xml = xml;
}
public override RAW MapURIsWrapped(Dictionary<string, string> old_to_new)
{
string copy = xml;
foreach (KeyValuePair<string, string> KeyVal in old_to_new)
copy = copy.Replace(KeyVal.Key, KeyVal.Value);
return new RAW(copy);
}
public override string ToString()
=> xml;
protected override bool EquivalentWrapped(RAW sd2)
=> throw new NotImplementedException(); //xml == sd2.xml; // only exact
protected internal override LambdaExpression GetLambdaExpression(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
{
throw new NotImplementedException();
}
}
[JsonConverter(typeof(JsonSubtypes), "kind")]
[JsonSubtypes.KnownSubType(typeof(MMTSymbolDeclaration), "general")]
[JsonSubtypes.KnownSubType(typeof(MMTValueDeclaration), "veq")]
public abstract class MMTDeclaration
{
public string kind;
public string label;
public FactReference @ref;
public static MMTDeclaration FromJson(string json)
{
MMTDeclaration mmtDecl = JsonConvert.DeserializeObject<MMTDeclaration>(json);
mmtDecl.label ??= string.Empty;
return mmtDecl;
}
public string ToJson()
{
label ??= string.Empty;
return JsonConvert.SerializeObject(this);
}
public abstract string getType();
public abstract string getApplicant();
}
/// <summary>MMTSymbolDeclaration: Class for facts without values, e.g. Points</summary>
public class MMTSymbolDeclaration : MMTDeclaration
{
public new string kind = "general";
[JsonProperty("tp")]
public SOMDoc type;
[JsonProperty("df")]
public SOMDoc defines;
[JsonConstructor]
private MMTSymbolDeclaration() { }
/// <summary>Constructor used for sending new declarations to mmt</summary>
public MMTSymbolDeclaration(string label, SOMDoc type, SOMDoc defines)
{
this.label = label;
this.type = type;
this.defines = defines;
}
public override string getType()
{
return type switch
{
OMS oMS => oMS.uri,
OMA oMA => ((oMA.arguments[0] as OMA).applicant as OMS).uri,
_ => null
};
}
public override string getApplicant()
{
return defines switch
{
OMA oMA when oMA.applicant is OMS oMS => oMS.uri,
_ => null
};
}
}
/// <summary>MMTValueDeclaration: Class for facts with values, e.g. Distances or Angles</summary>
public class MMTValueDeclaration : MMTDeclaration
{
public new string kind = "veq";
public SOMDoc lhs;
[JsonProperty("valueTp")]
public SOMDoc valueType;
public SOMDoc value;
public SOMDoc proof;
[JsonConstructor]
private MMTValueDeclaration() { }
/// <summary>Constructor used for sending new declarations to mmt</summary>
public MMTValueDeclaration(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
};
}
}
}