Fact.cs

            new OMA(
                new OMS(MMT_OMS_URI.TruncatedVolumeCone),
                new List<SOMDoc> {
                    new OMS(Cid1),
                    new OMS(Cid2),
                    new OMS(unequalCirclesProof),
                    proof,
                }
            );

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

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

    /// \copydoc Fact.hasDependentFacts
    public override bool HasDependentFacts => true;

    /// \copydoc Fact.getDependentFactIds
    protected override string[] GetGetDependentFactIds()
    {
        return 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 = Circle1.Label + Circle2.Label;
        obj.GetComponent<FactWrapper>().Fact = this;

        return obj;
    }

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

    protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
        => new TruncatedConeVolumeFact(old_to_new[this.Cid1], old_to_new[this.Cid2], this.vol, old_to_new[this.unequalCirclesProof], this.proof, organizer);
}

/// <summary>
/// The volume of a cylinder defined by a base area  <see cref="CircleFact">CircleFact</see>, a top area <see cref="CircleFact">CircleFact</see> and the volume as float
/// </summary>
public class CylinderVolumeFact : FactWrappedCRTP<CylinderVolumeFact>
{
    ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the base area </summary>
    public string Cid1;
    [JsonIgnore]
    public CircleFact Circle1 { get => (CircleFact)FactOrganizer.AllFacts[Cid1]; }

    ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the top area  </summary>
    public string Cid2;
    [JsonIgnore]
    public CircleFact Circle2 { get => (CircleFact)FactOrganizer.AllFacts[Cid2]; }

    ///  <summary> the volume of the cylinder as a float </summary>
    public float vol;
    /// <summary> a proof that both circles have the same size </summary>
    public string equalCirclesProof;
    ///  <summary> OMA proof that the two circles are parallel  </summary>
    public OMA proof;

    /// <summary> \copydoc Fact.Fact </summary>
    public CylinderVolumeFact() : base()
    {
        this.Cid1 = null;
        this.Cid2 = null;
        this.vol = 0.0f;
        this.proof = null;
        this.equalCirclesProof = null;
    }

    /// <summary>
    /// Standard Constructor:
    /// Initiates members and creates MMT %Fact Server-Side
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="cid2">sets <see cref="Cid2"/></param>
    /// <param name="vol">sets <see cref="vol"/></param>
    /// <param name="proof">sets <see cref="proof"/></param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public CylinderVolumeFact(string cid1, string cid2, float vol, string eqProof, OMA proof, FactOrganizer organizer) : base(organizer)
    {
        this.Cid1 = cid1;
        this.Cid2 = cid2;
        this.proof = proof;
        this.equalCirclesProof = eqProof;
        this.vol = vol;

        AddFactResponse.sendAdd(MakeMMTDeclaration(), out this._URI);
    }

    protected override void RecalculateTransform()
    {
        Position = Circle2.Position;
        Rotation = Circle2.Rotation;
    }

    /// <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="volume">sets <see cref="vol"/></param>
    /// <param name="proof">sets <see cref="proof"/></param>
    /// <param name="backendURI">MMT URI</param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public CylinderVolumeFact(string Cid1, string Cid2, float volume, string eqProof, OMA proof, string backendURI, FactOrganizer organizer) : base(organizer)
    {
        this.Cid1 = Cid1;
        this.Cid2 = Cid2;
        this.vol = volume;
        this.proof = proof;
        this.equalCirclesProof = eqProof;

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

    /// \copydoc Fact.parseFact(ScrollFact)
    public new static CylinderVolumeFact parseFact(MMTDeclaration fact)
    {
        string Circle1Uri = ((OMS)((OMA)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).arguments[0]).uri;
        string Circle2Uri = ((OMS)((OMA)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).arguments[1]).uri;
        float volume = ((OMF)((MMTValueDeclaration)fact).value).@float;
        string EqualCirclesProof = ((OMS)(((OMA)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).arguments[2])).uri;

        OMA proof = (OMA)(((OMA)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).arguments[3]);

        if (!FactOrganizer.AllFacts.ContainsKey(Circle1Uri)
         || !FactOrganizer.AllFacts.ContainsKey(Circle2Uri))
            return null;

        return new CylinderVolumeFact(Circle1Uri, Circle2Uri, volume, EqualCirclesProof, proof, fact.@ref.uri, StageStatic.stage.factState);
    }

    /// \copydoc Fact.generateLabel
    protected override string generateLabel()
        => "V(" + Circle1.Label + "," + Circle2.Label + ")";

    protected override MMTDeclaration MakeMMTDeclaration()
    {
        SOMDoc lhs =
            new OMA(
                new OMS(MMT_OMS_URI.CylinderVolume),

                new List<SOMDoc> {
                    new OMS(Cid1),
                    new OMS(Cid2),
                    new OMS(equalCirclesProof),
                    proof,
                }
            );

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

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

    /// \copydoc Fact.hasDependentFacts
    public override bool HasDependentFacts => true;

    /// \copydoc Fact.getDependentFactIds
    protected override string[] GetGetDependentFactIds()
    {
        return new string[] { Cid1, Cid2, equalCirclesProof };
    }

    /// \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 = Circle1.Label + Circle2.Label;
        obj.GetComponent<FactWrapper>().Fact = this;

        return obj;
    }

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

    protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
        => new CylinderVolumeFact(old_to_new[this.Cid1], old_to_new[this.Cid2], this.vol, old_to_new[this.equalCirclesProof], this.proof, organizer);
}

/// <summary>
/// A fact that describes, that two circles have the same size and is comprised of two <see cref="CircleFact">CircleFacts</see> 
/// </summary>
public class EqualCirclesFact : FactWrappedCRTP<EqualCirclesFact>
{
    /// @{ <summary>
    /// two circles that are meant to be equal in area
    /// </summary>
    public string Cid1, Cid2;
    /// @}

    [JsonIgnore]
    public CircleFact Circle1 { get => (CircleFact)FactOrganizer.AllFacts[Cid1]; }
    [JsonIgnore]
    public CircleFact Circle2 { get => (CircleFact)FactOrganizer.AllFacts[Cid2]; }

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

    /// <summary>
    /// Standard Constructor:
    /// Initiates members and creates MMT %Fact Server-Side
    /// </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)
    {
        this.Cid1 = cid1;
        this.Cid2 = cid2;

        AddFactResponse.sendAdd(MakeMMTDeclaration(), out this._URI);
    }

    protected override void RecalculateTransform()
    {
        Position = Circle1.Position;
        Rotation = Circle1.Rotation;
    }

    /// <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(ScrollFact)
    public new static EqualCirclesFact parseFact(MMTDeclaration fact)
    {
        if (((MMTSymbolDeclaration)fact).type is not OMA proof_OMA) // proof DED
            return null;

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

        string circleAUri = ((OMS)parallel_circles_OMA.arguments[0]).uri;
        string circleBUri = ((OMS)parallel_circles_OMA.arguments[1]).uri;

        if (!FactOrganizer.AllFacts.ContainsKey(circleAUri)
         || !FactOrganizer.AllFacts.ContainsKey(circleBUri))
            return null;

        return new EqualCirclesFact(circleAUri, circleBUri, fact.@ref.uri, StageStatic.stage.factState);
    }

    /// \copydoc Fact.generateLabel
    protected override string generateLabel()
        => Circle1.Label + " ≠ " + Circle2.Label;

    protected override MMTDeclaration MakeMMTDeclaration()
    {
        SOMDoc tp = new OMA(
            new OMS(MMT_OMS_URI.Ded),
            new List<SOMDoc> {
                new OMA(
                    new OMS(MMT_OMS_URI.EqualityCircles),
                    new List<SOMDoc> {
                        new OMS(Cid1),
                        new OMS(Cid2),
                    }
                )
            }
        );

        SOMDoc df = null;

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

    /// \copydoc Fact.hasDependentFacts
    public override bool HasDependentFacts => true;

    /// \copydoc Fact.getDependentFactIds
    protected override string[] GetGetDependentFactIds()
    {
        return 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 = Circle1.Label;
        obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = Circle2.Label;
        obj.GetComponent<FactWrapper>().Fact = this;
        return obj;
    }

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

    protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
        => new EqualCirclesFact(old_to_new[this.Cid1], old_to_new[this.Cid2], organizer);
}

/// <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>
{
    /// @{ <summary>
    /// two circles that are meant to be unequal in area
    /// </summary>
    public string Cid1, Cid2;
    /// @}

    [JsonIgnore]
    public CircleFact Circle1 { get => (CircleFact)FactOrganizer.AllFacts[Cid1]; }
    [JsonIgnore]
    public CircleFact Circle2 { get => (CircleFact)FactOrganizer.AllFacts[Cid2]; }

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

    /// <summary>
    /// Standard Constructor:
    /// Initiates members and creates MMT %Fact Server-Side
    /// </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)
    {
        this.Cid1 = cid1;
        this.Cid2 = cid2;

        AddFactResponse.sendAdd(MakeMMTDeclaration(), out this._URI);
    }

    protected override void RecalculateTransform()
    {
        Position = Circle2.Position;
        Rotation = Circle2.Rotation;
    }

    /// <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(ScrollFact)
    public new static UnEqualCirclesFact parseFact(MMTDeclaration fact)
    {
        if (((MMTSymbolDeclaration)fact).type is not OMA proof_OMA) // proof DED
            return null;

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

        string circleAUri = ((OMS)unequal_circles_OMA.arguments[0]).uri;
        string circleBUri = ((OMS)unequal_circles_OMA.arguments[1]).uri;

        if (!FactOrganizer.AllFacts.ContainsKey(circleAUri)
         || !FactOrganizer.AllFacts.ContainsKey(circleBUri))
            return null;

        return new UnEqualCirclesFact(circleAUri, circleBUri, fact.@ref.uri, StageStatic.stage.factState);
    }

    /// \copydoc Fact.generateLabel
    protected override string generateLabel()
        => Circle1.Label + " = " + Circle2.Label;

    protected override MMTDeclaration MakeMMTDeclaration()
    {
        SOMDoc tp = new OMA(
            new OMS(MMT_OMS_URI.Ded),
            new List<SOMDoc> {
                new OMA(new OMS(MMT_OMS_URI.UnEqualityCircles),
                new List<SOMDoc> {
                    new OMS(Cid1),
                    new OMS(Cid2),
        }),});

        SOMDoc df = null;

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

    /// \copydoc Fact.hasDependentFacts
    public override bool HasDependentFacts => true;

    /// \copydoc Fact.getDependentFactIds
    protected override string[] GetGetDependentFactIds()
    {
        return 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 = Circle1.Label;
        obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = Circle2.Label;
        obj.GetComponent<FactWrapper>().Fact = this;
        return obj;
    }

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

    protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
        => new UnEqualCirclesFact(old_to_new[this.Cid1], old_to_new[this.Cid2], organizer);
}


#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>
{
    /// <summary> \copydoc Fact.Fact </summary>
    public TestFact() : base()
    {

    }

    /// <summary>
    /// Standard Constructor:
    /// Initiates members 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>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public TestFact(FactOrganizer organizer) : base(organizer)
    {


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

        AddFactResponse.sendAdd(MakeMMTDeclaration(), out this._URI);
    }

    protected override void RecalculateTransform() { }

    /// <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(ScrollFact) 
    public new static TestFact parseFact(MMTDeclaration 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";
    }

    /// \copydoc Fact.hasDependentFacts
    public override bool HasDependentFacts => false;

    /// \copydoc Fact.getDependentFactIds
    protected override string[] GetGetDependentFactIds()
    {
        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 base.GetHashCode();// this.Pid1.GetHashCode() ^ this.Pid2.GetHashCode();
    }

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

    protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
        => new TestFact(organizer);

    protected override MMTDeclaration MakeMMTDeclaration()
    {
        throw new NotImplementedException();
    }
}

#pragma warning restore // Testing over