module OWL2.Unsafe.OBOGraph.Example where

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

jsonValue : JSON.JsonValue
jsonValue =
  importOBOGraphJsonValue "/Users/marcin/obographs-small/logicalDefinitionTest.json"

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

logicalDefinitionTest : P.OntologyDocument
logicalDefinitionTest =
  OGP.toOntologyDocument graphDocument

logicalDefinitionTestConvenience : P.OntologyDocument
logicalDefinitionTestConvenience =
  importOBOGraphDocument "/Users/marcin/obographs-small/logicalDefinitionTest.json"