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

module OWL2.Examples.OBOGraph.Json.PropertyChainAllValues 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 =
  "testdata/obographs-online/property-chain-all-values.json"

sourceJsonBytes : ℕ
sourceJsonBytes =
  1570

sourceJsonSha256 : String
sourceJsonSha256 =
  "sha256:50b17da1098209dcbef7eda608be682a679d7a8e97c270b5cbfaf6b2a007e4d4"

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 "https://example.org/obographs/property-chain-all-values") ∷ ("nodes" , JSON.jarray (JSON.jobject (("id" , JSON.jstring "https://example.org/obographs/A") ∷ ("lbl" , JSON.jstring "A") ∷ ("type" , JSON.jstring "CLASS") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "https://example.org/obographs/B") ∷ ("lbl" , JSON.jstring "B") ∷ ("type" , JSON.jstring "CLASS") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "https://example.org/obographs/hasParent") ∷ ("lbl" , JSON.jstring "has parent") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "https://example.org/obographs/hasGrandparent") ∷ ("lbl" , JSON.jstring "has grandparent") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "https://example.org/obographs/relatedTo") ∷ ("lbl" , JSON.jstring "related to") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ [])) ∷ ("domainRangeAxioms" , JSON.jarray (JSON.jobject (("predicateId" , JSON.jstring "https://example.org/obographs/relatedTo") ∷ ("allValuesFromEdges" , JSON.jarray (JSON.jobject (("sub" , JSON.jstring "https://example.org/obographs/A") ∷ ("pred" , JSON.jstring "https://example.org/obographs/relatedTo") ∷ ("obj" , JSON.jstring "https://example.org/obographs/B") ∷ []) ∷ [])) ∷ []) ∷ [])) ∷ ("propertyChainAxioms" , JSON.jarray (JSON.jobject (("predicateId" , JSON.jstring "https://example.org/obographs/hasGrandparent") ∷ ("chainPredicateIds" , JSON.jarray (JSON.jstring "https://example.org/obographs/hasParent" ∷ JSON.jstring "https://example.org/obographs/hasParent" ∷ [])) ∷ []) ∷ [])) ∷ []) ∷ [])) ∷ [])

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