Skip to content
Snippets Groups Projects
Commit 3697e791 authored by Richard Marcus's avatar Richard Marcus
Browse files

distance request seems to be okish

parent 9ea37b3e
Branches tsc/fact-interaction
No related tags found
No related merge requests found
......@@ -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}
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
......
......@@ -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);
......
......@@ -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;
}
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment