Fact.cs

    /// <summary> \copydoc Fact.Fact </summary>
    public EqualCirclesFact() : base()
    {
        this.Cid1 = null;
        this.Cid2 = null;
    }

    /// <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 EqualCirclesFact(EqualCirclesFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer) 
        => init(old_to_new[fact.Cid1], old_to_new[fact.Cid2]);

    /// <summary>
    /// Standard Constructor
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="cid2">sets <see cref="Cid2"/></param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public EqualCirclesFact(string cid1, string cid2, FactOrganizer organizer) : base(organizer)
        => init(cid1, cid2);

    /// <summary>
    /// Initiates <see cref="Cid1"/>, <see cref="Cid2"/>, <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="cid2">sets <see cref="Cid2"/></param>
    private void init(string cid1, string cid2)
    {
        this.Cid1 = cid1;
        this.Cid2 = cid2;

        MMTDeclaration mmtDecl = generateEqualCirclesFactDeclaration(cid1, cid2);
        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="Cid1">sets <see cref="Cid1"/></param>
    /// <param name="Cid2">sets <see cref="Cid2"/></param>
    /// <param name="backendURI">MMT URI</param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public EqualCirclesFact(string Cid1, string Cid2, string backendURI, FactOrganizer organizer) : base(organizer)
    {
        this.Cid1 = Cid1;
        this.Cid2 = Cid2;

        this._URI = backendURI;
        _ = this.Label;
    }

    /// \copydoc Fact.parseFact(Scroll.ScrollFact)
    public new static EqualCirclesFact parseFact(Scroll.ScrollFact fact)
    {
        OMA tp = (OMA)((Scroll.ScrollSymbolFact)fact).tp;
        if (tp == null)
            return null;

        string circleAUri = "";
        string circleBUri = "";

        string uri = fact.@ref.uri;
        OMA proof_OMA = (OMA)((Scroll.ScrollSymbolFact)fact).tp; // proof DED

        OMA parallel_circles_OMA = (OMA)proof_OMA.arguments[0]; // parallel

        if (parallel_circles_OMA.arguments[0] is OMS)
        {
            // Normaler Fall 
            circleAUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0]).uri;
            circleBUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).uri;
        }

        if (StageStatic.stage.factState.ContainsKey(circleAUri)
         && StageStatic.stage.factState.ContainsKey(circleBUri))

            return new EqualCirclesFact(circleAUri, circleBUri, uri, StageStatic.stage.factState);

        else    //If dependent facts do not exist return null
            return null;
    }

    /// \copydoc Fact.generateLabel
    protected override string generateLabel() 
        => _Facts[Cid1].Label + " ≠ " + _Facts[Cid2].Label;

    /// <summary>
    /// Constructs struct for equalCirclesFact <see cref="AddFactResponse"/>
    /// </summary>
    /// <param name="c1URI"><see cref="Cid1"/></param>
    /// <param name="c2URI"><see cref="Cid2"/></param>
    /// <returns>struct for <see cref="AddFactResponse"/></returns>
    private MMTDeclaration generateEqualCirclesFactDeclaration(string c1URI, string c2URI)
    {
        MMTTerm tp = new OMA(
            new OMS(MMTURIs.Ded), 
            new List<MMTTerm> {
                new OMA(
                    new OMS(MMTURIs.EqualityCircles), 
                    new List<MMTTerm> {
                        new OMS(c1URI),
                        new OMS(c2URI),
                    }
                )
            }
        );

        MMTTerm df = null;

        MMTSymbolDeclaration mmtDecl = new MMTSymbolDeclaration(this.Label, tp, df);
        AddFactResponse.sendAdd(mmtDecl, out this._URI);

        return mmtDecl;
    }

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

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

    /// \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 = _Facts[this.Cid1].Label;
        obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Cid2].Label;
        obj.GetComponent<FactWrapper>().fact = this;
        return obj;
    }

    /// \copydoc Fact.GetHashCode
    public override int GetHashCode() 
        => this.Cid1.GetHashCode() ^ this.Cid2.GetHashCode();

    /// \copydoc Fact.Equivalent(Fact, Fact)
    protected override bool EquivalentWrapped(EqualCirclesFact f1, EqualCirclesFact f2)
    {
        if ((f1.Cid1 == f2.Cid1 && f1.Cid2 == f2.Cid2))
            return true;

        CircleFact e1f1 = (CircleFact)_Facts[f1.Cid1];
        CircleFact e2f1 = (CircleFact)_Facts[f1.Cid2];
        CircleFact e1f2 = (CircleFact)_Facts[f2.Cid1];
        CircleFact e2f2 = (CircleFact)_Facts[f2.Cid2];

        return (e1f1.Equivalent(e1f2) && e2f1.Equivalent(e2f2));
    }
}

/// <summary>
/// A fact that describes, that two circles have not the same size and is comprised of two <see cref="CircleFact">CircleFacts</see> 
/// </summary>
public class UnEqualCirclesFact : FactWrappedCRTP<UnEqualCirclesFact>
{
    /// \copydoc Fact.s_type
    [JsonProperty]
    protected static new string s_type = "UnEqualCirclesFact";

    /// @{ <summary>
    /// two circles that are meant to be unequal in area
    /// </summary>
    public string Cid1, Cid2;
    /// @}


    /// <summary> \copydoc Fact.Fact </summary>
    public UnEqualCirclesFact() : base()
    {
        this.Cid1 = null;
        this.Cid2 = null;
    }

    /// <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 UnEqualCirclesFact(UnEqualCirclesFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer) 
        => init(old_to_new[fact.Cid1], old_to_new[fact.Cid2]);

    /// <summary>
    /// Standard Constructor
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="cid2">sets <see cref="Cid2"/></param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public UnEqualCirclesFact(string cid1, string cid2, FactOrganizer organizer) : base(organizer)
        => init(cid1, cid2);

    /// <summary>
    /// Initiates <see cref="Cid1"/>, <see cref="Cid2"/>, <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="cid2">sets <see cref="Cid2"/></param>
    private void init(string cid1, string cid2)
    {
        this.Cid1 = cid1;
        this.Cid2 = cid2;

        MMTDeclaration mmtDecl = generateUnEqualCirclesFactDeclaration(cid1, cid2);
        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="Cid1">sets <see cref="Cid1"/></param>
    /// <param name="Cid2">sets <see cref="Cid2"/></param>
    /// <param name="backendURI">MMT URI</param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public UnEqualCirclesFact(string Cid1, string Cid2, string backendURI, FactOrganizer organizer) : base(organizer)
    {
        this.Cid1 = Cid1;
        this.Cid2 = Cid2;

        this._URI = backendURI;
        _ = this.Label;
    }

    /// \copydoc Fact.parseFact(Scroll.ScrollFact)
    public new static UnEqualCirclesFact parseFact(Scroll.ScrollFact fact)
    {
        OMA tp = (OMA)((Scroll.ScrollSymbolFact)fact).tp;
        if (tp == null)
            return null;

        string circleAUri = "";
        string circleBUri = "";

        string uri = fact.@ref.uri;
        OMA proof_OMA = (OMA)((Scroll.ScrollSymbolFact)fact).tp; // proof DED

        OMA unequal_circles_OMA = (OMA)proof_OMA.arguments[0]; // unequal

        if (unequal_circles_OMA.arguments[0] is OMS)
        {
            // Normaler Fall 
            circleAUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0]).uri;
            circleBUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).uri;
        }

        if (StageStatic.stage.factState.ContainsKey(circleAUri)
         && StageStatic.stage.factState.ContainsKey(circleBUri))

            return new UnEqualCirclesFact(circleAUri, circleBUri, uri, StageStatic.stage.factState);

        else    //If dependent facts do not exist return null
            return null;
    }

    /// \copydoc Fact.generateLabel
    protected override string generateLabel()
        => _Facts[Cid1].Label + " = " + _Facts[Cid2].Label;

    /// <summary>
    /// Constructs struct for equalCirclesFact <see cref="AddFactResponse"/>
    /// </summary>
    /// <param name="c1URI"><see cref="Cid1"/></param>
    /// <param name="c2URI"><see cref="Cid2"/></param>
    /// <returns>struct for <see cref="AddFactResponse"/></returns>
    private MMTDeclaration generateUnEqualCirclesFactDeclaration(string c1URI, string c2URI)
    {
        MMTTerm tp = new OMA(
            new OMS(MMTURIs.Ded), 
            new List<MMTTerm> {
                new OMA(new OMS(MMTURIs.UnEqualityCircles), 
                new List<MMTTerm> {
                    new OMS(c1URI),
                    new OMS(c2URI),
        }),});

        MMTTerm df = null;

        MMTSymbolDeclaration mmtDecl = new (this.Label, tp, df);
        AddFactResponse.sendAdd(mmtDecl, out this._URI);
        return mmtDecl;
    }

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

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

    /// \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 = _Facts[this.Cid1].Label;
        obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Cid2].Label;
        obj.GetComponent<FactWrapper>().fact = this;
        return obj;
    }

    /// \copydoc Fact.GetHashCode
    public override int GetHashCode()
        => this.Cid1.GetHashCode() ^ this.Cid2.GetHashCode();

    /// \copydoc Fact.Equivalent(Fact, Fact)
    protected override bool EquivalentWrapped(UnEqualCirclesFact f1, UnEqualCirclesFact f2)
    {
        if ((f1.Cid1 == f2.Cid1 && f1.Cid2 == f2.Cid2))
            return true;

        CircleFact e1f1 = (CircleFact)_Facts[f1.Cid1];
        CircleFact e2f1 = (CircleFact)_Facts[f1.Cid2];
        CircleFact e1f2 = (CircleFact)_Facts[f2.Cid1];
        CircleFact e2f2 = (CircleFact)_Facts[f2.Cid2];

        return (e1f1.Equivalent(e1f2) && e2f1.Equivalent(e2f2));
    }
}


#pragma warning disable // Testing...

/// TEST FACT
/// use this if you need to test certain implementations of facts.

/// <summary>
/// just for testing purposes  
/// </summary>
public class TestFact : FactWrappedCRTP<TestFact>
{
    /// \copydoc Fact.s_type
    [JsonProperty]
    protected static new string s_type = "TestFact";


    /// <summary> \copydoc Fact.Fact </summary>
    public TestFact() : 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 TestFact(TestFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
    {
        init();
    }

    /// <summary>
    /// Standard Constructor
    /// </summary>
    /// <param name="pid1">sets <see cref="Pid1"/></param>
    /// <param name="pid2">sets <see cref="Pid2"/></param>
    /// <param name="radius">sets <see cref="radius"/></param>
    /// <param name="normal">sets <see cref="normal"/></param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public TestFact(FactOrganizer organizer) : base(organizer)
    {
        init();
    }

    /// <summary>
    /// Initiates <see cref="Pid1"/>, <see cref="Pid2"/>, <see cref="radius"/>,<see cref="dir1"/>,<see cref="dir2"/>, <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="radius">sets <see cref="radius"/></param>
    /// <param name="normal">sets <see cref="normal"/></param>
    private void init()
    {


        // mmtDecl = generateCircleFactDeclaration(p1URI, p2URI, radius, normal);

        //  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="radius">sets <see cref="radius"/></param>
    /// <param name="normal">sets <see cref="normal"/></param>
    /// <param name="backendURI">MMT URI</param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public TestFact(string backendURI, FactOrganizer organizer) : base(organizer)
    {

        this._URI = backendURI;
        _ = this.Label;
    }

    /// <summary>
    /// parses the Circlefact response of the MMT-Server
    /// </summary>
    /// \copydoc Fact.parseFact(Scroll.ScrollFact) 
    public new static TestFact parseFact(Scroll.ScrollFact fact)
    {
        string uri = fact.@ref.uri;
        Debug.Log("TestFact Uri:" + uri);
        return new TestFact(uri, StageStatic.stage.factState);

    }

    /// \copydoc Fact.generateLabel
    protected override string generateLabel()
    {

        return "test";
    }



    /// <summary>
    /// Constructs struct for right-angled MMT %Fact <see cref="AddFactResponse"/>
    /// </summary>
    /// <param name="p1URI"> <see cref="Pid1"/></param>
    /// <param name="p2URI"> <see cref="Pid2"/></param>
    /// <param name="radius"> <see cref="radius"/></param>
    /// <returns>struct for <see cref="AddFactResponse"/></returns>
    private MMTDeclaration generateCircleFactDeclaration(string p1URI, string p2URI, float radius, Vector3 normal)
    {
        PointFact p1 = _Facts[p1URI] as PointFact;
        PointFact p2 = _Facts[p2URI] as PointFact;


        List<MMTTerm> normalArgs = new List<MMTTerm>
        {
            new OMF(normal.x),
            new OMF(normal.y),
            new OMF(normal.z)
        };
        OMA NormalVector = new OMA(new OMS(MMTURIs.Tuple), normalArgs);



        List<MMTTerm> planeArgs = new List<MMTTerm>
        {
            new OMS(p2URI),
            NormalVector //n
        };

        OMA CirclePlane = new OMA(new OMS(MMTURIs.pointNormalPlane), planeArgs);
        OMS middlePoint = new OMS(p1URI);
        OMF Radius = new OMF(radius);

        List<MMTTerm> outerArguments = new List<MMTTerm>
        {
           CirclePlane,
           middlePoint,
           Radius
        };

        //OMS constructor generates full URI
        // Do i need this here? doubt 
        MMTTerm tp = new OMS(MMTURIs.CircleType3d);
        MMTTerm df = new OMA(new OMS(MMTURIs.MkCircle3d), outerArguments);

        MMTSymbolDeclaration mmtDecl = new MMTSymbolDeclaration(this.Label, tp, df);
        AddFactResponse.sendAdd(mmtDecl, out this._URI);


        return mmtDecl;
    }


    /// \copydoc Fact.hasDependentFacts
    public override Boolean hasDependentFacts()
    {
        return false;
    }



    /// \copydoc Fact.getDependentFactIds
    public override string[] getDependentFactIds()
    {
        return new string[] { };
    }

    /// \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(1).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Lid2].Label;

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

    /// \copydoc Fact.GetHashCode
    public override int GetHashCode()
    {
        return 112315414;// this.Pid1.GetHashCode() ^ this.Pid2.GetHashCode();
    }

    /// \copydoc Fact.Equivalent(Fact, Fact)
    protected override bool EquivalentWrapped(TestFact f1, TestFact f2)
    {
        return false;
    }
}

#pragma warning restore // Testing over