Skip to content
Snippets Groups Projects
Fact.cs 145 KiB
Newer Older
  • Learn to ignore specific revisions
  •     /// <summary> \copydoc Fact.Fact </summary>
        public OnCircleFact() : base()
        {
            this.Pid = null;
            this.Cid = 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 OnCircleFact(OnCircleFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
    
            => init(old_to_new[fact.Pid], old_to_new[fact.Cid]);
    
    
        /// <summary>
        /// Standard Constructor
        /// </summary>
        /// <param name="pid">sets <see cref="Pid"/></param>
        /// <param name="cid">sets <see cref="Cid"/></param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public OnCircleFact(string pid, string cid, FactOrganizer organizer) : base(organizer)
    
            => init(pid, cid);
    
    
        /// <summary>
        /// Initiates <see cref="Pid"/>, <see cref="Rid"/>, <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
        /// </summary>
        /// <param name="pid">sets <see cref="Pid"/></param>
        /// <param name="cid">sets <see cref="Cid"/></param>
        private void init(string pid, string cid)
        {
            this.Pid = pid;
    
            this.Cid = cid;;
    
            MMTTerm tp = 
                new OMA(
                    new OMS(MMTURIs.Ded), 
                    new List<MMTTerm> {
                        new OMA(
                            new OMS(MMTURIs.OnCircle),
                            new List<MMTTerm> {
                                new OMS(cid),
                                new OMS(pid),
            }),});
    
            AddFactResponse.sendAdd(new MMTSymbolDeclaration(Label, tp, df), out _URI);
    
        }
    
        /// <summary>
        /// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
        /// </summary>
        /// <param name="pid">sets <see cref="Pid"/></param>
        /// <param name="cid">sets <see cref="Cid"/></param>
        /// <param name="uri">MMT URI</param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public OnCircleFact(string pid, string cid, string uri, FactOrganizer organizer) : base(organizer)
        {
            this.Pid = pid;
            this.Cid = cid;
            this._URI = uri;
            _ = this.Label;
        }
    
        /// \copydoc Fact.parseFact(Scroll.ScrollFact)
        public new static OnCircleFact parseFact(Scroll.ScrollFact fact)
        {
            string uri = fact.@ref.uri;
    
            OMA tp = (OMA)((Scroll.ScrollSymbolFact)fact).tp;
            if (tp == null)
                return null;
    
            string circleUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0]).uri;
            string pointUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).uri;
    
            if (StageStatic.stage.factState.ContainsKey(pointUri)
             && StageStatic.stage.factState.ContainsKey(circleUri))
                return new OnCircleFact(pointUri, circleUri, uri, StageStatic.stage.factState);
    
            //If dependent facts do not exist return null
            else
                return null;
        }
    
        /// \copydoc Fact.generateLabel
        protected override string generateLabel()
    
            => _Facts[Pid].Label + "∈" + _Facts[Cid].Label;
    
    
        /// \copydoc Fact.hasDependentFacts
        public override Boolean hasDependentFacts()
    
    
        /// \copydoc Fact.getDependentFactIds
        public override string[] getDependentFactIds()
    
            => new string[] { Pid, Cid };
    
    
        /// \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.Pid].Label + "∈" + _Facts[this.Cid].Label;
            obj.GetComponent<FactWrapper>().fact = this;
    
            return obj;
        }
    
        /// \copydoc Fact.GetHashCode
        public override int GetHashCode()
    
            => Pid.GetHashCode() ^ Cid.GetHashCode();
    
    
        /// \copydoc Fact.Equivalent(Fact, Fact)
        protected override bool EquivalentWrapped(OnCircleFact c1, OnCircleFact c2)
        {
            if (c1.Pid == c2.Pid && c1.Cid == c2.Pid)
                return true;
    
            PointFact pc1 = (PointFact)_Facts[c1.Pid];
            CircleFact cc1 = (CircleFact)_Facts[c1.Cid];
    
            PointFact pc2 = (PointFact)_Facts[c2.Pid];
            CircleFact cc2 = (CircleFact)_Facts[c2.Cid];
    
            return pc1.Equivalent(pc2) && cc1.Equivalent(cc2);
        }
    }
    
    /// <summary>
    
    /// Angle comprised of a line and a circle 
    
    /// </summary>
    public class AngleCircleLineFact : FactWrappedCRTP<AngleCircleLineFact>
    {
    
    MaZiFAU's avatar
    MaZiFAU committed
        /// \copydoc Fact.s_type
        [JsonProperty]
        protected static new string s_type = "AngleCircleLineFact";
    
    
        /// One <see cref="Fact.Id">Id</see> of a <see cref="RayFact">RayFact</see> and a <see cref="CircleFact">CircleFact</see>  defining Angle [<see cref="Cid1"/>, <see cref="Rid2"/>].
    
        /// </summary>
        public string Cid1, Rid2;
        /// @}
    
    ki7077's avatar
    ki7077 committed
        public float angle;
    
    
        /// <summary> \copydoc Fact.Fact </summary>
        public AngleCircleLineFact() : base()
        {
            this.Cid1 = null;
            this.Rid2 = null;
            this.angle = 0.0f;
        }
    
        /// <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 AngleCircleLineFact(AngleCircleLineFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
    
            => init(old_to_new[fact.Cid1], old_to_new[fact.Rid2], fact.angle);
    
    
        /// <summary>
        /// Standard Constructor
        /// </summary>
    
        /// <param name="cid1">sets <see cref="Cid1"/></param>
        /// <param name="rid2">sets <see cref="Rid2"/></param>
        /// <param name="angle"> sets the angle </param>
    
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public AngleCircleLineFact(string cid1, string rid2, float angle, FactOrganizer organizer) : base(organizer)
    
            => init(cid1, rid2, angle);
    
        /// Initiates <see cref="Cid1"/>, <see cref="Rid2"/>, <see cref="angle"/> <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
    
        /// <param name="cid1">sets <see cref="Cid1"/></param>
        /// <param name="rid2">sets <see cref="Rid2"/></param>
        /// <param name="angle"> sets the angle </param>
    
        private void init(string cid1, string rid2, float angle)
        {
            this.Cid1 = cid1;
            this.Rid2 = rid2;
            this.angle = angle;
    
    
            MMTDeclaration mmtDecl = generateMMTDeclaration(angle, cid1, rid2);
    
            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="´Rid2">sets <see cref="Rid2"/></param>
        /// <param name="angle"> sets the angle </param>
    
        /// <param name="backendURI">MMT URI</param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public AngleCircleLineFact(string Cid1, string Rid2, float angle, string backendURI, FactOrganizer organizer) : base(organizer)
        {
            this.Cid1 = Cid1;
            this.Rid2 = Rid2;
            this.angle = angle;
    
            this._URI = backendURI;
            _ = this.Label;
        }
    
        /// \copydoc Fact.parseFact(Scroll.ScrollFact)
        public new static AngleCircleLineFact parseFact(Scroll.ScrollFact fact)
        {
            string uri = fact.@ref.uri;
            string
                CircleUri,
                RayUri;
    
            OMA df = (OMA)((Scroll.ScrollValueFact)fact).lhs;
            if (df == null)
                return null;
    
            // init it with 0 degrees, so we don't accidentally generate orthogonalfacts 
            // and the parsing works correctly if smb ever adds a scroll for this
            float angle = 0.0f;
    
    
            if ((((Scroll.ScrollValueFact)fact).value) != null)
    
                angle = ((OMF)(((Scroll.ScrollValueFact)fact).value)).f;
    
    
            CircleUri = ((OMS)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).uri;
            RayUri = ((OMS)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[1]).uri;
    
            if (StageStatic.stage.factState.ContainsKey(CircleUri)
             && StageStatic.stage.factState.ContainsKey(RayUri))
    
                return new AngleCircleLineFact(CircleUri, RayUri, angle, uri, StageStatic.stage.factState);
    
            else return null; //If dependent facts do not exist return null
    
        }
    
        /// \copydoc Fact.generateLabel
        protected override string generateLabel()
    
            => "∠" + _Facts[Cid1].Label + _Facts[Rid2].Label;
    
    
        /// <summary>
        /// Constructs struct for not-right-angled MMT %Fact <see cref="AddFactResponse"/>
        /// </summary>
        /// <param name="val">Angle != 90f, _not checked_</param>
    
        /// <param name="c1URI"><see cref="Cid1"/></param>
        /// <param name="R2URI"><see cref="Rid2"/></param>
        /// <param name="val"><see cref="angle"/></param>
    
        /// <returns>struct for <see cref="AddFactResponse"/></returns>
        private MMTDeclaration generateMMTDeclaration(float val, string c1URI, string r2URI)
        {
            MMTTerm lhs =
                new OMA(
                    new OMS(MMTURIs.AnglePlaneLine),
                    new List<MMTTerm> {
                        new OMS(c1URI),
                        new OMS(r2URI),
                    }
                );
    
            MMTTerm valueTp = new OMS(MMTURIs.RealLit);
            MMTTerm value = new OMF(val);
    
            return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
        }
    
    
        /// \copydoc Fact.hasDependentFacts
        public override Boolean hasDependentFacts()
            => true;
    
    
        /// \copydoc Fact.getDependentFactIds
        public override string[] getDependentFactIds()
    
            => new string[] { Cid1, Rid2 };
    
    
        /// \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.Rid2].Label;
            obj.GetComponent<FactWrapper>().fact = this;
            return obj;
        }
    
        /// \copydoc Fact.GetHashCode
        public override int GetHashCode()
    
            => this.Cid1.GetHashCode() ^ this.Rid2.GetHashCode();
    
    
        /// \copydoc Fact.Equivalent(Fact, Fact)
        protected override bool EquivalentWrapped(AngleCircleLineFact f1, AngleCircleLineFact f2)
        {
    
            if (f1.Cid1 == f2.Cid1 && f1.Rid2 == f2.Rid2)
    
                return true;
    
            CircleFact c1f1 = (CircleFact)_Facts[f1.Cid1];
            RayFact r2f1 = (RayFact)_Facts[f1.Rid2];
    
            CircleFact c1f2 = (CircleFact)_Facts[f2.Cid1];
            RayFact r2f2 = (RayFact)_Facts[f2.Rid2];
    
            return (c1f1.Equivalent(c1f2) && r2f1.Equivalent(r2f2));
        }
    }
    
    /// <summary>
    /// A RadiusFact that corresponds to a <see cref="CircleFact">PointFacts</see> and has a float value (the actual radius).
    /// </summary>
    public class RadiusFact : FactWrappedCRTP<RadiusFact>
    {
    
    MaZiFAU's avatar
    MaZiFAU committed
        /// \copydoc Fact.s_type
        [JsonProperty]
        protected static new string s_type = "RadiusFact";
    
    
        /// <summary> The circle corresponding to the radius </summary>
    
        /// <summary> The radius as a float </summary>
    
        public float rad;
    
        /// <summary> \copydoc Fact.Fact </summary>
        public RadiusFact() : base()
        {
            this.Cid1 = null;
            this.rad = 0.0f;
        }
    
        /// <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 RadiusFact(RadiusFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
    
            => init(old_to_new[fact.Cid1]);
    
    
        /// <summary>
        /// Standard Constructor
        /// </summary>
        /// <param name="cid1">sets <see cref="Cid1"/></param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public RadiusFact(string cid1, FactOrganizer organizer) : base(organizer)
    
            => init(cid1);
    
    
        /// <summary>
        /// Initiates <see cref="Cid1"/> and <see cref="rad"/>
        /// </summary>
        /// <param name="cid1">sets <see cref="Cid1"/></param>
        private void init(string cid1)
        {
            this.Cid1 = cid1;
    
            CircleFact cf1 = _Facts[cid1] as CircleFact;
            this.rad = cf1.radius;
    
    
            MMTDeclaration mmtDecl = generateMMTDeclaration(cid1, this.rad);
            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="backendURI">MMT URI</param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public RadiusFact(string Cid1, string backendURI, FactOrganizer organizer) : base(organizer)
        {
            this.Cid1 = Cid1;
    
            this._URI = backendURI;
            _ = this.Label;
        }
    
        /// \copydoc Fact.parseFact(Scroll.ScrollFact)
        public new static RadiusFact parseFact(Scroll.ScrollFact fact)
        {
            string uri = fact.@ref.uri;
            string CircleUri = ((OMS)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).uri;
    
            if (StageStatic.stage.factState.ContainsKey(CircleUri))
    
                return new RadiusFact(CircleUri, uri, StageStatic.stage.factState);
    
            else    //If dependent facts do not exist return null
                return null;
        }
    
        /// \copydoc Fact.generateLabel
        protected override string generateLabel()
    
            => "r " + _Facts[Cid1].Label;
    
    
        /// <summary>
        /// Constructs struct for not-right-angled MMT %Fact <see cref="AddFactResponse"/>
        /// </summary>
        /// <param name="rad"> see <see cref="rad"/></param>
        /// <param name="c1URI"> see <see cref="Cid1"/></param>
    
        /// <returns>struct for <see cref="AddFactResponse"/></returns>
    
        private MMTDeclaration generateMMTDeclaration(string c1URI, float rad)
    
        {
            MMTTerm lhs =
                new OMA(
                    new OMS(MMTURIs.RadiusCircleMetric),
                    new List<MMTTerm> {
                        new OMS(c1URI),
                    }
                );
    
            MMTTerm valueTp = new OMS(MMTURIs.RealLit);
            MMTTerm value = new OMF(rad);
    
            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 };
    
    
        /// \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 = "r: " + _Facts[this.Cid1].Label;
    
            obj.GetComponent<FactWrapper>().fact = this;
            return obj;
        }
    
        /// \copydoc Fact.GetHashCode
        public override int GetHashCode()
    
            => this.Cid1.GetHashCode();
    
    
        /// \copydoc Fact.Equivalent(Fact, Fact)
        protected override bool EquivalentWrapped(RadiusFact f1, RadiusFact f2)
        {
    
            if (f1.Cid1 == f2.Cid1) // if they correspond to the same circle, then automatically the radius has to be the same
    
                return true;
    
            CircleFact c1f1 = (CircleFact)_Facts[f1.Cid1];
            CircleFact c1f2 = (CircleFact)_Facts[f2.Cid1];
            return (c1f1.Equivalent(c1f2));
        }
    }
    
    /// <summary>
    /// Area of a <see cref="CircleFact">CircleFact</see> 
    /// </summary>
    public class AreaCircleFact : FactWrappedCRTP<AreaCircleFact>
    {
    
    MaZiFAU's avatar
    MaZiFAU committed
        /// \copydoc Fact.s_type
        [JsonProperty]
        protected static new string s_type = "AreaCircleFact";
    
        /// <summary> the circle <see cref="CircleFact">CircleFact</see>  </summary>
    
        public string Cid1;
        /// <summary> the area which is contained by the circle </summary>
        public float A;
    
    
        /// <summary> \copydoc Fact.Fact </summary>
        public AreaCircleFact() : base()
        {
            this.Cid1 = null;
            this.A = 0.0f;
        }
    
        /// <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 AreaCircleFact(AreaCircleFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
    
            => init(old_to_new[fact.Cid1]);
    
    
        /// <summary>
        /// Standard Constructor
        /// </summary>
        /// <param name="cid1">sets <see cref="Cid1"/></param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public AreaCircleFact(string cid1, FactOrganizer organizer) : base(organizer)
    
            => init(cid1);
    
    
        /// <summary>
        /// Initiates <see cref="Cid1"/> and creates MMT %Fact Server-Side
        /// </summary>
        /// <param name="cid1">sets <see cref="Cid1"/></param>
    
        private void init(string cid1)
        {
            this.Cid1 = cid1;
    
            CircleFact cf1 = _Facts[cid1] as CircleFact;
    
            this.A = cf1.radius * cf1.radius * ((float)System.Math.PI);
    
            MMTDeclaration mmtDecl = generateMMTDeclaration(cid1, this.A);
    
            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="backendURI">MMT URI</param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public AreaCircleFact(string Cid1, string backendURI, FactOrganizer organizer) : base(organizer)
        {
            this.Cid1 = Cid1;
    
            this._URI = backendURI;
            _ = this.Label;
        }
    
        /// \copydoc Fact.parseFact(Scroll.ScrollFact)
        public new static AreaCircleFact parseFact(Scroll.ScrollFact fact)
        {
            string uri = fact.@ref.uri;
            string CircleUri = ((OMS)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).uri;
    
            if (StageStatic.stage.factState.ContainsKey(CircleUri))
                return new AreaCircleFact(CircleUri, uri, StageStatic.stage.factState);
            else    //If dependent facts do not exist return null
                return null;
        }
    
        /// \copydoc Fact.generateLabel
        protected override string generateLabel()
    
            => "A(" + _Facts[Cid1].Label + ")";
    
    
        /// <summary>
        /// Constructs a response, that is sent to the MMT-Server
        /// </summary>
        /// <param name="area"> area of the circle </param>
        /// <param name="c1URI">  <see cref="Cid1"/></param>
        /// <returns>struct for <see cref="AddFactResponse"/></returns>
        private MMTDeclaration generateMMTDeclaration(string c1URI, float area)
        {
            MMTTerm lhs =
                new OMA(
                    new OMS(MMTURIs.AreaCircle),
                    new List<MMTTerm> {
                        new OMS(c1URI),
                    }
                );
    
            MMTTerm valueTp = new OMS(MMTURIs.RealLit);
            MMTTerm value = new OMF(area);
    
            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 };
    
    
        /// \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.GetComponent<FactWrapper>().fact = this;
            return obj;
        }
    
        /// \copydoc Fact.GetHashCode
        /// is this a problem?
        public override int GetHashCode()
    
            => this.Cid1.GetHashCode();
    
    
        /// \copydoc Fact.Equivalent(Fact, Fact)
        protected override bool EquivalentWrapped(AreaCircleFact f1, AreaCircleFact f2)
        {
            if (f1.Cid1 == f2.Cid1)
                return true;
    
            CircleFact c1f1 = (CircleFact)_Facts[f1.Cid1];
            CircleFact c1f2 = (CircleFact)_Facts[f2.Cid1];
            return (c1f1.Equivalent(c1f2) && f1.A == f2.A);
        }
    }
    
    /// <summary>
    /// The volume of a cone A  defined by a base area  <see cref="CircleFact">CircleFact</see>, an apex <see cref="PointFact">PointFact</see> and the volume as float
    /// </summary>
    public class ConeVolumeFact : FactWrappedCRTP<ConeVolumeFact>
    {
    
    MaZiFAU's avatar
    MaZiFAU committed
        /// \copydoc Fact.s_type
        [JsonProperty]
        protected static new string s_type = "ConeVolumeFact";
    
    
        ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the base area </summary>
        public string Cid1;
        ///  <summary> a <see cref="PointFact">PointFact</see> describing the apex point  </summary>
        public string Pid1;
        ///  <summary> the volume of the cone as a float </summary>
        public float vol;
    
        /// <summary> \copydoc Fact.Fact </summary>
        public ConeVolumeFact() : base()
        {
            this.Cid1 = null;
            this.Pid1 = null;
            this.vol = 0.0f;
        }
    
        /// <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 ConeVolumeFact(ConeVolumeFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
    
            => init(old_to_new[fact.Cid1], old_to_new[fact.Pid1], fact.vol);
    
    
        /// <summary>
        /// Standard Constructor
        /// </summary>
        /// <param name="cid1">sets <see cref="Cid1"/></param>
        /// <param name="pid1">sets <see cref="Pid1"/></param>
        /// <param name="vol">sets <see cref="vol"/></param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    
        public ConeVolumeFact(string cid1, string pid1, float vol, FactOrganizer organizer) : base(organizer)
            => init(cid1, pid1, vol);
    
        /// Initiates <see cref="Cid1"/>, <see cref="Pid1"/>, <see cref="vol"/>,  <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
    
        /// </summary>
        /// <param name="cid1">sets <see cref="Cid1"/></param>
        /// <param name="pid1">sets <see cref="Pid1"/></param>
        /// <param name="vol">sets <see cref="vol"/></param>
    
        private void init(string cid1, string pid1, float vol)
    
        {
            this.Cid1 = cid1;
            this.Pid1 = pid1;
            this.vol = vol;
    
    
            MMTDeclaration mmtDecl = generateMMTDeclaration(cid1, pid1, vol);
    
            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="Pid1">sets <see cref="Pid1"/></param>
        /// <param name="volume">sets <see cref="vol"/></param>
    
        /// <param name="backendURI">MMT URI</param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    
        public ConeVolumeFact(string Cid1, string Pid1, float volume, string backendURI, FactOrganizer organizer) : base(organizer)
    
        {
            this.Cid1 = Cid1;
            this.Pid1 = Pid1;
            this.vol = volume;
    
            this._URI = backendURI;
            _ = this.Label;
        }
    
        /// \copydoc Fact.parseFact(Scroll.ScrollFact)
        public new static ConeVolumeFact parseFact(Scroll.ScrollFact fact)
        {
            string uri = fact.@ref.uri;
    
            if (((Scroll.ScrollValueFact)fact).lhs == null)
                return null;
    
            string CircleUri = ((OMS)((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[0]).uri;
            string PointUri = ((OMS)((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[1]).uri;
            float volume = 0.0f;
    
            if ((((Scroll.ScrollValueFact)fact).value) != null)
                volume = ((OMF)((Scroll.ScrollValueFact)fact).value).f;
    
            if (StageStatic.stage.factState.ContainsKey(CircleUri) && StageStatic.stage.factState.ContainsKey(PointUri))
    
                return new ConeVolumeFact(CircleUri, PointUri, volume, uri, StageStatic.stage.factState);
    
    
            else    //If dependent facts do not exist return null
                return null;
        }
    
        /// \copydoc Fact.generateLabel
        protected override string generateLabel()
    
            => "V(" + _Facts[Cid1].Label + "," + _Facts[Pid1].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="p1URI"> Uri for <see cref="Pid1"/></param>
        /// <param name="val"> <see cref="vol"/></param>
        /// <returns>struct for <see cref="AddFactResponse"/></returns>
        private MMTDeclaration generateMMTDeclaration(string c1URI, string p1URI, float val)
        {
            MMTTerm lhs =
                new OMA(
                    new OMS(MMTURIs.VolumeCone),
    
                    new List<MMTTerm> {
                        new OMA(new OMS(MMTURIs.ConeOfCircleApex),
                            new List<MMTTerm> {
                                new OMS(c1URI),
                                new OMS(p1URI),
                             }
                        ),
                    }
                );
    
            MMTTerm valueTp = new OMS(MMTURIs.RealLit);
            MMTTerm 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, Pid1 };
    
    
        /// \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 + _Facts[this.Pid1].Label;
    
            obj.GetComponent<FactWrapper>().fact = this;
    
            return obj;
        }
    
        /// \copydoc Fact.GetHashCode
        /// uhhh is this a problem?
        public override int GetHashCode()
    
            => this.Cid1.GetHashCode() ^ this.Pid1.GetHashCode();
    
    
        /// \copydoc Fact.Equivalent(Fact, Fact)
        protected override bool EquivalentWrapped(ConeVolumeFact f1, ConeVolumeFact f2)
        {
            if (f1.Cid1 == f2.Cid1 && f1.Pid1 == f2.Pid1)
                return true;
    
            CircleFact c1f1 = (CircleFact)_Facts[f1.Cid1];
            CircleFact c1f2 = (CircleFact)_Facts[f2.Cid1];
    
            PointFact p1f1 = (PointFact)_Facts[f1.Pid1];
            PointFact p1f2 = (PointFact)_Facts[f2.Pid1];
    
    
            return (c1f1.Equivalent(c1f2) && p1f1.Equivalent(p1f2) && (Mathf.Abs(f1.vol - f2.vol) < 0.001));
    
        }
    }
    
    /// <summary>
    /// The fact that the plane of a <see cref="CircleFact">CircleFact</see> and the line <see cref="RayFact>RayFact</see> are orthogonal
    /// </summary>
    public class OrthogonalCircleLineFact : FactWrappedCRTP<OrthogonalCircleLineFact>
    {
    
    MaZiFAU's avatar
    MaZiFAU committed
        /// \copydoc Fact.s_type
        [JsonProperty]
        protected static new string s_type = "OrthogonalCircleLineFact";
    
    
        ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the base area </summary>
        public string Cid1;
        ///  <summary> a <see cref="RayFact">Rayfact</see> describing the line </summary>
        public string Lid1;
    
    
        /// <summary> \copydoc Fact.Fact </summary>
        public OrthogonalCircleLineFact() : base()
        {
            this.Cid1 = null;
            this.Lid1 = 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 OrthogonalCircleLineFact(OrthogonalCircleLineFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
    
            => init(old_to_new[fact.Cid1], old_to_new[fact.Lid1]);
    
    
        /// <summary>
        /// Standard Constructor
        /// </summary>
        /// <param name="cid1">sets <see cref="Cid1"/></param>
    
        /// <param name="lid1">sets <see cref="Lid1"/></param>
    
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public OrthogonalCircleLineFact(string cid1, string lid1, FactOrganizer organizer) : base(organizer)
    
            => init(cid1, lid1);
    
    
        /// <summary>
        /// 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="cid1">sets <see cref="Cid1"/></param>
    
        /// <param name="lid1">sets <see cref="Lid1"/></param>
    
        private void init(string cid1, string lid1)
        {
            this.Cid1 = cid1;
            this.Lid1 = lid1;
    
    
            MMTDeclaration mmtDecl = generateMMTDeclaration(cid1, lid1);
    
            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="Lid1">sets <see cref="Lid1"/></param>
    
        /// <param name="backendURI">MMT URI</param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    
        public OrthogonalCircleLineFact(string Cid1, string Lid1, string backendURI, FactOrganizer organizer) : base(organizer)
    
        {
            this.Cid1 = Cid1;
            this.Lid1 = Lid1;
    
            this._URI = backendURI;
            _ = this.Label;
        }
    
        /// \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()
    
            => _Facts[Cid1].Label + "⊥" + _Facts[Lid1].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)
        {
    
            MMTTerm tp = new OMA(
                new OMS(MMTURIs.Ded), 
                new List<MMTTerm>{
                    new OMA(
                        new OMS(MMTURIs.OrthoCircleLine), 
                        new List<MMTTerm>{
                            new OMS(c1URI),
                            new OMS(l1URI),
                        }
                    ),
                }
            );
    
    
            MMTTerm df = null;
    
            return new MMTSymbolDeclaration(this.Label, tp, df);
        }
    
        /// \copydoc Fact.hasDependentFacts
        public override Boolean 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);
            obj.transform.GetChild(0).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Cid1].Label;
            obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Lid1].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)
        {
            if (f1.Cid1 == f2.Cid1 && f1.Lid1 == f2.Lid1)
                return true;
    
            CircleFact c1f1 = (CircleFact)_Facts[f1.Cid1];
            CircleFact c1f2 = (CircleFact)_Facts[f2.Cid1];
    
            RayFact l1f1 = (RayFact)_Facts[f1.Lid1];
            RayFact l1f2 = (RayFact)_Facts[f2.Lid1];
    
            return (c1f1.Equivalent(c1f2) && l1f1.Equivalent(l1f2));
        }
    }
    
    /// <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>
    {
    
    MaZiFAU's avatar
    MaZiFAU committed
        /// \copydoc Fact.s_type
        [JsonProperty]
        protected static new string s_type = "TruncatedConeVolumeFact";
    
    
        ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the base area </summary>
        public string Cid1;
    
        ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the top area  </summary>
    
        ///  <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>
        /// 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 TruncatedConeVolumeFact(TruncatedConeVolumeFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer) 
            => init(old_to_new[fact.Cid1], old_to_new[fact.Cid2], fact.vol, old_to_new[fact.unequalCirclesProof], fact.proof);
    
    
        /// <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;
    
            MMTDeclaration mmtDecl = generateMMTDeclaration(cid1, cid2, vol, unequalproof, proof);
    
            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="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;