using System.Collections.Generic; using Newtonsoft.Json; using JsonSubTypes; using System.Linq.Expressions; using System.Reflection; using UnityEngine.UIElements; using System; using static UnityEngine.Windows.Speech.PhraseRecognitionSystem; using System.Linq; public static class JSONManager { public static class MMTURIs { 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 class MMTtoLambdaExpression<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 private static readonly Dictionary<string, Func<LambdaExpression[], LambdaExpression>> MMTtoLambdaMaker = new() { { "sin", MakeSin}, { "cos", MakeCos}, }; private static readonly Dictionary<string, ExpressionType> MMTtoBinaryExpressionType = new() { { "Add", ExpressionType.Add}, { "AddAssign", ExpressionType.AddAssign}, { "AddAssignChecked", ExpressionType.AddAssignChecked}, { "AddChecked", ExpressionType.AddChecked}, { "And", ExpressionType.And}, { "AndAlso", ExpressionType.AndAlso}, { "AndAssign", ExpressionType.AndAssign}, { "Assign", ExpressionType.Assign}, { "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}, { "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}, { "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() )); } ParameterExpression[] args_param = args_lamda?.SelectMany(l => l.Parameters).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(Expression 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(Expression 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 Expression<Func<U, U>> 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 ); } public class URI { public string uri; public URI(string uri) { this.uri = uri; } } [JsonConverter(typeof(JsonSubtypes), "kind")] public class MMTTerm { string kind; virtual public LambdaExpression GetLambdaExpression(LambdaExpression[] args = null) => Expression.Lambda(Expression.Empty(), null); } public class OMA : MMTTerm { public MMTTerm applicant; public List<MMTTerm> arguments; public string kind = "OMA"; public OMA(MMTTerm applicant, List<MMTTerm> arguments) { this.applicant = applicant; this.arguments = arguments; } override public LambdaExpression GetLambdaExpression(LambdaExpression[] args = null) => applicant.GetLambdaExpression(arguments?.Select(mmt => mmt.GetLambdaExpression()).ToArray()); } public class OMS : MMTTerm { public string uri; public string kind = "OMS"; public OMS(string uri) { this.uri = uri; } override public LambdaExpression GetLambdaExpression(LambdaExpression[] args) => MMTtoLambdaExpression<float>.MakeLambdaExpression(uri, args); } public class OMSTR : MMTTerm { [JsonProperty("float")] public string s; public string kind = "OMSTR"; public OMSTR(string s) { this.s = s; } override public LambdaExpression GetLambdaExpression(LambdaExpression[] args = null) => Expression.Lambda(Expression.Constant(s, typeof(string)), null); } public class OMF : MMTTerm { [JsonProperty("float")] public float f; public string kind = "OMF"; public OMF(float f) { this.f = f; } override public LambdaExpression GetLambdaExpression(LambdaExpression[] args = null) => Expression.Lambda(Expression.Constant(f, typeof(float)), null); } 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 MMTTerm tp; public MMTTerm df; /** * Constructor used for sending new declarations to mmt */ public MMTSymbolDeclaration(string label, MMTTerm tp, MMTTerm 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 MMTTerm lhs; public MMTTerm valueTp; public MMTTerm value; /** * Constructor used for sending new declarations to mmt */ public MMTValueDeclaration(string label, MMTTerm lhs, MMTTerm valueTp, MMTTerm value) { this.label = label; this.lhs = lhs; this.valueTp = valueTp; this.value = value; } } }