Skip to content
Snippets Groups Projects
Commit 44735002 authored by John Schihada's avatar John Schihada
Browse files

Adjusted Line-/ and AngleFact-Json

parent 528fb656
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Assets/Scripts/InteractionEngine/Fact.cs
+ 31
− 114
View file @ 44735002
......@@ -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);
}
}
......
Assets/Scripts/InventoryStuff/Inventory.meta deleted 100644 → 0
+ 0
− 8
View file @ 528fb656
fileFormatVersion: 2
guid: 8c00acf0711308b4eac44fb21f04a06f
folderAsset: yes
DefaultImporter:
externalObjects: {}
userData:
assetBundleName:
assetBundleVariant:
Assets/Scripts/JSONManager.cs
+ 27
− 14
View file @ 44735002
......@@ -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;
}
}
}
Assets/StreamingAssets.meta deleted 100644 → 0
+ 0
− 8
View file @ 528fb656
fileFormatVersion: 2
guid: 809deaa1d951e5741bce0ace20cdaed8
folderAsset: yes
DefaultImporter:
externalObjects: {}
userData:
assetBundleName:
assetBundleVariant:
ProjectSettings/ProjectVersion.txt
+ 2
− 2
View file @ 44735002
m_EditorVersion: 2019.4.1f1
m_EditorVersionWithRevision: 2019.4.1f1 (e6c045e14e4e)
m_EditorVersion: 2019.4.3f1
m_EditorVersionWithRevision: 2019.4.3f1 (f880dceab6fe)
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment