AbstractAngleFact.cs

using Newtonsoft.Json;
using System;
using System.Collections.Generic;
using static SOMDocManager;
using TMPro;
using UnityEngine;
using UnityEngine.UIElements;

public abstract class AbstractAngleFact : FactWrappedCRTP<AbstractAngleFact>
{
    /// @{ <summary>
    /// One <see cref="Fact.Id">Id</see> of three <see cref="PointFact">PointFacts</see> defining Angle [<see cref="Pid1"/>, <see cref="Pid2"/>, <see cref="Pid3"/>].
    /// </summary>
    public string Pid1, Pid2, Pid3;
    /// @}

    [JsonIgnore]
    public PointFact Point1 { get => (PointFact)FactOrganizer.AllFacts[Pid1]; }
    [JsonIgnore]
    public PointFact Point2 { get => (PointFact)FactOrganizer.AllFacts[Pid2]; }
    [JsonIgnore]
    public PointFact Point3 { get => (PointFact)FactOrganizer.AllFacts[Pid3]; }

    /// <summary> <see langword="true"/>, if AngleFact is approximately 90° or 270°</summary>
    virtual public bool is_right_angle { get; set; } = false;

    /// <summary>
    /// Smallets angle in Degrees between [< see cref = "Pid1" />, < see cref = "Pid2" />] and[< see cref = "Pid2" />, < see cref = "Pid3" />]
    /// </summary>
    [JsonIgnore]
    virtual public float angle { get; set; } = -0f;

    /// <summary>\copydoc Fact.Fact</summary>
    protected AbstractAngleFact() : base()
    {
        this.Pid1 = null;
        this.Pid2 = null;
        this.Pid3 = null;
    }

    /// <summary>\copydoc AbstractAngleFact.AbstractAngleFact(AbstractAngleFact, Dictionary{string, string}, FactOrganizer)</summary>
    protected AbstractAngleFact(AbstractAngleFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer)
        : this(old_to_new[fact.Pid1], old_to_new[fact.Pid2], old_to_new[fact.Pid3], organizer) { }

    /// <summary>\copydoc AbstractAngleFact.AbstractAngleFact(string, string, FactOrganizer)</summary>
    protected AbstractAngleFact(string pid1, string pid2, string pid3, FactOrganizer organizer) : base(organizer)
    {
        this.Pid1 = pid1;
        this.Pid2 = pid2;
        this.Pid3 = pid3;

        RecalulateTransform();
    }

    /// <summary>\copydoc AbstractAngleFact.AbstractAngleFact(string, string, string, FactOrganizer)</summary>
    protected AbstractAngleFact(string pid1, string pid2, string pid3, float angle, string backendURI, FactOrganizer organizer)
        : this(pid1, pid2, pid3, organizer)
    {
        this.angle = angle;
        this._URI = backendURI;
    }

    /// \copydoc Fact.hasDependentFacts
    public override Boolean hasDependentFacts()
        => true;

    /// \copydoc Fact.getDependentFactIds
    public override string[] getDependentFactIds()
        => new string[] { Pid1, Pid2, Pid3 };

    protected override void RecalulateTransform()
    {
        Position = Point2.Position;
        { //Rotation
            Vector3 from = (Point1.Position - Position).normalized;
            Vector3 to = (Point3.Position - Position).normalized;

            Vector3 up = Vector3.Cross(from, to);
            Vector3 forwoard = (from + to).normalized;

            if (up.sqrMagnitude < Math3d.vectorPrecission)
            { //Angle is 180° (or 0°)
                Vector3 from_arbitary = from.normalized == Vector3.forward ? Vector3.right : Vector3.forward;
                up = Vector3.Cross(from_arbitary, to);
                forwoard = Vector3.Cross(up, to);
            }

            Rotation = Quaternion.LookRotation(forwoard, up);
        }
    }
}

public abstract class AbstractAngleFactWrappedCRTP<T> : AbstractAngleFact where T : AbstractAngleFactWrappedCRTP<T>
{
    /// <summary>\copydoc Fact.Fact</summary>
    protected AbstractAngleFactWrappedCRTP() : base() { }

    /// <summary>\copydoc AbstractAngleFactWrappedCRTP.AbstractAngleFactWrappedCRTP(AbstractAngleFactWrappedCRTP, Dictionary{string, string}, FactOrganizer)</summary>
    protected AbstractAngleFactWrappedCRTP(AbstractAngleFactWrappedCRTP<T> fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, old_to_new, organizer) { }

    /// <summary>\copydoc AbstractAngleFactWrappedCRTP.AbstractAngleFactWrappedCRTP(string, string, FactOrganizer)</summary>
    protected AbstractAngleFactWrappedCRTP(string pid1, string pid2, string pid3, FactOrganizer organizer) : base(pid1, pid2, pid3, organizer) { }

    /// <summary>\copydoc AbstractAngleFactWrappedCRTP.AbstractAngleFactWrappedCRTP(string, string, string, FactOrganizer)</summary>
    protected AbstractAngleFactWrappedCRTP(string pid1, string pid2, string pid3, float angle, string backendURI, FactOrganizer organizer) : base(pid1, pid2, pid3, angle, backendURI, organizer) { }

    /// \copydoc Fact.Equivalent(Fact, Fact)
    protected override bool EquivalentWrapped(AbstractAngleFact f1, AbstractAngleFact f2)
        => EquivalentWrapped((T)f1, (T)f2);

    /// <summary>CRTP step of <see cref="EquivalentWrapped(AbstractAngleFact, AbstractAngleFact)"/></summary>
    protected abstract bool EquivalentWrapped(T f1, T f2);
}

/// <summary>
/// Angle comprised of three <see cref="PointFact">PointFacts</see> [A,B,C]
/// </summary>
public class AngleFact : AbstractAngleFactWrappedCRTP<AngleFact>
{
    /// <summary> \copydoc Fact.Fact </summary>
    public AngleFact() : base() { }

    /// <summary>
    /// Copies <paramref name="fact"/> by initiating new MMT %Fact.
    /// </summary>
    /// <param name="fact">Fact to be copied</param>
    /// <param name="old_to_new"><c>Dictionary</c> mapping <paramref name="fact"/>.<see cref="getDependentFactIds"/> in <paramref name="fact"/>.<see cref="Fact._Facts"/> to corresponding <see cref="Fact.Id"/> in <paramref name="organizer"/> </param>
    /// <param name="organizer">sets <see cref="_Facts"/></param>
    public AngleFact(AngleFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer)
        : this(old_to_new[fact.Pid1], old_to_new[fact.Pid2], old_to_new[fact.Pid3], organizer) { }

    /// <summary>
    /// Standard Constructor:
    /// Initiates <see cref="Pid1"/>, <see cref="Pid2"/>, <see cref="Pid3"/>, <see cref="is_right_angle"/>, <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
    /// </summary>
    /// <param name="pid1">sets <see cref="Pid1"/></param>
    /// <param name="pid2">sets <see cref="Pid2"/></param>
    /// <param name="pid3">sets <see cref="Pid3"/></param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public AngleFact(string pid1, string pid2, string pid3, FactOrganizer organizer) : base(pid1, pid2, pid3, organizer)
    {
        angle = Vector3.Angle((Point1.Point - Point2.Point), (Point3.Point - Point2.Point));

        this.is_right_angle = Mathf.Abs(angle - 90.0f) < Math3d.vectorPrecission;

        angle = is_right_angle ? 90f : angle;

        MMTDeclaration mmtDecl = MakeMMTDeclaration(angle, pid1, pid2, pid3);
        AddFactResponse.sendAdd(mmtDecl, out this._URI);
    }

    /// <summary>
    /// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
    /// </summary>
    /// <param name="Pid1">sets <see cref="Pid1"/></param>
    /// <param name="Pid2">sets <see cref="Pid2"/></param>
    /// <param name="Pid3">sets <see cref="Pid3"/></param>
    /// <param name="backendURI">MMT URI</param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public AngleFact(string Pid1, string Pid2, string Pid3, float angle, string backendURI, FactOrganizer organizer) 
        : base(Pid1, Pid2, Pid3, angle, backendURI, organizer) { }

    /// <summary>
    /// Constructs struct for not-right-angled MMT %Fact <see cref="AddFactResponse"/>
    /// </summary>
    /// <param name="val">Angle != 90f, _not checked_</param>
    /// <param name="p1URI"><see cref="Pid1"/></param>
    /// <param name="p2URI"><see cref="Pid2"/></param>
    /// <param name="p3URI"><see cref="Pid3"/></param>
    /// <returns>struct for <see cref="AddFactResponse"/></returns>
    private MMTDeclaration MakeMMTDeclaration(float val, string p1URI, string p2URI, string p3URI)
    {
        SOMDoc lhs =
            new OMA(
                new OMS(MMT_OMS_URI.Angle),
                new List<SOMDoc> {
                    new OMS(p1URI),
                    new OMS(p2URI),
                    new OMS(p3URI)
                }
            );

        SOMDoc valueTp = new OMS(MMT_OMS_URI.RealLit);
        SOMDoc value = new OMF(val);

        return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
    }

    /// \copydoc Fact.parseFact(Scroll.ScrollFact)
    public new static AngleFact parseFact(Scroll.ScrollFact fact)
    {
        if (fact is not Scroll.ScrollValueFact value_fact) //If angle is a 90Degree-Angle
            throw new ArgumentException("Angle 90 degrees parsed. This shouldn't happen anymore");

        if (value_fact.lhs is not OMA df)
            return null;

        float angle = value_fact.value == null
            ? 0f
            : ((OMF)value_fact.value).f;

        string pointAUri = ((OMS)df.arguments[0]).uri;
        string pointBUri = ((OMS)df.arguments[1]).uri;
        string pointCUri = ((OMS)df.arguments[2]).uri;

        if (!StageStatic.stage.factState.ContainsKey(pointAUri)
         || !StageStatic.stage.factState.ContainsKey(pointBUri)
         || !StageStatic.stage.factState.ContainsKey(pointCUri))
            return null; //If dependent facts do not exist return null

        return new AngleFact(pointAUri, pointBUri, pointCUri, angle, fact.@ref.uri, StageStatic.stage.factState);
    }

    /// \copydoc Fact.generateLabel
    protected override string generateLabel()
        => (is_right_angle ? "⊾" : "∠") + Point1.Label + Point2.Label + Point3.Label;

    /// \copydoc Fact.instantiateDisplay(GameObject, Transform)
    public override GameObject instantiateDisplay(GameObject prefab, Transform transform)
    {
        var obj = GameObject.Instantiate(prefab, Vector3.zero, Quaternion.identity, transform);
        obj.transform.GetChild(0).gameObject.GetComponent<TextMeshProUGUI>().text = Point1.Label;
        obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = Point2.Label;
        obj.transform.GetChild(2).gameObject.GetComponent<TextMeshProUGUI>().text = Point3.Label;
        obj.GetComponent<FactWrapper>().fact = this;
        return obj;
    }

    /// \copydoc Fact.Equivalent(Fact, Fact)
    protected override bool EquivalentWrapped(AngleFact f1, AngleFact f2)
        => DependentFactsEquivalent(f1, f2);
}

/// <summary>
/// A RightAngleFact defined by 3  <see cref="PointFact">Pointfact</see> 
/// </summary>
public class RightAngleFact : AbstractAngleFactWrappedCRTP<RightAngleFact>
{
    override public bool is_right_angle { get => true; }
    override public float angle {get => 90f;}

    /// <summary> \copydoc Fact.Fact </summary>
    public RightAngleFact() : base() { }

    /// <summary>
    /// Copies <paramref name="fact"/> by initiating new MMT %Fact.
    /// </summary>
    /// <param name="fact">Fact to be copied</param>
    /// <param name="old_to_new"><c>Dictionary</c> mapping <paramref name="fact"/>.<see cref="getDependentFactIds"/> in <paramref name="fact"/>.<see cref="Fact._Facts"/> to corresponding <see cref="Fact.Id"/> in <paramref name="organizer"/> </param>
    /// <param name="organizer">sets <see cref="_Facts"/></param>
    public RightAngleFact(RightAngleFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer)
        : this(old_to_new[fact.Pid1], old_to_new[fact.Pid2], old_to_new[fact.Pid3], organizer) { }

    /// <summary>
    /// Standard Constructor:
    /// Initiates <see cref="Pid1"/>, <see cref="Pid2"/>, <see cref="Pid3"/>, <see cref="is_right_angle"/>, <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
    /// </summary>
    /// <param name="pid1">sets <see cref="Pid1"/></param>
    /// <param name="pid2">sets <see cref="Pid2"/></param>
    /// <param name="pid3">sets <see cref="Pid3"/></param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public RightAngleFact(string pid1, string pid2, string pid3, FactOrganizer organizer) : base(pid1, pid2, pid3, organizer)
    {
        angle = 90f;

        MMTDeclaration mmtDecl = MakeMMTDeclaration(pid1, pid2, pid3);
        AddFactResponse.sendAdd(mmtDecl, out this._URI);
    }

    /// <summary>
    /// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
    /// </summary>
    /// <param name="Pid1">sets <see cref="Pid1"/></param>
    /// <param name="Pid2">sets <see cref="Pid2"/></param>
    /// <param name="Pid3">sets <see cref="Pid3"/></param>
    /// <param name="backendURI">MMT URI</param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public RightAngleFact(string Pid1, string Pid2, string Pid3, string backendURI, FactOrganizer organizer)
        : base(Pid1, Pid2, Pid3, 90f, backendURI, organizer) { }

    /// <summary>
    /// Constructs struct for right-angled MMT %Fact <see cref="AddFactResponse"/>
    /// </summary>
    /// <param name="p1URI"> Uri for <see cref="Pid1"/></param>
    /// <param name="p2URI"> Uri for <see cref="Pid2"/></param>
    /// <param name="p3URI"> Uri for <see cref="Pid3"/></param>
    /// <returns>struct for <see cref="AddFactResponse"/></returns>
    private MMTDeclaration MakeMMTDeclaration(string p1URI, string p2URI, string p3URI)
    {
        SOMDoc tp =
            new OMA(
                new OMS(MMT_OMS_URI.Ded),
                new List<SOMDoc> {
                    new OMA(
                        new OMS(MMT_OMS_URI.RightAngle),
                        new List<SOMDoc> {
                            new OMS(p1URI),
                            new OMS(p2URI),
                            new OMS(p3URI),
        }),});

        SOMDoc df = null;

        return new MMTSymbolDeclaration(this.Label, tp, df);
    }

    /// \copydoc Fact.parseFact(Scroll.ScrollFact)
    public new static RightAngleFact parseFact(Scroll.ScrollFact fact)
    {
        if (((Scroll.ScrollSymbolFact)fact).tp
                is not OMA proof_OMA // proof DED
            || proof_OMA.arguments[0]
                is not OMA rightAngleOMA // rightAngle OMA
            || rightAngleOMA.arguments[0]
                is not OMS // rightAngle Arg0
        )
            return null;

        string Point1Uri = ((OMS)rightAngleOMA.arguments[0]).uri;
        string Point2Uri = ((OMS)rightAngleOMA.arguments[1]).uri;
        string Point3Uri = ((OMS)rightAngleOMA.arguments[2]).uri;

        if (!StageStatic.stage.factState.ContainsKey(Point1Uri)
         || !StageStatic.stage.factState.ContainsKey(Point2Uri)
         || !StageStatic.stage.factState.ContainsKey(Point3Uri))
            return null; //If dependent facts do not exist return null

        return new RightAngleFact(Point1Uri, Point2Uri, Point3Uri, fact.@ref.uri, StageStatic.stage.factState);
    }

    /// \copydoc Fact.generateLabel
    protected override string generateLabel()
        => Point1.Label + Point2.Label + Point3.Label + "⊥";

    /// \copydoc Fact.instantiateDisplay(GameObject, Transform)
    public override GameObject instantiateDisplay(GameObject prefab, Transform transform)
    {
        var obj = GameObject.Instantiate(prefab, Vector3.zero, Quaternion.identity, transform);
        obj.transform.GetChild(0).gameObject.GetComponent<TextMeshProUGUI>().text = Point1.Label;
        obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = Point2.Label;
        obj.transform.GetChild(2).gameObject.GetComponent<TextMeshProUGUI>().text = Point3.Label;

        obj.GetComponent<FactWrapper>().fact = this;
        return obj;
    }

    /// \copydoc Fact.Equivalent(Fact, Fact)
    protected override bool EquivalentWrapped(RightAngleFact f1, RightAngleFact f2)
        => DependentFactsEquivalent(f1, f2);
}