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

module OWL2.Corpus.Accepted.OBOGraph.Decode where

open import OWL2.Prelude
open import OWL2.OBOGraph
import FF.Json.Native as JSON

sectionMeta : String → Meta
sectionMeta text =
  meta absent (text ∷ []) [] [] [] [] false []

sectionMetaJson : String → JSON.JsonValue
sectionMetaJson text =
  JSON.jobject
    (("comments" ,
      JSON.jarray (JSON.jstring text ∷ [])) ∷ [])

decodedLogicalDefinitionAxiom : LogicalDefinitionAxiom
decodedLogicalDefinitionAxiom =
  logicalDefinitionAxiom
    "A"
    ("B" ∷ [])
    []
    (sectionMeta "logical metadata")

decodedDomainRangeAxiom : DomainRangeAxiom
decodedDomainRangeAxiom =
  domainRangeAxiom
    "R"
    ("A" ∷ [])
    ("B" ∷ [])
    []
    (sectionMeta "domain/range metadata")

decodedPropertyChainAxiom : PropertyChainAxiom
decodedPropertyChainAxiom =
  propertyChainAxiom
    "R"
    ("S" ∷ "T" ∷ [])
    (sectionMeta "property-chain metadata")

decodedMetaDocument : GraphDocument
decodedMetaDocument =
  graphDocument
    (graph
      absent
      absent
      emptyMeta
      []
      []
      []
      (decodedLogicalDefinitionAxiom ∷ [])
      (decodedDomainRangeAxiom ∷ [])
      (decodedPropertyChainAxiom ∷ [])
      []
    ∷ [])

metaSectionsJson : JSON.JsonValue
metaSectionsJson =
  JSON.jobject
    (("graphs" ,
      JSON.jarray
        (JSON.jobject
          (("logicalDefinitionAxioms" ,
            JSON.jarray
              (JSON.jobject
                (("definedClassId" , JSON.jstring "A") ∷
                 ("genusIds" ,
                  JSON.jarray (JSON.jstring "B" ∷ [])) ∷
                 ("restrictions" , JSON.jarray []) ∷
                 ("meta" , sectionMetaJson "logical metadata") ∷
                 []) ∷ [])) ∷
           ("domainRangeAxioms" ,
            JSON.jarray
              (JSON.jobject
                (("predicateId" , JSON.jstring "R") ∷
                 ("domainClassIds" ,
                  JSON.jarray (JSON.jstring "A" ∷ [])) ∷
                 ("rangeClassIds" ,
                  JSON.jarray (JSON.jstring "B" ∷ [])) ∷
                 ("allValuesFromEdges" , JSON.jarray []) ∷
                 ("meta" , sectionMetaJson "domain/range metadata") ∷
                 []) ∷ [])) ∷
           ("propertyChainAxioms" ,
            JSON.jarray
              (JSON.jobject
                (("predicateId" , JSON.jstring "R") ∷
                 ("chainPredicateIds" ,
                  JSON.jarray
                    (JSON.jstring "S" ∷ JSON.jstring "T" ∷ [])) ∷
                 ("meta" , sectionMetaJson "property-chain metadata") ∷
                 []) ∷ [])) ∷
           []) ∷ [])) ∷ [])

metaSectionsSchemaDiagnostics :
  schemaDiagnostics metaSectionsJson ≡ []
metaSectionsSchemaDiagnostics =
  refl

metaSectionsDecode :
  decodeGraphDocument metaSectionsJson ≡ present decodedMetaDocument
metaSectionsDecode =
  refl