SOMDocManager.cs 24.58 KiB
using System.Collections.Generic;
using Newtonsoft.Json;
using JsonSubTypes;
using System.Linq.Expressions;
using System;
using System.Linq;
using MoreLinq;
using UnityEngine;
using static UnityEditor.PlayerSettings;
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 TestType = "http://mathhub.info/FrameIT/frameworld?FrameITCircle?xcircleType3D";
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 class SOMDoctoLambdaExpression<T>
{
public static readonly LambdaExpression @default = Expression.Lambda(Expression.Default(typeof(T)), null);
private static uint param_counter = 0; //for better debugs
// TODO: Populate Dictionaries
#region ExpressionDictionaries
delegate LambdaExpression CustomFunction(LambdaExpression[] args_lamda);
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.MakeUnityEngineVector3,
MakeUnityEngineVector3},
};
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
public static LambdaExpression MakeLambdaExpression(string URI, LambdaExpression[] args_lamda = null)
{
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, args_lamda.Count()
));
} //TODO distinct! (in args_lamda and duplicate?)
ParameterExpression[] args_param = args_lamda?.SelectMany(l => l.Parameters).ToArray(); //.DistinctBy(p => p.Name).ToArray();
if (MMTtoUnaryExpressionType.TryGetValue(URI, out var unnary_type))
{
if (args_lamda == null)
{
ParameterExpression[] args = new ParameterExpression[] {
Expression.Parameter(typeof(T), "PNamed_" + param_counter++.ToString()),
};
return Expression.Lambda(Expression.MakeUnary(unnary_type, args[0], typeof(T)), args);
}
else
{
if (args_lamda.Count() < 1)
ThrowArgumentException(unnary_type, 1);
Type UnarySecondArgument = args_lamda.Count() < 2 ? null : args_lamda[1].ReturnType;
return Expression.Lambda(Expression.MakeUnary(unnary_type, args_lamda[0].Body, UnarySecondArgument), args_param);
}
}
else if (MMTtoBinaryExpressionType.TryGetValue(URI, out var binary_type))
{
if (args_lamda == null)
{
ParameterExpression[] args = new ParameterExpression[] {
Expression.Parameter(typeof(T), "PNamed_" + param_counter++.ToString()),
Expression.Parameter(typeof(T), "PNamed_" + param_counter++.ToString()),
};
return Expression.Lambda(Expression.MakeBinary(binary_type, args[0], args[1]), args);
}
else
{
if (args_lamda.Count() != 2)
ThrowArgumentException(binary_type, 2);
return Expression.Lambda(Expression.MakeBinary(binary_type, args_lamda[0].Body, args_lamda[1].Body), args_param);
}
}
else if (MMTtoLambdaMaker.TryGetValue(URI, out var lamda_maker))
{
return lamda_maker(args_lamda ?? null); //args_lamda == null ok
}
throw new NotImplementedException("Could not map URI: \"" + URI + "\"");
}
private static LambdaExpression ExpresionFuncToLambda(LambdaExpression func, string name, uint nTargs)
{
ParameterExpression[] args = new ParameterExpression[nTargs];
for (int i = 0; i < nTargs; i++)
args[i] = Expression.Parameter(typeof(T));
return Expression.Lambda(Expression.Invoke(func, args), name, args);
}
private static LambdaExpression ExpresionFuncToLambda(LambdaExpression func, string name, LambdaExpression[] args_lamda, uint nTargs_fallback)
=> args_lamda == null || args_lamda.Count() == 0
? ExpresionFuncToLambda(func, name, nTargs_fallback)
: Expression.Lambda(Expression.Invoke(func, args_lamda.Select(l => l.Body)), name, args_lamda.SelectMany(l => l.Parameters));
private static LambdaExpression ParseFuncUUToExpression<U>(Func<U, U> func)
=> (Expression<Func<U, U>>)((x) => func(x));
private static LambdaExpression MakeSin(LambdaExpression[] args_lamda)
=> ExpresionFuncToLambda(
default(T) switch // TODO? cleaner switch
{
float => ParseFuncUUToExpression<float>(MathF.Sin), double => ParseFuncUUToExpression<double>(Math.Sin),
_ => throw new NotImplementedException("Sinus for " + typeof(T))
},
"Sin", args_lamda, 1
);
private static LambdaExpression MakeCos(LambdaExpression[] args_lamda)
=> ExpresionFuncToLambda(
default(T) switch // TODO? cleaner switch
{
float => ParseFuncUUToExpression<float>(MathF.Cos),
double => ParseFuncUUToExpression<double>(Math.Cos),
_ => throw new NotImplementedException("Cosinus for " + typeof(T))
},
"Cos", args_lamda, 1
);
private static LambdaExpression MakeUnityEngineVector3(LambdaExpression[] args_lamda)
=> ExpresionFuncToLambda(
(Expression<Func<float, float, float, Vector3>>)((x, y, z) => new Vector3(x, y, z)),
"UnityEngineVector3", args_lamda, 3
);
}
[JsonConverter(typeof(JsonSubtypes), "kind")]
[JsonSubtypes.KnownSubType(typeof(OMA), "OMA")]
[JsonSubtypes.KnownSubType(typeof(OMS), "OMS")]
[JsonSubtypes.KnownSubType(typeof(OMSTR), "OMSTR")]
[JsonSubtypes.KnownSubType(typeof(OMF), "OMF")]
[JsonSubtypes.KnownSubType(typeof(OMV), "OMV")]
//[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
{
string kind;
[JsonIgnore]
public static readonly Dictionary<string, Type> allowedTypes =
new Type[] { typeof(float), typeof(double), typeof(string), typeof(UnityEngine.Vector3) }
.ToDictionary(t => t.ToString());
protected SOMDoc() { }
public static LambdaExpression ReduceArguments(LambdaExpression expr)
{
var reduced_params = expr.Parameters.GroupBy(p => p.Name).Select(p => p.First()).ToArray();
var name_to_params = reduced_params.ToDictionary(p => p.Name);
return
Expression.Lambda(
Expression.Invoke(
expr,
expr.Parameters.Select(p => name_to_params[p.Name])),
reduced_params);
}
public static bool Equivalent(SOMDoc sd1, SOMDoc sd2)
=> sd1.Equivalent(sd2);
public abstract bool Equivalent(SOMDoc sd2);
public LambdaExpression GetReducedLambdaExpression()
=> ReduceArguments(this.GetLambdaExpression());
public abstract LambdaExpression GetLambdaExpression(LambdaExpression[] args = null);
public abstract override string ToString();
public abstract SOMDoc MapURIs(Dictionary<string, string> old_to_new);
#region MakeMMT_OMS_URItoSOMDoc
public static SOMDoc MakeUnityEngineVector3(Vector3 vec)
=> new OMA(
new OMS(MMT_OMS_URI.MakeUnityEngineVector3),
new() {
new OMF(vec.x),
new OMF(vec.y),
new OMF(vec.z),
}
);
#endregion MakeMMT_OMS_URItoSOMDoc
}
public abstract class SOMDocCRTP<T> : SOMDoc where T : SOMDocCRTP<T>
{
protected SOMDocCRTP() : base() { }
/// \copydoc Fact.Equivalent(Fact)
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 OMA : SOMDocCRTP<OMA>
{
public string kind = "OMA";
public SOMDoc applicant;
public List<SOMDoc> arguments;
[JsonConstructor]
public OMA(SOMDoc applicant, List<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);
public override LambdaExpression GetLambdaExpression(LambdaExpression[] args = null)
=> applicant.GetLambdaExpression(arguments?.Select(mmt => mmt.GetLambdaExpression()).ToArray());
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)).ToList()
);
}
public class OMS : SOMDocCRTP<OMS> //OMSTR?
{
public 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;
public override LambdaExpression GetLambdaExpression(LambdaExpression[] args)
=> SOMDoctoLambdaExpression<float>.MakeLambdaExpression(uri, args);
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 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;
public override LambdaExpression GetLambdaExpression(LambdaExpression[] args = null)
=> 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 string kind = "OMF";
[JsonProperty("float")]
public float f;
[JsonConstructor]
public OMF(float f) : base()
{
this.f = f;
}
protected override bool EquivalentWrapped(OMF sd2)
=> this.f.IsApproximatelyEqual(sd2.f);
public override LambdaExpression GetLambdaExpression(LambdaExpression[] args = null) => Expression.Lambda(Expression.Constant(f, typeof(float)), null);
public override string ToString()
=> f.ToString();
public override OMF MapURIsWrapped(Dictionary<string, string> old_to_new)
=> (OMF)this.MemberwiseClone();
}
public class OMC<T> : SOMDocCRTP<OMC<T>>
{
public 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);
}
public override LambdaExpression GetLambdaExpression(LambdaExpression[] args = null)
=> 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 string kind = "OMV";
public string name;
/// <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 => type.ToString();
set => type = allowedTypes[value];
}
[JsonConstructor]
public OMV(string name, string typeString) : base()
{
this.name = name;
this.typeString = typeString;
}
public OMV(string name, Type type) : base()
{
this.name = name;
this.type = type;
}
protected override bool EquivalentWrapped(OMV sd2)
=> this.type == sd2.type;
public override LambdaExpression GetLambdaExpression(LambdaExpression[] args = null)
{
ParameterExpression v = Expression.Parameter(type, name);
return Expression.Lambda(v, new[] { v });
}
public override string ToString()
=> "V_" + name + "(" + typeString + ")";
public override OMV MapURIsWrapped(Dictionary<string, string> old_to_new)
=> (OMV)this.MemberwiseClone();
}
public class MMTDeclaration
{
public string label;
public static MMTDeclaration FromJson(string json)
{
MMTDeclaration mmtDecl = JsonConvert.DeserializeObject<MMTDeclaration>(json);
mmtDecl.label ??= string.Empty;
return mmtDecl;
}
public static string ToJson(MMTDeclaration mmtDecl)
{
mmtDecl.label ??= string.Empty;
string json = JsonConvert.SerializeObject(mmtDecl);
return json;
}
}
/**
* MMTSymbolDeclaration: Class for facts without values, e.g. Points
*/
public class MMTSymbolDeclaration : MMTDeclaration
{
public string kind = "general";
public SOMDoc tp;
public SOMDoc df;
/**
* Constructor used for sending new declarations to mmt
*/
public MMTSymbolDeclaration(string label, SOMDoc tp, SOMDoc df)
{
this.label = label;
this.tp = tp;
this.df = df;
}
}
/**
* MMTValueDeclaration: Class for facts with values, e.g. Distances or Angles
*/
public class MMTValueDeclaration : MMTDeclaration
{
public string kind = "veq";
public SOMDoc lhs;
public SOMDoc valueTp;
public SOMDoc value;
/**
* Constructor used for sending new declarations to mmt
*/
public MMTValueDeclaration(string label, SOMDoc lhs, SOMDoc valueTp, SOMDoc value)
{ this.label = label;
this.lhs = lhs;
this.valueTp = valueTp;
this.value = value;
}
}
}