Skip to content
Snippets Groups Projects
Fact.cs 147 KiB
Newer Older
  • Learn to ignore specific revisions
  •         PointFact pf = _Facts[pid] as PointFact;
            RayFact rf = _Facts[rid] as RayFact;
    
    
            List<MMTTerm> innerArguments = new List<MMTTerm>
            {
                new OMS(rURI),
                new OMS(pURI)
            };
    
            List<MMTTerm> outerArguments = new List<MMTTerm>
            {
    
                new OMA(new OMS(JSONManager.MMTURIs.OnLine), innerArguments)
    
            MMTTerm tp = new OMA(new OMS(JSONManager.MMTURIs.Ded), outerArguments);
    
            MMTTerm df = null;
    
            MMTSymbolDeclaration mmtDecl = new MMTSymbolDeclaration(this.Label, tp, df);
    
            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="pid">sets <see cref="Pid"/></param>
        /// <param name="rid">sets <see cref="Rid"/></param>
        /// <param name="uri">MMT URI</param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    
        public OnLineFact(string pid, string rid, string uri, FactOrganizer organizer) : base(organizer)
    
            this._URI = uri;
    
        /// \copydoc Fact.parseFact(Scroll.ScrollFact)
        public new static OnLineFact parseFact(Scroll.ScrollFact fact)
    
            string uri = fact.@ref.uri;
    
            string lineUri = "";
            string pointUri = "";
            
            if (((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0] is OMS)
            {
                // standard case
                lineUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0]).uri;
                pointUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).uri;
            }
            else {
                // case when line Uri has a projl on the line Argument 
                lineUri = ((OMS)((OMA)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0]).arguments[0]).uri;
                pointUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).uri;
    
    
            }
    
            if (StageStatic.stage.factState.ContainsKey(pointUri)
             && StageStatic.stage.factState.ContainsKey(lineUri))
                return new OnLineFact(pointUri, lineUri, uri, StageStatic.stage.factState);
    
            //If dependent facts do not exist return null
            else
                return null;
    
        protected override string generateLabel()
        {
    
            return _Facts[Pid].Label + "∈" + _Facts[Rid].Label;
    
    BenniHome's avatar
    BenniHome committed
    
    
        public override Boolean hasDependentFacts()
        {
            return true;
        }
    
    
        /// \copydoc Fact.getDependentFactIds
    
        public override string[] getDependentFactIds()
    
            return new string[] { Pid, Rid };
    
        /// \copydoc Fact.instantiateDisplay(GameObject, Transform)
    
    John Schihada's avatar
    John Schihada committed
        public override GameObject instantiateDisplay(GameObject prefab, Transform transform)
    
    John Schihada's avatar
    John Schihada committed
        {
            var obj = GameObject.Instantiate(prefab, Vector3.zero, Quaternion.identity, transform);
    
            obj.transform.GetChild(0).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Pid].Label;
            obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Rid].Label;
    
    John Schihada's avatar
    John Schihada committed
            obj.GetComponent<FactWrapper>().fact = this;
            return obj;
        }
    
    
            return this.Pid.GetHashCode() ^ this.Rid.GetHashCode();
    
    BenniHome's avatar
    BenniHome committed
    
    
        /// \copydoc Fact.Equivalent(Fact, Fact)
    
        protected override bool EquivalentWrapped(OnLineFact f1, OnLineFact f2)
    
            if (f1.Pid == f2.Pid && f1.Rid == f2.Rid)
                return true;
    
    
            PointFact pf1 = (PointFact)_Facts[f1.Pid];
            RayFact rf1 = (RayFact)_Facts[f1.Rid];
            PointFact pf2 = (PointFact)_Facts[f2.Pid];
            RayFact rf2 = (RayFact)_Facts[f2.Rid];
    
    
            return pf1.Equivalent(pf2) && rf1.Equivalent(rf2);
    
    /// <summary>
    /// Angle comprised of three <see cref="PointFact">PointFacts</see> [A,B,C]
    /// </summary>
    
    public class AngleFact : FactWrappedCRTP<AngleFact>
    
        [JsonProperty]
    
        protected static new string s_type = "AngleFact";
    
        /// @{ <summary>
        /// One <see cref="Fact.Id">Id</see> of three <see cref="PointFact">PointFacts</see> defining Angle [<see cref="Pid1"/>, <see cref="Pid2"/>, <see cref="Pid3"/>].
        /// </summary>
    
        public string Pid1, Pid2, Pid3;
    
        /// @}
    
        /// <summary> <see langword="true"/>, if AngleFact is approximately 90° or 270°</summary>
    
        public bool is_right_angle;
    
    
        /// <summary> \copydoc Fact.Fact </summary>
    
        public AngleFact() : base()
        {
            this.Pid1 = null;
            this.Pid2 = null;
            this.Pid3 = null;
            this.is_right_angle = false;
        }
    
    
        /// <summary>
        /// Copies <paramref name="fact"/> by initiating new MMT %Fact.
        /// </summary>
        /// <param name="fact">Fact to be copied</param>
        /// <param name="old_to_new"><c>Dictionary</c> mapping <paramref name="fact"/>.<see cref="getDependentFactIds"/> in <paramref name="fact"/>.<see cref="Fact._Facts"/> to corresponding <see cref="Fact.Id"/> in <paramref name="organizer"/> </param>
        /// <param name="organizer">sets <see cref="_Facts"/></param>
    
        public AngleFact(AngleFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
        {
            init(old_to_new[fact.Pid1], old_to_new[fact.Pid2], old_to_new[fact.Pid3]);
        }
    
    
        /// <summary>
        /// Standard Constructor
        /// </summary>
        /// <param name="pid1">sets <see cref="Pid1"/></param>
        /// <param name="pid2">sets <see cref="Pid2"/></param>
        /// <param name="pid3">sets <see cref="Pid3"/></param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    
        public AngleFact(string pid1, string pid2, string pid3, FactOrganizer organizer) : base(organizer)
    
        /// <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="pid1">sets <see cref="Pid1"/></param>
        /// <param name="pid2">sets <see cref="Pid2"/></param>
        /// <param name="pid3">sets <see cref="Pid3"/></param>
    
        private void init(string pid1, string pid2, string pid3)
    
            this.Pid1 = pid1;
            this.Pid2 = pid2;
            this.Pid3 = pid3;
    
            PointFact pf1 = _Facts[pid1] as PointFact;
            PointFact pf2 = _Facts[pid2] as PointFact;
            PointFact pf3 = _Facts[pid3] as PointFact;
    
            float v = GetAngle(); // sets is_right_angle
    
            string p1URI = pf1.Id;
            string p2URI = pf2.Id;
            string p3URI = pf3.Id;
    
    ki7077's avatar
    ki7077 committed
    
            mmtDecl = generateNot90DegreeAngleDeclaration(v, p1URI, p2URI, p3URI);
    
            AddFactResponse.sendAdd(mmtDecl, out this._URI);
    
        /// <summary>
        /// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
        /// </summary>
        /// <param name="Pid1">sets <see cref="Pid1"/></param>
        /// <param name="Pid2">sets <see cref="Pid2"/></param>
        /// <param name="Pid3">sets <see cref="Pid3"/></param>
        /// <param name="backendURI">MMT URI</param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    
        public AngleFact(string Pid1, string Pid2, string Pid3, string backendURI, FactOrganizer organizer) : base(organizer)
    
        {
            this.Pid1 = Pid1;
            this.Pid2 = Pid2;
            this.Pid3 = Pid3;
    
            float v = GetAngle();
            this._URI = backendURI;
            _ = this.Label;
        }
    
        public AngleFact(string Pid1, string Pid2, string Pid3,float angle, string backendURI, FactOrganizer organizer) : base(organizer)
        {
            this.Pid1 = Pid1;
            this.Pid2 = Pid2;
            this.Pid3 = Pid3;
    
    
            this._URI = backendURI;
    
        /// \copydoc Fact.parseFact(Scroll.ScrollFact)
        public new static AngleFact parseFact(Scroll.ScrollFact fact)
    
            string uri = fact.@ref.uri;
            string
                pointAUri,
                pointBUri,
                pointCUri;
    
            //If angle is not a 90Degree-Angle
            if (fact.GetType().Equals(typeof(Scroll.ScrollValueFact)))
            {
    
                OMA df = (OMA)((Scroll.ScrollValueFact)fact).lhs;
    
                if (df == null)
                    return null;
    
          
    
                if (((Scroll.ScrollValueFact)fact).value != null)
                    angle = ((OMF)(((Scroll.ScrollValueFact)fact).value)).f;
    
    
    
                pointAUri = ((OMS)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).uri;
                pointBUri = ((OMS)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[1]).uri;
                pointCUri = ((OMS)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[2]).uri;
    
            // this should never happen anymore
    
            //If angle is a 90Degree-Angle
            else {
    
                Debug.Log("Angle 90 degrees parsed. This shouldn't happen anymore");
                
    
                pointAUri = ((OMS)((OMA)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).arguments[0]).uri;
                pointBUri = ((OMS)((OMA)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).arguments[1]).uri;
                pointCUri = ((OMS)((OMA)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).arguments[2]).uri;
            }
    
    
            if (StageStatic.stage.factState.ContainsKey(pointAUri)
             && StageStatic.stage.factState.ContainsKey(pointBUri)
             && StageStatic.stage.factState.ContainsKey(pointCUri))
    
            {
    //                return new AngleFact(pointAUri, pointBUri, pointCUri, uri, StageStatic.stage.factState);
                    return new AngleFact(pointAUri, pointBUri, pointCUri,angle, uri, StageStatic.stage.factState);
            }
            else
            {   //If dependent facts do not exist return null
    
        protected override string generateLabel()
        {
    
            return (is_right_angle ? "⊾" : "∠") + _Facts[Pid1].Label + _Facts[Pid2].Label + _Facts[Pid3].Label;
    
        /// <summary>
        /// Computes smallest angle and sets <see cref="is_right_angle"/>
        /// </summary>
        /// <returns>Smallets angle between [<see cref="Pid1"/>, <see cref="Pid2"/>] and [<see cref="Pid2"/>, <see cref="Pid3"/>]</returns>
    
        private float GetAngle()
        {
    
            PointFact pf1 = _Facts[Pid1] as PointFact;
            PointFact pf2 = _Facts[Pid2] as PointFact;
            PointFact pf3 = _Facts[Pid3] as PointFact;
    
    
            float v = Vector3.Angle((pf1.Point - pf2.Point), (pf3.Point - pf2.Point));
            this.is_right_angle = Mathf.Abs(v - 90.0f) < 0.01;
    
            return is_right_angle ? 90f : v;
        }
    
    
        /// <summary>
        /// Constructs struct for right-angled MMT %Fact <see cref="AddFactResponse"/>
        /// </summary>
        /// <param name="val">Angle == 90f, _not checked_</param>
        /// <param name="p1URI"><see cref="Pid1"/></param>
        /// <param name="p2URI"><see cref="Pid2"/></param>
        /// <param name="p3URI"><see cref="Pid3"/></param>
        /// <returns>struct for <see cref="AddFactResponse"/></returns>
    
        private MMTDeclaration generate90DegreeAngleDeclaration(float val, string p1URI, string p2URI, string p3URI) {
    
            MMTTerm argument = new OMA(
    
                new OMS(JSONManager.MMTURIs.Eq),
    
                    new OMS(JSONManager.MMTURIs.RealLit),
    
                        new OMS(JSONManager.MMTURIs.Angle),
    
                    new OMF(val) // 90f
    
    
            MMTTerm tp = new OMA(new OMS(JSONManager.MMTURIs.Ded), new List<MMTTerm> { argument });
    
            MMTTerm df = null;
    
            return new MMTSymbolDeclaration(this.Label, tp, df);
        }
    
    
        /// <summary>
        /// Constructs struct for not-right-angled MMT %Fact <see cref="AddFactResponse"/>
        /// </summary>
        /// <param name="val">Angle != 90f, _not checked_</param>
        /// <param name="p1URI"><see cref="Pid1"/></param>
        /// <param name="p2URI"><see cref="Pid2"/></param>
        /// <param name="p3URI"><see cref="Pid3"/></param>
        /// <returns>struct for <see cref="AddFactResponse"/></returns>
    
        private MMTDeclaration generateNot90DegreeAngleDeclaration(float val, string p1URI, string p2URI, string p3URI)
        {
            MMTTerm lhs =
                new OMA(
    
                    new OMS(JSONManager.MMTURIs.Angle),
    
            MMTTerm valueTp = new OMS(JSONManager.MMTURIs.RealLit);
    
            MMTTerm value = new OMF(val);
            
            return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
        }
    
        public override Boolean hasDependentFacts()
        {
            return true;
        }
    
    
        /// \copydoc Fact.getDependentFactIds
    
        public override string[] getDependentFactIds()
    
            return new string[] { Pid1, Pid2, Pid3 };
    
        /// \copydoc Fact.instantiateDisplay(GameObject, Transform)
    
    John Schihada's avatar
    John Schihada committed
        public override GameObject instantiateDisplay(GameObject prefab, Transform transform) {
    
    John Schihada's avatar
    John Schihada committed
            var obj = GameObject.Instantiate(prefab, Vector3.zero, Quaternion.identity, transform);
    
            obj.transform.GetChild(0).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Pid1].Label;
            obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Pid2].Label;
            obj.transform.GetChild(2).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Pid3].Label;
    
    John Schihada's avatar
    John Schihada committed
            obj.GetComponent<FactWrapper>().fact = this;
            return obj;
        }
    
    
            return this.Pid1.GetHashCode() ^ this.Pid2.GetHashCode() ^ this.Pid3.GetHashCode();
    
        /// \copydoc Fact.Equivalent(Fact, Fact)
    
        protected override bool EquivalentWrapped(AngleFact f1, AngleFact f2)
    
            if ((f1.Pid1 == f2.Pid1 && f1.Pid2 == f2.Pid2 && f1.Pid3 == f2.Pid3))// || 
                //(f1.Pid1 == f2.Pid3 && f1.Pid2 == f2.Pid2 && f1.Pid3 == f2.Pid1))
                return true;
    
    
            PointFact p1f1 = (PointFact)_Facts[f1.Pid1];
            PointFact p2f1 = (PointFact)_Facts[f1.Pid2];
            PointFact p3f1 = (PointFact)_Facts[f1.Pid3];
            PointFact p1f2 = (PointFact)_Facts[f2.Pid1];
            PointFact p2f2 = (PointFact)_Facts[f2.Pid2];
            PointFact p3f2 = (PointFact)_Facts[f2.Pid3];
    
            return (p1f1.Equivalent(p1f2) && p2f1.Equivalent(p2f2) && p3f1.Equivalent(p3f2));
            //|| (p1f1.Equivalent(p3f2) && p2f1.Equivalent(p2f2) && p1f1.Equivalent(p3f2));
        }
    }
    
    
    MaZiFAU's avatar
    MaZiFAU committed
    /// <summary>
    /// A RightAngleFact defined by 3  <see cref="PointFact">Pointfact</see> 
    /// </summary>
    public class RightAngleFact : FactWrappedCRTP<RightAngleFact>
    {
        /// \copydoc Fact.s_type
        [JsonProperty]
        protected static new string s_type = "RightAngleFact";
    
        ///  <summary> three <see cref="PointFact">Pointfacts</see> defining the right angle </summary>
        public string Pid1, Pid2, Pid3;
    
        /// <summary> \copydoc Fact.Fact </summary>
        public RightAngleFact() : base()
        {
            this.Pid1 = null;
            this.Pid2 = null;
            this.Pid3 = 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 RightAngleFact(RightAngleFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
        {
            init(old_to_new[fact.Pid1], old_to_new[fact.Pid2], old_to_new[fact.Pid3]);
        }
    
        /// <summary>
        /// Standard Constructor
        /// </summary>
        /// <param name="pid1">sets <see cref="Pid1"/></param>
        /// <param name="pid2">sets <see cref="Pid2"/></param>
        /// <param name="pid3">sets <see cref="Pid3"/></param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public RightAngleFact(string pid1, string pid2, string pid3, FactOrganizer organizer) : base(organizer)
        {
            init(pid1, pid2, pid3);
        }
    
        /// <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="pid1">sets <see cref="Pid1"/></param>
        /// <param name="pid2">sets <see cref="Pid2"/></param>
        /// <param name="pid3">sets <see cref="Pid3"/></param>
        private void init(string pid1, string pid2, string pid3)
        {
            this.Pid1 = pid1;
            this.Pid2 = pid2;
            this.Pid3 = pid3;
    
            PointFact pf1 = _Facts[pid1] as PointFact;
            PointFact pf2 = _Facts[pid2] as PointFact;
            PointFact pf3 = _Facts[pid3] as PointFact;
    
    
    MaZiFAU's avatar
    MaZiFAU committed
            MMTDeclaration mmtDecl;
            string p1URI = pf1.Id;
            string p2URI = pf2.Id;
            string p3URI = pf3.Id;
    
    
            mmtDecl = generateMMTDeclaration(p1URI, p2URI, p3URI);
    
            AddFactResponse.sendAdd(mmtDecl, out this._URI);
        }
    
        /// <summary>
        /// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
        /// </summary>
        /// <param name="Pid1">sets <see cref="Pid1"/></param>
        /// <param name="Pid2">sets <see cref="Pid2"/></param>
        /// <param name="Pid3">sets <see cref="Pid3"/></param>
        /// <param name="backendURI">MMT URI</param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public RightAngleFact(string Pid1, string Pid2, string Pid3, string backendURI, FactOrganizer organizer) : base(organizer)
        {
            this.Pid1 = Pid1;
            this.Pid2 = Pid2;
            this.Pid3 = Pid3;
    
            this._URI = backendURI;
            _ = this.Label;
        }
    
        /// \copydoc Fact.parseFact(Scroll.ScrollFact)
        public new static RightAngleFact parseFact(Scroll.ScrollFact fact)
        {
            OMA tp = (OMA)((Scroll.ScrollSymbolFact)fact).tp;
            if (tp == null)
                return null;
    
            string Point1Uri = "";
            string Point2Uri = "";
            string Point3Uri = "";
    
            string uri = fact.@ref.uri;
            OMA proof_OMA = (OMA)((Scroll.ScrollSymbolFact)fact).tp; // proof DED
            OMA rightAngleOMA = (OMA)proof_OMA.arguments[0]; // rightAngle OMA
    
            if (rightAngleOMA.arguments[0] is OMS)
            {
                Point1Uri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0]).uri;
                Point2Uri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).uri;
                Point3Uri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[2]).uri;
            }
    
            if (StageStatic.stage.factState.ContainsKey(Point1Uri)
             && StageStatic.stage.factState.ContainsKey(Point2Uri)
             && StageStatic.stage.factState.ContainsKey(Point3Uri))
    
                return new RightAngleFact(Point1Uri, Point2Uri, Point3Uri, uri, StageStatic.stage.factState);
    
            else    //If dependent facts do not exist return null
                return null;
        }
    
    
        /// \copydoc Fact.generateLabel
        protected override string generateLabel()
        {
            return _Facts[Pid1].Label + _Facts[Pid2].Label + _Facts[Pid3].Label + "⊥";
        }
    
    
        /// <summary>
        /// Constructs struct for not-right-angled MMT %Fact <see cref="AddFactResponse"/>
        /// </summary>
        /// <param name="p1URI"> Uri for <see cref="Pid1"/></param>
        /// <param name="p2URI"> Uri for <see cref="Pid2"/></param>
        /// <param name="p3URI"> Uri for <see cref="Pid3"/></param>
        /// <returns>struct for <see cref="AddFactResponse"/></returns>
        private MMTDeclaration generateMMTDeclaration(string p1URI, string p2URI, string p3URI)
        {
            List<MMTTerm> innerArguments = new List<MMTTerm>
            {
                new OMS(p1URI),
                new OMS(p2URI),
                new OMS(p3URI)
            };
    
            List<MMTTerm> outerArguments = new List<MMTTerm>
            {
                new OMA(new OMS(MMTURIs.RightAngle), innerArguments)
            };
            MMTTerm tp = new OMA(new OMS(MMTURIs.Ded), outerArguments);
            MMTTerm df = null;
    
            return new MMTSymbolDeclaration(this.Label, tp, df);
        }
    
        /// \copydoc Fact.hasDependentFacts
        public override Boolean hasDependentFacts()
        {
            return true;
        }
    
        /// \copydoc Fact.getDependentFactIds
        public override string[] getDependentFactIds()
        {
            return new string[] { Pid1, Pid2, Pid3 };
        }
    
        /// \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.Pid1].Label;
            obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Pid2].Label;
            obj.transform.GetChild(2).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Pid3].Label;
    
    
            obj.GetComponent<FactWrapper>().fact = this;
            return obj;
        }
    
        /// \copydoc Fact.GetHashCode
        /// uhhh is this a problem?
        public override int GetHashCode()
        {
            return this.Pid1.GetHashCode() ^ this.Pid2.GetHashCode() ^ this.Pid3.GetHashCode();
        }
    
        /// \copydoc Fact.Equivalent(Fact, Fact)
        protected override bool EquivalentWrapped(RightAngleFact f1, RightAngleFact f2)
        {
            if (f1.Pid1 == f2.Pid1 && f1.Pid2 == f2.Pid2 && f1.Pid3 == f2.Pid3)
                return true;
    
            PointFact p1f1 = (PointFact)_Facts[f1.Pid1];
            PointFact p2f1 = (PointFact)_Facts[f1.Pid2];
            PointFact p3f1 = (PointFact)_Facts[f1.Pid3];
    
            PointFact p1f2 = (PointFact)_Facts[f2.Pid1];
            PointFact p2f2 = (PointFact)_Facts[f2.Pid2];
            PointFact p3f2 = (PointFact)_Facts[f2.Pid3];
    
    
    
    
            return (p1f1.Equivalent(p1f2) && p2f1.Equivalent(p2f2) && p3f1.Equivalent(p3f2));
    
        }
    }
    
    ki7077's avatar
    ki7077 committed
    
    
    /// <summary>
    /// Two parallel Lines comprised of two <see cref="LineFact">LineFacts</see> 
    /// </summary>
    public class ParallelLineFact : FactWrappedCRTP<ParallelLineFact>
    {
    
    MaZiFAU's avatar
    MaZiFAU committed
        /// \copydoc Fact.s_type
        [JsonProperty]
        protected static new string s_type = "ParallelLineFact";
    
    
        /// @{ <summary>
        /// One <see cref="Fact.Id">Id</see> of thwo <see cref="LineFact">PointFacts</see> defining Angle [<see cref="Lid1"/>, <see cref="Lid2"/>].
        /// </summary>
        public string Lid1, Lid2;
        /// @}
    
    
    
    
        /// <summary> \copydoc Fact.Fact </summary>
        public ParallelLineFact() : base()
        {
            this.Lid1 = null;
            this.Lid2 = 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 ParallelLineFact(ParallelLineFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
        {
            init(old_to_new[fact.Lid1], old_to_new[fact.Lid2]);
        }
    
        /// <summary>
        /// Standard Constructor
        /// </summary>
        /// <param name="lid1">sets <see cref="Lid1"/></param>
        /// <param name="lid2">sets <see cref="Lid2"/></param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public ParallelLineFact(string lid1, string lid2, FactOrganizer organizer) : base(organizer)
        {
            init(lid1, lid2);
        }
    
        /// <summary>
        /// Initiates <see cref="Lid1"/>, <see cref="Lid2"/>, <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
        /// </summary>
        /// <param name="lid1">sets <see cref="Lid1"/></param>
        /// <param name="lid2">sets <see cref="Lid2"/></param>
        private void init(string lid1, string lid2)
        {
    
    ki7077's avatar
    ki7077 committed
            
    
            this.Lid1 = lid1;
            this.Lid2 = lid2;
    
            RayFact lf1 = _Facts[lid1] as RayFact;
            RayFact lf2 = _Facts[lid2] as RayFact;
    
            MMTDeclaration mmtDecl;
            string l1URI = lf1.Id;
            string l2URI = lf2.Id;
            mmtDecl = generateParallelLineDeclaration( l1URI, l2URI);
        
            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="Lid1">sets <see cref="Lid1"/></param>
        /// <param name="Lid2">sets <see cref="Lid2"/></param>
        /// <param name="backendURI">MMT URI</param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public ParallelLineFact(string Lid1, string Lid2, string backendURI, FactOrganizer organizer) : base(organizer)
        {
            this.Lid1 = Lid1;
            this.Lid2 = Lid2;
    
            this._URI = backendURI;
            _ = this.Label;
        }
    
        /// \copydoc Fact.parseFact(Scroll.ScrollFact)
        public new static ParallelLineFact parseFact(Scroll.ScrollFact fact)
        {
            OMA tp = (OMA)((Scroll.ScrollSymbolFact)fact).tp;
            if (tp == null)
                return null;
    
            string lineAUri = "";
            string lineBUri = "";
    
            string uri = fact.@ref.uri;
            OMA proof_OMA = (OMA)((Scroll.ScrollSymbolFact)fact).tp; // proof DED
       
    
            OMA parallel_lines_OMA = (OMA) proof_OMA.arguments[0]; // parallel
    
            if (parallel_lines_OMA.arguments[0] is OMS) {
                // Normaler Fall 
                lineAUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0]).uri;
                lineBUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).uri;
    
            }
            // Second case might be redundant by now
            else {
                OMA Projl_line_A_OMA = (OMA)parallel_lines_OMA.arguments[0]; // ProjectL
                lineAUri = ((OMS)Projl_line_A_OMA.arguments[0]).uri;
                OMA Projl_line_B_OMA = (OMA)parallel_lines_OMA.arguments[1]; // ProjectL
                lineBUri = ((OMS)Projl_line_B_OMA.arguments[0]).uri;
    
    
            }
    
    
            if (StageStatic.stage.factState.ContainsKey(lineAUri)
             && StageStatic.stage.factState.ContainsKey(lineBUri))
    
                return new ParallelLineFact(lineAUri,lineBUri, uri, StageStatic.stage.factState);
    
            else    //If dependent facts do not exist return null
                return null;
        }
    
        /// \copydoc Fact.generateLabel
        protected override string generateLabel()
        {
            return "||" + _Facts[Lid1].Label + _Facts[Lid2].Label;
        }
    
    
    
        /// <summary>
        /// Constructs struct for right-angled MMT %Fact <see cref="AddFactResponse"/>
        /// </summary>
        /// <param name="l1URI"><see cref="Lid1"/></param>
        /// <param name="l2URI"><see cref="Lid2"/></param>
        /// <returns>struct for <see cref="AddFactResponse"/></returns>
        private MMTDeclaration generateParallelLineDeclaration(string l1URI, string l2URI)
        {
            
            List<MMTTerm> innerArguments = new List<MMTTerm>
            {
                new OMS(l1URI),
                new OMS(l2URI)
            };
    
            List<MMTTerm> outerArguments = new List<MMTTerm>
            {
                new OMA(new OMS(MMTURIs.ParallelLine), innerArguments)
            };
    
            //OMS constructor generates full URI
            MMTTerm tp = new OMA(new OMS(MMTURIs.Ded), outerArguments);
            MMTTerm df = null;
    
            MMTSymbolDeclaration mmtDecl = new MMTSymbolDeclaration(this.Label, tp, df);
            AddFactResponse.sendAdd(mmtDecl, out this._URI);
    
    
            return mmtDecl;
        }
    
    
        /// \copydoc Fact.hasDependentFacts
        public override Boolean hasDependentFacts()
        {
            return true;
        }
    
        /// \copydoc Fact.getDependentFactIds
        public override string[] getDependentFactIds()
        {
            return new string[] { Lid1, Lid2 };
        }
    
        /// \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.Lid1].Label;
            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 this.Lid1.GetHashCode() ^ this.Lid2.GetHashCode() ;
        }
    
        /// \copydoc Fact.Equivalent(Fact, Fact)
        protected override bool EquivalentWrapped(ParallelLineFact f1, ParallelLineFact f2)
        {
            if ((f1.Lid1 == f2.Lid1 && f1.Lid2 == f2.Lid2))
                return true;
    
            RayFact r1f1 = (RayFact)_Facts[f1.Lid1];
            RayFact r2f1 = (RayFact)_Facts[f1.Lid2];
            RayFact r1f2 = (RayFact)_Facts[f2.Lid1];
            RayFact r2f2 = (RayFact)_Facts[f2.Lid2];
    
            return (r1f1.Equivalent(r1f2) && r2f1.Equivalent(r2f2)) ;
        }
    }
    
    /// <summary>
    /// A Circle that is made out of a middle point, a plane and a radius  
    /// </summary>
    public class CircleFact : FactWrappedCRTP<CircleFact>
    {
    
    MaZiFAU's avatar
    MaZiFAU committed
        /// \copydoc Fact.s_type
        [JsonProperty]
        protected static new string s_type = "CircleFact";
    
    
        /// <summary> defining the middle point of the circle  </summary>
        public string Pid1;
        /// <summary>  defining the base point of the circle plane </summary>
        public string Pid2;
        /// <summary>  radius of the circle </summary>
        public float radius;
        /// <summary> normal vector of the plane </summary>
        public Vector3 normal;
       
        /// <summary> \copydoc Fact.Fact </summary>
        public CircleFact() : base()
        {
            this.normal = Vector3.zero;
            this.Pid1 = null;
            this.Pid2 = null;
            this.radius = 0;
        }
    
        /// <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 CircleFact(CircleFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
        {
            init(old_to_new[fact.Pid1], old_to_new[fact.Pid2], fact.radius, fact.normal);
    
    
        /// <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 CircleFact(string pid1, string pid2, float radius, Vector3 normal, FactOrganizer organizer) : base(organizer)
        {
            init(pid1, pid2, radius, normal);
        }
    
        /// <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(string pid1, string pid2, float radius, Vector3 normal)
        {
            this.Pid1 = pid1;
            this.Pid2 = pid2;
    
            PointFact pf1 = _Facts[pid1] as PointFact;
            PointFact pf2 = _Facts[pid2] as PointFact;
    
    
            this.radius = radius;
            this.normal = normal;
    
            MMTDeclaration mmtDecl;
            string p1URI = pf1.Id;
            string p2URI = pf2.Id;
    
            mmtDecl = generateCircleFactDeclaration(p1URI, p2URI, radius, normal);
    
            AddFactResponse.sendAdd(mmtDecl, out this._URI);
        }
    
        /// <summary>
        /// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
        /// </summary>
        /// <param name="Pid1">sets <see cref="Pid1"/></param>
        /// <param name="Pid2">sets <see cref="Pid2"/></param>
        /// <param name="radius">sets <see cref="radius"/></param>
        /// <param name="normal">sets <see cref="normal"/></param>
        /// <param name="backendURI">MMT URI</param>
        /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
        public CircleFact(string Pid1, string Pid2, float radius, Vector3 normal, string backendURI, FactOrganizer organizer) : base(organizer)
        {
            this.Pid1 = Pid1;
            this.Pid2 = Pid2;
    
            this.radius = radius;
            this.normal = normal;
     
            this._URI = backendURI;
            _ = this.Label;
        }
    
        /// <summary>
        /// parses the Circlefact response of the MMT-Server
        /// </summary>
        /// \copydoc Fact.parseFact(Scroll.ScrollFact) 
        public new static CircleFact parseFact(Scroll.ScrollFact fact)
        {
            string uri = fact.@ref.uri;
    
    Marcel Dreier's avatar
    Marcel Dreier committed
            string M_uri = "";
            string A_uri = "";
            float radius = 0.0f;
            Vector3 normal = Vector3.zero;
    
            OMA df = (OMA)((Scroll.ScrollSymbolFact)fact).df;
    
            if (df == null)
                return null;
    
            Scroll.ScrollSymbolFact casted_fact = (Scroll.ScrollSymbolFact)fact;
    
    
    
            // get the mid point uri
            string parse_id_M = ParsingDictionary.MMTermToString(((OMA)casted_fact.df).arguments[1]);
    
    
    Marcel Dreier's avatar
    Marcel Dreier committed
            M_uri = ParsingDictionary.parseTermsToId[parse_id_M];
    
    Marcel Dreier's avatar
    Marcel Dreier committed
            radius = ((OMF)((OMA)casted_fact.df).arguments[2]).f;
    
            OMA planeOMA = (OMA)((OMA)casted_fact.df).arguments[0];
            string planeApplicant = ((OMS)planeOMA.applicant).uri;
    
    
            // Getting the plane
            // IN case of a normale plane
            if (planeApplicant.Equals(MMTURIs.pointNormalPlane))
            {
    
    Marcel Dreier's avatar
    Marcel Dreier committed
    
                OMA pointAOMA = (OMA)planeOMA.arguments[0];
    
                string parse_id_A = ParsingDictionary.MMTermToString(planeOMA.arguments[0]);
                A_uri = ParsingDictionary.parseTermsToId[parse_id_A];
    
                OMA n = (OMA)planeOMA.arguments[1];
                normal = new Vector3(((OMF)n.arguments[0]).f, ((OMF)n.arguments[1]).f, ((OMF)n.arguments[2]).f);
    
    Marcel Dreier's avatar
    Marcel Dreier committed
    
    
            }
            // In case of parametrized plane
            else if(planeApplicant.Equals(MMTURIs.ParametrizedPlane))
            {
    
    Marcel Dreier's avatar
    Marcel Dreier committed
    
                OMA pointAOMA = (OMA)planeOMA.arguments[0];
                string parse_id_A = ParsingDictionary.MMTermToString(planeOMA.arguments[0]);
                A_uri = ParsingDictionary.parseTermsToId[parse_id_A];
    
    
                OMA vOMA = (OMA)planeOMA.arguments[1];
                OMA wOMA = (OMA)planeOMA.arguments[2];
    
                Vector3 v = new Vector3(((OMF)vOMA.arguments[0]).f, ((OMF)vOMA.arguments[1]).f, ((OMF)vOMA.arguments[2]).f);
                Vector3 w = new Vector3(((OMF)wOMA.arguments[0]).f, ((OMF)wOMA.arguments[1]).f, ((OMF)wOMA.arguments[2]).f);
    
                normal = Vector3.Cross(v, w).normalized;
    
    
    Marcel Dreier's avatar
    Marcel Dreier committed
    
            }