-
MaZiFAU authored
ListFact: +Intrduction, needed for lists on MMT server side +Incomplete +-> see SOMDocManager.MMT_OMS_URI.FactRef Bug Fix: +Fact Ordering was broken +ScrollFactContainer marked as IsSet wrongly +Angle Hint showed up with 0° HotFix; +Game Crash when Scrolls not loaded +-> patched with guard clausel (pls find better way)
MaZiFAU authoredListFact: +Intrduction, needed for lists on MMT server side +Incomplete +-> see SOMDocManager.MMT_OMS_URI.FactRef Bug Fix: +Fact Ordering was broken +ScrollFactContainer marked as IsSet wrongly +Angle Hint showed up with 0° HotFix; +Game Crash when Scrolls not loaded +-> patched with guard clausel (pls find better way)
Fact.cs 86.01 KiB
using System;
using System.Collections.Generic;
using UnityEngine;
using UnityEngine.Networking;
using Newtonsoft.Json;
using JsonSubTypes;
using System.Linq;
using static SOMDocManager;
using static Scroll;
public static class ParsingDictionary
{
//TODO? get rid of this, use reflection? instead, if possible
//TODO: docu
public static Dictionary<string, Func<MMTDeclaration, Fact>> parseFactDictionary = new() {
{ MMT_OMS_URI.Point,
PointFact.parseFact },
{ MMT_OMS_URI.Metric,
LineFact.parseFact },
{ MMT_OMS_URI.Angle,
AngleFact.parseFact },
{ MMT_OMS_URI.Eq,
AngleFact.parseFact },
{ MMT_OMS_URI.RightAngle,
RightAngleFact.parseFact },
{ MMT_OMS_URI.LineType,
RayFact.parseFact },
{ MMT_OMS_URI.LineOf,
RayFact.parseFact },
{ MMT_OMS_URI.OnLine,
OnLineFact.parseFact },
{ MMT_OMS_URI.ParallelLine,
ParallelLineFact.parseFact },
{ MMT_OMS_URI.CircleType3d,
CircleFact.parseFact },
{ MMT_OMS_URI.OnCircle,
OnCircleFact.parseFact },
{ MMT_OMS_URI.AnglePlaneLine,
AngleCircleLineFact.parseFact },
{ MMT_OMS_URI.RadiusCircleMetric,
RadiusFact.parseFact },
{ MMT_OMS_URI.AreaCircle,
AreaCircleFact.parseFact },
{ MMT_OMS_URI.OrthoCircleLine,
OrthogonalCircleLineFact.parseFact },
{ MMT_OMS_URI.VolumeCone,
ConeVolumeFact.parseFact },
{ MMT_OMS_URI.TruncatedVolumeCone,
TruncatedConeVolumeFact.parseFact },
{ MMT_OMS_URI.CylinderVolume,
CylinderVolumeFact.parseFact },
{ MMT_OMS_URI.TestType,
TestFact.parseFact },
{ MMT_OMS_URI.EqualityCircles,
EqualCirclesFact.parseFact },
{ MMT_OMS_URI.UnEqualityCircles,
UnEqualCirclesFact.parseFact },
{ MMT_OMS_URI.ListLiteral,
ListFact.parseFact },
};
// TODO: get rid of this
public static Dictionary<string, string> parseTermsToId = new();
}
/// <summary>
/// %Fact representation of Unity; mostly mirrors Facts of MMT.
/// </summary>
[JsonConverter(typeof(JsonSubtypes), "s_type")]
[JsonSubtypes.KnownSubType(typeof(PointFact), nameof(PointFact))]
[JsonSubtypes.KnownSubType(typeof(LineFact), nameof(LineFact))]
[JsonSubtypes.KnownSubType(typeof(RayFact), nameof(RayFact))]
[JsonSubtypes.KnownSubType(typeof(OnLineFact), nameof(OnLineFact))]
[JsonSubtypes.KnownSubType(typeof(AngleFact), nameof(AngleFact))]
[JsonSubtypes.KnownSubType(typeof(CircleFact), nameof(CircleFact))]
[JsonSubtypes.KnownSubType(typeof(ParallelLineFact), nameof(ParallelLineFact))]
[JsonSubtypes.KnownSubType(typeof(OnCircleFact), nameof(OnCircleFact))]
[JsonSubtypes.KnownSubType(typeof(AngleCircleLineFact), nameof(AngleCircleLineFact))]
[JsonSubtypes.KnownSubType(typeof(OrthogonalCircleLineFact), nameof(OrthogonalCircleLineFact))]
[JsonSubtypes.KnownSubType(typeof(AreaCircleFact), nameof(AreaCircleFact))]
[JsonSubtypes.KnownSubType(typeof(RadiusFact), nameof(RadiusFact))]
[JsonSubtypes.KnownSubType(typeof(ConeVolumeFact), nameof(ConeVolumeFact))]
[JsonSubtypes.KnownSubType(typeof(TruncatedConeVolumeFact), nameof(TruncatedConeVolumeFact))]
[JsonSubtypes.KnownSubType(typeof(RightAngleFact), nameof(RightAngleFact))]
[JsonSubtypes.KnownSubType(typeof(CylinderVolumeFact), nameof(CylinderVolumeFact))]
[JsonSubtypes.KnownSubType(typeof(TestFact), nameof(TestFact))]
[JsonSubtypes.KnownSubType(typeof(EqualCirclesFact), nameof(EqualCirclesFact))]
[JsonSubtypes.KnownSubType(typeof(UnEqualCirclesFact), nameof(UnEqualCirclesFact))]
[JsonSubtypes.KnownSubType(typeof(AttachedPositionFunction), nameof(AttachedPositionFunction))]
[JsonSubtypes.KnownSubType(typeof(FunctionFact), nameof(FunctionFact))]
[JsonSubtypes.KnownSubType(typeof(FunctionCallFact), nameof(FunctionCallFact))]
[JsonSubtypes.KnownSubType(typeof(ListFact), nameof(ListFact))]
//[JsonSubtypes.KnownSubType(typeof(FunctionFact<T0, TResult>), "FunctionFact<T0, TResult>")] //TODO: generics? => nameof does not work (generic agnostic)
//[JsonSubtypes.KnownSubType(typeof(FunctionFactFloat<Vector3>), "FunctionFact<System.Single, UnityEngine.Vector3>")]
public abstract class Fact
{
/// <summary>
/// Reference to <c>GameObject</c> that represents this Fact in the GameWorld.
/// </summary>
/// <seealso cref="FactObject3D"/>
[JsonIgnore]
public FactWrapper WorldRepresentation;
/// <summary>
/// Collection of <c>Type</c>s of *all* available <see cref="Fact"/>s to choose from.
/// </summary>
[JsonIgnore]
public static readonly Type[] Types = TypeExtensions<Fact>.UAssemblyInheritenceTypes;
/// <value>
/// [ClassName] for JSON de-/serialization.
/// Automatically set in <see cref="Fact()"/> for <b>NON-Generiy-Types</b>!
/// Also add JsonSubtypes.KnownSubType decorator for deserialization to Fact!
/// </value>
[JsonProperty]
protected string s_type;
/// <returns><see langword="true"/> if Fact depends on other \ref Fact "Facts"; equivalent to <see cref="getDependentFactIds"/> returns non empty array</returns>
[JsonIgnore]
public abstract bool HasDependentFacts { get; }
/// <returns> array of Fact <see cref="Id"> Ids </see> on which this Fact depends.</returns>
/// <example><see cref="AngleFact"/> needs 3 <see cref="PointFact"/>s to be defined.</example>
public string[] DependentFactIds => _DependentFactIds ??= GetGetDependentFactIds();
private string[] _DependentFactIds;
/// <returns> array of Fact <see cref="Id"> Ids </see> on which this Fact depends.</returns>
/// <example><see cref="AngleFact"/> needs 3 <see cref="PointFact"/>s to be defined.</example>
protected abstract string[] GetGetDependentFactIds();
/// <value>
/// Unique Id. e.g.: MMT URI
/// </value>
[JsonIgnore]
public string Id
{
get
{
//while (FetchURICoroutine.MoveNext()) ; //active wait for server
return _URI;
}
}
//private IEnumerator FetchURICoroutine = IEnumeratorExtensions.yield_break;
/// <summary>
/// MMT URI
/// </summary>
[JsonProperty]
protected string _URI;
/// <value>
/// <c>get</c> initiates and subsequently updates a human readable name. <remarks>Should be called once a constructor call to be initiated.</remarks>
/// <c>set</c> calls <see cref="rename(string)"/>
/// </value>
public string Label
{
get
{ // in case of renamed dependables
return _Facts == null // JsonSerialization toggle (_Facts.GetNumberOfFacts() == 0 && this is not PointFact) // JsonSerialization toggle && allow first (Point)Fact to be created
|| (hasCustomLabel && _CustomLabel != null)
? _CustomLabel
: generateLabel();
}
set
{
if (_Facts == null) // JsonSerialization toggle)
{
_CustomLabel = value;
LabelId = -LabelId;
return;
}
rename(value);
}
}
/// <value>
/// Is true if Fact has a custom <see cref="Label"/> which is not <c>null</c> or <c>""</c>.
/// </value>
public bool hasCustomLabel => LabelId < 0;
/// <summary>
/// Stores custom <see cref="Label"/> if set.
/// </summary>
protected string _CustomLabel = null;
/// <summary>
/// Counter to organize auto generated <see cref="Label"/>.
/// Set to negative, if custom \ref Label is assigned.
/// </summary>
// property for JSON to set AFTER Label => declare AFTER Label
public int LabelId { get; set; }
/// <summary>
/// Reference to <see cref="FactOrganizer"/> in which this Fact and all its <see cref="getDependentFactIds">depending Facts</see> are beeing organized.
/// </summary>
[JsonIgnore]
protected FactOrganizer _Facts;
[JsonIgnore]
bool ForceRecalculateTransform = true;
[JsonIgnore]
public Vector3 Position
{
get
{
if (ForceRecalculateTransform)
RecalculateTransform();
return _Position;
}
protected set
{
ForceRecalculateTransform = false;
_Position = value;
}
}
private Vector3 _Position = Vector3.zero;
[JsonIgnore]
public Quaternion Rotation
{
get
{
if (ForceRecalculateTransform)
RecalculateTransform();
return _Rotation;
}
protected set
{
ForceRecalculateTransform = false;
_Rotation = value;
}
}
private Quaternion _Rotation = Quaternion.identity;
[JsonIgnore]
public Vector3 LocalScale
{
get
{
if (ForceRecalculateTransform)
RecalculateTransform();
return _LocalScale;
}
protected set
{
ForceRecalculateTransform = false;
_LocalScale = value;
}
}
private Vector3 _LocalScale = Vector3.one;
/// <summary>
/// Only being used by [JsonReader](https://www.newtonsoft.com/json/help/html/T_Newtonsoft_Json_JsonReader.htm) to initiate empty \ref Fact "Facts".
/// <seealso cref="SOMDocManager"/>
/// </summary>
protected Fact()
{
this._Facts = null; // new FactOrganizer();
LabelId = 0;
s_type = this.GetType().Name;
}
/// <summary>
/// Standard base-constructor.
/// </summary>
/// <param name="organizer"><see cref="_Facts"/></param>
protected Fact(FactOrganizer organizer) : this()
{
this._Facts = organizer;
}
/// <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"><see cref="_Facts"/></param>
public Fact ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
{
Fact ret = _ReInitializeMe(old_to_new, organizer);
ret.LabelId = this.LabelId;
if (ret.hasCustomLabel)
ret._CustomLabel = this.Label;
return ret;
}
protected abstract Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer);
/// <summary>
/// Assignes a custom <see cref="Label"/>, if <paramref name="newLabel"/> is not yet taken;
/// or clears custom <see cref="Label"/>.
/// </summary>
/// <param name="newLabel">To be new <see cref="Label"/>. To reset to auto-generation set to <c>null</c> or <c>""</c>.</param>
/// <returns></returns>
//TODO: notify about updated dependable Labelnames for UI
//TODO: check for colissions with not yet generated names
public bool rename(string newLabel)
// returns true if succeded
{
if (string.IsNullOrEmpty(newLabel) && _Facts.GetNumberOfFacts() != 0)
// switch back to autogenerated
{
generateLabel();
_CustomLabel = null;
return true;
}
else
// set CustomLabel if available
{
if (_Facts.ContainsLabel(newLabel))
return false;
freeAutoLabel();
_CustomLabel = newLabel;
return true;
}
}
protected abstract void RecalculateTransform();
public abstract MMTDeclaration MakeMMTDeclaration();
/// <summary>
/// Frees ressources e.g. <see cref="Label"/> and will eventually delete %Fact Server-Side in far-near future when feature is supported.
/// </summary>
~Fact()
{
//TODO: MMT: delete over there
freeAutoLabel();
if (CommunicationEvents.VerboseURI)
Debug.Log("Server removed Fact:\n" + this.Id);
}
/// <summary>
/// Compares \ref Fact "this" against <paramref name="f2"/>.
/// </summary>
/// <param name="f2">Fact to compare to</param>
/// <returns><c>true</c> if <paramref name="f2"/> is semantical very similar to \ref Fact "this"</returns>
public abstract bool Equivalent(Fact f2);
/// <summary>
/// Compares <paramref name="f1"/> against <paramref name="f2"/>.
/// </summary>
/// <param name="f1">Fact to compare to</param>
/// <param name="f2">Fact to compare to</param>
/// <returns><c>true</c> if <paramref name="f2"/> is semantical very similar to <paramref name="f1"/></returns>
public abstract bool Equivalent(Fact f1, Fact f2);
/// <summary>
/// canonical
/// </summary>
/// <returns>unique-ish Hash</returns>
public new virtual int GetHashCode()
=> DependentFactIds
.Select(id => id.GetHashCode())
.Aggregate((hash1, hash2) => hash1 ^ hash2);
/// <summary>
/// auto-generates <see cref="Label"/> using generation variable(s) e.g. <see cref="LabelId"/>;
/// if custom <see cref="Label"/> is set, tries to restore original generated <see cref="Label"/> **without** resetting <see cref="_CustomLabel"/>. If original <see cref="Label"/> is already taken, a new one will be generated.
/// </summary>
/// <returns>auto-generated <see cref="Label"/></returns>
protected virtual string generateLabel()
{
if (LabelId < 0)
// reload Label if possible
LabelId = _Facts.UnusedLabelIds.Remove(-LabelId) ? -LabelId : 0;
if (LabelId == 0)
if (_Facts.UnusedLabelIds.Count == 0)
LabelId = ++_Facts.MaxLabelId;
else
{
LabelId = _Facts.UnusedLabelIds.Min;
_Facts.UnusedLabelIds.Remove(LabelId);
}
return ((char)(64 + LabelId)).ToString();
}
/// <summary>
/// Parses <see cref="MMTDeclaration"/> to actual Fact
/// </summary>
/// <param name="fact">instance to be parsed</param>
/// <returns>parsed Fact</returns>
public static Fact parseFact(MMTDeclaration fact)
=> null;
/// <summary>
/// Tells <see cref="_Facts"/> that \ref Fact "this" no longer uses auto-generated <see cref="Label"/>, but remembers current generation variable(s).
/// </summary>
// TODO? only get _Fact to freeLabel/
public /*protected internal*/ void freeAutoLabel()
{
if (LabelId > 0)
{
_Facts.UnusedLabelIds.Add(LabelId);
// store Label for name-persistance
LabelId = -LabelId;
}
}
/// <summary>
///
/// </summary>
/// <remarks>Asynchron version has proofen inefficent, since <see cref="Fact.Id"/> is usually called in close proximity.</remarks>
// Asynchron version in comments
public void SendToMMT()
{
MMTDeclaration mmtDecl = MakeMMTDeclaration();
//GlobalBehaviour.Instance.StartCoroutine(
// FetchURICoroutine =
_URI =
_SendAdd(
CommunicationEvents.ServerAdress + "/fact/add",
mmtDecl.ToJson()
//,(string uri) => _SendURICallback(mmtDecl, uri)
);//);
//return;
//void _SendURICallback(MMTDeclaration mmtDecl, string uri)
//{
// _URI = uri;
if (mmtDecl is MMTSymbolDeclaration mMTSymbol && mMTSymbol.defines != null)
ParsingDictionary.parseTermsToId[mMTSymbol.defines.ToString()] = _URI;
//}
/*IEnumerator*/
string _SendAdd(string path, string body)//, Action<string> uriCallback)
{
if (!CommunicationEvents.ServerRunning)
{
Debug.LogWarning("Server not running");
//uriCallback(null);
return null; // yield break;
}
if (CommunicationEvents.VerboseURI)
Debug.Log("Sending to Server:\n" + body);
//Put constructor parses stringbody to byteArray internally (goofy workaround)
using UnityWebRequest www = UnityWebRequest.Put(path, body);
www.method = UnityWebRequest.kHttpVerbPOST;
www.SetRequestHeader("Content-Type", "application/json");
www.timeout = 1;
//yield return
UnityWebRequestAsyncOperation web =
www.SendWebRequest();
while (!web.isDone) ;
if (www.result == UnityWebRequest.Result.ConnectionError
|| www.result == UnityWebRequest.Result.ProtocolError)
{
Debug.LogWarning(www.error);
//uriCallback(null);
return null; // yield break;
}
else
{
string answer = null;
while (string.IsNullOrEmpty(answer))
{
//yield return null;
answer = www.downloadHandler.text;
}
UriReference res = JsonUtility.FromJson<UriReference>(answer);
if (CommunicationEvents.VerboseURI)
Debug.Log("Server added Fact:\n" + res.uri);
//uriCallback(res.uri);
return res.uri; // yield break;
}
}
}
}
/// <summary>
/// Implements CRTP for <see cref="Fact"/>; Escalates constructors;
/// </summary>
/// <typeparam name="T">class, which inherits from FactWrappedCRTP</typeparam>
public abstract class FactWrappedCRTP<T> : Fact where T : FactWrappedCRTP<T>
{
/// <summary>\copydoc Fact.Fact()</summary>
protected FactWrappedCRTP() : base() { }
/// <summary>\copydoc Fact.Fact(FactOrganizer)</summary>
protected FactWrappedCRTP(FactOrganizer organizer) : base(organizer) { }
/// \copydoc Fact.Equivalent(Fact)
public override bool Equivalent(Fact f2)
=> Equivalent(this, f2);
/// \copydoc Fact.Equivalent(Fact, Fact)
public override bool Equivalent(Fact f1, Fact f2)
=> f1.GetType() == f2.GetType() && EquivalentWrapped((T)f1, (T)f2);
/// <summary>CRTP step of <see cref="Equivalent(Fact)"/> and <see cref="Equivalent(Fact, Fact)"/></summary>
protected abstract bool EquivalentWrapped(T f1, T f2);
protected bool DependentFactsEquivalent(T f1, T f2)
=> f1.GetGetDependentFactIds()
.Zip(f2.GetGetDependentFactIds(),
(id1, id2) =>
id1 == id2
|| FactOrganizer.AllFacts[id1].Equivalent(FactOrganizer.AllFacts[id2])
)
.All(b => b);
}
/// <summary>
/// Point in 3D Space
/// </summary>
public class PointFact : FactWrappedCRTP<PointFact>
{
/// <summary> Position </summary>
public Vector3 Point;
/// <summary> Orientation for <see cref="Fact.WorldRepresentation"/> </summary>
[JsonProperty]
private Vector3 Normal;
/// <summary> \copydoc Fact.Fact </summary>
public PointFact() : base()
{
this.Point = Vector3.zero;
this.Normal = Vector3.up;
}
/// <summary>
/// Standard Constructor:
/// Initiates <see cref="Point"/>, <see cref="Normal"/>, <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
/// </summary>
/// <param name="P">sets <see cref="Point"/></param>
/// <param name="N">sets <see cref="Normal"/></param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public PointFact(Vector3 P, Vector3 N, FactOrganizer organizer) : base(organizer)
{
this.Point = P;
this.Normal = N;
SendToMMT();
}
protected override void RecalculateTransform()
{
Position = Point;
{ // Rotation
Vector3 notNormal = Vector3.forward != Normal ? Vector3.forward : Vector3.up;
Rotation = Quaternion.LookRotation(
Vector3.Cross(Normal, notNormal),
Normal
);
}
}
/// <summary>
/// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
/// <see cref="Normal"/> set to <c>Vector3.up</c>
/// </summary>
/// <param name="point">sets <see cref="Point"/></param>
/// <param name="uri">MMT URI</param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public PointFact(Vector3 point, string uri, FactOrganizer organizer) : base(organizer)
{
this.Point = point;
this.Normal = Vector3.up;
this._URI = uri;
_ = this.Label;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static PointFact parseFact(MMTDeclaration fact)
{
if (((MMTSymbolDeclaration)fact).defines is not OMA defines)
return null;
ParsingDictionary.parseTermsToId.TryAdd(defines.ToString(), fact.@ref.uri);
Vector3 point = (defines.GetLambdaExpression().Compile() as Func<Vector3>)();
return new PointFact(point, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => false;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> new string[] { };
/// \copydoc Fact.GetHashCode
public override int GetHashCode()
=> this.Point.GetHashCode();
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(PointFact f1, PointFact f2)
=> Math3d.IsApproximatelyEqual(f1.Point, f2.Point);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
=> new PointFact(this.Point, this.Normal, organizer);
public override MMTDeclaration MakeMMTDeclaration()
{
SOMDoc tp = new OMS(MMT_OMS_URI.Point);
SOMDoc df = new OMA(
new OMS(MMT_OMS_URI.Tuple),
new List<SOMDoc> {
new OMF(Point.x),
new OMF(Point.y),
new OMF(Point.z),
}
);
return new MMTSymbolDeclaration(Label, tp, df);
}
}
/// <summary>
/// A <see cref="PointFact"/> on a <see cref="AbstractLineFact"/>
/// </summary>
public class OnLineFact : FactWrappedCRTP<OnLineFact>
{
/// <summary> <see cref="PointFact"/>.<see cref="Fact.Id">Id</see> </summary>
public string Pid;
[JsonIgnore]
public PointFact Point { get => (PointFact)FactOrganizer.AllFacts[Pid]; }
/// <summary> <see cref="AbstractLineFact"/>.<see cref="Fact.Id">Id</see> </summary>
public string Rid;
[JsonIgnore]
public AbstractLineFact Ray { get => (AbstractLineFact)FactOrganizer.AllFacts[Rid]; }
/// <summary> \copydoc Fact.Fact </summary>
public OnLineFact() : base()
{
this.Pid = null;
this.Rid = 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="rid">sets <see cref="Rid"/></param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public OnLineFact(string pid, string rid, FactOrganizer organizer) : base(organizer)
{
this.Pid = pid;
this.Rid = rid;
SendToMMT();
}
protected override void RecalculateTransform()
{
Position = Point.Position;
{ //Rotation
Vector3 up = Point.Rotation * Vector3.up;
Vector3 forward = Ray.Dir;
if (Math3d.IsApproximatelyEqual(up, forward))
{
Vector3 arbitary = Math3d.IsApproximatelyEqual(forward, Vector3.forward)
? Vector3.right
: Vector3.forward;
up = Vector3.Cross(arbitary, forward);
}
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="pid">sets <see cref="Pid"/></param>
/// <param name="rid">sets <see cref="Rid"/></param>
/// <param name="uri">MMT URI</param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public OnLineFact(string pid, string rid, string uri, FactOrganizer organizer) : base(organizer)
{
this.Pid = pid;
this.Rid = rid;
this._URI = uri;
_ = this.Label;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static OnLineFact parseFact(MMTDeclaration fact)
{
string pointUri = ((OMS)((OMA)((OMA)((MMTSymbolDeclaration)fact).type).arguments[0]).arguments[1]).uri;
string lineUri = ((OMA)((OMA)((MMTSymbolDeclaration)fact).type).arguments[0]).arguments[0] is OMS
// standard case
? ((OMS)((OMA)((OMA)((MMTSymbolDeclaration)fact).type).arguments[0]).arguments[0]).uri
// case when line Uri has a projl on the line Argument
: ((OMS)((OMA)((OMA)((OMA)((MMTSymbolDeclaration)fact).type).arguments[0]).arguments[0]).arguments[0]).uri;
if (!FactOrganizer.AllFacts.ContainsKey(pointUri)
|| !FactOrganizer.AllFacts.ContainsKey(lineUri))
return null;
return new OnLineFact(pointUri, lineUri, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> Point.Label + "∈" + Ray.Label;
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> new string[] { Pid, Rid };
protected override bool EquivalentWrapped(OnLineFact f1, OnLineFact f2)
=> DependentFactsEquivalent(f1, f2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
=> new OnLineFact(old_to_new[this.Pid], old_to_new[this.Rid], 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.OnLine),
new List<SOMDoc> {
new OMS(Rid),
new OMS(Pid)
}),});
SOMDoc df = null;
return new MMTSymbolDeclaration(this.Label, tp, df);
}
}
/// <summary>
/// Two parallel Lines comprised of two <see cref="LineFact">LineFacts</see>
/// </summary>
public class ParallelLineFact : FactWrappedCRTP<ParallelLineFact>
{
/// @{ <summary>
/// One <see cref="Fact.Id">Id</see> of two <see cref="LineFact"/> that are parallel [<see cref="Lid1"/>, <see cref="Lid2"/>].
/// </summary>
public string Lid1, Lid2;
/// @}
[JsonIgnore]
public AbstractLineFact Ray1 { get => (AbstractLineFact)FactOrganizer.AllFacts[Lid1]; }
[JsonIgnore]
public AbstractLineFact Ray2 { get => (AbstractLineFact)FactOrganizer.AllFacts[Lid2]; }
/// <summary> \copydoc Fact.Fact </summary>
public ParallelLineFact() : base()
{
this.Lid1 = null;
this.Lid2 = null;
}
/// <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)
{
this.Lid1 = lid1;
this.Lid2 = lid2;
SendToMMT();
}
protected override void RecalculateTransform() { }
/// <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(ScrollFact)
public new static ParallelLineFact parseFact(MMTDeclaration fact)
{
if (((MMTSymbolDeclaration)fact).type is not OMA type) // proof DED
return null;
OMA parallel_lines_OMA = (OMA)type.arguments[0]; // parallel
string lineAUri = ((OMS)parallel_lines_OMA.arguments[0]).uri;
string lineBUri = ((OMS)parallel_lines_OMA.arguments[1]).uri;
if (!FactOrganizer.AllFacts.ContainsKey(lineAUri)
|| !FactOrganizer.AllFacts.ContainsKey(lineBUri))
return null;
return new ParallelLineFact(lineAUri, lineBUri, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> Ray1.Label + "||" + Ray2.Label;
public override MMTDeclaration MakeMMTDeclaration()
{
SOMDoc tp = new OMA(
new OMS(MMT_OMS_URI.Ded),
new List<SOMDoc> {
new OMA(
new OMS(MMT_OMS_URI.ParallelLine),
new List<SOMDoc> {
new OMS(Lid1),
new OMS(Lid2),
}
),
}
);
SOMDoc df = null;
return new MMTSymbolDeclaration(this.Label, tp, df);
}
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> new string[] { Lid1, Lid2 };
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(ParallelLineFact f1, ParallelLineFact f2)
=> DependentFactsEquivalent(f1, f2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
=> new ParallelLineFact(old_to_new[this.Lid1], old_to_new[this.Lid2], organizer);
}
/// <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 Pid1;
/// <summary> defining the base point of the circle plane </summary>
public string Pid2;
[JsonIgnore]
public PointFact Point1 { get => (PointFact)FactOrganizer.AllFacts[Pid1]; }
[JsonIgnore]
public PointFact Point2 { get => (PointFact)FactOrganizer.AllFacts[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>
/// Standard Constructor:
/// 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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public CircleFact(string pid1, string pid2, float radius, Vector3 normal, FactOrganizer organizer) : base(organizer)
{
this.Pid1 = pid1;
this.Pid2 = pid2;
this.radius = radius;
this.normal = normal;
SendToMMT();
}
protected override void RecalculateTransform()
{
Position = Point1.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="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(ScrollFact)
public new static CircleFact parseFact(MMTDeclaration fact)
{
if (((MMTSymbolDeclaration)fact).defines is not OMA df)
return null;
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(MMT_OMS_URI.pointNormalPlane))
{
//OMA pointAOMA = (OMA)planeOMA.arguments[0];
normal = (planeOMA.arguments[1].GetLambdaExpression().Compile() as Func<Vector3>)();
}
// In case of parametrized plane
else if (planeApplicant.Equals(MMT_OMS_URI.ParametrizedPlane))
{
Vector3 v = (planeOMA.arguments[1].GetLambdaExpression().Compile() as Func<Vector3>)();
Vector3 w = (planeOMA.arguments[2].GetLambdaExpression().Compile() as Func<Vector3>)();
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()];
float radius = ((OMF)df.arguments[2]).@float;
if (!FactOrganizer.AllFacts.ContainsKey(M_uri)
|| !FactOrganizer.AllFacts.ContainsKey(A_uri))
return null; //If dependent facts do not exist return null
return new CircleFact(M_uri, A_uri, radius, normal, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> "○" + Point1.Label;
/// <summary>
/// Constructs struct for right-angled MMT %Fact <see cref="AddFactResponse"/>
/// </summary>
/// <param name="Pid1"> <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>
public override MMTDeclaration MakeMMTDeclaration()
{
List<SOMDoc> outerArguments = new List<SOMDoc>
{
//CirclePlane,
new OMA(
//PointNormalPlane,
new OMS(MMT_OMS_URI.pointNormalPlane),
//planeArgs,
new List<SOMDoc> {
//base point of the circle plane?,
new OMS(Pid2),
//NormalVector,
new OMA(
//"Vector"
new OMS(MMT_OMS_URI.Tuple),
//normalArgs,
new List<SOMDoc> {
new OMF(normal.x),
new OMF(normal.y),
new OMF(normal.z)
}
),
}
),
//middlePoint,
new OMS(Pid1),
//Radius,
new OMF(radius),
};
// Do i need this here? doubt
SOMDoc tp = new OMS(MMT_OMS_URI.CircleType3d);
SOMDoc df = new OMA(new OMS(MMT_OMS_URI.MkCircle3d), outerArguments);
return new MMTSymbolDeclaration(Label, tp, df);
}
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> new string[] { Pid1, Pid2 };
/// \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, FactOrganizer organizer)
=> new CircleFact(old_to_new[this.Pid1], old_to_new[this.Pid2], this.radius, this.normal, organizer);
}
/// <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)FactOrganizer.AllFacts[Pid]; }
[JsonIgnore]
public CircleFact Circle { get => (CircleFact)FactOrganizer.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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public OnCircleFact(string pid, string cid, FactOrganizer organizer) : base(organizer)
{
this.Pid = pid;
this.Cid = cid; ;
SendToMMT();
}
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>
/// <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(ScrollFact)
public new static OnCircleFact parseFact(MMTDeclaration fact)
{
if (((MMTSymbolDeclaration)fact).type is not OMA type)
return null;
string circleUri = ((OMS)((OMA)type.arguments[0]).arguments[0]).uri;
string pointUri = ((OMS)((OMA)type.arguments[0]).arguments[1]).uri;
if (!FactOrganizer.AllFacts.ContainsKey(pointUri)
|| !FactOrganizer.AllFacts.ContainsKey(circleUri))
return null;
return new OnCircleFact(pointUri, circleUri, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> Point.Label + "∈" + Circle.Label;
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> 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, FactOrganizer organizer)
=> new OnCircleFact(old_to_new[this.Pid], old_to_new[this.Cid], 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.OnCircle),
new List<SOMDoc> {
new OMS(Cid),
new OMS(Pid),
}),});
SOMDoc df = null;
return new MMTSymbolDeclaration(Label, tp, df);
}
}
/// <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)FactOrganizer.AllFacts[Rid2]; }
[JsonIgnore]
public CircleFact Circle { get => (CircleFact)FactOrganizer.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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public AngleCircleLineFact(string cid1, string rid2, FactOrganizer organizer) : base(organizer)
{
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);
SendToMMT();
}
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>
/// <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(ScrollFact)
public new static AngleCircleLineFact parseFact(MMTDeclaration fact)
{
if (((MMTValueDeclaration)fact).lhs is not OMA lhs)
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 (((MMTValueDeclaration)fact).value is OMF oMFangle)
angle = oMFangle.@float;
string CircleUri = ((OMS)lhs.arguments[0]).uri;
string RayUri = ((OMS)lhs.arguments[1]).uri;
if (!FactOrganizer.AllFacts.ContainsKey(CircleUri)
|| !FactOrganizer.AllFacts.ContainsKey(RayUri))
return null;
return new AngleCircleLineFact(CircleUri, RayUri, angle, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> "∠" + Circle.Label + Ray.Label;
public override MMTDeclaration MakeMMTDeclaration()
{
SOMDoc lhs =
new OMA(
new OMS(MMT_OMS_URI.AnglePlaneLine),
new List<SOMDoc> {
new OMS(Cid1),
new OMS(Rid2),
}
);
SOMDoc valueTp = new OMS(MMT_OMS_URI.RealLit);
SOMDoc value = new OMF(angle);
return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
}
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> 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, FactOrganizer organizer)
=> new AngleCircleLineFact(old_to_new[this.Cid1], old_to_new[this.Rid2], organizer);
}
/// <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)FactOrganizer.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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public RadiusFact(string cid1, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = cid1;
this.rad = Circle.radius;
SendToMMT();
}
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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public RadiusFact(string Cid1, string backendURI, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = Cid1;
this._URI = backendURI;
_ = this.Label;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static RadiusFact parseFact(MMTDeclaration fact)
{
string CircleUri = ((OMS)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).uri;
if (!FactOrganizer.AllFacts.ContainsKey(CircleUri))
return null;
return new RadiusFact(CircleUri, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> "r " + Circle.Label;
/// <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 MMTDeclaration MakeMMTDeclaration()
{
SOMDoc lhs =
new OMA(
new OMS(MMT_OMS_URI.RadiusCircleMetric),
new List<SOMDoc> {
new OMS(Cid1),
}
);
SOMDoc valueTp = new OMS(MMT_OMS_URI.RealLit);
SOMDoc value = new OMF(rad);
return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
}
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> 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, FactOrganizer organizer)
=> new RadiusFact(old_to_new[this.Cid1], organizer);
}
/// <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)FactOrganizer.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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public AreaCircleFact(string cid1, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = cid1;
this.A = Circle.radius * Circle.radius * ((float)System.Math.PI);
SendToMMT();
}
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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public AreaCircleFact(string Cid1, string backendURI, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = Cid1;
this._URI = backendURI;
_ = this.Label;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static AreaCircleFact parseFact(MMTDeclaration fact)
{
string CircleUri = ((OMS)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).uri;
if (!FactOrganizer.AllFacts.ContainsKey(CircleUri))
return null;
return new AreaCircleFact(CircleUri, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> "A(" + Circle.Label + ")";
public override MMTDeclaration MakeMMTDeclaration()
{
SOMDoc lhs =
new OMA(
new OMS(MMT_OMS_URI.AreaCircle),
new List<SOMDoc> {
new OMS(Cid1),
}
);
SOMDoc valueTp = new OMS(MMT_OMS_URI.RealLit);
SOMDoc value = new OMF(A);
return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
}
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> 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, FactOrganizer organizer)
=> new AreaCircleFact(old_to_new[this.Cid1], organizer);
}
/// <summary>
/// The volume of a cone A defined by a base area <see cref="CircleFact">CircleFact</see>, an apex <see cref="PointFact">PointFact</see> and the volume as float
/// </summary>
public class ConeVolumeFact : FactWrappedCRTP<ConeVolumeFact>
{
/// <summary> a <see cref="CircleFact">CircleFact</see> describing the base area </summary>
public string Cid1;
[JsonIgnore]
public CircleFact Circle { get => (CircleFact)FactOrganizer.AllFacts[Cid1]; }
/// <summary> a <see cref="PointFact">PointFact</see> describing the apex point </summary>
public string Pid1;
[JsonIgnore]
public PointFact Point { get => (PointFact)FactOrganizer.AllFacts[Pid1]; }
/// <summary> the volume of the cone as a float </summary>
public float vol;
/// <summary> \copydoc Fact.Fact </summary>
public ConeVolumeFact() : base()
{
this.Cid1 = null;
this.Pid1 = null;
this.vol = 0.0f;
}
/// <summary>
/// Standard Constructor:
/// Initiates members and creates MMT %Fact Server-Side
/// </summary>
/// <param name="cid1">sets <see cref="Cid1"/></param>
/// <param name="pid1">sets <see cref="Pid1"/></param>
/// <param name="vol">sets <see cref="vol"/></param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public ConeVolumeFact(string cid1, string pid1, float vol, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = cid1;
this.Pid1 = pid1;
this.vol = vol;
SendToMMT();
}
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="Cid1">sets <see cref="Cid1"/></param>
/// <param name="Pid1">sets <see cref="Pid1"/></param>
/// <param name="volume">sets <see cref="vol"/></param>
/// <param name="backendURI">MMT URI</param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public ConeVolumeFact(string Cid1, string Pid1, float volume, string backendURI, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = Cid1;
this.Pid1 = Pid1;
this.vol = volume;
this._URI = backendURI;
_ = this.Label;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static ConeVolumeFact parseFact(MMTDeclaration fact)
{
if (((MMTValueDeclaration)fact).lhs is not OMA lhs)
return null;
string CircleUri = ((OMS)((OMA)lhs.arguments[0]).arguments[0]).uri;
string PointUri = ((OMS)((OMA)lhs.arguments[0]).arguments[1]).uri;
float volume = 0.0f;
if (((MMTValueDeclaration)fact).value is OMF oMFvolume)
volume = oMFvolume.@float;
if (!FactOrganizer.AllFacts.ContainsKey(CircleUri)
|| !FactOrganizer.AllFacts.ContainsKey(PointUri))
return null;
return new ConeVolumeFact(CircleUri, PointUri, volume, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> "V(" + Circle.Label + "," + Point.Label + ")";
public override MMTDeclaration MakeMMTDeclaration()
{
SOMDoc lhs =
new OMA(
new OMS(MMT_OMS_URI.VolumeCone),
new List<SOMDoc> {
new OMA(new OMS(MMT_OMS_URI.ConeOfCircleApex),
new List<SOMDoc> {
new OMS(Cid1),
new OMS(Pid1),
}
),
}
);
SOMDoc valueTp = new OMS(MMT_OMS_URI.RealLit);
SOMDoc value = new OMF(vol);
return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
}
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> new string[] { Cid1, Pid1 };
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(ConeVolumeFact f1, ConeVolumeFact f2)
=> DependentFactsEquivalent(f1, f2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
=> new ConeVolumeFact(old_to_new[this.Cid1], old_to_new[this.Pid1], this.vol, organizer);
}
/// <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)FactOrganizer.AllFacts[Cid1]; }
/// <summary> a <see cref="RayFact">Rayfact</see> describing the line </summary>
public string Lid1;
[JsonIgnore]
public AbstractLineFact Ray { get => (AbstractLineFact)FactOrganizer.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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public OrthogonalCircleLineFact(string cid1, string lid1, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = cid1;
this.Lid1 = lid1;
Math3d.LinePlaneIntersection(out intersection, Ray.Point1.Position, Ray.Dir, Circle.normal, Circle.Position);
SendToMMT();
}
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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public OrthogonalCircleLineFact(string Cid1, string Lid1, string backendURI, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = Cid1;
this.Lid1 = Lid1;
this._URI = backendURI;
_ = this.Label;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static OrthogonalCircleLineFact parseFact(MMTDeclaration fact)
{
if (((MMTSymbolDeclaration)fact).type is not OMA type)
return null;
string CircleUri = ((OMS)((OMA)type.arguments[0]).arguments[0]).uri;
string LineUri = ((OMS)((OMA)type.arguments[0]).arguments[1]).uri;
if (!FactOrganizer.AllFacts.ContainsKey(CircleUri)
|| !FactOrganizer.AllFacts.ContainsKey(LineUri))
return null;
return new OrthogonalCircleLineFact(CircleUri, LineUri, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> Circle.Label + "⊥" + Ray.Label;
public override MMTDeclaration MakeMMTDeclaration()
{
SOMDoc tp = new OMA(
new OMS(MMT_OMS_URI.Ded),
new List<SOMDoc>{
new OMA(
new OMS(MMT_OMS_URI.OrthoCircleLine),
new List<SOMDoc>{
new OMS(Cid1),
new OMS(Lid1),
}
),
}
);
SOMDoc df = null;
return new MMTSymbolDeclaration(this.Label, tp, df);
}
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> 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, FactOrganizer organizer)
=> new OrthogonalCircleLineFact(old_to_new[this.Cid1], old_to_new[this.Lid1], organizer);
}
/// <summary>
/// The volume of a cone A defined by a base area <see cref="CircleFact">CircleFact</see>, a top area <see cref="CircleFact">CircleFact</see> and the volume as float
/// </summary>
public class TruncatedConeVolumeFact : FactWrappedCRTP<TruncatedConeVolumeFact>
{
/// <summary> a <see cref="CircleFact">CircleFact</see> describing the base area </summary>
public string Cid1;
[JsonIgnore]
public CircleFact Circle1 { get => (CircleFact)FactOrganizer.AllFacts[Cid1]; }
/// <summary> a <see cref="CircleFact">CircleFact</see> describing the top area </summary>
public string Cid2;
[JsonIgnore]
public CircleFact Circle2 { get => (CircleFact)FactOrganizer.AllFacts[Cid2]; }
/// <summary> the volume of Truncated the cone as a float </summary>
public float vol;
/// <summary> a proof that both circles have not the same size </summary>
public string unequalCirclesProof;
/// <summary> OMA proof that the two circles are parallel </summary>
public OMA proof;
/// <summary> \copydoc Fact.Fact </summary>
public TruncatedConeVolumeFact() : base()
{
this.Cid1 = null;
this.Cid2 = null;
this.vol = 0.0f;
this.unequalCirclesProof = null;
this.proof = 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>
/// <param name="vol">sets <see cref="vol"/></param>
/// <param name="proof">sets <see cref="proof"/></param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public TruncatedConeVolumeFact(string cid1, string cid2, float vol, string unequalproof, OMA proof, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = cid1;
this.Cid2 = cid2;
this.proof = proof;
this.unequalCirclesProof = unequalproof;
this.vol = vol;
SendToMMT();
}
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="volume">sets <see cref="vol"/></param>
/// <param name="proof">sets <see cref="proof"/></param>
/// <param name="backendURI">MMT URI</param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public TruncatedConeVolumeFact(string Cid1, string Cid2, float volume, string unequalproof, OMA proof, string backendURI, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = Cid1;
this.Cid2 = Cid2;
this.vol = volume;
this.proof = proof;
this.unequalCirclesProof = unequalproof;
this._URI = backendURI;
_ = this.Label;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static TruncatedConeVolumeFact parseFact(MMTDeclaration fact)
{
string Circle1Uri = ((OMS)((OMA)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).arguments[0]).uri;
string Circle2Uri = ((OMS)((OMA)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).arguments[1]).uri;
float volume = ((OMF)((MMTValueDeclaration)fact).value).@float;
string UnEqualCirclesProof = ((OMS)(((OMA)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).arguments[2])).uri;
OMA proof = (OMA)(((OMA)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).arguments[3]);
if (!FactOrganizer.AllFacts.ContainsKey(Circle1Uri)
|| !FactOrganizer.AllFacts.ContainsKey(Circle2Uri))
return null;
return new TruncatedConeVolumeFact(Circle1Uri, Circle2Uri, volume, UnEqualCirclesProof, proof, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> "V(" + Circle1.Label + "," + Circle2.Label + ")";
public override MMTDeclaration MakeMMTDeclaration()
{
SOMDoc lhs =
new OMA(
new OMS(MMT_OMS_URI.TruncatedVolumeCone),
new List<SOMDoc> {
new OMS(Cid1),
new OMS(Cid2),
new OMS(unequalCirclesProof),
proof,
}
);
SOMDoc valueTp = new OMS(MMT_OMS_URI.RealLit);
SOMDoc value = new OMF(vol);
return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
}
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> new string[] { Cid1, Cid2 };
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(TruncatedConeVolumeFact f1, TruncatedConeVolumeFact f2)
=> DependentFactsEquivalent(f1, f2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
=> new TruncatedConeVolumeFact(old_to_new[this.Cid1], old_to_new[this.Cid2], this.vol, old_to_new[this.unequalCirclesProof], this.proof, organizer);
}
/// <summary>
/// The volume of a cylinder defined by a base area <see cref="CircleFact">CircleFact</see>, a top area <see cref="CircleFact">CircleFact</see> and the volume as float
/// </summary>
public class CylinderVolumeFact : FactWrappedCRTP<CylinderVolumeFact>
{
/// <summary> a <see cref="CircleFact">CircleFact</see> describing the base area </summary>
public string Cid1;
[JsonIgnore]
public CircleFact Circle1 { get => (CircleFact)FactOrganizer.AllFacts[Cid1]; }
/// <summary> a <see cref="CircleFact">CircleFact</see> describing the top area </summary>
public string Cid2;
[JsonIgnore]
public CircleFact Circle2 { get => (CircleFact)FactOrganizer.AllFacts[Cid2]; }
/// <summary> the volume of the cylinder as a float </summary>
public float vol;
/// <summary> a proof that both circles have the same size </summary>
public string equalCirclesProof;
/// <summary> OMA proof that the two circles are parallel </summary>
public OMA proof;
/// <summary> \copydoc Fact.Fact </summary>
public CylinderVolumeFact() : base()
{
this.Cid1 = null;
this.Cid2 = null;
this.vol = 0.0f;
this.proof = null;
this.equalCirclesProof = 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>
/// <param name="vol">sets <see cref="vol"/></param>
/// <param name="proof">sets <see cref="proof"/></param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public CylinderVolumeFact(string cid1, string cid2, float vol, string eqProof, OMA proof, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = cid1;
this.Cid2 = cid2;
this.proof = proof;
this.equalCirclesProof = eqProof;
this.vol = vol;
SendToMMT();
}
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="volume">sets <see cref="vol"/></param>
/// <param name="proof">sets <see cref="proof"/></param>
/// <param name="backendURI">MMT URI</param>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public CylinderVolumeFact(string Cid1, string Cid2, float volume, string eqProof, OMA proof, string backendURI, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = Cid1;
this.Cid2 = Cid2;
this.vol = volume;
this.proof = proof;
this.equalCirclesProof = eqProof;
this._URI = backendURI;
_ = this.Label;
}
/// \copydoc Fact.parseFact(ScrollFact)
public new static CylinderVolumeFact parseFact(MMTDeclaration fact)
{
string Circle1Uri = ((OMS)((OMA)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).arguments[0]).uri;
string Circle2Uri = ((OMS)((OMA)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).arguments[1]).uri;
float volume = ((OMF)((MMTValueDeclaration)fact).value).@float;
string EqualCirclesProof = ((OMS)(((OMA)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).arguments[2])).uri;
OMA proof = (OMA)(((OMA)((OMA)((MMTValueDeclaration)fact).lhs).arguments[0]).arguments[3]);
if (!FactOrganizer.AllFacts.ContainsKey(Circle1Uri)
|| !FactOrganizer.AllFacts.ContainsKey(Circle2Uri))
return null;
return new CylinderVolumeFact(Circle1Uri, Circle2Uri, volume, EqualCirclesProof, proof, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> "V(" + Circle1.Label + "," + Circle2.Label + ")";
public override MMTDeclaration MakeMMTDeclaration()
{
SOMDoc lhs =
new OMA(
new OMS(MMT_OMS_URI.CylinderVolume),
new List<SOMDoc> {
new OMS(Cid1),
new OMS(Cid2),
new OMS(equalCirclesProof),
proof,
}
);
SOMDoc valueTp = new OMS(MMT_OMS_URI.RealLit);
SOMDoc value = new OMF(vol);
return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
}
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> new string[] { Cid1, Cid2, equalCirclesProof };
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(CylinderVolumeFact f1, CylinderVolumeFact f2)
=> DependentFactsEquivalent(f1, f2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
=> new CylinderVolumeFact(old_to_new[this.Cid1], old_to_new[this.Cid2], this.vol, old_to_new[this.equalCirclesProof], this.proof, organizer);
}
/// <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)FactOrganizer.AllFacts[Cid1]; }
[JsonIgnore]
public CircleFact Circle2 { get => (CircleFact)FactOrganizer.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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public EqualCirclesFact(string cid1, string cid2, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = cid1;
this.Cid2 = cid2;
SendToMMT();
}
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>
/// <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(ScrollFact)
public new static EqualCirclesFact parseFact(MMTDeclaration fact)
{
if (((MMTSymbolDeclaration)fact).type is not OMA proof_OMA) // proof DED
return null;
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 (!FactOrganizer.AllFacts.ContainsKey(circleAUri)
|| !FactOrganizer.AllFacts.ContainsKey(circleBUri))
return null;
return new EqualCirclesFact(circleAUri, circleBUri, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> Circle1.Label + " ≠ " + Circle2.Label;
public override MMTDeclaration MakeMMTDeclaration()
{
SOMDoc tp = new OMA(
new OMS(MMT_OMS_URI.Ded),
new List<SOMDoc> {
new OMA(
new OMS(MMT_OMS_URI.EqualityCircles),
new List<SOMDoc> {
new OMS(Cid1),
new OMS(Cid2),
}
)
}
);
SOMDoc df = null;
return new MMTSymbolDeclaration(this.Label, tp, df);
}
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> 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, FactOrganizer organizer)
=> new EqualCirclesFact(old_to_new[this.Cid1], old_to_new[this.Cid2], organizer);
}
/// <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)FactOrganizer.AllFacts[Cid1]; }
[JsonIgnore]
public CircleFact Circle2 { get => (CircleFact)FactOrganizer.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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public UnEqualCirclesFact(string cid1, string cid2, FactOrganizer organizer) : base(organizer)
{
this.Cid1 = cid1;
this.Cid2 = cid2;
SendToMMT();
}
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>
/// <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(ScrollFact)
public new static UnEqualCirclesFact parseFact(MMTDeclaration fact)
{
if (((MMTSymbolDeclaration)fact).type is not OMA proof_OMA) // proof DED
return null;
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 (!FactOrganizer.AllFacts.ContainsKey(circleAUri)
|| !FactOrganizer.AllFacts.ContainsKey(circleBUri))
return null;
return new UnEqualCirclesFact(circleAUri, circleBUri, fact.@ref.uri, StageStatic.stage.factState);
}
/// \copydoc Fact.generateLabel
protected override string generateLabel()
=> Circle1.Label + " = " + Circle2.Label;
public override MMTDeclaration MakeMMTDeclaration()
{
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(Cid1),
new OMS(Cid2),
}),});
SOMDoc df = null;
return new MMTSymbolDeclaration(this.Label, tp, df);
}
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => true;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> new string[] { Cid1, Cid2 };
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(UnEqualCirclesFact f1, UnEqualCirclesFact f2)
=> DependentFactsEquivalent(f1, f2);
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
=> new UnEqualCirclesFact(old_to_new[this.Cid1], old_to_new[this.Cid2], organizer);
}
/// <summary>
///
/// </summary>
/// <seealso cref="SOMDoc.MakeList(string[], string)"/>
/// <remarks>Needed to refere to lists serverside</remarks>
public class ListFact : FactWrappedCRTP<ListFact>
{
public string[] lids;
//public string typeURI;
//[JsonIgnore]
//public Type type => MMT_OMS_URI.OMS_TO_TYPE[typeURI];
public ListFact() : base()
{
lids = new string[0];
}
public ListFact(string[] lids, FactOrganizer organizer) : base(organizer)
{
this.lids = lids;
SendToMMT();
}
public ListFact(string[] lids, string backendURI, FactOrganizer organizer) : base(organizer)
{
this.lids = lids;
_URI = backendURI;
}
protected override bool EquivalentWrapped(ListFact f1, ListFact f2)
=> //f1.typeURI == f2.typeURI &&
DependentFactsEquivalent(f1, f2);
public override bool HasDependentFacts
=> true;
protected override string[] GetGetDependentFactIds()
=> lids;
public override MMTDeclaration MakeMMTDeclaration()
{
OMA List = SOMDoc.MakeList(lids, typeof(OMS));
return new MMTSymbolDeclaration(Label, List.applicant, List.applicant);
}
public static new ListFact parseFact(MMTDeclaration fact)
=> new(parseFactList(fact).ToArray(), fact.@ref.uri, StageStatic.stage.factState);
public static List<string> parseFactList(MMTDeclaration decl)
{
if (decl is not MMTSymbolDeclaration mMTSymbol)
return null;
List<string> ret = new();
SOMDoc next_element = mMTSymbol.defines;
while (true)
{
if (next_element is not OMA current_element)
return ret;
switch (current_element.arguments.Count)
{
case 2:
if (current_element.arguments[1] is not OMS oMS)
return ret;
ret.Add(oMS.uri);
next_element = current_element.arguments[0];
break;
case 0:
case 1:
default:
return ret;
}
}
}
public static List<T> parseFactList<T>(MMTDeclaration decl)
{
if (decl is not MMTSymbolDeclaration mMTSymbol)
return null;
List<T> ret = new();
SOMDoc next_element = mMTSymbol.defines;
while (true)
{
if (next_element is not OMA current_element)
return ret;
switch (current_element.arguments.Count)
{
case 2:
ret.Add((current_element.arguments[1].GetLambdaExpression().Compile() as Func<T>)());
next_element = current_element.arguments[0];
break;
case 0:
case 1:
default:
return ret;
}
}
}
protected override void RecalculateTransform() { }
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
{
throw new NotImplementedException();
}
}
#pragma warning disable // Testing...
/// TEST FACT
/// use this if you need to test certain implementations of facts.
/// <summary>
/// just for testing purposes
/// </summary>
public class TestFact : FactWrappedCRTP<TestFact>
{
/// <summary> \copydoc Fact.Fact </summary>
public TestFact() : base()
{
}
/// <summary>
/// Standard Constructor:
/// Initiates members 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>
/// <param name="organizer">sets <see cref="Fact._Facts"/></param>
public TestFact(FactOrganizer organizer) : base(organizer)
{
SendToMMT();
}
protected override void RecalculateTransform() { }
/// <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(ScrollFact)
public new static TestFact parseFact(MMTDeclaration 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()
=> "test";
/// \copydoc Fact.hasDependentFacts
public override bool HasDependentFacts => false;
/// \copydoc Fact.getDependentFactIds
protected override string[] GetGetDependentFactIds()
=> new string[] { };
/// \copydoc Fact.GetHashCode
public override int GetHashCode()
=> base.GetHashCode();// this.Pid1.GetHashCode() ^ this.Pid2.GetHashCode();
/// \copydoc Fact.Equivalent(Fact, Fact)
protected override bool EquivalentWrapped(TestFact f1, TestFact f2)
{
return DependentFactsEquivalent(f1, f2);
}
protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new, FactOrganizer organizer)
=> new TestFact(organizer);
public override MMTDeclaration MakeMMTDeclaration()
{
throw new NotImplementedException();
}
}
#pragma warning restore // Testing over