Newer
Older
John Schihada
committed
new List<MMTTerm> {
new OMS(p1URI),
new OMS(p2URI),
new OMS(p3URI)
}
),
John Schihada
committed
}
);
MMTTerm tp = new OMA(new OMS(MMTURIs.Ded), new List<MMTTerm> { argument });
John Schihada
committed
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>
John Schihada
committed
private MMTDeclaration generateNot90DegreeAngleDeclaration(float val, string p1URI, string p2URI, string p3URI)
{
MMTTerm lhs =
new OMA(
John Schihada
committed
new List<MMTTerm> {
new OMS(p1URI),
new OMS(p2URI),
new OMS(p3URI)
}
);
MMTTerm valueTp = new OMS(MMTURIs.RealLit);
John Schihada
committed
MMTTerm value = new OMF(val);
John Schihada
committed
return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
}
/// \copydoc Fact.hasDependentFacts
public override Boolean hasDependentFacts()
/// \copydoc Fact.getDependentFactIds
public override string[] getDependentFactIds()
=> 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
Marco Zimmer
committed
public override int GetHashCode()
=> this.Pid1.GetHashCode() ^ this.Pid2.GetHashCode() ^ this.Pid3.GetHashCode();
/// \copydoc Fact.Equivalent(Fact, Fact)
Marco Zimmer
committed
protected override bool EquivalentWrapped(AngleFact f1, AngleFact f2)
Marco Zimmer
committed
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];
Marco Zimmer
committed
return (p1f1.Equivalent(p1f2) && p2f1.Equivalent(p2f2) && p3f1.Equivalent(p3f2));
//|| (p1f1.Equivalent(p3f2) && p2f1.Equivalent(p2f2) && p1f1.Equivalent(p3f2));
}
}
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
/// <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)
/// <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;
AddFactResponse.sendAdd(generateMMTDeclaration(pid1, pid2, pid3), out this._URI);
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
}
/// <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()
=> _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)
{
MMTTerm tp =
new OMA(
new OMS(MMTURIs.Ded),
new List<MMTTerm> {
new OMA(
new OMS(MMTURIs.RightAngle),
new List<MMTTerm> {
new OMS(p1URI),
new OMS(p2URI),
new OMS(p3URI),
}),});
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[] { 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()
=> 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));
}
}
/// <summary>
/// Two parallel Lines comprised of two <see cref="LineFact">LineFacts</see>
/// </summary>
public class ParallelLineFact : FactWrappedCRTP<ParallelLineFact>
{
/// \copydoc Fact.s_type
[JsonProperty]
protected static new string s_type = "ParallelLineFact";
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
/// @{ <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)
{
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);
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
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 uri = fact.@ref.uri;
string lineAUri;
string lineBUri;
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) parallel_lines_OMA.arguments[0]).uri;
lineBUri = ((OMS) parallel_lines_OMA.arguments[1]).uri;
else // TODO: Second case might be redundant by now
{
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()
=> _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)
{
MMTTerm tp = new OMA(
new OMS(MMTURIs.Ded),
new List<MMTTerm> {
new OMA(
new OMS(MMTURIs.ParallelLine),
new List<MMTTerm> {
new OMS(l1URI),
new OMS(l2URI),
}
),
}
);
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()
=> true;
/// \copydoc Fact.getDependentFactIds
public override string[] getDependentFactIds()
=> 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()
=> 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>
{
/// \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;
this.radius = radius;
this.normal = normal;
MMTDeclaration mmtDecl = generateCircleFactDeclaration(pid1, pid2, 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;
OMA df = (OMA)((Scroll.ScrollSymbolFact)fact).df;
if (df == null)
return null;
Scroll.ScrollSymbolFact scoll_symbol_fact = (Scroll.ScrollSymbolFact)fact;
float radius = ((OMF)((OMA)scoll_symbol_fact.df).arguments[2]).f;
OMA planeOMA = (OMA)((OMA)scoll_symbol_fact.df).arguments[0];
string planeApplicant = ((OMS)planeOMA.applicant).uri;
string A_uri;
Vector3 normal;
// Getting the plane
// IN case of a normale plane
if (planeApplicant.Equals(MMTURIs.pointNormalPlane))
{
//OMA pointAOMA = (OMA)planeOMA.arguments[0];
A_uri = ParsingDictionary.parseTermsToId[planeOMA.arguments[0].ToString()];
OMA n = (OMA)planeOMA.arguments[1];
normal = new Vector3(((OMF)n.arguments[0]).f, ((OMF)n.arguments[1]).f, ((OMF)n.arguments[2]).f);
}
// In case of parametrized plane
else if (planeApplicant.Equals(MMTURIs.ParametrizedPlane))
A_uri = ParsingDictionary.parseTermsToId[planeOMA.arguments[0].ToString()];
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;
}
// 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 = ((OMA)scoll_symbol_fact.df).arguments[1].ToString();
string M_uri = ParsingDictionary.parseTermsToId[parse_id_M];
if (StageStatic.stage.factState.ContainsKey(M_uri)
&& StageStatic.stage.factState.ContainsKey(A_uri))
return new CircleFact(M_uri, A_uri, radius, normal, uri, StageStatic.stage.factState);
else //If dependent facts do not exist return null
return null;
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
/// <summary>
/// Constructs struct for right-angled MMT %Fact <see cref="AddFactResponse"/>
/// </summary>
/// <param name="p1URI"> <see cref="Pid1"/></param>
/// <param name="p2URI"> <see cref="Pid2"/></param>
/// <param name="radius"> <see cref="radius"/></param>
/// <returns>struct for <see cref="AddFactResponse"/></returns>
private MMTDeclaration generateCircleFactDeclaration(string p1URI, string p2URI, float radius, Vector3 normal)
{
List<MMTTerm> outerArguments = new List<MMTTerm>
{
1618
1619
1620
1621
1622
1623
1624
1625
1626
1627
1628
1629
1630
1631
1632
1633
1634
1635
1636
1637
1638
1639
1640
1641
1642
//CirclePlane,
new OMA(
//PointNormalPlane,
new OMS(MMTURIs.pointNormalPlane),
//planeArgs,
new List<MMTTerm> {
//base point of the circle plane?,
new OMS(p2URI),
//NormalVector,
new OMA(
//"Vector"
new OMS(MMTURIs.Tuple),
//normalArgs,
new List<MMTTerm> {
new OMF(normal.x),
new OMF(normal.y),
new OMF(normal.z)
}
),
}
),
//middlePoint,
new OMS(p1URI),
//Radius,
new OMF(radius),
};
// Do i need this here? doubt
MMTTerm tp = new OMS(MMTURIs.CircleType3d);
MMTTerm df = new OMA(new OMS(MMTURIs.MkCircle3d), outerArguments);
MMTSymbolDeclaration mmtDecl = new MMTSymbolDeclaration(Label, tp, df);
AddFactResponse.sendAdd(mmtDecl, out _URI);
return mmtDecl;
}
/// \copydoc Fact.hasDependentFacts
public override Boolean hasDependentFacts()
/// \copydoc Fact.getDependentFactIds
public override string[] getDependentFactIds()
/// \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.Lid2].Label;
obj.GetComponent<FactWrapper>().fact = this;
return obj;
}
/// \copydoc Fact.GetHashCode
public override int GetHashCode()
=> Pid1.GetHashCode() ^ Pid2.GetHashCode();
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(CircleFact f1, CircleFact f2)
{
if (f1.Pid1 == f2.Pid1 && f1.normal == f2.normal && f1.radius == f2.radius)
return true;
PointFact p1f1 = (PointFact)_Facts[f1.Pid1];
PointFact p1f2 = (PointFact)_Facts[f2.Pid1];
return p1f1.Equivalent(p1f2)
&& Math3d.IsApproximatelyEqual(f1.normal, f2.normal)
&& Mathf.Approximately(f1.radius, f2.radius);
}
}
/// <summary>
/// A <see cref="PointFact"/> on a <see cref="CircleFact"/>
/// </summary>
public class OnCircleFact : FactWrappedCRTP<OnCircleFact>
{
/// \copydoc Fact.s_type
[JsonProperty]
protected static new string s_type = "OnCircleFact";
/// <summary> the point on the circle </summary>
public string Pid;
/// <summary> the circle, which the point is on </summary>
public string Cid;
/// <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)
/// <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;
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),
}),});
MMTTerm df = null;
AddFactResponse.sendAdd(new MMTSymbolDeclaration(Label, tp, df), out _URI);
1757
1758
1759
1760
1761
1762
1763
1764
1765
1766
1767
1768
1769
1770
1771
1772
1773
1774
1775
1776
1777
1778
1779
1780
1781
1782
1783
1784
}
/// <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()
/// \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>
{
/// \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;
/// @}
/// <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)
/// 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>
1902
1903
1904
1905
1906
1907
1908
1909
1910
1911
1912
1913
1914
1915
1916
1917
1918
1919
1920
1921
1922
1923
1924
1925
1926
1927
1928
1929
/// <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()
/// \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)