Skip to content
Snippets Groups Projects
Fact.cs 105 KiB
Newer Older
  • Learn to ignore specific revisions
  • MaZiFAU's avatar
    MaZiFAU committed
    
    
    MaZiFAU's avatar
    MaZiFAU committed
            RecalculateTransform();
    
        }
    
        /// \copydoc Fact.parseFact(Scroll.ScrollFact)
        public new static OrthogonalCircleLineFact parseFact(Scroll.ScrollFact fact)
        {
            OMA tp = (OMA)((Scroll.ScrollSymbolFact)fact).tp;
            if (tp == null)
                return null;
    
            string uri = fact.@ref.uri;
    
            string CircleUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0]).uri;
            string LineUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).uri;
    
            if (StageStatic.stage.factState.ContainsKey(CircleUri)
             && StageStatic.stage.factState.ContainsKey(LineUri))
    
                return new OrthogonalCircleLineFact(CircleUri, LineUri, uri, StageStatic.stage.factState);
    
            else    //If dependent facts do not exist return null
                return null;
        }
    
        /// \copydoc Fact.generateLabel
        protected override string generateLabel()
    
    MaZiFAU's avatar
    MaZiFAU committed
            => Circle.Label + "⊥" + Ray.Label;
    
    
        /// <summary>
        /// Constructs struct for not-right-angled MMT %Fact <see cref="AddFactResponse"/>
        /// </summary>
        /// <param name="c1URI"> Uri for <see cref="Cid1"/></param>
        /// <param name="l1URI"> Uri for <see cref="Lid1"/></param>
        /// <returns>struct for <see cref="AddFactResponse"/></returns>
        private MMTDeclaration generateMMTDeclaration(string c1URI, string l1URI)
        {
    
                new OMS(MMT_OMS_URI.Ded),
    
                        new OMS(MMT_OMS_URI.OrthoCircleLine),
    
                            new OMS(c1URI),
                            new OMS(l1URI),
                        }
                    ),
                }
            );
    
    
            return new MMTSymbolDeclaration(this.Label, tp, df);
        }
    
        /// \copydoc Fact.hasDependentFacts
    
    MaZiFAU's avatar
    MaZiFAU committed
        public override bool hasDependentFacts()
    
    
        /// \copydoc Fact.getDependentFactIds
        public override string[] getDependentFactIds()
    
            => new string[] { Cid1, Lid1 };
    
    
        /// \copydoc Fact.instantiateDisplay(GameObject, Transform)
        public override GameObject instantiateDisplay(GameObject prefab, Transform transform)
        {
            var obj = GameObject.Instantiate(prefab, Vector3.zero, Quaternion.identity, transform);
    
    MaZiFAU's avatar
    MaZiFAU committed
            obj.transform.GetChild(0).gameObject.GetComponent<TextMeshProUGUI>().text = Circle.Label;
            obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = Ray.Label;
    
    
            obj.GetComponent<FactWrapper>().fact = this;
            return obj;
        }
    
        /// \copydoc Fact.GetHashCode
        /// uhhh is this a problem?
        public override int GetHashCode()
    
            => this.Cid1.GetHashCode() ^ this.Lid1.GetHashCode();
    
    
        /// \copydoc Fact.Equivalent(Fact, Fact)
        protected override bool EquivalentWrapped(OrthogonalCircleLineFact f1, OrthogonalCircleLineFact f2)
    
    MaZiFAU's avatar
    MaZiFAU committed
            => DependentFactsEquivalent(f1, f2);
    
    MaZiFAU's avatar
    MaZiFAU committed
    
        protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
            => new OrthogonalCircleLineFact(old_to_new[this.Cid1], old_to_new[this.Lid1], organizer);
    
    }
    
    /// <summary>
    /// The volume of a cone A  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 TruncatedConeVolumeFact : FactWrappedCRTP<TruncatedConeVolumeFact>
    {
        ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the base area </summary>
        public string Cid1;
    
    MaZiFAU's avatar
    MaZiFAU committed
        public CircleFact Circle1 { get => (CircleFact)FactOrganizer.AllFacts[Cid1]; }
    
        ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the top area  </summary>
    
    MaZiFAU's avatar
    MaZiFAU committed
        public CircleFact Circle2 { get => (CircleFact)FactOrganizer.AllFacts[Cid2]; }
    
        ///  <summary> the volume of Truncated the cone as a float </summary>
    
        /// <summary> a proof that both circles have not the same size </summary>
        public string unequalCirclesProof;
    
        ///  <summary> OMA proof that the two circles are parallel  </summary>
        public OMA proof;
    
    
        /// <summary> \copydoc Fact.Fact </summary>
        public TruncatedConeVolumeFact() : base()
        {
            this.Cid1 = null;
            this.Cid2 = null;
            this.vol = 0.0f;
    
            this.unequalCirclesProof = null;
    
            this.proof = null;
        }
    
        /// <summary>
        /// Standard Constructor
        /// </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 TruncatedConeVolumeFact(string cid1, string cid2, float vol, string unequalproof, OMA proof, FactOrganizer organizer) : base(organizer)
    
            => init(cid1, cid2, vol, unequalproof, proof);
    
    
        /// <summary>
        /// sets variables and generates MMT Declaration
        /// </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>
    
        private void init(string cid1, string cid2, float vol, string unequalproof, OMA proof)
    
        {
            this.Cid1 = cid1;
            this.Cid2 = cid2;
            this.proof = proof;
    
            this.unequalCirclesProof = unequalproof;
    
    MaZiFAU's avatar
    MaZiFAU committed
            RecalculateTransform();
    
            MMTDeclaration mmtDecl = generateMMTDeclaration(cid1, cid2, vol, unequalproof, proof);
    
            AddFactResponse.sendAdd(mmtDecl, out this._URI);
        }
    
    
    MaZiFAU's avatar
    MaZiFAU committed
        protected override void RecalculateTransform()
    
    MaZiFAU's avatar
    MaZiFAU committed
        {
            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 TruncatedConeVolumeFact(string Cid1, string Cid2, float volume, string unequalproof, OMA proof, string backendURI, FactOrganizer organizer) : base(organizer)
    
        {
            this.Cid1 = Cid1;
            this.Cid2 = Cid2;
            this.vol = volume;
            this.proof = proof;
    
            this.unequalCirclesProof = unequalproof;
    
    
            this._URI = backendURI;
            _ = this.Label;
    
    MaZiFAU's avatar
    MaZiFAU committed
    
    
    MaZiFAU's avatar
    MaZiFAU committed
            RecalculateTransform();
    
        }
    
        /// \copydoc Fact.parseFact(Scroll.ScrollFact)
        public new static TruncatedConeVolumeFact parseFact(Scroll.ScrollFact fact)
        {
            string uri = fact.@ref.uri;
    
            string Circle1Uri = ((OMS)((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[0]).uri;
            string Circle2Uri = ((OMS)((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[1]).uri;
            float volume = ((OMF)((Scroll.ScrollValueFact)fact).value).f;
    
    
            string UnEqualCirclesProof = ((OMS)(((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[2])).uri;
            OMA proof = (OMA)(((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[3]);
    
    
    
            if (StageStatic.stage.factState.ContainsKey(Circle1Uri) && StageStatic.stage.factState.ContainsKey(Circle2Uri))
    
    
                return new TruncatedConeVolumeFact(Circle1Uri, Circle2Uri, volume, UnEqualCirclesProof, proof, uri, StageStatic.stage.factState);
    
    
            else    //If dependent facts do not exist return null
                return null;
        }
    
        /// \copydoc Fact.generateLabel
    
        protected override string generateLabel()
    
    MaZiFAU's avatar
    MaZiFAU committed
            => "V(" + Circle1.Label + "," + Circle2.Label + ")";
    
    
        /// <summary>
        /// Constructs struct for not-right-angled MMT %Fact <see cref="AddFactResponse"/>
        /// </summary>
        /// <param name="c1URI"> Uri for <see cref="Cid1"/></param>
        /// <param name="c2URI"> Uri for <see cref="Cid2"/></param>
        /// <param name="val"> <see cref="vol"/></param>
        /// <returns>struct for <see cref="AddFactResponse"/></returns>
    
        private MMTDeclaration generateMMTDeclaration(string c1URI, string c2URI, float val, string unequalproof, OMA proof)
    
                        new OMS(c1URI),
                        new OMS(c2URI),
    
                        new OMS(unequalproof),
    
            SOMDoc valueTp = new OMS(MMT_OMS_URI.RealLit);
            SOMDoc value = new OMF(val);
    
    
            return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
        }
    
        /// \copydoc Fact.hasDependentFacts
    
        public override Boolean hasDependentFacts()
    
    
        /// \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);
    
    MaZiFAU's avatar
    MaZiFAU committed
            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)
    
    MaZiFAU's avatar
    MaZiFAU committed
            => DependentFactsEquivalent(f1, f2);
    
    MaZiFAU's avatar
    MaZiFAU committed
    
        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;
    
    MaZiFAU's avatar
    MaZiFAU committed
        public CircleFact Circle1 { get => (CircleFact)FactOrganizer.AllFacts[Cid1]; }
    
        ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the top area  </summary>
        public string Cid2;
    
    MaZiFAU's avatar
    MaZiFAU committed
        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
        /// </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)
    
            => init(cid1, cid2, vol, eqProof, proof);
    
    
        /// <summary>
        /// sets variables and generates MMT Declaration
        /// </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>
    
        private void init(string cid1, string cid2, float vol, string eqProof, OMA proof)
    
        {
            this.Cid1 = cid1;
            this.Cid2 = cid2;
            this.proof = proof;
    
            this.equalCirclesProof = eqProof;
    
    MaZiFAU's avatar
    MaZiFAU committed
            RecalculateTransform();
    
            MMTDeclaration mmtDecl = generateMMTDeclaration(cid1, cid2, vol, eqProof, proof);
    
            AddFactResponse.sendAdd(mmtDecl, out this._URI);
        }
    
    
    MaZiFAU's avatar
    MaZiFAU committed
        protected override void RecalculateTransform()
    
    MaZiFAU's avatar
    MaZiFAU committed
        {
            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;
    
    MaZiFAU's avatar
    MaZiFAU committed
    
    
    MaZiFAU's avatar
    MaZiFAU committed
            RecalculateTransform();
    
        }
    
        /// \copydoc Fact.parseFact(Scroll.ScrollFact)
        public new static CylinderVolumeFact parseFact(Scroll.ScrollFact fact)
        {
            string uri = fact.@ref.uri;
    
            string Circle1Uri = ((OMS)((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[0]).uri;
            string Circle2Uri = ((OMS)((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[1]).uri;
            float volume = ((OMF)((Scroll.ScrollValueFact)fact).value).f;
    
            string EqualCirclesProof = ((OMS)(((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[2])).uri;
    
            OMA proof = (OMA)(((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[3]);
    
    
            if (StageStatic.stage.factState.ContainsKey(Circle1Uri) && StageStatic.stage.factState.ContainsKey(Circle2Uri))
    
    
                return new CylinderVolumeFact(Circle1Uri, Circle2Uri, volume, EqualCirclesProof, proof, uri, StageStatic.stage.factState);
    
    
            else    //If dependent facts do not exist return null
                return null;
        }
    
        /// \copydoc Fact.generateLabel
        protected override string generateLabel()
    
    MaZiFAU's avatar
    MaZiFAU committed
            => "V(" + Circle1.Label + "," + Circle2.Label + ")";
    
    
        /// <summary>
        /// Constructs struct for not-right-angled MMT %Fact <see cref="AddFactResponse"/>
        /// </summary>
        /// <param name="c1URI"> Uri for <see cref="Cid1"/></param>
        /// <param name="c2URI"> Uri for <see cref="Cid2"/></param>
        /// <param name="val"> <see cref="vol"/></param>
        /// <returns>struct for <see cref="AddFactResponse"/></returns>
    
        private MMTDeclaration generateMMTDeclaration(string c1URI, string c2URI, float val, string p1URI, OMA proof)
    
            SOMDoc valueTp = new OMS(MMT_OMS_URI.RealLit);
            SOMDoc value = new OMF(val);
    
    
            return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
        }
    
        /// \copydoc Fact.hasDependentFacts
    
    MaZiFAU's avatar
    MaZiFAU committed
        public override bool hasDependentFacts()
    
    
        /// \copydoc Fact.getDependentFactIds
        public override string[] getDependentFactIds()
    
            => 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);
    
    MaZiFAU's avatar
    MaZiFAU committed
            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)
    
    MaZiFAU's avatar
    MaZiFAU committed
            => DependentFactsEquivalent(f1, f2);
    
    MaZiFAU's avatar
    MaZiFAU committed
    
        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;
        /// @}
    
    
    MaZiFAU's avatar
    MaZiFAU committed
        public CircleFact Circle1 { get => (CircleFact)FactOrganizer.AllFacts[Cid1]; }
    
    MaZiFAU's avatar
    MaZiFAU committed
        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
        /// </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;
    
    
    MaZiFAU's avatar
    MaZiFAU committed
            RecalculateTransform();
    
            MMTDeclaration mmtDecl = generateEqualCirclesFactDeclaration(cid1, cid2);
    
            AddFactResponse.sendAdd(mmtDecl, out this._URI);
        }
    
    
    MaZiFAU's avatar
    MaZiFAU committed
        protected override void RecalculateTransform()
    
    MaZiFAU's avatar
    MaZiFAU committed
        {
            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;
    
    MaZiFAU's avatar
    MaZiFAU committed
    
    
    MaZiFAU's avatar
    MaZiFAU committed
            RecalculateTransform();
    
        }
    
        /// \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()
    
    MaZiFAU's avatar
    MaZiFAU committed
            => Circle1.Label + " ≠ " + Circle2.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)
        {
    
                new OMS(MMT_OMS_URI.Ded),
    
                        new OMS(MMT_OMS_URI.EqualityCircles),
    
                            new OMS(c1URI),
                            new OMS(c2URI),
                        }
                    )
                }
            );
    
    
            MMTSymbolDeclaration mmtDecl = new MMTSymbolDeclaration(this.Label, tp, df);
            AddFactResponse.sendAdd(mmtDecl, out this._URI);
    
            return mmtDecl;
        }
    
        /// \copydoc Fact.hasDependentFacts
        public override Boolean hasDependentFacts()
    
    
        /// \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);
    
    MaZiFAU's avatar
    MaZiFAU committed
            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)
    
    MaZiFAU's avatar
    MaZiFAU committed
            => DependentFactsEquivalent(f1, f2);
    
    MaZiFAU's avatar
    MaZiFAU committed
    
        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;
        /// @}
    
    
    MaZiFAU's avatar
    MaZiFAU committed
        public CircleFact Circle1 { get => (CircleFact)FactOrganizer.AllFacts[Cid1]; }
    
    MaZiFAU's avatar
    MaZiFAU committed
        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
        /// </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;
    
    
    MaZiFAU's avatar
    MaZiFAU committed
            RecalculateTransform();
    
            MMTDeclaration mmtDecl = generateUnEqualCirclesFactDeclaration(cid1, cid2);
    
            AddFactResponse.sendAdd(mmtDecl, out this._URI);
        }
    
    
    MaZiFAU's avatar
    MaZiFAU committed
        protected override void RecalculateTransform()
    
    MaZiFAU's avatar
    MaZiFAU committed
        {
            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;
    
    MaZiFAU's avatar
    MaZiFAU committed
    
    
    MaZiFAU's avatar
    MaZiFAU committed
            RecalculateTransform();
    
        }
    
        /// \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()
    
    MaZiFAU's avatar
    MaZiFAU committed
            => Circle1.Label + " = " + Circle2.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)
        {
    
                new OMS(MMT_OMS_URI.Ded),
    
                    new OMA(new OMS(MMT_OMS_URI.UnEqualityCircles),
    
                        new OMS(c1URI),
                        new OMS(c2URI),
            }),});
    
            MMTSymbolDeclaration mmtDecl = new(this.Label, tp, df);
    
            AddFactResponse.sendAdd(mmtDecl, out this._URI);
            return mmtDecl;
        }
    
        /// \copydoc Fact.hasDependentFacts
    
        public override Boolean hasDependentFacts()
    
    
        /// \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);
    
    MaZiFAU's avatar
    MaZiFAU committed
            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)
    
    MaZiFAU's avatar
    MaZiFAU committed
            => DependentFactsEquivalent(f1, f2);
    
    MaZiFAU's avatar
    MaZiFAU committed
    
        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...
    
    
    ki7077's avatar
    ki7077 committed
    /// use this if you need to test certain implementations of facts.
    
    ki7077's avatar
    ki7077 committed
    /// just for testing purposes  
    
    /// </summary>
    public class TestFact : FactWrappedCRTP<TestFact>
    {
        /// <summary> \copydoc Fact.Fact </summary>
        public TestFact() : base()
        {
    
        }
    
        /// <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);
    
    MaZiFAU's avatar
    MaZiFAU committed
        protected override void RecalculateTransform() { }
    
    MaZiFAU's avatar
    MaZiFAU committed
    
    
        /// <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)
        {
    
    MaZiFAU's avatar
    MaZiFAU committed
            PointFact p1 = FactOrganizer.AllFacts[p1URI] as PointFact;
            PointFact p2 = FactOrganizer.AllFacts[p2URI] as PointFact;
    
            {
                new OMF(normal.x),
                new OMF(normal.y),
                new OMF(normal.z)
            };
    
            OMA NormalVector = new OMA(new OMS(MMT_OMS_URI.Tuple), normalArgs);
    
            {
                new OMS(p2URI),
                NormalVector //n
            };
    
    
            OMA CirclePlane = new OMA(new OMS(MMT_OMS_URI.pointNormalPlane), planeArgs);
    
            OMS middlePoint = new OMS(p1URI);
            OMF Radius = new OMF(radius);
    
    
            List<SOMDoc> outerArguments = new List<SOMDoc>
    
            {
               CirclePlane,
               middlePoint,
               Radius
            };
    
            //OMS constructor generates full URI
            // Do i need this here? doubt 
    
            SOMDoc tp = new OMS(MMT_OMS_URI.CircleType3d);
            SOMDoc df = new OMA(new OMS(MMT_OMS_URI.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()
        {
    
    MaZiFAU's avatar
    MaZiFAU committed
            return base.GetHashCode();// this.Pid1.GetHashCode() ^ this.Pid2.GetHashCode();
    
        }
    
        /// \copydoc Fact.Equivalent(Fact, Fact)
        protected override bool EquivalentWrapped(TestFact f1, TestFact f2)
        {
    
    MaZiFAU's avatar
    MaZiFAU committed
            return DependentFactsEquivalent(f1, f2);
    
    MaZiFAU's avatar
    MaZiFAU committed
    
        protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
            => new TestFact(organizer);
    
    }
    
    #pragma warning restore // Testing over