Skip to content
Snippets Groups Projects
JSONManager.cs 3.61 KiB
Newer Older
using JsonSubTypes;
using Newtonsoft.Json;
using System.Collections;
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 Angle = "http://mathhub.info/MitM/core/geometry?Geometry?Common?angle_between";
    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")]
    public class MMTTerm
    {
        string kind;
    }

    public class OMA : MMTTerm
    {
        public MMTTerm applicant;
        public List<MMTTerm> arguments;
        public string kind = "OMA";
        public OMA(MMTTerm applicant, List<MMTTerm> arguments)
        {
            this.applicant = applicant;
            this.arguments = arguments;
        }
    }

    public class OMS : MMTTerm
    {
        public string uri;
        public string kind = "OMS";

        public OMS(string uri)
        {
            this.uri = uri;
        }
    }

    public class OMSTR : MMTTerm
    {
        [JsonProperty("float")]
        public string s;
        public string kind = "OMSTR";

        public OMSTR(string s)
            this.s = s;
        }
    }


    public class OMF : MMTTerm
    {
        [JsonProperty("float")]
        public float f;
        public string kind = "OMF";

        public OMF(float f)
        {
            this.f = 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 MMTSymbolDeclaration(string label, MMTTerm tp, MMTTerm df)
        {
            this.label = label;
            this.tp = tp;
            this.df = df;
        }
    public class MMTValueDeclaration : MMTDeclaration
        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;
        }