diff --git a/Assets/Scripts/InteractionEngine/Fact.cs b/Assets/Scripts/InteractionEngine/Fact.cs
index 37e69962d60504bb63ce233fd60bbfb3608002ab..097bd482a7830572be870cd28f5a21ff9ba1638f 100644
--- a/Assets/Scripts/InteractionEngine/Fact.cs
+++ b/Assets/Scripts/InteractionEngine/Fact.cs
@@ -95,20 +95,12 @@ public PointFact(int i, Vector3 P, Vector3 N)
MMTTerm df = new OMA(new OMS(MMTURIs.Tuple), arguments);
//TODO: rework fact list + labeling
- MMTDeclaration mmtDecl = new MMTDeclaration(this.Label, tp, df);
- string body = ToJson(mmtDecl);
+ MMTSymbolDeclaration mmtDecl = new MMTSymbolDeclaration(this.Label, tp, df);
+ string body = MMTSymbolDeclaration.ToJson(mmtDecl);
AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress+"/fact/add", body);
this.backendURI = res.uri;
Debug.Log(this.backendURI);
-
- /*
- * old approach
- string body = @"{ ""a"":" + format(P.x) + @"," + @"""b"":" + format(P.y) + @"," + @"""c"":" + format(P.y) + "}";
- Debug.Log(body);
- AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress+"/fact/add/vector", body);
- this.backendURI = res.uri;
- */
}
public PointFact(int i, float a, float b, float c, string uri)
@@ -122,9 +114,6 @@ public PointFact(int i, float a, float b, float c, string uri)
}
-
-
-
public class LineFact : DirectedFact
{
//Id's of the 2 Point-Facts that are connected
@@ -144,72 +133,24 @@ public LineFact(int i, int pid1, int pid2)
string p2URI = pf2.backendURI;
float v = (pf1.Point - pf2.Point).magnitude;
-
- /* string body = @"{ ""pointA"":""" + p1URI + @"""," + @"""pointB"":""" + p2URI + @"""," + @"""value"":" + format(v) + "}";
- AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress+"/fact/add/distance", body);
- */
- MMTTerm tp =
+ MMTTerm lhs =
new OMA(
- new OMS(MMTURIs.Ded),
+ new OMS(MMTURIs.Metric),
new List<MMTTerm> {
- new OMA(
- new OMS(MMTURIs.Eq),
- new List<MMTTerm> {
- new OMA(
- new OMS(MMTURIs.Metric),
- new List<MMTTerm>{
- new OMS(p1URI),
- new OMS(p2URI)}
- ),
- new OMF(v)
- }
- )
+ new OMS(p1URI),
+ new OMS(p2URI)
}
);
- //github + predikate => -ded -eq
-
-
+ MMTTerm rhs = new OMF(v);
- MMTTerm df = null;
//see point label
- MMTDeclaration mmtDecl = new MMTDeclaration(this.Label, tp, df);
- string body = ToJson(mmtDecl);
+ MMTValueDeclaration mmtDecl = new MMTValueDeclaration(this.Label, lhs, rhs);
+ string body = MMTDeclaration.ToJson(mmtDecl);
AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress + "/fact/add", body);
this.backendURI = res.uri;
- // this.backendValueURI = res.factValUri;
- // this.flippedFact = new LineFact(pid2, pid1);
- }
-
- /* // to create flipped fact
- public LineFact(int pid1, int pid2)
- {
- this.Pid1 = pid1;
- this.Pid2 = pid2;
- PointFact pf1 = CommunicationEvents.Facts.Find((x => x.Id == pid1)) as PointFact;
- PointFact pf2 = CommunicationEvents.Facts.Find((x => x.Id == pid2)) as PointFact;
- string p1URI = pf1.backendURI;
- string p2URI = pf2.backendURI;
- float v = (pf1.Point - pf2.Point).magnitude;
- string body = @"{ ""pointA"":""" + p1URI + @"""," + @"""pointB"":""" + p2URI + @"""," + @"""value"":" + format(v) + "}";
- AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress+"/fact/add/distance", body);
- this.backendURI = res.uri;
- this.backendValueURI = res.factValUri;
+ Debug.Log(this.backendURI);
}
-
- //pushout return
- public LineFact(int i, int pid1, int pid2, string uri, string valuri)
- {
- this.Id = i;
- this.Pid1 = pid1;
- this.Pid2 = pid2;
- this.backendURI = uri;
- this.backendValueURI = valuri;
- this.flippedFact = new LineFact(pid2, pid1);
-
- }*/
-
-
}
public class OpenLineFact : Fact
@@ -298,58 +239,34 @@ public AngleFact(int i, int pid1, int pid2, int pid3)
PointFact pf1 = CommunicationEvents.Facts.Find((x => x.Id == pid1)) as PointFact;
PointFact pf2 = CommunicationEvents.Facts.Find((x => x.Id == pid2)) as PointFact;
PointFact pf3 = CommunicationEvents.Facts.Find((x => x.Id == pid3)) as PointFact;
-
+ string p1URI = pf1.backendURI;
+ string p2URI = pf2.backendURI;
+ string p3URI = pf3.backendURI;
float v = Vector3.Angle((pf1.Point - pf2.Point), (pf3.Point - pf2.Point));
if (Mathf.Abs(v - 90.0f) < 0.01) v = 90.0f;
+
Debug.Log("angle: " + v);
- string body = @"{" +
- @"""left"":""" + pf1.backendURI + @"""," +
- @"""middle"":""" + pf2.backendURI + @"""," +
- @"""right"":""" + pf3.backendURI + @"""," +
- @"""value"":" + format(v) +
- "}";
- Debug.Log(body);
- AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress+"/fact/add/angle", body);
- this.backendURI = res.uri;
- // this.backendValueURI = res.factValUri;
- this.flippedFact = new AngleFact(pid3, pid2, pid1);
- }
- //to create flipped fact
- public AngleFact(int pid1, int pid2, int pid3)
- {
- this.Pid1 = pid1;
- this.Pid2 = pid2;
- this.Pid3 = pid3;
- PointFact pf1 = CommunicationEvents.Facts.Find((x => x.Id == pid1)) as PointFact;
- PointFact pf2 = CommunicationEvents.Facts.Find((x => x.Id == pid2)) as PointFact;
- PointFact pf3 = CommunicationEvents.Facts.Find((x => x.Id == pid3)) as PointFact;
+ MMTTerm lhs =
+ new OMA(
+ new OMS(MMTURIs.Angle),
+ new List<MMTTerm> {
+ new OMS(p1URI),
+ new OMS(p2URI),
+ new OMS(p3URI)
+ }
+ );
+
+ MMTTerm rhs = new OMF(v);
+
+ //see point label
+ MMTValueDeclaration mmtDecl = new MMTValueDeclaration(this.Label, lhs, rhs);
+ string body = MMTDeclaration.ToJson(mmtDecl);
- float v = Vector3.Angle((pf1.Point - pf2.Point), (pf3.Point - pf2.Point));
- if (Mathf.Abs(v - 90.0f) < 0.01) v = 90.0f;
- Debug.Log("angle: " + v);
- string body = @"{" +
- @"""left"":""" + pf1.backendURI + @"""," +
- @"""middle"":""" + pf2.backendURI + @"""," +
- @"""right"":""" + pf3.backendURI + @"""," +
- @"""value"":" + format(v) +
- "}";
Debug.Log(body);
- AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress+"/fact/add/angle", body);
+ AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress+"/fact/add", body);
this.backendURI = res.uri;
- // this.backendValueURI = res.factValUri;
- }
-
- //pushout return
- public AngleFact(int i, int pid1, int pid2, int pid3, string uri, string valuri)
- {
- this.Id = i;
- this.Pid1 = pid1;
- this.Pid2 = pid2;
- this.Pid3 = pid3;
- this.backendURI = uri;
- this.backendValueURI = valuri;
- this.flippedFact = new AngleFact(pid3, pid2, pid1);
+ Debug.Log(this.backendURI);
}
}
diff --git a/Assets/Scripts/InventoryStuff/Inventory.meta b/Assets/Scripts/InventoryStuff/Inventory.meta
deleted file mode 100644
index 354d69c1005dcfdcdfd0baaabed1376dd2fb318a..0000000000000000000000000000000000000000
--- a/Assets/Scripts/InventoryStuff/Inventory.meta
+++ /dev/null
@@ -1,8 +0,0 @@
-fileFormatVersion: 2
-guid: 8c00acf0711308b4eac44fb21f04a06f
-folderAsset: yes
-DefaultImporter:
- externalObjects: {}
- userData:
- assetBundleName:
- assetBundleVariant:
diff --git a/Assets/Scripts/JSONManager.cs b/Assets/Scripts/JSONManager.cs
index ccafd3bee97d4967b888c95d36056d90e476c800..11eefbbc45063627f2bf4b2b26671162a9720685 100644
--- a/Assets/Scripts/JSONManager.cs
+++ b/Assets/Scripts/JSONManager.cs
@@ -14,6 +14,7 @@ public class MMTURICollection
public string Ded = "http://mathhub.info/MitM/Foundation?Logic?ded";
public string Eq = "http://mathhub.info/MitM/Foundation?Logic?eq";
public string Metric = "http://mathhub.info/MitM/core/geometry?Geometry?Common?metric";
+ public string Angle = "http://mathhub.info/MitM/core/geometry?Geometry?Common?angle_between";
public string Sketch = "http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch";
}
@@ -86,17 +87,27 @@ public OMF(float f)
}
}
-
-
-
-
public class MMTDeclaration
+ {
+ public static MMTDeclaration FromJson(string json)
+ {
+ MMTDeclaration mmtDecl = JsonConvert.DeserializeObject<MMTDeclaration>(json);
+ return mmtDecl;
+ }
+ public static string ToJson(MMTDeclaration mmtDecl)
+ {
+ string json = JsonConvert.SerializeObject(mmtDecl);
+ return json;
+ }
+ }
+
+ public class MMTSymbolDeclaration : MMTDeclaration
{
public string label;
public MMTTerm tp;
public MMTTerm df;
- public MMTDeclaration(string label, MMTTerm tp, MMTTerm df)
+ public MMTSymbolDeclaration(string label, MMTTerm tp, MMTTerm df)
{
this.label = label;
this.tp = tp;
@@ -104,16 +115,18 @@ public MMTDeclaration(string label, MMTTerm tp, MMTTerm df)
}
}
-
- public static MMTDeclaration FromJson(string json)
+ public class MMTValueDeclaration : MMTDeclaration
{
- MMTDeclaration mmtDecl = JsonConvert.DeserializeObject<MMTDeclaration>(json);
- return mmtDecl;
- }
- public static string ToJson(MMTDeclaration mmtDecl)
- {
- string json = JsonConvert.SerializeObject(mmtDecl);
- return json;
+ public string label;
+ public MMTTerm lhs;
+ public MMTTerm rhs;
+
+ public MMTValueDeclaration(string label, MMTTerm lhs, MMTTerm rhs)
+ {
+ this.label = label;
+ this.lhs = lhs;
+ this.rhs = rhs;
+ }
}
}
diff --git a/Assets/StreamingAssets.meta b/Assets/StreamingAssets.meta
deleted file mode 100644
index 7a25ae40aa44a6a0fc806ba87069449a4c6a6d6f..0000000000000000000000000000000000000000
--- a/Assets/StreamingAssets.meta
+++ /dev/null
@@ -1,8 +0,0 @@
-fileFormatVersion: 2
-guid: 809deaa1d951e5741bce0ace20cdaed8
-folderAsset: yes
-DefaultImporter:
- externalObjects: {}
- userData:
- assetBundleName:
- assetBundleVariant:
diff --git a/ProjectSettings/ProjectVersion.txt b/ProjectSettings/ProjectVersion.txt
index 7404e2513688bc5aab9d111c3b6dbd681ba74e05..4b6255b417e38275e0bcc9d7e1543b961e589d45 100644
--- a/ProjectSettings/ProjectVersion.txt
+++ b/ProjectSettings/ProjectVersion.txt
@@ -1,2 +1,2 @@
-m_EditorVersion: 2019.4.1f1
-m_EditorVersionWithRevision: 2019.4.1f1 (e6c045e14e4e)
+m_EditorVersion: 2019.4.3f1
+m_EditorVersionWithRevision: 2019.4.3f1 (f880dceab6fe)