SOMDocManager.cs

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

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 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) },

            { RealLit,
                typeof(float) },
            { Tuple,
                typeof(Vector3) },
            { 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();
            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,
                MakeUnityEngineVector3 },
            { MMT_OMS_URI.MakeObjectArray,
                MakeArray },
            { "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;
            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(
                    default(T) switch // TODO? cleaner switch
                    {
                        float => ParseFuncUUToExpression<float>(MathF.Sin),
                        double => ParseFuncUUToExpression<double>(Math.Sin),
                        _ => throw new NotImplementedException("Sinus for " + nameof(T) + "=" + typeof(T))
                    },
                    "Sin", lambda_applicant, bound_params, 1
                );

        private static LambdaExpression MakeCos(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
            => ExpresionFuncToLambda(
                    default(T) switch // TODO? cleaner switch
                    {
                        float => ParseFuncUUToExpression<float>(MathF.Cos),
                        double => ParseFuncUUToExpression<double>(Math.Cos),
                        _ => throw new NotImplementedException("Cosinus for " + nameof(T) + "=" + typeof(T))
                    },
                    "Cos", lambda_applicant, bound_params, 1
                );

        private static LambdaExpression MakeUnityEngineVector3(LambdaExpression[] lambda_applicant, LambdaExpression[] lambda_arguments, ParameterExpression[] bound_params)
            => ExpresionFuncToLambda(
                    (Expression<Func<float, float, float, Vector3>>)((x, y, z) => new Vector3(x, y, z)),
                    "UnityEngineVector3", lambda_applicant, bound_params, 3
                );

        private static LambdaExpression MakeArray(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>")]
    [JsonSubtypes.FallBackSubType(typeof(OMS))] // dirty fix for wrong formated ScrollApplicationCheckingError.fact
    abstract public class SOMDoc
    {
        public string kind;

        protected SOMDoc() { kind = this.GetType().Name; }

        public static bool Equivalent(SOMDoc sd1, SOMDoc sd2)
            => 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 MakeUnityEngineVector3(Vector3 vec)
            => new OMA(
                new OMS(MMT_OMS_URI.Tuple),
                    new() {
                        new OMF(vec.x),
                        new OMF(vec.y),
                        new OMF(vec.z),
                    }
                );

        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)
        {
            List<SOMDoc> end_of_list = new() {
                new OMA(
                    new OMS(MMT_OMS_URI.ListEnd),
                    new() {
                        new OMS(typeURI),
            }),};

            if (lids.Length > 0)
                end_of_list.Add(new OMS(lids[^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 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);

        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)).ToList()
            );
    }

    public class OMS : SOMDocCRTP<OMS> //OMSTR?
    {
        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 UriReference @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
            };
        }
    }
}