diff --git a/Assets/Scenes/TreeWorld_02.unity b/Assets/Scenes/TreeWorld_02.unity
index 947462c0b74a8d09f8b84f136bd6518c631a7d4b..e5643ffc183324e7fa6f48487b004fe3643ebc53 100644
--- a/Assets/Scenes/TreeWorld_02.unity
+++ b/Assets/Scenes/TreeWorld_02.unity
@@ -41107,7 +41107,7 @@ PrefabInstance:
- target: {fileID: 2089306640899292912, guid: 4d99275c6663c25469ad3b65efcd4f5f,
type: 3}
propertyPath: m_AnchoredPosition.y
- value: -0.00035664605
+ value: -0.000012699486
objectReference: {fileID: 0}
- target: {fileID: 2524590709578595355, guid: 4d99275c6663c25469ad3b65efcd4f5f,
type: 3}
diff --git a/Assets/Scripts/InteractionEngine/Fact.cs b/Assets/Scripts/InteractionEngine/Fact.cs
index a63e2dd3b75d94c06cc682f5a388239ab7cd0ffe..13a8e445269a282f8c6dfdb24e899819a1e80e0d 100644
--- a/Assets/Scripts/InteractionEngine/Fact.cs
+++ b/Assets/Scripts/InteractionEngine/Fact.cs
@@ -1,6 +1,8 @@
-using System.Collections.Generic;
+using System;
+using System.Collections.Generic;
using UnityEngine;
using UnityEngine.Networking;
+using static JSONManager;
public abstract class Fact
{
@@ -23,8 +25,9 @@ public abstract class DirectedFact : Fact
public class AddFactResponse
{
//class to Read AddFact Responses.
- public string factUri;
- public string factValUri;
+ // public string factUri;
+ // public string factValUri;
+ public string uri;
public static AddFactResponse sendAdd(string path, string body)
{
@@ -69,29 +72,31 @@ public PointFact(int i, Vector3 P, Vector3 N)
this.Point = P;
this.Normal = N;
- List<JSONManager.MMTTerm> arguments = new List<JSONManager.MMTTerm>
+ List<MMTTerm> arguments = new List<MMTTerm>
{
- new JSONManager.OMF(P.x),
- new JSONManager.OMF(P.y),
- new JSONManager.OMF(P.z)
+ new OMF(P.x),
+ new OMF(P.y),
+ new OMF(P.z)
};
//OMS constructor generates full URI
- JSONManager.MMTTerm tp = new JSONManager.OMS("point");
- JSONManager.MMTTerm df = new JSONManager.OMA(new JSONManager.OMS("tuple"), arguments);
+ MMTTerm tp = new OMS(MMTURIs.Point);
+ MMTTerm df = new OMA(new OMS(MMTURIs.Tuple), arguments);
- JSONManager.MMTDeclaration mmtDecl = new JSONManager.MMTDeclaration("test", tp, df);
- string body = JSONManager.ToJson(mmtDecl);
+ //TODO: rework fact list + labeling
+ MMTDeclaration mmtDecl = new MMTDeclaration(((Char)(64 + Id + 1)).ToString(), tp, df);
+ string body = ToJson(mmtDecl);
AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress+"/fact/add", body);
- this.backendURI = res.factUri;
+ 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.factUri;
+ this.backendURI = res.uri;
*/
}
@@ -127,14 +132,41 @@ public LineFact(int i, int pid1, int pid2)
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.factUri;
- this.backendValueURI = res.factValUri;
- this.flippedFact = new LineFact(pid2, pid1);
+
+
+ /* string body = @"{ ""pointA"":""" + p1URI + @"""," + @"""pointB"":""" + p2URI + @"""," + @"""value"":" + format(v) + "}";
+ AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress+"/fact/add/distance", body);
+ */
+ MMTTerm tp =
+ new OMA(
+ new OMS(MMTURIs.Ded),
+ 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)
+ }
+ )
+ }
+ );
+
+ MMTTerm df = null;
+ //see point label
+ MMTDeclaration mmtDecl = new MMTDeclaration(((Char)(64 + Id + 1)).ToString(), tp, df);
+ string body = 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
+ /* // to create flipped fact
public LineFact(int pid1, int pid2)
{
this.Pid1 = pid1;
@@ -146,7 +178,7 @@ public LineFact(int pid1, int pid2)
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.factUri;
+ this.backendURI = res.uri;
this.backendValueURI = res.factValUri;
}
@@ -160,7 +192,7 @@ public LineFact(int i, int pid1, int pid2, string uri, string valuri)
this.backendValueURI = valuri;
this.flippedFact = new LineFact(pid2, pid1);
- }
+ }*/
}
@@ -192,8 +224,8 @@ public RayFact(int i, int pid1, int pid2)
//TODO: fix body
string body = @"{ ""base"":""" + p1URI + @"""," + @"""second"":""" + p2URI + @"""" + "}";
AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress+"/fact/add/line", body);
- this.backendURI = res.factUri;
- this.backendValueURI = res.factValUri;
+ this.backendURI = res.uri;
+ // this.backendValueURI = res.factValUri;
}
public RayFact(int i, int pid1, int pid2, string uri, string valuri)
@@ -225,8 +257,8 @@ public OnLineFact(int i, int pid, int lid)
string lURI = lf.backendURI;
string body = @"{ ""vector"":""" + pURI + @"""," + @"""line"":""" + lURI + @"""" + "}";
AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress+"/fact/add/onLine", body);
- this.backendURI = res.factUri;
- this.backendValueURI = res.factValUri;
+ this.backendURI = res.uri;
+ // this.backendValueURI = res.factValUri;
Debug.Log("created onLine" + this.backendURI + " " + this.backendValueURI);
}
@@ -263,8 +295,8 @@ public AngleFact(int i, int pid1, int pid2, int pid3)
"}";
Debug.Log(body);
AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress+"/fact/add/angle", body);
- this.backendURI = res.factUri;
- this.backendValueURI = res.factValUri;
+ this.backendURI = res.uri;
+ // this.backendValueURI = res.factValUri;
this.flippedFact = new AngleFact(pid3, pid2, pid1);
}
@@ -289,8 +321,8 @@ public AngleFact(int pid1, int pid2, int pid3)
"}";
Debug.Log(body);
AddFactResponse res = AddFactResponse.sendAdd(CommunicationEvents.ServerAdress+"/fact/add/angle", body);
- this.backendURI = res.factUri;
- this.backendValueURI = res.factValUri;
+ this.backendURI = res.uri;
+ // this.backendValueURI = res.factValUri;
}
//pushout return
diff --git a/Assets/Scripts/InventoryStuff/ScrollDetails.cs b/Assets/Scripts/InventoryStuff/ScrollDetails.cs
index 2715bba29d3f1d7da538367fe205867806690bc1..210867e59de974d401d74ba901da9e8c05fe1173 100644
--- a/Assets/Scripts/InventoryStuff/ScrollDetails.cs
+++ b/Assets/Scripts/InventoryStuff/ScrollDetails.cs
@@ -321,7 +321,7 @@ private void readPushout(string txt)
int id = factManager.GetFirstEmptyID();
int pid1 = getIdforBackendURI(f.pointA);
int pid2 = getIdforBackendURI(f.pointB);
- LineFact lf = new LineFact(id, pid1, pid2, f.uri, f.value);
+ LineFact lf = new LineFact();//id, pid1, pid2, f.uri, f.value);
CommunicationEvents.Facts.Insert(id, lf);
CommunicationEvents.AddFactEvent.Invoke(lf);
CommunicationEvents.PushoutFactEvent.Invoke(lf);
diff --git a/Assets/Scripts/JSONManager.cs b/Assets/Scripts/JSONManager.cs
index e1e552bbfe4667e18fd0f579d3c728e1da1974e4..a0049c8940e6b620249ad429bd12687069d045c8 100644
--- a/Assets/Scripts/JSONManager.cs
+++ b/Assets/Scripts/JSONManager.cs
@@ -4,17 +4,32 @@
using System.Collections.Generic;
using UnityEngine;
+
+public class MMTURICollection
+{
+ public string Point = "http://mathhub.info/MitM/core/geometry?3DGeometry?point";
+ public string Tuple = "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Tuple";
+ public string Line_type = "http://mathhub.info/MitM/core/geometry?Geometry?Common?line_type";
+ public string LineOf = "http://mathhub.info/MitM/core/geometry?Geometry?Common?lineOf";
+ 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 Sketch = "http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch";
+}
+
public static class JSONManager
{
+ //could init the strings of MMTURIs with JSON or other settings file instead
+ public static MMTURICollection MMTURIs = new MMTURICollection();
+ /*
public static Dictionary<string, string> URIDictionary = new Dictionary<string, string> {
{"point", "http://mathhub.info/MitM/core/geometry?3DGeometry?point" },
{"tuple", "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Tuple"},
{"line", "http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type" },
{"distance", "http://mathhub.info/MitM/core/geometry?Geometry/Common?lineOf" }
};
-
-
+ */
[JsonConverter(typeof(JsonSubtypes), "kind")]
@@ -40,12 +55,21 @@ public class OMS : MMTTerm
public string uri;
public string kind = "OMS";
- public OMS(string uri, bool convertToURI = true)
+ public OMS(string uri)
+ {
+ this.uri = uri;
+ }
+ }
+
+ public class OMSTR : MMTTerm
+ {
+ [JsonProperty("float")]
+ public string s;
+ public string kind = "OMSTR";
+
+ public OMSTR(string s)
{
- if (convertToURI)
- this.uri = URIDictionary[uri];
- else
- this.uri = uri;
+ this.s = s;
}
}