Newer
Older
using System;
using System.Collections.Generic;
using UnityEngine;
using Newtonsoft.Json;
using REST_JSON_API;
using System.Xml.Linq;
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
/// <summary>
/// A Circle that is made out of a middle point, a plane and a radius
/// </summary>
public class CircleFact : FactWrappedCRTP<CircleFact>
{
/// <summary> defining the middle point of the circle </summary>
public string PidCenter;
/// <summary> defining the base point of the circle plane </summary>
public string PidBase;
[JsonIgnore]
public PointFact PointCenter { get => (PointFact)FactRecorder.AllFacts[PidCenter]; }
[JsonIgnore]
public PointFact PointBase { get => (PointFact)FactRecorder.AllFacts[PidBase]; }
/// <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.PidCenter = null;
this.PidBase = null;
this.radius = 0;
}
/// <summary>
/// Standard Constructor:
/// Initiates <see cref="PidCenter"/>, <see cref="PidBase"/>, <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="PidCenter"/></param>
/// <param name="pid2">sets <see cref="PidBase"/></param>
/// <param name="radius">sets <see cref="radius"/></param>
/// <param name="normal">sets <see cref="normal"/></param>
public CircleFact(string pid1, string pid2, float radius, Vector3 normal) : base()
{
this.PidCenter = pid1;
this.PidBase = pid2;
this.radius = radius;
this.normal = normal;
}
protected override void RecalculateTransform()
{
Position = PointCenter.Position;
{ //Rotation
Vector3 arbitary_not_normal = normal == Vector3.forward ? Vector3.right : Vector3.forward;
Vector3 forwoard = Vector3.Cross(arbitary_not_normal, normal);
Rotation = Quaternion.LookRotation(forwoard, normal);
}
LocalScale = new Vector3(radius, 1, radius);
}
/// <summary>
/// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
/// </summary>
/// <param name="Pid1">sets <see cref="PidCenter"/></param>
/// <param name="Pid2">sets <see cref="PidBase"/></param>
/// <param name="radius">sets <see cref="radius"/></param>
/// <param name="normal">sets <see cref="normal"/></param>
/// <param name="backendURI">MMT URI</param>
public CircleFact(string Pid1, string Pid2, float radius, Vector3 normal, SOMDoc _ServerDefinition) : base()
{
this.PidCenter = Pid1;
this.PidBase = Pid2;
this.radius = radius;
this.normal = normal;
this.ServerDefinition = _ServerDefinition;
}
/// <summary>
/// parses the Circlefact response of the MMT-Server
/// </summary>
/// \copydoc Fact.parseFact(ScrollFact)
public new static IEnumerator parseFact(List<Fact> ret, MMTFact fact)
{
if (((MMTGeneralFact)fact).defines is not OMA df)
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
OMA planeOMA = (OMA)df.arguments[0];
string planeApplicant = ((OMS)planeOMA.applicant).uri;
Vector3 normal;
// Getting the plane
// IN case of a normale plane
if (planeApplicant.Equals(MMTConstants.pointNormalPlane))
{
//OMA pointAOMA = (OMA)planeOMA.arguments[0];
normal = SOMDoc.MakeVector3((OMA)planeOMA.arguments[1]);
}
// In case of parametrized plane
else if (planeApplicant.Equals(MMTConstants.ParametrizedPlane))
{
Vector3 v = SOMDoc.MakeVector3((OMA)planeOMA.arguments[1]);
Vector3 w = SOMDoc.MakeVector3((OMA)planeOMA.arguments[2]);
normal = Vector3.Cross(v, w).normalized;
}
// incase of smth else. Shouldn't hapepen unless there is an error
else throw new ArgumentException("Invalid planeApplicant: " + planeApplicant);
// get the mid point uri
string parse_id_M = df.arguments[1].ToString();
string M_uri = ParsingDictionary.parseTermsToId[parse_id_M];
string A_uri = ParsingDictionary.parseTermsToId[planeOMA.arguments[0].ToString()];
if (!FactRecorder.AllFacts.ContainsKey(M_uri)
|| !FactRecorder.AllFacts.ContainsKey(A_uri))
yield break; //If dependent facts do not exist return null
ret.Add(new CircleFact(M_uri, A_uri, radius, normal, fact.@ref));
}
/// \copydoc Fact.generateLabel
protected override string generateLabel(FactRecorder name_space)
=> "○" + PointCenter.GetLabel(name_space);
/// <summary>
/// Constructs struct for right-angled MMT %Fact <see cref="AddFactResponse"/>
/// </summary>
/// <param name="Pid1"> <see cref="PidCenter"/></param>
/// <param name="p2URI"> <see cref="PidBase"/></param>
/// <param name="radius"> <see cref="radius"/></param>
/// <returns>struct for <see cref="AddFactResponse"/></returns>
public override MMTFact MakeMMTDeclaration()
{
SOMDoc tp = new OMS(MMTConstants.CircleType3d);
return new MMTGeneralFact(_LastLabel, tp, Defines());
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
public override SOMDoc Defines()
=> new OMA(
new OMS(MMTConstants.MkCircle3d),
new SOMDoc[] {
//CirclePlane,
new OMA(
//PointNormalPlane,
new OMS(MMTConstants.pointNormalPlane),
//planeArgs,
new SOMDoc[] {
//base point of the circle plane?,
new OMS(PidBase),
//NormalVector,
new OMA(
//"Vector"
new OMS(MMTConstants.Tuple),
//normalArgs,
new[] {
new OMLIT<float>(normal.x),
new OMLIT<float>(normal.y),
new OMLIT<float>(normal.z)
}
),
}
),
//middlePoint,
new OMS(PidCenter),
//Radius,
new OMLIT<float>(radius),
}
);
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetDependentFactIds()
=> new string[] { PidCenter, PidBase };
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(CircleFact f1, CircleFact f2)
=> DependentFactsEquivalent(f1, f2)
&& Math3d.IsApproximatelyEqual(f1.normal, f2.normal)
&& Mathf.Approximately(f1.radius, f2.radius);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new)
=> new CircleFact(old_to_new[this.PidCenter], old_to_new[this.PidBase], this.radius, this.normal);
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
}
/// <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>
{
/// <summary> The circle corresponding to the radius </summary>
public string Cid1;
[JsonIgnore]
public CircleFact Circle { get => (CircleFact)FactRecorder.AllFacts[Cid1]; }
/// <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>
/// Standard Constructor:
/// Initiates <see cref="Cid1"/> and <see cref="rad"/>
/// </summary>
/// <param name="cid1">sets <see cref="Cid1"/></param>
public RadiusFact(string cid1) : base()
{
this.Cid1 = cid1;
this.rad = Circle.radius;
}
protected override void RecalculateTransform()
{
Position = Circle.Position;
Rotation = Circle.Rotation;
}
/// <summary>
/// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
/// </summary>
/// <param name="Cid1">sets <see cref="Cid1"/></param>
/// <param name="backendURI">MMT URI</param>
public RadiusFact(string Cid1, SOMDoc _ServerDefinition) : base()
{
this.Cid1 = Cid1;
this.ServerDefinition = _ServerDefinition;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static IEnumerator parseFact(List<Fact> ret, MMTFact fact)
{
string CircleUri = ((OMS)((OMA)((MMTValueFact)fact).lhs).arguments[0]).uri;
if (!FactRecorder.AllFacts.ContainsKey(CircleUri))
ret.Add(new RadiusFact(CircleUri, fact.@ref));
}
/// \copydoc Fact.generateLabel
protected override string generateLabel(FactRecorder name_space)
=> "r " + Circle.GetLabel(name_space);
/// <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>
public override MMTFact MakeMMTDeclaration()
{
SOMDoc valueTp = new OMS(MMTConstants.RealLit);
return new MMTValueFact(_LastLabel, Defines(), valueTp, value);
public override SOMDoc Defines()
=> new OMA(
new OMS(MMTConstants.RadiusCircleMetric),
new[] {
new OMS(Cid1),
}
);
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetDependentFactIds()
=> new string[] { Cid1 };
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(RadiusFact f1, RadiusFact f2)
=> DependentFactsEquivalent(f1, f2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new)
=> new RadiusFact(old_to_new[this.Cid1]);
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
}
/// <summary>
/// Area of a <see cref="CircleFact">CircleFact</see>
/// </summary>
public class AreaCircleFact : FactWrappedCRTP<AreaCircleFact>
{
/// <summary> the circle <see cref="CircleFact">CircleFact</see> </summary>
public string Cid1;
[JsonIgnore]
public CircleFact Circle { get => (CircleFact)FactRecorder.AllFacts[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>
/// Standard Constructor:
/// Initiates <see cref="Cid1"/> and creates MMT %Fact Server-Side
/// </summary>
/// <param name="cid1">sets <see cref="Cid1"/></param>
public AreaCircleFact(string cid1) : base()
{
this.Cid1 = cid1;
}
protected override void RecalculateTransform()
{
Position = Circle.Position;
Rotation = Circle.Rotation;
}
/// <summary>
/// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
/// </summary>
/// <param name="Cid1">sets <see cref="Cid1"/></param>
/// <param name="backendURI">MMT URI</param>
public AreaCircleFact(string Cid1, SOMDoc _ServerDefinition) : base()
{
this.Cid1 = Cid1;
this.ServerDefinition = _ServerDefinition;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static IEnumerator parseFact(List<Fact> ret, MMTFact fact)
{
string CircleUri = ((OMS)((OMA)((MMTValueFact)fact).lhs).arguments[0]).uri;
if (!FactRecorder.AllFacts.ContainsKey(CircleUri))
ret.Add(new AreaCircleFact(CircleUri, fact.@ref));
}
/// \copydoc Fact.generateLabel
protected override string generateLabel(FactRecorder name_space)
=> "A(" + Circle.GetLabel(name_space) + ")";
public override MMTFact MakeMMTDeclaration()
{
SOMDoc valueTp = new OMS(MMTConstants.RealLit);
return new MMTValueFact(_LastLabel, Defines(), valueTp, value);
public override SOMDoc Defines()
=> new OMA(
new OMS(MMTConstants.AreaCircle),
new[] {
new OMS(Cid1),
}
);
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetDependentFactIds()
=> new string[] { Cid1 };
/// \copydoc Fact.GetHashCode
public override int GetHashCode()
=> base.GetHashCode() ^ A.GetHashCode();
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(AreaCircleFact f1, AreaCircleFact f2)
=> DependentFactsEquivalent(f1, f2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new)
=> new AreaCircleFact(old_to_new[this.Cid1]);
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
}
/// <summary>
/// A <see cref="PointFact"/> on a <see cref="CircleFact"/>
/// </summary>
public class OnCircleFact : FactWrappedCRTP<OnCircleFact>
{
/// <summary> the point on the circle </summary>
public string Pid;
/// <summary> the circle, which the point is on </summary>
public string Cid;
[JsonIgnore]
public PointFact Point { get => (PointFact)FactRecorder.AllFacts[Pid]; }
[JsonIgnore]
public CircleFact Circle { get => (CircleFact)FactRecorder.AllFacts[Cid]; }
/// <summary> \copydoc Fact.Fact </summary>
public OnCircleFact() : base()
{
this.Pid = null;
this.Cid = null;
}
/// <summary>
/// Standard Constructor:
/// 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>
public OnCircleFact(string pid, string cid) : base()
{
this.Pid = pid;
}
protected override void RecalculateTransform()
{
Position = Point.Position;
Rotation = Circle.Rotation;
}
/// <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>
public OnCircleFact(string pid, string cid, SOMDoc _ServerDefinition) : base()
{
this.Pid = pid;
this.Cid = cid;
this.ServerDefinition = _ServerDefinition;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static IEnumerator parseFact(List<Fact> ret, MMTFact fact)
{
if (((MMTGeneralFact)fact).type is not OMA type)
string circleUri = ((OMS)((OMA)type.arguments[0]).arguments[0]).uri;
string pointUri = ((OMS)((OMA)type.arguments[0]).arguments[1]).uri;
if (!FactRecorder.AllFacts.ContainsKey(pointUri)
|| !FactRecorder.AllFacts.ContainsKey(circleUri))
ret.Add(new OnCircleFact(pointUri, circleUri, fact.@ref));
}
/// \copydoc Fact.generateLabel
protected override string generateLabel(FactRecorder name_space)
=> Point.GetLabel(name_space) + "∈" + Circle.GetLabel(name_space);
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetDependentFactIds()
=> new string[] { Pid, Cid };
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(OnCircleFact c1, OnCircleFact c2)
=> DependentFactsEquivalent(c1, c2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new)
=> new OnCircleFact(old_to_new[this.Pid], old_to_new[this.Cid]);
public override MMTFact MakeMMTDeclaration()
{
SOMDoc tp =
new OMA(
new OMS(MMTConstants.Ded),
new[] {
new OMA(
new OMS(MMTConstants.OnCircle),
new[] {
new OMS(Cid),
new OMS(Pid),
}),});
return new MMTGeneralFact(_LastLabel, tp, Defines());
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
}
/// <summary>
/// Angle comprised of a line and a circle
/// </summary>
public class AngleCircleLineFact : FactWrappedCRTP<AngleCircleLineFact>
{
/// @{ <summary>
/// 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;
/// @}
[JsonIgnore]
public AbstractLineFact Ray { get => (AbstractLineFact)FactRecorder.AllFacts[Rid2]; }
[JsonIgnore]
public CircleFact Circle { get => (CircleFact)FactRecorder.AllFacts[Cid1]; }
//TODO? deg or rad?
[JsonIgnore]
public float angle;
[JsonIgnore]
public Vector3 intersection;
/// <summary> \copydoc Fact.Fact </summary>
public AngleCircleLineFact() : base()
{
this.Cid1 = null;
this.Rid2 = null;
this.angle = 0.0f;
}
/// <summary>
/// Standard Constructor:
/// Initiates <see cref="Cid1"/>, <see cref="Rid2"/>, <see cref="angle"/> <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
/// </summary>
/// <param name="cid1">sets <see cref="Cid1"/></param>
/// <param name="rid2">sets <see cref="Rid2"/></param>
/// <param name="angle"> sets the angle </param>
public AngleCircleLineFact(string cid1, string rid2) : base()
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
{
this.Cid1 = cid1;
this.Rid2 = rid2;
this.angle = Math3d.AngleVectorPlane(Ray.Dir, Circle.normal).ToDegrees();
Math3d.LinePlaneIntersection(out intersection, Ray.Point1.Position, Ray.Dir, Circle.normal, Circle.Position);
}
protected override void RecalculateTransform()
{
Position = intersection;
{ //Rotation
Vector3 from = (Circle.Position - Position).normalized;
Vector3 angle_to = Math3d.IsApproximatelyEqual(intersection, Ray.Point1.Position)
? Ray.Point2.Position
: Ray.Point1.Position;
Vector3 to = (angle_to - Position).normalized;
Vector3 up = Vector3.Cross(to, from);
Vector3 forwoard = (from + to).normalized;
if (up.sqrMagnitude < Math3d.vectorPrecission)
{ //Angle is 180° (or 0°)
Vector3 arbitary = up.normalized == Vector3.forward ? Vector3.right : Vector3.forward;
up = Vector3.Cross(arbitary, to);
forwoard = Vector3.Cross(up, to);
}
Rotation = Quaternion.LookRotation(forwoard, up);
}
}
/// <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>
public AngleCircleLineFact(string Cid1, string Rid2, float angle, SOMDoc _ServerDefinition) : base()
{
this.Cid1 = Cid1;
this.Rid2 = Rid2;
this.angle = angle;
this.ServerDefinition = _ServerDefinition;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static IEnumerator parseFact(List<Fact> ret, MMTFact fact)
{
if (((MMTValueFact)fact).lhs is not OMA lhs)
// 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 (((MMTValueFact)fact).value is OMLIT<float> oMFangle)
angle = oMFangle.value;
string CircleUri = ((OMS)lhs.arguments[0]).uri;
string RayUri = ((OMS)lhs.arguments[1]).uri;
if (!FactRecorder.AllFacts.ContainsKey(CircleUri)
|| !FactRecorder.AllFacts.ContainsKey(RayUri))
ret.Add(new AngleCircleLineFact(CircleUri, RayUri, angle, fact.@ref));
}
/// \copydoc Fact.generateLabel
protected override string generateLabel(FactRecorder name_space)
=> "∠" + Circle.GetLabel(name_space) + Ray.GetLabel(name_space);
public override MMTFact MakeMMTDeclaration()
{
SOMDoc valueTp = new OMS(MMTConstants.RealLit);
SOMDoc value = new OMLIT<float>(angle);
return new MMTValueFact(_LastLabel, Defines(), valueTp, value);
}
public override SOMDoc Defines()
=> new OMA(
new OMS(MMTConstants.AnglePlaneLine),
new[] {
new OMS(Cid1),
new OMS(Rid2),
}
);
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetDependentFactIds()
=> new string[] { Cid1, Rid2 };
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(AngleCircleLineFact f1, AngleCircleLineFact f2)
=> DependentFactsEquivalent(f1, f2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new)
=> new AngleCircleLineFact(old_to_new[this.Cid1], old_to_new[this.Rid2]);
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
}
/// <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>
{
/// <summary> a <see cref="CircleFact">CircleFact</see> describing the base area </summary>
public string Cid1;
[JsonIgnore]
public CircleFact Circle { get => (CircleFact)FactRecorder.AllFacts[Cid1]; }
/// <summary> a <see cref="RayFact">Rayfact</see> describing the line </summary>
public string Lid1;
[JsonIgnore]
public AbstractLineFact Ray { get => (AbstractLineFact)FactRecorder.AllFacts[Lid1]; }
//TODO? deg or rad?
[JsonIgnore]
public float angle = 90f;
[JsonIgnore]
public Vector3 intersection;
/// <summary> \copydoc Fact.Fact </summary>
public OrthogonalCircleLineFact() : base()
{
this.Cid1 = null;
this.Lid1 = null;
}
/// <summary>
/// Standard Constructor:
/// Initiates members and creates MMT %Fact Server-Side
/// </summary>
/// <param name="cid1">sets <see cref="Cid1"/></param>
/// <param name="lid1">sets <see cref="Lid1"/></param>
public OrthogonalCircleLineFact(string cid1, string lid1) : base()
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
{
this.Cid1 = cid1;
this.Lid1 = lid1;
Math3d.LinePlaneIntersection(out intersection, Ray.Point1.Position, Ray.Dir, Circle.normal, Circle.Position);
}
protected override void RecalculateTransform()
{
Position = intersection;
{ //Rotation
Vector3 from = (Circle.Position - Position).normalized;
Vector3 angle_to = Math3d.IsApproximatelyEqual(intersection, Ray.Point1.Position)
? Ray.Point2.Position
: Ray.Point1.Position;
Vector3 to = (angle_to - Position).normalized;
Vector3 up = Vector3.Cross(to, from);
Vector3 forward = (from + to).normalized;
Rotation = Quaternion.LookRotation(forward, up);
}
}
/// <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>
public OrthogonalCircleLineFact(string Cid1, string Lid1, SOMDoc _ServerDefinition) : base()
{
this.Cid1 = Cid1;
this.Lid1 = Lid1;
this.ServerDefinition = _ServerDefinition;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static IEnumerator parseFact(List<Fact> ret, MMTFact fact)
{
if (((MMTGeneralFact)fact).type is not OMA type)
string CircleUri = ((OMS)((OMA)type.arguments[0]).arguments[0]).uri;
string LineUri = ((OMS)((OMA)type.arguments[0]).arguments[1]).uri;
if (!FactRecorder.AllFacts.ContainsKey(CircleUri)
|| !FactRecorder.AllFacts.ContainsKey(LineUri))
ret.Add(new OrthogonalCircleLineFact(CircleUri, LineUri, fact.@ref));
}
/// \copydoc Fact.generateLabel
protected override string generateLabel(FactRecorder name_space)
=> Circle.GetLabel(name_space) + "⊥" + Ray.GetLabel(name_space);
public override MMTFact MakeMMTDeclaration()
{
SOMDoc tp = new OMA(
new OMS(MMTConstants.Ded),
new[]{
new OMA(
new OMS(MMTConstants.OrthoCircleLine),
new[] {
new OMS(Cid1),
new OMS(Lid1),
}
),
}
);
return new MMTGeneralFact(_LastLabel, tp, Defines());
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetDependentFactIds()
=> new string[] { Cid1, Lid1 };
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(OrthogonalCircleLineFact f1, OrthogonalCircleLineFact f2)
=> DependentFactsEquivalent(f1, f2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new)
=> new OrthogonalCircleLineFact(old_to_new[this.Cid1], old_to_new[this.Lid1]);
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
}
/// <summary>
/// A fact that describes, that two circles have the same size and is comprised of two <see cref="CircleFact">CircleFacts</see>
/// </summary>
public class EqualCirclesFact : FactWrappedCRTP<EqualCirclesFact>
{
/// @{ <summary>
/// two circles that are meant to be equal in area
/// </summary>
public string Cid1, Cid2;
/// @}
[JsonIgnore]
public CircleFact Circle1 { get => (CircleFact)FactRecorder.AllFacts[Cid1]; }
[JsonIgnore]
public CircleFact Circle2 { get => (CircleFact)FactRecorder.AllFacts[Cid2]; }
/// <summary> \copydoc Fact.Fact </summary>
public EqualCirclesFact() : base()
{
this.Cid1 = null;
this.Cid2 = null;
}
/// <summary>
/// Standard Constructor:
/// Initiates members and creates MMT %Fact Server-Side
/// </summary>
/// <param name="cid1">sets <see cref="Cid1"/></param>
/// <param name="cid2">sets <see cref="Cid2"/></param>
public EqualCirclesFact(string cid1, string cid2) : base()
{
this.Cid1 = cid1;
this.Cid2 = cid2;
}
protected override void RecalculateTransform()
{
Position = Circle1.Position;
Rotation = Circle1.Rotation;
}
/// <summary>
/// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
/// </summary>
/// <param name="Cid1">sets <see cref="Cid1"/></param>
/// <param name="Cid2">sets <see cref="Cid2"/></param>
/// <param name="backendURI">MMT URI</param>
public EqualCirclesFact(string Cid1, string Cid2, SOMDoc _ServerDefinition) : base()
{
this.Cid1 = Cid1;
this.Cid2 = Cid2;
this.ServerDefinition = _ServerDefinition;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static IEnumerator parseFact(List<Fact> ret, MMTFact fact)
{
if (((MMTGeneralFact)fact).type is not OMA proof_OMA) // proof DED
OMA parallel_circles_OMA = (OMA)proof_OMA.arguments[0]; // parallel
string circleAUri = ((OMS)parallel_circles_OMA.arguments[0]).uri;
string circleBUri = ((OMS)parallel_circles_OMA.arguments[1]).uri;
if (!FactRecorder.AllFacts.ContainsKey(circleAUri)
|| !FactRecorder.AllFacts.ContainsKey(circleBUri))
ret.Add(new EqualCirclesFact(circleAUri, circleBUri, fact.@ref));
}
/// \copydoc Fact.generateLabel
protected override string generateLabel(FactRecorder name_space)
=> Circle1.GetLabel(name_space) + " ≠ " + Circle2.GetLabel(name_space);
public override MMTFact MakeMMTDeclaration()
{
SOMDoc tp = new OMA(
new OMS(MMTConstants.Ded),
new[] {
new OMA(
new OMS(MMTConstants.EqualityCircles),
new[] {
new OMS(Cid1),
new OMS(Cid2),
}
)
}
);
return new MMTGeneralFact(_LastLabel, tp, Defines());
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetDependentFactIds()
=> new string[] { Cid1, Cid2 };
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(EqualCirclesFact f1, EqualCirclesFact f2)
=> DependentFactsEquivalent(f1, f2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new)
=> new EqualCirclesFact(old_to_new[this.Cid1], old_to_new[this.Cid2]);
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
}
/// <summary>
/// A fact that describes, that two circles have not the same size and is comprised of two <see cref="CircleFact">CircleFacts</see>
/// </summary>
public class UnEqualCirclesFact : FactWrappedCRTP<UnEqualCirclesFact>
{
/// @{ <summary>
/// two circles that are meant to be unequal in area
/// </summary>
public string Cid1, Cid2;
/// @}
[JsonIgnore]
public CircleFact Circle1 { get => (CircleFact)FactRecorder.AllFacts[Cid1]; }
[JsonIgnore]
public CircleFact Circle2 { get => (CircleFact)FactRecorder.AllFacts[Cid2]; }
/// <summary> \copydoc Fact.Fact </summary>
public UnEqualCirclesFact() : base()
{
this.Cid1 = null;
this.Cid2 = null;
}
/// <summary>
/// Standard Constructor:
/// Initiates members and creates MMT %Fact Server-Side
/// </summary>
/// <param name="cid1">sets <see cref="Cid1"/></param>
/// <param name="cid2">sets <see cref="Cid2"/></param>
public UnEqualCirclesFact(string cid1, string cid2) : base()
{
this.Cid1 = cid1;
this.Cid2 = cid2;
}
protected override void RecalculateTransform()
{
Position = Circle2.Position;
Rotation = Circle2.Rotation;
}
/// <summary>
/// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
/// </summary>
/// <param name="Cid1">sets <see cref="Cid1"/></param>
/// <param name="Cid2">sets <see cref="Cid2"/></param>
/// <param name="backendURI">MMT URI</param>
public UnEqualCirclesFact(string Cid1, string Cid2, SOMDoc _ServerDefinition) : base()
{
this.Cid1 = Cid1;
this.Cid2 = Cid2;
this.ServerDefinition = _ServerDefinition;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static IEnumerator parseFact(List<Fact> ret, MMTFact fact)
{
if (((MMTGeneralFact)fact).type is not OMA proof_OMA) // proof DED
OMA unequal_circles_OMA = (OMA)proof_OMA.arguments[0]; // unequal
string circleAUri = ((OMS)unequal_circles_OMA.arguments[0]).uri;
string circleBUri = ((OMS)unequal_circles_OMA.arguments[1]).uri;
if (!FactRecorder.AllFacts.ContainsKey(circleAUri)
|| !FactRecorder.AllFacts.ContainsKey(circleBUri))
ret.Add(new UnEqualCirclesFact(circleAUri, circleBUri, fact.@ref));
}
/// \copydoc Fact.generateLabel
protected override string generateLabel(FactRecorder name_space)
=> Circle1.GetLabel(name_space) + " = " + Circle2.GetLabel(name_space);
public override MMTFact MakeMMTDeclaration()
{
SOMDoc tp = new OMA(
new OMS(MMTConstants.Ded),
new[] {
new OMA(new OMS(MMTConstants.UnEqualityCircles),
new[] {
new OMS(Cid1),
new OMS(Cid2),
}),});
return new MMTGeneralFact(_LastLabel, tp, Defines());
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetDependentFactIds()
=> new string[] { Cid1, Cid2 };
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(UnEqualCirclesFact f1, UnEqualCirclesFact f2)
=> DependentFactsEquivalent(f1, f2);