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

module OWL2.Examples.OBOGraph.Json.CheckedKernelSmoke 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/checked-kernel-smoke.json"

sourceJsonBytes : ℕ
sourceJsonBytes =
  979

sourceJsonSha256 : String
sourceJsonSha256 =
  "sha256:94b4675a706aa57757f4436f29c38528bcbdc00f94195986ad9b3b774b26fb14"

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 (("nodes" , JSON.jarray (JSON.jobject (("id" , JSON.jstring "http://example.test/A") ∷ ("type" , JSON.jstring "CLASS") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://example.test/B") ∷ ("type" , JSON.jstring "CLASS") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://example.test/R") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://example.test/x") ∷ ("type" , JSON.jstring "INDIVIDUAL") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://example.test/y") ∷ ("type" , JSON.jstring "INDIVIDUAL") ∷ []) ∷ [])) ∷ ("edges" , JSON.jarray (JSON.jobject (("sub" , JSON.jstring "http://example.test/A") ∷ ("pred" , JSON.jstring "is_a") ∷ ("obj" , JSON.jstring "http://example.test/B") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://example.test/x") ∷ ("pred" , JSON.jstring "type") ∷ ("obj" , JSON.jstring "http://example.test/A") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://example.test/x") ∷ ("pred" , JSON.jstring "http://example.test/R") ∷ ("obj" , JSON.jstring "http://example.test/y") ∷ []) ∷ [])) ∷ []) ∷ [])) ∷ [])

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