using JsonSubTypes;
using Newtonsoft.Json;
using System.Collections.Generic;
using System.Linq;
using System.Text.RegularExpressions;
using static JSONsavable;

/// <summary>
/// Implements REST/JSON API
/// </summary>
/// <seealso href="https://github.com/UniFormal/MMT/tree/devel/src/frameit-mmt#rest-api"/>
namespace REST_JSON_API
{
    public class ScrollApplicationInfo
    {
        /// <remarks>Invariant: <see cref="valid"/> == <c>false</c> => <see cref="errors"/><c>.Length > 0</c></remarks>
        [JsonProperty("valid")]
        public bool valid;

        [JsonProperty("errors")]
        public ScrollApplicationCheckingError[] errors;

        [JsonProperty("acquiredFacts")]
        public List<MMTFact> acquiredFacts;
    }

    /// <summary>Response to "POST /scroll/dynamic" using <see cref="ScrollApplication"/></summary>
    public class ScrollDynamicInfo : IJSONsavable<ScrollDynamicInfo>
    {
        /// <summary>Contains the original scroll.</summary>
        [JsonProperty("original"), JsonAutoPostProcess]
        public Scroll original;

        /// <summary>All fact and scroll labels, all fact types, and all fact definitions are subject to being dynamically adapted to the (possibly utterly partial) scroll application.</summary>
        /// <remarks>Contains <see cref="Scroll.requiredFacts"/> inferred/forward hints (A,B,C => °ABC)</remarks>
        [JsonProperty("rendered"), JsonAutoPostProcess]
        public Scroll rendered;

        /// <summary>
        /// An array of scroll view completion suggestions for the yet missing assignments. 
        /// For instance, the first element of completions might be a list of some (possibly not all) of the yet missing assignments of the request's scroll view. 
        /// Analogously for the other elements of completions, if they exist. 
        /// It might happen that multiple mutually exclusive completions exist, hence the response contains an array of them.
        /// </summary>
        /// <remarks>Contains backwart hints (°ABC => A,B,C)</remarks>
        [JsonProperty("completions")]
        public List<List<ScrollAssignment>> backward_completions;

        /// <remarks>Invariant: <see cref="valid"/> == <c>false</c> => <see cref="errors"/><c>.Length > 0</c></remarks>
        [JsonProperty("valid")]
        public bool valid;

        [JsonProperty("errors")]
        public ScrollApplicationCheckingError[] errors;

        public string name { get => throw new System.NotImplementedException(); set => throw new System.NotImplementedException(); }
        public string path { get => throw new System.NotImplementedException(); set => throw new System.NotImplementedException(); }
    }

    public class FactReference
    {
        /// <summary>MMT URI</summary>
        [JsonProperty("uri")]
        public string uri;

        public FactReference(string uri)
        {
            this.uri = uri;
        }
    }

    [JsonConverter(typeof(JsonSubtypes), "kind")]
    [JsonSubtypes.KnownSubType(typeof(MMTGeneralFact), "general")]
    [JsonSubtypes.KnownSubType(typeof(MMTValueFact), "veq")]
    public abstract class MMTFact
    {
        [JsonProperty("kind")]
        public abstract string kind { get; }

        [JsonProperty("label")]
        public string label
        {
            get => _label ??= Regex.Match(@ref.uri, @".*\?(.*)").Captures[0].Value;
            set => _label = value;
        }
        private string _label;

        [JsonProperty("ref")]
        public OMS @ref;

        public abstract string getType();

        public abstract string getApplicant();

        public abstract SOMDoc GetDefines();

        public abstract MMTFact MapURIs(Dictionary<string, string> old_to_new);

        public abstract string[] GetDependentFactIds();

        public static bool Equivalent(MMTFact f1, MMTFact f2)
            => f1.Equivalent(f2);

        public bool Equivalent(MMTFact f2)
            => this.getType().Equals(f2.getType())
            && EquivalentWrapped(this, f2);

        protected abstract bool EquivalentWrapped(MMTFact f1, MMTFact f2);

        public abstract SOMDoc GetMMTType();

        public new abstract string ToString();
    }

    /// <summary>Class for facts without values, e.g. Points</summary>
    public class MMTGeneralFact : MMTFact
    {
        public override string kind => "general";

        [JsonProperty("tp")]
        public SOMDoc type;
        [JsonProperty("df")]
        public SOMDoc defines;


        [JsonConstructor]
        private MMTGeneralFact(OMS @ref, string label, SOMDoc type, SOMDoc defines)
        {
            this.@ref = @ref;
            this.label = label;
            this.type = type;
            this.defines = defines;
        }

        /// <summary>Constructor used for sending new declarations to mmt</summary>
        public MMTGeneralFact(string label, SOMDoc type, SOMDoc defines)
        {
            this.label = label;
            this.type = type;
            this.defines = defines;
        }

        public override string getType()
        {
            if (type is OMS oms)
                return oms.uri;

            if (type is OMA oma)
            {
                if (oma.applicant is OMS ded
                 && ded.uri == MMTConstants.Ded)
                    return ((oma.arguments[0] as OMA)
                        .applicant as OMS).uri;
                else
                    return (oma
                        .applicant as OMS).uri;
            }

            if (type is FUNTYPE)
                return MMTConstants.FunctionFact;

            return null;
        }

        public override string getApplicant()
        {
            return defines switch
            {
                OMA oMA when oMA.applicant is OMS oMS => oMS.uri,
                _ => null
            };
        }

        public override MMTFact MapURIs(Dictionary<string, string> old_to_new)
            => new MMTGeneralFact(@ref, label, type.MapURIs(old_to_new), defines.MapURIs(old_to_new));

        public override SOMDoc GetDefines() => defines;

        public override string[] GetDependentFactIds()
            => type.GetDependentFactIds().ShallowCloneAppend(defines.GetDependentFactIds());

        protected override bool EquivalentWrapped(MMTFact f1, MMTFact f2)
        {
            MMTGeneralFact g1 = (MMTGeneralFact)f1;
            MMTGeneralFact g2 = (MMTGeneralFact)f2;

            return g1.type.Equivalent(g2.type)
                && g1.defines.Equivalent(g2.defines);
        }

        public override SOMDoc GetMMTType()
            => type;

        public override string ToString()
            => $"[{type}]: {defines}";
    }

    /// <summary>Class for facts with values, e.g. Distances or Angles</summary>
    public class MMTValueFact : MMTFact
    {
        public override string kind => "veq";

        [JsonProperty("lhs")]
        public SOMDoc lhs;

        [JsonProperty("valueTp")]
        public SOMDoc valueType;

        [JsonProperty("value")]
        public SOMDoc value;

        [JsonProperty("proof")]
        public SOMDoc proof;

        [JsonConstructor]
        private MMTValueFact(OMS @ref, string label, SOMDoc lhs, SOMDoc valueType, SOMDoc value, SOMDoc proof = null)
        {
            this.@ref = @ref;
            this.label = label;
            this.lhs = lhs;
            this.valueType = valueType;
            this.value = value;
            this.proof = proof;
        }

        /// <summary>Constructor used for sending new declarations to mmt</summary>
        public MMTValueFact(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
            };
        }

        public override MMTFact MapURIs(Dictionary<string, string> old_to_new)
            => new MMTValueFact(@ref, label,
                    lhs.MapURIs(old_to_new),
                    valueType.MapURIs(old_to_new),
                    value.MapURIs(old_to_new),
                    proof.MapURIs(old_to_new)
                );

        public override SOMDoc GetDefines() => value;

        public override string[] GetDependentFactIds()
            => lhs.GetDependentFactIds().ShallowCloneAppend(value.GetDependentFactIds());

        protected override bool EquivalentWrapped(MMTFact f1, MMTFact f2)
        {
            MMTValueFact g1 = (MMTValueFact)f1;
            MMTValueFact g2 = (MMTValueFact)f2;

            return g1.lhs.Equivalent(g2.lhs)
                && g1.value.Equivalent(g2.value);
        }

        public override SOMDoc GetMMTType()
        {
            throw new System.NotImplementedException();
        }

        public override string ToString()
            => $"<{lhs}> == <{value}>";
    }

    public class Scroll: IJSONsavable<Scroll>
    {
        /// <summary>MMT URI to theory declaring the scroll</summary>
        [JsonProperty("ref")]
        public string ScrollReference;

        /// <summary>"some label"</summary>
        [JsonProperty("label")]
        public string label;

        /// <summary>"some description"</summary>
        [JsonProperty("description")]
        public string description;

        /// <summary>array of facts; facts that the scroll required you to give for scroll application</summary>
        [JsonProperty("requiredFacts")]
        public List<MMTFact> requiredFacts;

        /// <summary>array of facts; facts that the scroll gives you upon successful scroll application</summary>
        [JsonProperty("acquiredFacts")]
        public List<MMTFact> acquiredFacts;

#region IJSONsavable<Scroll>
        public string name { get => throw new System.NotImplementedException(); set => throw new System.NotImplementedException(); }
        public string path { get => throw new System.NotImplementedException(); set => throw new System.NotImplementedException(); }

        Scroll IJSONsavable<Scroll>._IJPostProcess(Scroll payload)
        {
            // remove already defined facts
            payload.requiredFacts = payload.requiredFacts
                .Where(f => f.GetDefines() == null)
                .ToList();

            return payload;
        }
#endregion IJSONsavable<Scroll>
    }

    public class ScrollAssignment
    {
        [JsonProperty("fact")]
        public FactReference fact; // Key

        [JsonProperty("assignment")]
        public SOMDoc assignment; // Value

        [JsonConstructor]
        private ScrollAssignment() { }

        public ScrollAssignment(string fact_id, string assignment_id)
        {
            this.fact = new FactReference(fact_id);
            this.assignment = new OMS(assignment_id);
        }

        public ScrollAssignment(string fact_id, SOMDoc assignment)
        {
            this.fact = new FactReference(fact_id);
            this.assignment = assignment;
        }
    }

    public class ScrollApplication
    {
        /// <summary>MMT URI to theory declaring the scroll</summary>
        [JsonProperty("scroll")]
        public string ScrollReference;

        [JsonProperty("assignments")]
        public List<ScrollAssignment> assignments;

        public ScrollApplication(string scroll, List<ScrollAssignment> assignments)
        {
            this.ScrollReference = scroll;
            this.assignments = assignments;
        }
    }

    public class ScrollApplicationCheckingError
    {
        /// <summary>"invalidAssignment" | "unknown"</summary>
        /// <remarks>above list maybe incomplete</remarks>
        [JsonProperty("kind")]
        public string kind;

        /// <summary>some human-readable message</summary>
        [JsonProperty("msg")]
        public string msg;

        /// <summary>a fact reference to the fact whose assignment was erroneous</summary>
        [JsonProperty("fact")]
        public FactReference fact;
    }
}