Newer
Older
/// \copydoc Fact.getDependentFactIds
public override string[] getDependentFactIds()
=> new string[] { Cid1, Cid2, equalCirclesProof };
/// \copydoc Fact.instantiateDisplay(GameObject, Transform)
public override GameObject instantiateDisplay(GameObject prefab, Transform transform)
{
var obj = GameObject.Instantiate(prefab, Vector3.zero, Quaternion.identity, transform);
obj.transform.GetChild(0).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Cid1].Label + _Facts[this.Cid2].Label;
obj.GetComponent<FactWrapper>().fact = this;
return obj;
}
/// \copydoc Fact.GetHashCode
/// uhhh is this a problem?
public override int GetHashCode()
=> this.Cid1.GetHashCode() ^ this.Cid2.GetHashCode();
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(CylinderVolumeFact f1, CylinderVolumeFact f2)
{
if (f1.Cid1 == f2.Cid1 && f1.Cid2 == f2.Cid2)
return true;
CircleFact c1f1 = (CircleFact)_Facts[f1.Cid1];
CircleFact c1f2 = (CircleFact)_Facts[f2.Cid1];
CircleFact c2f1 = (CircleFact)_Facts[f1.Cid2];
CircleFact c2f2 = (CircleFact)_Facts[f2.Cid2];
return c1f1.Equivalent(c1f2) && c2f1.Equivalent(c2f2) && Mathf.Approximately(f1.vol, f2.vol);
}
}
/// <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>
{
MaZiFAU
committed
protected new string s_type = "EqualCirclesFact";
/// @{ <summary>
/// two circles that are meant to be equal in area
/// </summary>
public string Cid1, Cid2;
/// @}
MaZiFAU
committed
[JsonIgnore]
public CircleFact Circle1 { get => (CircleFact)_Facts[Cid1]; }
[JsonIgnore]
public CircleFact Circle2 { get => (CircleFact)_Facts[Cid2]; }
/// <summary> \copydoc Fact.Fact </summary>
public EqualCirclesFact() : base()
{
this.Cid1 = null;
this.Cid2 = 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 EqualCirclesFact(EqualCirclesFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
=> init(old_to_new[fact.Cid1], old_to_new[fact.Cid2]);
/// <summary>
/// Standard Constructor
/// </summary>
/// <param name="cid1">sets <see cref="Cid1"/></param>
/// <param name="cid2">sets <see cref="Cid2"/></param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public EqualCirclesFact(string cid1, string cid2, FactOrganizer organizer) : base(organizer)
/// <summary>
/// Initiates <see cref="Cid1"/>, <see cref="Cid2"/>, <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
/// </summary>
/// <param name="cid1">sets <see cref="Cid1"/></param>
/// <param name="cid2">sets <see cref="Cid2"/></param>
private void init(string cid1, string cid2)
{
this.Cid1 = cid1;
this.Cid2 = cid2;
Position = Circle1.Position;
Rotation = Circle1.Rotation;
MMTDeclaration mmtDecl = generateEqualCirclesFactDeclaration(cid1, cid2);
3097
3098
3099
3100
3101
3102
3103
3104
3105
3106
3107
3108
3109
3110
3111
3112
3113
3114
3115
3116
3117
3118
3119
3120
3121
3122
3123
3124
3125
3126
3127
3128
3129
3130
3131
3132
3133
3134
3135
3136
3137
3138
3139
3140
3141
3142
3143
3144
3145
3146
3147
AddFactResponse.sendAdd(mmtDecl, out this._URI);
}
/// <summary>
/// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
/// </summary>
/// <param name="Cid1">sets <see cref="Cid1"/></param>
/// <param name="Cid2">sets <see cref="Cid2"/></param>
/// <param name="backendURI">MMT URI</param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public EqualCirclesFact(string Cid1, string Cid2, string backendURI, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = Cid1;
this.Cid2 = Cid2;
this._URI = backendURI;
_ = this.Label;
}
/// \copydoc Fact.parseFact(Scroll.ScrollFact)
public new static EqualCirclesFact parseFact(Scroll.ScrollFact fact)
{
OMA tp = (OMA)((Scroll.ScrollSymbolFact)fact).tp;
if (tp == null)
return null;
string circleAUri = "";
string circleBUri = "";
string uri = fact.@ref.uri;
OMA proof_OMA = (OMA)((Scroll.ScrollSymbolFact)fact).tp; // proof DED
OMA parallel_circles_OMA = (OMA)proof_OMA.arguments[0]; // parallel
if (parallel_circles_OMA.arguments[0] is OMS)
{
// Normaler Fall
circleAUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0]).uri;
circleBUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).uri;
}
if (StageStatic.stage.factState.ContainsKey(circleAUri)
&& StageStatic.stage.factState.ContainsKey(circleBUri))
return new EqualCirclesFact(circleAUri, circleBUri, uri, StageStatic.stage.factState);
else //If dependent facts do not exist return null
return null;
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> _Facts[Cid1].Label + " ≠ " + _Facts[Cid2].Label;
/// <summary>
/// Constructs struct for equalCirclesFact <see cref="AddFactResponse"/>
/// </summary>
/// <param name="c1URI"><see cref="Cid1"/></param>
/// <param name="c2URI"><see cref="Cid2"/></param>
/// <returns>struct for <see cref="AddFactResponse"/></returns>
private MMTDeclaration generateEqualCirclesFactDeclaration(string c1URI, string c2URI)
{
MaZiFAU
committed
SOMDoc tp = new OMA(
new OMS(MMT_OMS_URI.Ded),
new List<SOMDoc> {
MaZiFAU
committed
new OMS(MMT_OMS_URI.EqualityCircles),
new List<SOMDoc> {
new OMS(c1URI),
new OMS(c2URI),
}
)
}
);
MaZiFAU
committed
SOMDoc 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()
/// \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.Cid2].Label;
obj.GetComponent<FactWrapper>().fact = this;
return obj;
}
/// \copydoc Fact.GetHashCode
public override int GetHashCode()
=> this.Cid1.GetHashCode() ^ this.Cid2.GetHashCode();
3201
3202
3203
3204
3205
3206
3207
3208
3209
3210
3211
3212
3213
3214
3215
3216
3217
3218
3219
3220
3221
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(EqualCirclesFact f1, EqualCirclesFact f2)
{
if ((f1.Cid1 == f2.Cid1 && f1.Cid2 == f2.Cid2))
return true;
CircleFact e1f1 = (CircleFact)_Facts[f1.Cid1];
CircleFact e2f1 = (CircleFact)_Facts[f1.Cid2];
CircleFact e1f2 = (CircleFact)_Facts[f2.Cid1];
CircleFact e2f2 = (CircleFact)_Facts[f2.Cid2];
return (e1f1.Equivalent(e1f2) && e2f1.Equivalent(e2f2));
}
}
/// <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>
{
MaZiFAU
committed
protected new string s_type = "UnEqualCirclesFact";
/// @{ <summary>
/// two circles that are meant to be unequal in area
/// </summary>
public string Cid1, Cid2;
/// @}
MaZiFAU
committed
[JsonIgnore]
public CircleFact Circle1 { get => (CircleFact)_Facts[Cid1]; }
[JsonIgnore]
public CircleFact Circle2 { get => (CircleFact)_Facts[Cid2]; }
/// <summary> \copydoc Fact.Fact </summary>
public UnEqualCirclesFact() : base()
{
this.Cid1 = null;
this.Cid2 = 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 UnEqualCirclesFact(UnEqualCirclesFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
=> init(old_to_new[fact.Cid1], old_to_new[fact.Cid2]);
/// <summary>
/// Standard Constructor
/// </summary>
/// <param name="cid1">sets <see cref="Cid1"/></param>
/// <param name="cid2">sets <see cref="Cid2"/></param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public UnEqualCirclesFact(string cid1, string cid2, FactOrganizer organizer) : base(organizer)
/// <summary>
/// Initiates <see cref="Cid1"/>, <see cref="Cid2"/>, <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
/// </summary>
/// <param name="cid1">sets <see cref="Cid1"/></param>
/// <param name="cid2">sets <see cref="Cid2"/></param>
private void init(string cid1, string cid2)
{
this.Cid1 = cid1;
this.Cid2 = cid2;
Position = Circle2.Position;
Rotation = Circle2.Rotation;
MMTDeclaration mmtDecl = generateUnEqualCirclesFactDeclaration(cid1, cid2);
3276
3277
3278
3279
3280
3281
3282
3283
3284
3285
3286
3287
3288
3289
3290
3291
3292
3293
3294
3295
3296
3297
3298
3299
3300
3301
3302
3303
3304
3305
3306
3307
3308
3309
3310
3311
3312
3313
3314
3315
3316
3317
3318
3319
3320
3321
3322
3323
3324
3325
3326
3327
AddFactResponse.sendAdd(mmtDecl, out this._URI);
}
/// <summary>
/// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
/// </summary>
/// <param name="Cid1">sets <see cref="Cid1"/></param>
/// <param name="Cid2">sets <see cref="Cid2"/></param>
/// <param name="backendURI">MMT URI</param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public UnEqualCirclesFact(string Cid1, string Cid2, string backendURI, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = Cid1;
this.Cid2 = Cid2;
this._URI = backendURI;
_ = this.Label;
}
/// \copydoc Fact.parseFact(Scroll.ScrollFact)
public new static UnEqualCirclesFact parseFact(Scroll.ScrollFact fact)
{
OMA tp = (OMA)((Scroll.ScrollSymbolFact)fact).tp;
if (tp == null)
return null;
string circleAUri = "";
string circleBUri = "";
string uri = fact.@ref.uri;
OMA proof_OMA = (OMA)((Scroll.ScrollSymbolFact)fact).tp; // proof DED
OMA unequal_circles_OMA = (OMA)proof_OMA.arguments[0]; // unequal
if (unequal_circles_OMA.arguments[0] is OMS)
{
// Normaler Fall
circleAUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0]).uri;
circleBUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).uri;
}
if (StageStatic.stage.factState.ContainsKey(circleAUri)
&& StageStatic.stage.factState.ContainsKey(circleBUri))
return new UnEqualCirclesFact(circleAUri, circleBUri, uri, StageStatic.stage.factState);
else //If dependent facts do not exist return null
return null;
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> _Facts[Cid1].Label + " = " + _Facts[Cid2].Label;
/// <summary>
/// Constructs struct for equalCirclesFact <see cref="AddFactResponse"/>
/// </summary>
/// <param name="c1URI"><see cref="Cid1"/></param>
/// <param name="c2URI"><see cref="Cid2"/></param>
/// <returns>struct for <see cref="AddFactResponse"/></returns>
private MMTDeclaration generateUnEqualCirclesFactDeclaration(string c1URI, string c2URI)
{
MaZiFAU
committed
SOMDoc tp = new OMA(
new OMS(MMT_OMS_URI.Ded),
new List<SOMDoc> {
new OMA(new OMS(MMT_OMS_URI.UnEqualityCircles),
new List<SOMDoc> {
new OMS(c1URI),
new OMS(c2URI),
}),});
MaZiFAU
committed
SOMDoc df = null;
MMTSymbolDeclaration mmtDecl = new (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[] { Cid1, Cid2 };
/// \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.Cid2].Label;
obj.GetComponent<FactWrapper>().fact = this;
return obj;
}
/// \copydoc Fact.GetHashCode
public override int GetHashCode()
=> this.Cid1.GetHashCode() ^ this.Cid2.GetHashCode();
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(UnEqualCirclesFact f1, UnEqualCirclesFact f2)
{
if ((f1.Cid1 == f2.Cid1 && f1.Cid2 == f2.Cid2))
return true;
CircleFact e1f1 = (CircleFact)_Facts[f1.Cid1];
CircleFact e2f1 = (CircleFact)_Facts[f1.Cid2];
CircleFact e1f2 = (CircleFact)_Facts[f2.Cid1];
CircleFact e2f2 = (CircleFact)_Facts[f2.Cid2];
return (e1f1.Equivalent(e1f2) && e2f1.Equivalent(e2f2));
}
}
#pragma warning disable // Testing...
/// use this if you need to test certain implementations of facts.
/// </summary>
public class TestFact : FactWrappedCRTP<TestFact>
{
MaZiFAU
committed
protected new string s_type = "TestFact";
/// <summary> \copydoc Fact.Fact </summary>
public TestFact() : base()
{
3411
3412
3413
3414
3415
3416
3417
3418
3419
3420
3421
3422
3423
3424
3425
3426
3427
3428
3429
3430
3431
}
/// <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 TestFact(TestFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
{
init();
}
/// <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 TestFact(FactOrganizer organizer) : base(organizer)
{
init();
}
/// <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()
{
// 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 TestFact(string backendURI, FactOrganizer organizer) : base(organizer)
this._URI = backendURI;
_ = this.Label;
}
/// <summary>
/// parses the Circlefact response of the MMT-Server
/// </summary>
/// \copydoc Fact.parseFact(Scroll.ScrollFact)
public new static TestFact parseFact(Scroll.ScrollFact fact)
{
string uri = fact.@ref.uri;
Debug.Log("TestFact Uri:" + uri);
return new TestFact(uri, StageStatic.stage.factState);
}
/// \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)
{
PointFact p1 = _Facts[p1URI] as PointFact;
PointFact p2 = _Facts[p2URI] as PointFact;
MaZiFAU
committed
List<SOMDoc> normalArgs = new List<SOMDoc>
{
new OMF(normal.x),
new OMF(normal.y),
new OMF(normal.z)
};
MaZiFAU
committed
OMA NormalVector = new OMA(new OMS(MMT_OMS_URI.Tuple), normalArgs);
MaZiFAU
committed
List<SOMDoc> planeArgs = new List<SOMDoc>
{
new OMS(p2URI),
NormalVector //n
};
MaZiFAU
committed
OMA CirclePlane = new OMA(new OMS(MMT_OMS_URI.pointNormalPlane), planeArgs);
OMS middlePoint = new OMS(p1URI);
OMF Radius = new OMF(radius);
MaZiFAU
committed
List<SOMDoc> outerArguments = new List<SOMDoc>
{
CirclePlane,
middlePoint,
Radius
};
//OMS constructor generates full URI
// Do i need this here? doubt
MaZiFAU
committed
SOMDoc tp = new OMS(MMT_OMS_URI.CircleType3d);
SOMDoc df = new OMA(new OMS(MMT_OMS_URI.MkCircle3d), outerArguments);
MMTSymbolDeclaration mmtDecl = new MMTSymbolDeclaration(this.Label, tp, df);
AddFactResponse.sendAdd(mmtDecl, out this._URI);
return mmtDecl;
}
/// \copydoc Fact.hasDependentFacts
public override Boolean hasDependentFacts()
{
return false;
}
3550
3551
3552
3553
3554
3555
3556
3557
3558
3559
3560
3561
3562
3563
3564
3565
3566
3567
3568
3569
3570
3571
3572
3573
3574
3575
3576
3577
/// \copydoc Fact.getDependentFactIds
public override string[] getDependentFactIds()
{
return new string[] { };
}
/// \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(1).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Lid2].Label;
obj.GetComponent<FactWrapper>().fact = this;
return obj;
}
/// \copydoc Fact.GetHashCode
public override int GetHashCode()
{
return 112315414;// this.Pid1.GetHashCode() ^ this.Pid2.GetHashCode();
}
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(TestFact f1, TestFact f2)
{
return false;
}
#pragma warning restore // Testing over