Skip to content
Snippets Groups Projects
Scroll.cs 2.78 KiB
Newer Older
  • Learn to ignore specific revisions
  • using System.Collections;
    using System.Collections.Generic;
    
    Richard Marcus's avatar
    Richard Marcus committed
    using System.Linq;
    
    using System;
    using UnityEngine;
    
    using static JSONManager;
    
    using JsonSubTypes;
    
    using Newtonsoft.Json;
    
    Richard Marcus's avatar
    Richard Marcus committed
    {
    
        public ScrollTheoryReference @ref;
    
    Richard Marcus's avatar
    Richard Marcus committed
        public string label;
        public string description;
        public List<ScrollFact> requiredFacts;
    
        public List<ScrollFact> acquiredFacts;
    
    Richard Marcus's avatar
    Richard Marcus committed
    
        public static List<Scroll> FromJSON(string json)
        {
    
            List<Scroll> scrolls = JsonConvert.DeserializeObject<List<Scroll>>(json);
    
    Richard Marcus's avatar
    Richard Marcus committed
            return scrolls;
        }
        public static string ToJSON(FilledScroll scroll)
        {
    
            string json = Newtonsoft.Json.JsonConvert.SerializeObject(scroll);
    
    Richard Marcus's avatar
    Richard Marcus committed
            return json;
        }
    
        // id of fact, positions in Description
        public static List<KeyValuePair<int,int>>[] FactOccurences;
    
        public static void InitDynamicScroll(int n)
        {
            FactOccurences = new List<KeyValuePair<int, int>>[n];
        }
    
        public class FilledScroll
        {
    
            public ScrollTheoryReference scroll;
            //public List<List<KeyValuePair<JSONManager.URI, JSONManager.MMTTerm>>> assignments;
            public List<List<System.Object>> assignments;
    
    Richard Marcus's avatar
    Richard Marcus committed
    
    
            public FilledScroll(ScrollTheoryReference scroll, List<List<System.Object>> assignments)
    
    Richard Marcus's avatar
    Richard Marcus committed
            {
                this.scroll = scroll;
                this.assignments = assignments;
            }
        }
    
    
        public class ScrollTheoryReference
        {
            public string problemTheory;
            public string solutionTheory;
        }
    
    Richard Marcus's avatar
    Richard Marcus committed
    
    
        [JsonConverter(typeof(JsonSubtypes), "kind")]
        [JsonSubtypes.KnownSubType(typeof(ScrollSymbolFact), "general")]
        [JsonSubtypes.KnownSubType(typeof(ScrollValueFact), "veq")]
    
        public abstract class ScrollFact
    
    Richard Marcus's avatar
    Richard Marcus committed
        {
    
            public string kind;
    
            public UriReference @ref;
    
    Richard Marcus's avatar
    Richard Marcus committed
            public string label;
    
    
            public abstract String getType();
    
    Richard Marcus's avatar
    Richard Marcus committed
        }
    
    
        public class UriReference
        {
            public string uri;
        }
    
    
        /**
        * Class used for deserializing incoming symbol-declarations from mmt
        */
        public class ScrollSymbolFact : ScrollFact
        {
            public MMTTerm tp;
            public MMTTerm df;
    
            
            public override String getType() {
                if (this.tp is OMS)
                    return ((OMS)this.tp).uri;
                else
                    return null;
            }
    
        }
    
        /**
        * Class used for deserializing incoming value-declarations from mmt
        */
        public class ScrollValueFact : ScrollFact
    
    Richard Marcus's avatar
    Richard Marcus committed
        {
    
            public MMTTerm lhs;
            public MMTTerm valueTp;
            public MMTTerm value;
            public MMTTerm proof;
    
    Richard Marcus's avatar
    Richard Marcus committed
    
    
            public override String getType()
            {
                if (this.lhs is OMA & (((OMA)this.lhs).applicant is OMS))
                    return ((OMS)((OMA)this.lhs).applicant).uri;
                else
                    return null;
            }
        }