Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
using Newtonsoft.Json;
using System;
using System.Collections.Generic;
using static SOMDocManager;
using TMPro;
using UnityEngine;
using UnityEngine.UIElements;
public abstract class AbstractAngleFact : FactWrappedCRTP<AbstractAngleFact>
{
/// @{ <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;
/// @}
[JsonIgnore]
public PointFact Point1 { get => (PointFact)FactOrganizer.AllFacts[Pid1]; }
[JsonIgnore]
public PointFact Point2 { get => (PointFact)FactOrganizer.AllFacts[Pid2]; }
[JsonIgnore]
public PointFact Point3 { get => (PointFact)FactOrganizer.AllFacts[Pid3]; }
/// <summary> <see langword="true"/>, if AngleFact is approximately 90° or 270°</summary>
virtual public bool is_right_angle { get; set; } = false;
/// <summary>
/// Smallets angle in Degrees between [< see cref = "Pid1" />, < see cref = "Pid2" />] and[< see cref = "Pid2" />, < see cref = "Pid3" />]
/// </summary>
[JsonIgnore]
virtual public float angle { get; set; } = -0f;
/// <summary>\copydoc Fact.Fact</summary>
protected AbstractAngleFact() : base()
{
this.Pid1 = null;
this.Pid2 = null;
this.Pid3 = null;
}
/// <summary>\copydoc AbstractAngleFact.AbstractAngleFact(AbstractAngleFact, Dictionary{string, string}, FactOrganizer)</summary>
protected AbstractAngleFact(AbstractAngleFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer)
: this(old_to_new[fact.Pid1], old_to_new[fact.Pid2], old_to_new[fact.Pid3], organizer) { }
/// <summary>\copydoc AbstractAngleFact.AbstractAngleFact(string, string, FactOrganizer)</summary>
protected AbstractAngleFact(string pid1, string pid2, string pid3, FactOrganizer organizer) : base(organizer)
{
this.Pid1 = pid1;
this.Pid2 = pid2;
this.Pid3 = pid3;
}
/// <summary>\copydoc AbstractAngleFact.AbstractAngleFact(string, string, string, FactOrganizer)</summary>
protected AbstractAngleFact(string pid1, string pid2, string pid3, float angle, string backendURI, FactOrganizer organizer)
: this(pid1, pid2, pid3, organizer)
{
this.angle = angle;
this._URI = backendURI;
}
/// \copydoc Fact.hasDependentFacts
MaZiFAU
committed
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> new string[] { Pid1, Pid2, Pid3 };
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
{
Position = Point2.Position;
{ //Rotation
Vector3 from = (Point1.Position - Position).normalized;
Vector3 to = (Point3.Position - Position).normalized;
Vector3 up = Vector3.Cross(from, to);
Vector3 forwoard = (from + to).normalized;
if (up.sqrMagnitude < Math3d.vectorPrecission)
{ //Angle is 180° (or 0°)
Vector3 from_arbitary = from.normalized == Vector3.forward ? Vector3.right : Vector3.forward;
up = Vector3.Cross(from_arbitary, to);
forwoard = Vector3.Cross(up, to);
}
Rotation = Quaternion.LookRotation(forwoard, up);
}
}
}
public abstract class AbstractAngleFactWrappedCRTP<T> : AbstractAngleFact where T : AbstractAngleFactWrappedCRTP<T>
{
/// <summary>\copydoc Fact.Fact</summary>
protected AbstractAngleFactWrappedCRTP() : base() { }
/// <summary>\copydoc AbstractAngleFactWrappedCRTP.AbstractAngleFactWrappedCRTP(AbstractAngleFactWrappedCRTP, Dictionary{string, string}, FactOrganizer)</summary>
protected AbstractAngleFactWrappedCRTP(AbstractAngleFactWrappedCRTP<T> fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, old_to_new, organizer) { }
/// <summary>\copydoc AbstractAngleFactWrappedCRTP.AbstractAngleFactWrappedCRTP(string, string, FactOrganizer)</summary>
protected AbstractAngleFactWrappedCRTP(string pid1, string pid2, string pid3, FactOrganizer organizer) : base(pid1, pid2, pid3, organizer) { }
/// <summary>\copydoc AbstractAngleFactWrappedCRTP.AbstractAngleFactWrappedCRTP(string, string, string, FactOrganizer)</summary>
protected AbstractAngleFactWrappedCRTP(string pid1, string pid2, string pid3, float angle, string backendURI, FactOrganizer organizer) : base(pid1, pid2, pid3, angle, backendURI, organizer) { }
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(AbstractAngleFact f1, AbstractAngleFact f2)
=> EquivalentWrapped((T)f1, (T)f2);
/// <summary>CRTP step of <see cref="EquivalentWrapped(AbstractAngleFact, AbstractAngleFact)"/></summary>
protected abstract bool EquivalentWrapped(T f1, T f2);
}
/// <summary>
/// Angle comprised of three <see cref="PointFact">PointFacts</see> [A,B,C]
/// </summary>
public class AngleFact : AbstractAngleFactWrappedCRTP<AngleFact>
{
/// <summary> \copydoc Fact.Fact </summary>
public AngleFact() : base() { }
/// <summary>
/// Standard Constructor:
/// 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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public AngleFact(string pid1, string pid2, string pid3, FactOrganizer organizer) : base(pid1, pid2, pid3, organizer)
{
angle = Vector3.Angle((Point1.Point - Point2.Point), (Point3.Point - Point2.Point));
this.is_right_angle = Mathf.Approximately(angle, 90.0f);
angle = is_right_angle ? 90f : angle;
}
/// <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, float angle, string backendURI, FactOrganizer organizer)
: base(Pid1, Pid2, Pid3, angle, backendURI, organizer) { }
public override MMTDeclaration MakeMMTDeclaration()
{
SOMDoc lhs =
new OMA(
new OMS(MMT_OMS_URI.Angle),
new List<SOMDoc> {
new OMS(Pid1),
new OMS(Pid2),
new OMS(Pid3)
}
);
SOMDoc valueTp = new OMS(MMT_OMS_URI.RealLit);
return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static AngleFact parseFact(MMTDeclaration fact)
if (fact is not MMTValueDeclaration value_fact) //If angle is a 90Degree-Angle
throw new ArgumentException("Angle 90 degrees parsed. This shouldn't happen anymore");
return null;
float angle = value_fact.value == null
? 0f
string pointAUri = ((OMS)lhs.arguments[0]).uri;
string pointBUri = ((OMS)lhs.arguments[1]).uri;
string pointCUri = ((OMS)lhs.arguments[2]).uri;
if (!FactOrganizer.AllFacts.ContainsKey(pointAUri)
|| !FactOrganizer.AllFacts.ContainsKey(pointBUri)
|| !FactOrganizer.AllFacts.ContainsKey(pointCUri))
return null;
return new AngleFact(pointAUri, pointBUri, pointCUri, angle, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> (is_right_angle ? "⊾" : "∠") + Point1.Label + Point2.Label + Point3.Label;
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(AngleFact f1, AngleFact f2)
=> DependentFactsEquivalent(f1, f2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
=> new AngleFact(old_to_new[this.Pid1], old_to_new[this.Pid2], old_to_new[this.Pid3], organizer);
}
/// <summary>
/// A RightAngleFact defined by 3 <see cref="PointFact">Pointfact</see>
/// </summary>
public class RightAngleFact : AbstractAngleFactWrappedCRTP<RightAngleFact>
{
override public bool is_right_angle { get => true; }
override public float angle {get => 90f;}
/// <summary> \copydoc Fact.Fact </summary>
public RightAngleFact() : base() { }
/// <summary>
/// Standard Constructor:
/// 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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public RightAngleFact(string pid1, string pid2, string pid3, FactOrganizer organizer) : base(pid1, pid2, pid3, organizer)
{
angle = 90f;
}
/// <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(Pid1, Pid2, Pid3, 90f, backendURI, organizer) { }
public override MMTDeclaration MakeMMTDeclaration()
{
SOMDoc tp =
new OMA(
new OMS(MMT_OMS_URI.Ded),
new List<SOMDoc> {
new OMA(
new OMS(MMT_OMS_URI.RightAngle),
new List<SOMDoc> {
new OMS(Pid1),
new OMS(Pid2),
new OMS(Pid3),
}),});
SOMDoc df = null;
return new MMTSymbolDeclaration(this.Label, tp, df);
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static RightAngleFact parseFact(MMTDeclaration fact)
is not OMA proof_OMA // proof DED
|| proof_OMA.arguments[0]
is not OMA rightAngleOMA // rightAngle OMA
|| rightAngleOMA.arguments[0]
is not OMS // rightAngle Arg0
)
return null;
string Point1Uri = ((OMS)rightAngleOMA.arguments[0]).uri;
string Point2Uri = ((OMS)rightAngleOMA.arguments[1]).uri;
string Point3Uri = ((OMS)rightAngleOMA.arguments[2]).uri;
if (!FactOrganizer.AllFacts.ContainsKey(Point1Uri)
|| !FactOrganizer.AllFacts.ContainsKey(Point2Uri)
|| !FactOrganizer.AllFacts.ContainsKey(Point3Uri))
return null;
return new RightAngleFact(Point1Uri, Point2Uri, Point3Uri, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> Point1.Label + Point2.Label + Point3.Label + "⊥";
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(RightAngleFact f1, RightAngleFact f2)
=> DependentFactsEquivalent(f1, f2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
=> new RightAngleFact(old_to_new[this.Pid1], old_to_new[this.Pid2], old_to_new[this.Pid3], organizer);