JSONManager.cs

using System.Collections.Generic;
using Newtonsoft.Json;
using JsonSubTypes;
using System.Linq.Expressions;
using System;
using System.Linq;
using MoreLinq;
using UnityEngine;

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 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 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()
        {
            { MMTURIs.Sin, 
                MakeSin},
            { MMTURIs.Cos, 
                MakeCos},
            { MMTURIs.SquareRoot, 
                MakeCos},
        };

        private static readonly Dictionary<string, ExpressionType> MMTtoBinaryExpressionType = new()
        {
            { MMTURIs.Add, 
                ExpressionType.Add},
            { "AddAssign", 
                ExpressionType.AddAssign},
            { "AddAssignChecked", 
                ExpressionType.AddAssignChecked},
            { "AddChecked", 
                ExpressionType.AddChecked},
            { "And", 
                ExpressionType.And},
            { "AndAlso", 
                ExpressionType.AndAlso},
            { "AndAssign", 
                ExpressionType.AndAssign},
            { "Assign", 
                ExpressionType.Assign},
            { MMTURIs.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},
            { MMTURIs.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},
            { MMTURIs.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(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));

        // TODO: LambdaExpression?wtf
        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
                );
    }


    [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 MMTTerm
    {
        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());

        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 LambdaExpression GetReducedLambdaExpression()
            => ReduceArguments(this.GetLambdaExpression());

        public abstract LambdaExpression GetLambdaExpression(LambdaExpression[] args = null);

        public abstract override string ToString();
    }

    public class OMA : MMTTerm
    {
        public string kind = "OMA";

        public MMTTerm applicant;
        public List<MMTTerm> arguments;

        [JsonConstructor]
        public OMA(MMTTerm applicant, List<MMTTerm> arguments)
        {
            this.applicant = applicant;
            this.arguments = arguments;
        }

        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 class OMS : MMTTerm
    {
        public string kind = "OMS";

        public string uri;

        [JsonConstructor]
        public OMS(string uri)
        {
            this.uri = uri;
        }

        public override LambdaExpression GetLambdaExpression(LambdaExpression[] args)
            => MMTtoLambdaExpression<float>.MakeLambdaExpression(uri, args);

        public override string ToString()
            => uri;
    }

    public class OMSTR : MMTTerm
    {
        public string kind = "OMSTR";
        
        [JsonProperty("float")]
        public string s;

        [JsonConstructor]
        public OMSTR(string s)
        {
            this.s = s;
        }

        public override LambdaExpression GetLambdaExpression(LambdaExpression[] args = null)
            => Expression.Lambda(Expression.Constant(s, typeof(string)), null);

        public override string ToString()
            => s;
    }

    public class OMF : MMTTerm
    {
        public string kind = "OMF";
        
        [JsonProperty("float")]
        public float f;

        [JsonConstructor]
        public OMF(float f)
        {
            this.f = f;
        }

        public override LambdaExpression GetLambdaExpression(LambdaExpression[] args = null)
            => Expression.Lambda(Expression.Constant(f, typeof(float)), null);

        public override string ToString()
            => f.ToString();
    }

    public class OMC<T> : MMTTerm
    {
        public string kind = "OMC<" + typeof(T) + ">";

        public T value;

        [JsonConstructor]
        public OMC(T value)
        {
            this.value = 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() + ")";
    }

    // TODO doesntt work, needs Iconvertable for convert
    //public class OMC : MMTTerm
    //{
    //    public string kind = "OMC";

    //    /// <summary>@Type of this constant</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];
    //    }

    //    public object value;

    //    [JsonConstructor]
    //    public OMC(object value, string typeString)
    //    {
    //        this.value = value;
    //        this.typeString = typeString;
    //    }

    //    public OMC(object value, Type type)
    //    {
    //        this.value = value;
    //        this.type = type;
    //    }

    //    public override LambdaExpression GetLambdaExpression(LambdaExpression[] args = null)
    //        => Expression.Lambda(Expression.Constant(Convert.ChangeType(value, type), type), null);

    //    public override string ToString()
    //        => "C_" + typeString + "(" + Convert.ChangeType(value, type).ToString() + ")";
    //}

    public class OMV : MMTTerm
    {
        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)
        {
            this.name = name;
            this.typeString = typeString;
        }

        public OMV(string name, Type type)
        {
            this.name = name;
            this.type = 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 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;
        }
    }
}