OWL2.Examples.OBOGraph.Json.ABox

{-# OPTIONS --safe --cubical #-}

module OWL2.Examples.OBOGraph.Json.ABox where

open import OWL2.Prelude
  using ([]; _∷_; _,_; _≡_; refl; Bool; List; ℕ; false; true; Optional; String; present)
import FF.Json.Native as JSON
import OWL2.OBOGraph.Decode as Decode
import OWL2.OBOGraph.Schema as Schema
import OWL2.OBOGraph.Syntax as OG
import OWL2.OBOGraph.ToPortable as OGP
import OWL2.Portable.Syntax as P

sourceJson : String
sourceJson =
  "/Users/marcin/obographs-small/abox.json"

sourceJsonBytes : ℕ
sourceJsonBytes =
  7996

sourceJsonSha256 : String
sourceJsonSha256 =
  "sha256:e8b8219c3de6c11260716d8f996c0e8d21cc46db2e60d01f1a4d8d1dcb23efe6"

sourceGenerator : String
sourceGenerator =
  "/Users/marcin/agdaLibs/ff-owl/scripts/json_to_agda_value.py"

jsonValue : JSON.JsonValue
jsonValue =
  JSON.jobject (("graphs" , JSON.jarray (JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T") ∷ ("nodes" , JSON.jarray (JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/Female") ∷ ("type" , JSON.jstring "CLASS") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/Male") ∷ ("type" , JSON.jstring "CLASS") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/Person") ∷ ("type" , JSON.jstring "CLASS") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/ancestor-of") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/brother-of") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/child-of") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/descendant-of") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/father-of") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/genealogically-related-to") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/grandfather-of") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/grandmother-of") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/grandparent-of") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/mother-of") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/parent-of") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/sibling-of") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/sister-of") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/b") ∷ ("type" , JSON.jstring "INDIVIDUAL") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/b1") ∷ ("type" , JSON.jstring "INDIVIDUAL") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/b2") ∷ ("type" , JSON.jstring "INDIVIDUAL") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/c") ∷ ("type" , JSON.jstring "INDIVIDUAL") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/f1") ∷ ("type" , JSON.jstring "INDIVIDUAL") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/T/m1") ∷ ("type" , JSON.jstring "INDIVIDUAL") ∷ []) ∷ [])) ∷ ("edges" , JSON.jarray (JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/Female") ∷ ("pred" , JSON.jstring "is_a") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/Person") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/Male") ∷ ("pred" , JSON.jstring "is_a") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/Person") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/f1") ∷ ("pred" , JSON.jstring "type") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/Male") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/m1") ∷ ("pred" , JSON.jstring "type") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/Female") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/b") ∷ ("pred" , JSON.jstring "http://purl.obolibrary.org/obo/T/father-of") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/b1") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/b") ∷ ("pred" , JSON.jstring "http://purl.obolibrary.org/obo/T/father-of") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/b2") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/f1") ∷ ("pred" , JSON.jstring "http://purl.obolibrary.org/obo/T/father-of") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/b") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/f1") ∷ ("pred" , JSON.jstring "http://purl.obolibrary.org/obo/T/father-of") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/c") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/m1") ∷ ("pred" , JSON.jstring "http://purl.obolibrary.org/obo/T/mother-of") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/b") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/m1") ∷ ("pred" , JSON.jstring "http://purl.obolibrary.org/obo/T/mother-of") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/c") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/ancestor-of") ∷ ("pred" , JSON.jstring "subPropertyOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/genealogically-related-to") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/brother-of") ∷ ("pred" , JSON.jstring "subPropertyOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/sibling-of") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/child-of") ∷ ("pred" , JSON.jstring "subPropertyOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/descendant-of") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/descendant-of") ∷ ("pred" , JSON.jstring "subPropertyOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/genealogically-related-to") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/father-of") ∷ ("pred" , JSON.jstring "subPropertyOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/parent-of") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/grandfather-of") ∷ ("pred" , JSON.jstring "subPropertyOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/grandparent-of") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/grandmother-of") ∷ ("pred" , JSON.jstring "subPropertyOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/grandparent-of") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/grandparent-of") ∷ ("pred" , JSON.jstring "subPropertyOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/ancestor-of") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/mother-of") ∷ ("pred" , JSON.jstring "subPropertyOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/parent-of") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/parent-of") ∷ ("pred" , JSON.jstring "subPropertyOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/ancestor-of") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/sibling-of") ∷ ("pred" , JSON.jstring "subPropertyOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/genealogically-related-to") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/sister-of") ∷ ("pred" , JSON.jstring "subPropertyOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/sibling-of") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/ancestor-of") ∷ ("pred" , JSON.jstring "inverseOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/descendant-of") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/T/child-of") ∷ ("pred" , JSON.jstring "inverseOf") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/T/parent-of") ∷ []) ∷ [])) ∷ ("domainRangeAxioms" , JSON.jarray (JSON.jobject (("predicateId" , JSON.jstring "http://purl.obolibrary.org/obo/T/brother-of") ∷ ("domainClassIds" , JSON.jarray (JSON.jstring "http://purl.obolibrary.org/obo/T/Male" ∷ [])) ∷ []) ∷ JSON.jobject (("predicateId" , JSON.jstring "http://purl.obolibrary.org/obo/T/father-of") ∷ ("domainClassIds" , JSON.jarray (JSON.jstring "http://purl.obolibrary.org/obo/T/Male" ∷ [])) ∷ []) ∷ JSON.jobject (("predicateId" , JSON.jstring "http://purl.obolibrary.org/obo/T/mother-of") ∷ ("domainClassIds" , JSON.jarray (JSON.jstring "http://purl.obolibrary.org/obo/T/Female" ∷ [])) ∷ []) ∷ JSON.jobject (("predicateId" , JSON.jstring "http://purl.obolibrary.org/obo/T/sister-of") ∷ ("domainClassIds" , JSON.jarray (JSON.jstring "http://purl.obolibrary.org/obo/T/Female" ∷ [])) ∷ []) ∷ [])) ∷ ("propertyChainAxioms" , JSON.jarray (JSON.jobject (("predicateId" , JSON.jstring "http://purl.obolibrary.org/obo/T/sibling-of") ∷ ("chainPredicateIds" , JSON.jarray (JSON.jstring "http://purl.obolibrary.org/obo/T/child-of" ∷ JSON.jstring "http://purl.obolibrary.org/obo/T/parent-of" ∷ [])) ∷ []) ∷ JSON.jobject (("predicateId" , JSON.jstring "http://purl.obolibrary.org/obo/T/grandmother-of") ∷ ("chainPredicateIds" , JSON.jarray (JSON.jstring "http://purl.obolibrary.org/obo/T/mother-of" ∷ JSON.jstring "http://purl.obolibrary.org/obo/T/parent-of" ∷ [])) ∷ []) ∷ JSON.jobject (("predicateId" , JSON.jstring "http://purl.obolibrary.org/obo/T/grandfather-of") ∷ ("chainPredicateIds" , JSON.jarray (JSON.jstring "http://purl.obolibrary.org/obo/T/parent-of" ∷ JSON.jstring "http://purl.obolibrary.org/obo/T/parent-of" ∷ [])) ∷ []) ∷ JSON.jobject (("predicateId" , JSON.jstring "http://purl.obolibrary.org/obo/T/grandparent-of") ∷ ("chainPredicateIds" , JSON.jarray (JSON.jstring "http://purl.obolibrary.org/obo/T/parent-of" ∷ JSON.jstring "http://purl.obolibrary.org/obo/T/parent-of" ∷ [])) ∷ []) ∷ [])) ∷ []) ∷ [])) ∷ [])

jsonDiagnostics : List Schema.SchemaDiagnostic
jsonDiagnostics =
  Schema.schemaDiagnostics jsonValue

jsonDiagnostics-ok : jsonDiagnostics ≡ []
jsonDiagnostics-ok =
  refl


decodedGraphDocument : Optional OG.GraphDocument
decodedGraphDocument =
  Decode.decodeGraphDocument jsonValue

graphDocument : OG.GraphDocument
graphDocument =
  Decode.fromMaybe (OG.graphDocument []) decodedGraphDocument

decodeGraphDocument-ok : decodedGraphDocument ≡ present graphDocument
decodeGraphDocument-ok =
  refl

ontologyDocument : P.OntologyDocument
ontologyDocument =
  OGP.toOntologyDocument graphDocument