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> { private static LambdaExpression @default = Expression.Lambda(Expression.Default(typeof(T)), null); // TODO: Populate Dictionaries #region ExpressionDictionaries private static Dictionary<string, Func<LambdaExpression>> MMTtoLambdaMaker = new() { { "sin", MakeSin}, { "cos", MakeCos}, }; private static 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 Dictionary<string, ExpressionType> MMTtoUnaryExpressionType = new() { //{ "Constant", // Not Unary // ExpressionType.Constant}, { "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) { if (MMTtoUnaryExpressionType.TryGetValue(URI, out var unnary_type)) { ParameterExpression[] args = new ParameterExpression[] { Expression.Parameter(typeof(T)) }; return Expression.Lambda(Expression.MakeUnary(unnary_type, args[0], typeof(T)), args); } else if (MMTtoBinaryExpressionType.TryGetValue(URI, out var binary_type)) { ParameterExpression[] args = new ParameterExpression[] { Expression.Parameter(typeof(T)), Expression.Parameter(typeof(T)) }; return Expression.Lambda(Expression.MakeBinary(binary_type, args[0], args[1]), args); } else if (MMTtoLambdaMaker.TryGetValue(URI, out var lamda_maker)) { return lamda_maker(); } throw new NotImplementedException("Could not map URI: \"" + URI + "\""); } private static Expression<Func<T, T>> ParseFuncTUUT<U>(Func<U,U> func) => (T x) => (T) Convert.ChangeType( func( (U) Convert.ChangeType( x, typeof(U) ) ), typeof(T) ); private static LambdaExpression ExpresionFuncToLambda(Expression func, 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), args); } //TODO? more general/generics private static LambdaExpression ParseFuncTUUTToLambda<U>(Func<U, U> func) => ExpresionFuncToLambda(ParseFuncTUUT<U>(func), 1); private static LambdaExpression MakeSin() => default(T) switch // TODO? cleaner switch { float => ParseFuncTUUTToLambda<float>(MathF.Sin), double => ParseFuncTUUTToLambda<double>(Math.Sin), _ => throw new NotImplementedException("Sinus for " + typeof(T)) }; private static LambdaExpression MakeCos() => default(T) switch { float => ParseFuncTUUTToLambda<float>(MathF.Cos), double => ParseFuncTUUTToLambda<double>(Math.Cos), _ => throw new NotImplementedException("Sinus for " + typeof(T)) }; } 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() => 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() { // local variable for each arguments ParameterExpression[] line_variable = new ParameterExpression[arguments.Count]; // expression of computing arguments and assigning to corresponding variable Expression[] line_expression = new Expression[arguments.Count + 1]; // unbound parameters a.k.a. all params of arguments List<ParameterExpression> father_param = new(); for (int i = 0; i < arguments.Count; i++) { LambdaExpression child_lambda = arguments[i].GetLambdaExpression(); List<ParameterExpression> child_params = child_lambda.Parameters.ToList(); line_variable[i] = Expression.Variable(child_lambda.ReturnType); line_expression[i] = Expression.Assign(line_variable[i], Expression.Invoke(child_lambda, child_params)); foreach (ParameterExpression arg in child_params) father_param.Add(arg); } // invoke applicant with computed arguments line_expression[arguments.Count] = Expression.Invoke(applicant.GetLambdaExpression(), line_variable); // compile all this into LambdaExpression return Expression.Lambda(Expression.Block(line_variable, line_expression), father_param); } } public class OMS : MMTTerm { public string uri; public string kind = "OMS"; public OMS(string uri) { this.uri = uri; } override public LambdaExpression GetLambdaExpression() => MMTtoLambdaExpression<float>.MakeLambdaExpression(uri); } public class OMSTR : MMTTerm { [JsonProperty("float")] public string s; public string kind = "OMSTR"; public OMSTR(string s) { this.s = s; } override public LambdaExpression GetLambdaExpression() => 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() => 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); if (mmtDecl.label == null) mmtDecl.label = string.Empty; return mmtDecl; } public static string ToJson(MMTDeclaration mmtDecl) { if (mmtDecl.label == null) 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; } } }