OWL2.Examples.OBOGraph.Json.LogicalDefinitionTest

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

module OWL2.Examples.OBOGraph.Json.LogicalDefinitionTest 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/logicalDefinitionTest.json"

sourceJsonBytes : ℕ
sourceJsonBytes =
  3073

sourceJsonSha256 : String
sourceJsonSha256 =
  "sha256:333dd583827629c4d5e4dea298a0067c4d0e564b2feab0349b256f1333b51cf5"

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/TEMP") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#id") ∷ ("val" , JSON.jstring "logical_definition_test") ∷ []) ∷ [])) ∷ [])) ∷ ("nodes" , JSON.jarray (JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002101") ∷ ("lbl" , JSON.jstring "limb") ∷ ("type" , JSON.jstring "CLASS") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002102") ∷ ("lbl" , JSON.jstring "forelimb") ∷ ("type" , JSON.jstring "CLASS") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002398") ∷ ("lbl" , JSON.jstring "manus") ∷ ("type" , JSON.jstring "CLASS") ∷ ("meta" , JSON.jobject (("definition" , JSON.jobject (("val" , JSON.jstring ".") ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002470") ∷ ("lbl" , JSON.jstring "autopod region") ∷ ("type" , JSON.jstring "CLASS") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/BFO_0000050") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ ("meta" , JSON.jobject (("xrefs" , JSON.jarray (JSON.jobject (("val" , JSON.jstring "BFO:0000050") ∷ []) ∷ [])) ∷ ("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#shorthand") ∷ ("val" , JSON.jstring "part_of") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/IAO_0000115") ∷ ("lbl" , JSON.jstring "definition") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#hasDbXref") ∷ ("lbl" , JSON.jstring "database_cross_reference") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#id") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#shorthand") ∷ ("lbl" , JSON.jstring "shorthand") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.w3.org/2000/01/rdf-schema#label") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ [])) ∷ ("edges" , JSON.jarray (JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002102") ∷ ("pred" , JSON.jstring "is_a") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002101") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002398") ∷ ("pred" , JSON.jstring "is_a") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002470") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002398") ∷ ("pred" , JSON.jstring "http://purl.obolibrary.org/obo/BFO_0000050") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002102") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002470") ∷ ("pred" , JSON.jstring "http://purl.obolibrary.org/obo/BFO_0000050") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002101") ∷ []) ∷ [])) ∷ ("logicalDefinitionAxioms" , JSON.jarray (JSON.jobject (("definedClassId" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002398") ∷ ("genusIds" , JSON.jarray (JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002470" ∷ [])) ∷ ("restrictions" , JSON.jarray (JSON.jobject (("propertyId" , JSON.jstring "http://purl.obolibrary.org/obo/BFO_0000050") ∷ ("fillerId" , JSON.jstring "http://purl.obolibrary.org/obo/UBERON_0002102") ∷ []) ∷ [])) ∷ []) ∷ [])) ∷ []) ∷ [])) ∷ [])

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