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

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

sourceJsonBytes : ℕ
sourceJsonBytes =
  2596

sourceJsonSha256 : String
sourceJsonSha256 =
  "sha256:294da3ae1abca4daafd6f9ce9fe65ab9bac5b5329a64e3d13e8ebf0914be0803"

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/obsoletion_example.owl") ∷ ("nodes" , JSON.jarray (JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/X_1") ∷ ("lbl" , JSON.jstring "x1") ∷ ("type" , JSON.jstring "CLASS") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#hasOBONamespace") ∷ ("val" , JSON.jstring "x") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/X_2") ∷ ("lbl" , JSON.jstring "obsolete x2") ∷ ("type" , JSON.jstring "CLASS") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://purl.obolibrary.org/obo/IAO_0100001") ∷ ("val" , JSON.jstring "X:1") ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#hasOBONamespace") ∷ ("val" , JSON.jstring "x") ∷ []) ∷ [])) ∷ ("deprecated" , JSON.jbool true) ∷ [])) ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/Y_1") ∷ ("lbl" , JSON.jstring "y1") ∷ ("type" , JSON.jstring "CLASS") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#hasAlternativeId") ∷ ("val" , JSON.jstring "Y:2") ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#hasOBONamespace") ∷ ("val" , JSON.jstring "y") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/Y_2") ∷ ("type" , JSON.jstring "CLASS") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://purl.obolibrary.org/obo/IAO_0000231") ∷ ("val" , JSON.jstring "http://purl.obolibrary.org/obo/IAO_0000227") ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "http://purl.obolibrary.org/obo/IAO_0100001") ∷ ("val" , JSON.jstring "http://purl.obolibrary.org/obo/Y_1") ∷ []) ∷ [])) ∷ ("deprecated" , JSON.jbool true) ∷ [])) ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/IAO_0100001") ∷ ("lbl" , JSON.jstring "term replaced by") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#hasAlternativeId") ∷ ("lbl" , JSON.jstring "has_alternative_id") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#hasOBONamespace") ∷ ("lbl" , JSON.jstring "has_obo_namespace") ∷ ("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.w3.org/2000/01/rdf-schema#label") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.w3.org/2002/07/owl#deprecated") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ [])) ∷ []) ∷ [])) ∷ [])

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