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

module OWL2.Examples.OBOGraph.Json.Schema where

open import OWL2.Prelude using ([]; _∷_; _,_; _≡_; refl)
import FF.Json.Native as JSON
import OWL2.OBOGraph.Schema as Schema

emptyDocumentJson : JSON.JsonValue
emptyDocumentJson =
  JSON.jobject (("graphs" , JSON.jarray []) ∷ [])

emptyDocumentDiagnosticsClean :
  Schema.schemaDiagnostics emptyDocumentJson ≡ []
emptyDocumentDiagnosticsClean =
  refl

topLevelArrayJson : JSON.JsonValue
topLevelArrayJson =
  JSON.jarray []

topLevelArrayDiagnostics :
  Schema.schemaDiagnostics topLevelArrayJson ≡
  Schema.schemaErrorAt "$" "expected top-level object" ∷ []
topLevelArrayDiagnostics =
  refl

topLevelArrayDiagnosticCount :
  Schema.schemaDiagnosticCount (Schema.schemaDiagnostics topLevelArrayJson) ≡ 1
topLevelArrayDiagnosticCount =
  refl

graphsNotArrayJson : JSON.JsonValue
graphsNotArrayJson =
  JSON.jobject (("graphs" , JSON.jstring "bad") ∷ [])

graphsNotArrayDiagnostics :
  Schema.schemaDiagnostics graphsNotArrayJson ≡
  Schema.schemaErrorAt "$.graphs" "expected top-level graphs array" ∷ []
graphsNotArrayDiagnostics =
  refl

graphsNotArrayDiagnosticCount :
  Schema.schemaDiagnosticCount (Schema.schemaDiagnostics graphsNotArrayJson) ≡ 1
graphsNotArrayDiagnosticCount =
  refl

graphsMissingJson : JSON.JsonValue
graphsMissingJson =
  JSON.jobject []

graphsMissingDiagnostics :
  Schema.schemaDiagnostics graphsMissingJson ≡
  Schema.schemaWarningAt
    "$.graphs"
    "missing required top-level graphs array" ∷
  []
graphsMissingDiagnostics =
  refl

graphsMissingDiagnosticCount :
  Schema.schemaDiagnosticCount (Schema.schemaDiagnostics graphsMissingJson) ≡ 1
graphsMissingDiagnosticCount =
  refl

unknownDocumentFieldJson : JSON.JsonValue
unknownDocumentFieldJson =
  JSON.jobject
    (("graphs" , JSON.jarray []) ∷
     ("extra" , JSON.jstring "ignored") ∷ [])

unknownDocumentFieldDiagnostics :
  Schema.schemaDiagnostics unknownDocumentFieldJson ≡
  Schema.schemaWarningAt "$.extra" "ignored document field extra" ∷ []
unknownDocumentFieldDiagnostics =
  refl

unknownDocumentFieldDiagnosticCount :
  Schema.schemaDiagnosticCount
    (Schema.schemaDiagnostics unknownDocumentFieldJson)
  ≡ 1
unknownDocumentFieldDiagnosticCount =
  refl

graphArrayItemJson : JSON.JsonValue
graphArrayItemJson =
  JSON.jobject
    (("graphs" , JSON.jarray (JSON.jstring "bad" ∷ [])) ∷ [])

graphArrayItemDiagnostics :
  Schema.schemaDiagnostics graphArrayItemJson ≡
  Schema.schemaWarningAt "$.graphs[0]" "expected graph object" ∷ []
graphArrayItemDiagnostics =
  refl

graphArrayItemDiagnosticCount :
  Schema.schemaDiagnosticCount (Schema.schemaDiagnostics graphArrayItemJson) ≡ 1
graphArrayItemDiagnosticCount =
  refl

nodeWithoutIdJson : JSON.JsonValue
nodeWithoutIdJson =
  JSON.jobject
    (("graphs" ,
      JSON.jarray
        (JSON.jobject
          (("nodes" ,
            JSON.jarray (JSON.jobject [] ∷ [])) ∷ []) ∷ [])) ∷ [])

nodeWithoutIdDiagnostics :
  Schema.schemaDiagnostics nodeWithoutIdJson ≡
  Schema.schemaWarningAt
    "$.graphs[0].nodes[0].id"
    "missing required string field" ∷
  []
nodeWithoutIdDiagnostics =
  refl

nodeWithoutIdDiagnosticCount :
  Schema.schemaDiagnosticCount (Schema.schemaDiagnostics nodeWithoutIdJson) ≡ 1
nodeWithoutIdDiagnosticCount =
  refl

badNodeTypeJson : JSON.JsonValue
badNodeTypeJson =
  JSON.jobject
    (("graphs" ,
      JSON.jarray
        (JSON.jobject
          (("nodes" ,
            JSON.jarray
              (JSON.jobject
                (("id" , JSON.jstring "n") ∷
                 ("type" , JSON.jstring "BAD") ∷ []) ∷ [])) ∷ []) ∷ [])) ∷ [])

badNodeTypeDiagnostics :
  Schema.schemaDiagnostics badNodeTypeJson ≡
  Schema.schemaWarningAt
    "$.graphs[0].nodes[0].type"
    "expected node type CLASS/INDIVIDUAL/PROPERTY" ∷
  []
badNodeTypeDiagnostics =
  refl

badNodeTypeDiagnosticCount :
  Schema.schemaDiagnosticCount (Schema.schemaDiagnostics badNodeTypeJson) ≡ 1
badNodeTypeDiagnosticCount =
  refl

badPropertyTypeJson : JSON.JsonValue
badPropertyTypeJson =
  JSON.jobject
    (("graphs" ,
      JSON.jarray
        (JSON.jobject
          (("nodes" ,
            JSON.jarray
              (JSON.jobject
                (("id" , JSON.jstring "p") ∷
                 ("type" , JSON.jstring "PROPERTY") ∷
                 ("propertyType" , JSON.jstring "BAD") ∷ []) ∷ [])) ∷ []) ∷ [])) ∷ [])

badPropertyTypeDiagnostics :
  Schema.schemaDiagnostics badPropertyTypeJson ≡
  Schema.schemaWarningAt
    "$.graphs[0].nodes[0].propertyType"
    "expected property type OBJECT/DATA/ANNOTATION" ∷
  []
badPropertyTypeDiagnostics =
  refl

badPropertyTypeDiagnosticCount :
  Schema.schemaDiagnosticCount (Schema.schemaDiagnostics badPropertyTypeJson) ≡ 1
badPropertyTypeDiagnosticCount =
  refl

unknownNodeFieldJson : JSON.JsonValue
unknownNodeFieldJson =
  JSON.jobject
    (("graphs" ,
      JSON.jarray
        (JSON.jobject
          (("nodes" ,
            JSON.jarray
              (JSON.jobject
                (("id" , JSON.jstring "n") ∷
                 ("extra" , JSON.jstring "ignored") ∷ []) ∷ [])) ∷ []) ∷ [])) ∷ [])

unknownNodeFieldDiagnostics :
  Schema.schemaDiagnostics unknownNodeFieldJson ≡
  Schema.schemaWarningAt
    "$.graphs[0].nodes[0].extra"
    "ignored node field extra" ∷
  []
unknownNodeFieldDiagnostics =
  refl

unknownNodeFieldDiagnosticCount :
  Schema.schemaDiagnosticCount
    (Schema.schemaDiagnostics unknownNodeFieldJson)
  ≡ 1
unknownNodeFieldDiagnosticCount =
  refl

metaVersionAndSynonymXrefsJson : JSON.JsonValue
metaVersionAndSynonymXrefsJson =
  JSON.jobject
    (("graphs" ,
      JSON.jarray
        (JSON.jobject
          (("meta" ,
            JSON.jobject
              (("version" , JSON.jstring "v1") ∷
               ("synonyms" ,
                JSON.jarray
                  (JSON.jobject
                    (("val" , JSON.jstring "name") ∷
                     ("pred" , JSON.jstring "hasExactSynonym") ∷
                     ("synonymType" , JSON.jstring "exact") ∷
                     ("xrefs" , JSON.jarray (JSON.jstring "PMID:1" ∷ [])) ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ [])) ∷ [])

metaVersionAndSynonymXrefsClean :
  Schema.schemaDiagnostics metaVersionAndSynonymXrefsJson ≡ []
metaVersionAndSynonymXrefsClean =
  refl

duplicateNodeFieldJson : JSON.JsonValue
duplicateNodeFieldJson =
  JSON.jobject
    (("graphs" ,
      JSON.jarray
        (JSON.jobject
          (("nodes" ,
            JSON.jarray
              (JSON.jobject
                (("id" , JSON.jstring "first") ∷
                 ("id" , JSON.jstring "second") ∷ []) ∷ [])) ∷ []) ∷ [])) ∷ [])

duplicateNodeFieldDiagnostics :
  Schema.schemaDiagnostics duplicateNodeFieldJson ≡
  Schema.schemaWarningAt
    "$.graphs[0].nodes[0].id"
    "duplicate object field id" ∷
  []
duplicateNodeFieldDiagnostics =
  refl

duplicateNodeFieldDiagnosticCount :
  Schema.schemaDiagnosticCount
    (Schema.schemaDiagnostics duplicateNodeFieldJson)
  ≡ 1
duplicateNodeFieldDiagnosticCount =
  refl

metaXrefStringJson : JSON.JsonValue
metaXrefStringJson =
  JSON.jobject
    (("graphs" ,
      JSON.jarray
        (JSON.jobject
          (("meta" ,
            JSON.jobject
              (("xrefs" , JSON.jarray (JSON.jstring "PMID:1" ∷ [])) ∷ [])) ∷ []) ∷ [])) ∷ [])

metaXrefStringDiagnostics :
  Schema.schemaDiagnostics metaXrefStringJson ≡
  Schema.schemaWarningAt
    "$.graphs[0].meta.xrefs[0]"
    "expected xref object" ∷
  []
metaXrefStringDiagnostics =
  refl

metaXrefStringDiagnosticCount :
  Schema.schemaDiagnosticCount
    (Schema.schemaDiagnostics metaXrefStringJson)
  ≡ 1
metaXrefStringDiagnosticCount =
  refl

definitionXrefObjectJson : JSON.JsonValue
definitionXrefObjectJson =
  JSON.jobject
    (("graphs" ,
      JSON.jarray
        (JSON.jobject
          (("meta" ,
            JSON.jobject
              (("definition" ,
                JSON.jobject
                  (("val" , JSON.jstring "definition") ∷
                   ("xrefs" ,
                    JSON.jarray
                      (JSON.jobject (("val" , JSON.jstring "PMID:1") ∷ []) ∷ [])) ∷ [])) ∷ [])) ∷ []) ∷ [])) ∷ [])

definitionXrefObjectDiagnostics :
  Schema.schemaDiagnostics definitionXrefObjectJson ≡
  Schema.schemaWarningAt
    "$.graphs[0].meta.definition.xrefs[0]"
    "expected string array item" ∷
  []
definitionXrefObjectDiagnostics =
  refl

definitionXrefObjectDiagnosticCount :
  Schema.schemaDiagnosticCount
    (Schema.schemaDiagnostics definitionXrefObjectJson)
  ≡ 1
definitionXrefObjectDiagnosticCount =
  refl

edgeWithoutRequiredFieldsJson : JSON.JsonValue
edgeWithoutRequiredFieldsJson =
  JSON.jobject
    (("graphs" ,
      JSON.jarray
        (JSON.jobject
          (("edges" ,
            JSON.jarray (JSON.jobject [] ∷ [])) ∷ []) ∷ [])) ∷ [])

edgeWithoutRequiredFieldsDiagnostics :
  Schema.schemaDiagnostics edgeWithoutRequiredFieldsJson ≡
  Schema.schemaWarningAt
    "$.graphs[0].edges[0]"
    "missing required edge subject field sub/subj" ∷
  Schema.schemaWarningAt
    "$.graphs[0].edges[0].pred"
    "missing required string field" ∷
  Schema.schemaWarningAt
    "$.graphs[0].edges[0].obj"
    "missing required string field" ∷
  []
edgeWithoutRequiredFieldsDiagnostics =
  refl

edgeWithoutRequiredFieldsDiagnosticCount :
  Schema.schemaDiagnosticCount
    (Schema.schemaDiagnostics edgeWithoutRequiredFieldsJson)
  ≡ 3
edgeWithoutRequiredFieldsDiagnosticCount =
  refl

restrictionWithoutRequiredFieldsJson : JSON.JsonValue
restrictionWithoutRequiredFieldsJson =
  JSON.jobject
    (("graphs" ,
      JSON.jarray
        (JSON.jobject
          (("logicalDefinitionAxioms" ,
            JSON.jarray
              (JSON.jobject
                (("restrictions" ,
                  JSON.jarray (JSON.jobject [] ∷ [])) ∷ []) ∷ [])) ∷ []) ∷ [])) ∷ [])

restrictionWithoutRequiredFieldsDiagnostics :
  Schema.schemaDiagnostics restrictionWithoutRequiredFieldsJson ≡
  Schema.schemaWarningAt
    "$.graphs[0].logicalDefinitionAxioms[0].definedClassId"
    "missing required string field" ∷
  Schema.schemaWarningAt
    "$.graphs[0].logicalDefinitionAxioms[0].restrictions[0].propertyId"
    "missing required string field" ∷
  Schema.schemaWarningAt
    "$.graphs[0].logicalDefinitionAxioms[0].restrictions[0].fillerId"
    "missing required string field" ∷
  []
restrictionWithoutRequiredFieldsDiagnostics =
  refl

restrictionWithoutRequiredFieldsDiagnosticCount :
  Schema.schemaDiagnosticCount
    (Schema.schemaDiagnostics restrictionWithoutRequiredFieldsJson)
  ≡ 3
restrictionWithoutRequiredFieldsDiagnosticCount =
  refl