OWL2.OBOGraph.Schema

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

module OWL2.OBOGraph.Schema where

open import Agda.Builtin.Nat using (zero; suc)
open import Agda.Builtin.String using (primShowNat; primStringAppend)

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

infixr 5 _<>_

_<>_ : String → String → String
_<>_ =
  primStringAppend

showNat : ℕ → String
showNat =
  primShowNat

indexPath : String → ℕ → String
indexPath path n =
  path <> "[" <> showNat n <> "]"

data SchemaSeverity : Type₀ where
  schemaError schemaWarning : SchemaSeverity

data StringFieldState : Type₀ where
  stringFieldMissing stringFieldMalformed stringFieldValid : StringFieldState

record SchemaDiagnostic : Type₀ where
  constructor schemaDiagnostic
  field
    diagnosticSeverity : SchemaSeverity
    diagnosticPath     : String
    diagnosticMessage  : String

open SchemaDiagnostic public

schemaErrorAt : String → String → SchemaDiagnostic
schemaErrorAt =
  schemaDiagnostic schemaError

schemaWarningAt : String → String → SchemaDiagnostic
schemaWarningAt =
  schemaDiagnostic schemaWarning

schemaDiagnosticCount : List SchemaDiagnostic → ℕ
schemaDiagnosticCount [] =
  zero
schemaDiagnosticCount (x ∷ xs) =
  suc (schemaDiagnosticCount xs)

NoSchemaDiagnostics : List SchemaDiagnostic → Type₀
NoSchemaDiagnostics diagnostics =
  diagnostics ≡ []

fieldPath : String → String → String
fieldPath path key =
  path <> "." <> key

unknownFieldDiagnostics :
  String → String → List String → List (String × JSON.JsonValue) →
  List SchemaDiagnostic
unknownFieldDiagnostics path label known [] =
  []
unknownFieldDiagnostics path label known ((key , value) ∷ fields)
  with Decode.stringIn key known
... | true =
  unknownFieldDiagnostics path label known fields
... | false =
  schemaWarningAt (fieldPath path key) ("ignored " <> label <> " field " <> key) ∷
  unknownFieldDiagnostics path label known fields

duplicateFieldDiagnostics :
  String → List (String × JSON.JsonValue) → List SchemaDiagnostic
duplicateFieldDiagnostics path [] =
  []
duplicateFieldDiagnostics path ((key , value) ∷ fields) with Decode.lookupField key fields
... | present laterValue =
  schemaWarningAt (fieldPath path key) ("duplicate object field " <> key) ∷
  duplicateFieldDiagnostics path fields
... | absent =
  duplicateFieldDiagnostics path fields

expectStringField :
  String → String → List (String × JSON.JsonValue) → List SchemaDiagnostic
expectStringField path key fields with Decode.lookupField key fields
... | absent =
  []
... | present value with Decode.asString value
...   | present text =
  []
...   | absent =
  schemaWarningAt (fieldPath path key) "expected string field" ∷ []

expectStringEnumField :
  String → String → List String → String →
  List (String × JSON.JsonValue) → List SchemaDiagnostic
expectStringEnumField path key allowed message fields with Decode.lookupField key fields
... | absent =
  []
... | present value with Decode.asString value
...   | absent =
  schemaWarningAt (fieldPath path key) "expected string field" ∷ []
...   | present text with Decode.stringIn text allowed
...     | true =
  []
...     | false =
  schemaWarningAt (fieldPath path key) message ∷ []

nodeTypeValues : List String
nodeTypeValues =
  "CLASS" ∷ "INDIVIDUAL" ∷ "PROPERTY" ∷ []

propertyTypeValues : List String
propertyTypeValues =
  "OBJECT" ∷ "DATA" ∷ "ANNOTATION" ∷ []

stringFieldState : String → List (String × JSON.JsonValue) → StringFieldState
stringFieldState key fields with Decode.lookupField key fields
... | absent =
  stringFieldMissing
... | present value with Decode.asString value
...   | present text =
  stringFieldValid
...   | absent =
  stringFieldMalformed

requireStringField :
  String → String → List (String × JSON.JsonValue) → List SchemaDiagnostic
requireStringField path key fields with Decode.lookupField key fields
... | absent =
  schemaWarningAt (fieldPath path key) "missing required string field" ∷ []
... | present value with Decode.asString value
...   | present text =
  []
...   | absent =
  schemaWarningAt (fieldPath path key) "expected required string field" ∷ []

expectBoolField :
  String → String → List (String × JSON.JsonValue) → List SchemaDiagnostic
expectBoolField path key fields with Decode.lookupField key fields
... | absent =
  []
... | present value with Decode.asBool value
...   | present b =
  []
...   | absent =
  schemaWarningAt (fieldPath path key) "expected boolean field" ∷ []

expectObjectField :
  String → String → List (String × JSON.JsonValue) →
  (String → List (String × JSON.JsonValue) → List SchemaDiagnostic) →
  List SchemaDiagnostic
expectObjectField path key fields validate with Decode.lookupField key fields
... | absent =
  []
... | present value with Decode.asObject value
...   | present objectFields =
  validate (fieldPath path key) objectFields
...   | absent =
  schemaWarningAt (fieldPath path key) "expected object field" ∷ []

expectStringArrayItems :
  String → ℕ → List JSON.JsonValue → List SchemaDiagnostic
expectStringArrayItems path n [] =
  []
expectStringArrayItems path n (value ∷ values) with Decode.asString value
... | present text =
  expectStringArrayItems path (suc n) values
... | absent =
  schemaWarningAt (indexPath path n) "expected string array item" ∷
  expectStringArrayItems path (suc n) values

expectStringArrayField :
  String → String → List (String × JSON.JsonValue) → List SchemaDiagnostic
expectStringArrayField path key fields with Decode.lookupField key fields
... | absent =
  []
... | present value with Decode.asArray value
...   | present values =
  expectStringArrayItems (fieldPath path key) zero values
...   | absent =
  schemaWarningAt (fieldPath path key) "expected string array field" ∷ []

validateXrefObjectItem : String → JSON.JsonValue → List SchemaDiagnostic
validateXrefObjectItem path value with Decode.asObject value
... | present fields =
  duplicateFieldDiagnostics path fields ++
  requireStringField path "val" fields ++
  expectStringField path "lbl" fields ++
  expectStringField path "pred" fields ++
  expectStringArrayField path "xrefs" fields ++
  expectObjectField path "meta" fields (λ path fields → []) ++
  unknownFieldDiagnostics
    path
    "xref"
    ("lbl" ∷ "pred" ∷ "val" ∷ "xrefs" ∷ "meta" ∷ [])
    fields
... | absent =
  schemaWarningAt path "expected xref object" ∷ []

validateXrefObjectItems : String → ℕ → List JSON.JsonValue → List SchemaDiagnostic
validateXrefObjectItems path n [] =
  []
validateXrefObjectItems path n (value ∷ values) =
  validateXrefObjectItem (indexPath path n) value ++
  validateXrefObjectItems path (suc n) values

expectXrefObjectArrayField :
  String → String → List (String × JSON.JsonValue) → List SchemaDiagnostic
expectXrefObjectArrayField path key fields with Decode.lookupField key fields
... | absent =
  []
... | present value with Decode.asArray value
...   | present values =
  validateXrefObjectItems (fieldPath path key) zero values
...   | absent =
  schemaWarningAt (fieldPath path key) "expected xref array field" ∷ []

expectArrayField :
  String → String → List (String × JSON.JsonValue) →
  (String → ℕ → List JSON.JsonValue → List SchemaDiagnostic) →
  List SchemaDiagnostic
expectArrayField path key fields validate with Decode.lookupField key fields
... | absent =
  []
... | present value with Decode.asArray value
...   | present values =
  validate (fieldPath path key) zero values
...   | absent =
  schemaWarningAt (fieldPath path key) "expected array field" ∷ []

validateMetaPropertyValue : String → List (String × JSON.JsonValue) → List SchemaDiagnostic
validateMetaPropertyValue path fields =
  duplicateFieldDiagnostics path fields ++
  requireStringField path "pred" fields ++
  requireStringField path "val" fields ++
  expectStringArrayField path "xrefs" fields ++
  expectObjectField path "meta" fields (λ path fields → []) ++
  expectStringField path "valType" fields ++
  unknownFieldDiagnostics
    path
    "property value"
    ("pred" ∷ "val" ∷ "xrefs" ∷ "meta" ∷ "valType" ∷ [])
    fields

validateMetaPropertyValues :
  String → ℕ → List JSON.JsonValue → List SchemaDiagnostic
validateMetaPropertyValues path n [] =
  []
validateMetaPropertyValues path n (value ∷ values) with Decode.asObject value
... | present fields =
  validateMetaPropertyValue (indexPath path n) fields ++
  validateMetaPropertyValues path (suc n) values
... | absent =
  schemaWarningAt (indexPath path n) "expected property value object" ∷
  validateMetaPropertyValues path (suc n) values

validateSynonym : String → List (String × JSON.JsonValue) → List SchemaDiagnostic
validateSynonym path fields =
  duplicateFieldDiagnostics path fields ++
  expectStringField path "synonymType" fields ++
  expectStringField path "pred" fields ++
  requireStringField path "val" fields ++
  expectStringArrayField path "xrefs" fields ++
  expectObjectField path "meta" fields (λ path fields → []) ++
  unknownFieldDiagnostics
    path
    "synonym"
    ("synonymType" ∷ "pred" ∷ "val" ∷ "xrefs" ∷ "meta" ∷ [])
    fields

validateSynonyms : String → ℕ → List JSON.JsonValue → List SchemaDiagnostic
validateSynonyms path n [] =
  []
validateSynonyms path n (value ∷ values) with Decode.asObject value
... | present fields =
  validateSynonym (indexPath path n) fields ++
  validateSynonyms path (suc n) values
... | absent =
  schemaWarningAt (indexPath path n) "expected synonym object" ∷
  validateSynonyms path (suc n) values

validateDefinition : String → JSON.JsonValue → List SchemaDiagnostic
validateDefinition path value with Decode.asString value
... | present text =
  []
... | absent with Decode.asObject value
...   | present fields =
  duplicateFieldDiagnostics path fields ++
  expectStringField path "pred" fields ++
  requireStringField path "val" fields ++
  expectStringArrayField path "xrefs" fields ++
  expectObjectField path "meta" fields (λ path fields → []) ++
  unknownFieldDiagnostics
    path
    "definition"
    ("pred" ∷ "val" ∷ "xrefs" ∷ "meta" ∷ [])
    fields
...   | absent =
  schemaWarningAt path "expected definition string or object" ∷ []

validateMetaFields : String → List (String × JSON.JsonValue) → List SchemaDiagnostic
validateMetaFields path fields =
  duplicateFieldDiagnostics path fields ++
  validateDefinitionField ++
  expectStringArrayField path "comments" fields ++
  expectXrefObjectArrayField path "xrefs" fields ++
  expectStringArrayField path "subsets" fields ++
  expectArrayField path "synonyms" fields validateSynonyms ++
  expectArrayField path "basicPropertyValues" fields validateMetaPropertyValues ++
  expectStringField path "version" fields ++
  expectBoolField path "deprecated" fields ++
  unknownFieldDiagnostics
    path
    "meta"
    ("definition" ∷ "comments" ∷ "xrefs" ∷ "subsets" ∷ "synonyms" ∷
     "basicPropertyValues" ∷ "version" ∷ "deprecated" ∷ [])
    fields
  where
  validateDefinitionField : List SchemaDiagnostic
  validateDefinitionField with Decode.lookupField "definition" fields
  ... | absent =
    []
  ... | present value =
    validateDefinition (fieldPath path "definition") value

validateMetaValue : String → JSON.JsonValue → List SchemaDiagnostic
validateMetaValue path value with Decode.asObject value
... | present fields =
  validateMetaFields path fields
... | absent =
  schemaWarningAt path "expected meta object" ∷ []

expectMetaField :
  String → String → List (String × JSON.JsonValue) → List SchemaDiagnostic
expectMetaField path key fields with Decode.lookupField key fields
... | absent =
  []
... | present value =
  validateMetaValue (fieldPath path key) value

validateNode : String → List (String × JSON.JsonValue) → List SchemaDiagnostic
validateNode path fields =
  duplicateFieldDiagnostics path fields ++
  requireStringField path "id" fields ++
  expectStringField path "lbl" fields ++
  expectStringEnumField
    path
    "type"
    nodeTypeValues
    "expected node type CLASS/INDIVIDUAL/PROPERTY"
    fields ++
  expectStringEnumField
    path
    "propertyType"
    propertyTypeValues
    "expected property type OBJECT/DATA/ANNOTATION"
    fields ++
  expectMetaField path "meta" fields ++
  unknownFieldDiagnostics
    path
    "node"
    ("id" ∷ "lbl" ∷ "type" ∷ "propertyType" ∷ "meta" ∷ [])
    fields

validateNodes : String → ℕ → List JSON.JsonValue → List SchemaDiagnostic
validateNodes path n [] =
  []
validateNodes path n (value ∷ values) with Decode.asObject value
... | present fields =
  validateNode (indexPath path n) fields ++
  validateNodes path (suc n) values
... | absent =
  schemaWarningAt (indexPath path n) "expected node object" ∷
  validateNodes path (suc n) values

requireEdgeSubject : String → List (String × JSON.JsonValue) → List SchemaDiagnostic
requireEdgeSubject path fields with stringFieldState "sub" fields
... | stringFieldValid =
  []
... | stringFieldMalformed =
  schemaWarningAt (fieldPath path "sub") "expected required string field" ∷ []
... | stringFieldMissing with stringFieldState "subj" fields
...   | stringFieldValid =
  []
...   | stringFieldMalformed =
  schemaWarningAt (fieldPath path "subj") "expected required string field" ∷ []
...   | stringFieldMissing =
  schemaWarningAt path "missing required edge subject field sub/subj" ∷ []

validateEdge : String → List (String × JSON.JsonValue) → List SchemaDiagnostic
validateEdge path fields =
  duplicateFieldDiagnostics path fields ++
  requireEdgeSubject path fields ++
  requireStringField path "pred" fields ++
  requireStringField path "obj" fields ++
  expectMetaField path "meta" fields ++
  unknownFieldDiagnostics
    path
    "edge"
    ("sub" ∷ "subj" ∷ "pred" ∷ "obj" ∷ "meta" ∷ [])
    fields

validateEdges : String → ℕ → List JSON.JsonValue → List SchemaDiagnostic
validateEdges path n [] =
  []
validateEdges path n (value ∷ values) with Decode.asObject value
... | present fields =
  validateEdge (indexPath path n) fields ++
  validateEdges path (suc n) values
... | absent =
  schemaWarningAt (indexPath path n) "expected edge object" ∷
  validateEdges path (suc n) values

validateRestriction : String → List (String × JSON.JsonValue) → List SchemaDiagnostic
validateRestriction path fields =
  duplicateFieldDiagnostics path fields ++
  requireStringField path "propertyId" fields ++
  requireStringField path "fillerId" fields ++
  unknownFieldDiagnostics
    path
    "restriction"
    ("propertyId" ∷ "fillerId" ∷ [])
    fields

validateRestrictions : String → ℕ → List JSON.JsonValue → List SchemaDiagnostic
validateRestrictions path n [] =
  []
validateRestrictions path n (value ∷ values) with Decode.asObject value
... | present fields =
  validateRestriction (indexPath path n) fields ++
  validateRestrictions path (suc n) values
... | absent =
  schemaWarningAt (indexPath path n) "expected restriction object" ∷
  validateRestrictions path (suc n) values

validateLogicalDefinitionAxiom :
  String → List (String × JSON.JsonValue) → List SchemaDiagnostic
validateLogicalDefinitionAxiom path fields =
  duplicateFieldDiagnostics path fields ++
  requireStringField path "definedClassId" fields ++
  expectStringArrayField path "genusIds" fields ++
  expectArrayField path "restrictions" fields validateRestrictions ++
  expectMetaField path "meta" fields ++
  unknownFieldDiagnostics
    path
    "logical definition axiom"
    ("definedClassId" ∷ "genusIds" ∷ "restrictions" ∷ "meta" ∷ [])
    fields

validateLogicalDefinitionAxioms :
  String → ℕ → List JSON.JsonValue → List SchemaDiagnostic
validateLogicalDefinitionAxioms path n [] =
  []
validateLogicalDefinitionAxioms path n (value ∷ values) with Decode.asObject value
... | present fields =
  validateLogicalDefinitionAxiom (indexPath path n) fields ++
  validateLogicalDefinitionAxioms path (suc n) values
... | absent =
  schemaWarningAt (indexPath path n) "expected logical definition axiom object" ∷
  validateLogicalDefinitionAxioms path (suc n) values

validateDomainRangeAxiom :
  String → List (String × JSON.JsonValue) → List SchemaDiagnostic
validateDomainRangeAxiom path fields =
  duplicateFieldDiagnostics path fields ++
  requireStringField path "predicateId" fields ++
  expectStringArrayField path "domainClassIds" fields ++
  expectStringArrayField path "rangeClassIds" fields ++
  expectArrayField path "allValuesFromEdges" fields validateEdges ++
  expectMetaField path "meta" fields ++
  unknownFieldDiagnostics
    path
    "domain/range axiom"
    ("predicateId" ∷ "domainClassIds" ∷ "rangeClassIds" ∷
     "allValuesFromEdges" ∷ "meta" ∷ [])
    fields

validateDomainRangeAxioms :
  String → ℕ → List JSON.JsonValue → List SchemaDiagnostic
validateDomainRangeAxioms path n [] =
  []
validateDomainRangeAxioms path n (value ∷ values) with Decode.asObject value
... | present fields =
  validateDomainRangeAxiom (indexPath path n) fields ++
  validateDomainRangeAxioms path (suc n) values
... | absent =
  schemaWarningAt (indexPath path n) "expected domain/range axiom object" ∷
  validateDomainRangeAxioms path (suc n) values

validatePropertyChainAxiom :
  String → List (String × JSON.JsonValue) → List SchemaDiagnostic
validatePropertyChainAxiom path fields =
  duplicateFieldDiagnostics path fields ++
  requireStringField path "predicateId" fields ++
  expectStringArrayField path "chainPredicateIds" fields ++
  expectMetaField path "meta" fields ++
  unknownFieldDiagnostics
    path
    "property-chain axiom"
    ("predicateId" ∷ "chainPredicateIds" ∷ "meta" ∷ [])
    fields

validatePropertyChainAxioms :
  String → ℕ → List JSON.JsonValue → List SchemaDiagnostic
validatePropertyChainAxioms path n [] =
  []
validatePropertyChainAxioms path n (value ∷ values) with Decode.asObject value
... | present fields =
  validatePropertyChainAxiom (indexPath path n) fields ++
  validatePropertyChainAxioms path (suc n) values
... | absent =
  schemaWarningAt (indexPath path n) "expected property-chain axiom object" ∷
  validatePropertyChainAxioms path (suc n) values

validateEquivalentNodesSet :
  String → List (String × JSON.JsonValue) → List SchemaDiagnostic
validateEquivalentNodesSet path fields =
  duplicateFieldDiagnostics path fields ++
  expectStringField path "representativeNodeId" fields ++
  expectStringArrayField path "nodeIds" fields ++
  expectMetaField path "meta" fields ++
  unknownFieldDiagnostics
    path
    "equivalent nodes set"
    ("representativeNodeId" ∷ "nodeIds" ∷ "meta" ∷ [])
    fields

validateEquivalentNodesSets :
  String → ℕ → List JSON.JsonValue → List SchemaDiagnostic
validateEquivalentNodesSets path n [] =
  []
validateEquivalentNodesSets path n (value ∷ values) with Decode.asObject value
... | present fields =
  validateEquivalentNodesSet (indexPath path n) fields ++
  validateEquivalentNodesSets path (suc n) values
... | absent =
  schemaWarningAt (indexPath path n) "expected equivalent nodes set object" ∷
  validateEquivalentNodesSets path (suc n) values

validateGraph : String → List (String × JSON.JsonValue) → List SchemaDiagnostic
validateGraph path fields =
  duplicateFieldDiagnostics path fields ++
  expectStringField path "id" fields ++
  expectStringField path "lbl" fields ++
  expectMetaField path "meta" fields ++
  expectArrayField path "nodes" fields validateNodes ++
  expectArrayField path "edges" fields validateEdges ++
  expectArrayField path "equivalentNodesSets" fields validateEquivalentNodesSets ++
  expectArrayField path "logicalDefinitionAxioms" fields validateLogicalDefinitionAxioms ++
  expectArrayField path "domainRangeAxioms" fields validateDomainRangeAxioms ++
  expectArrayField path "propertyChainAxioms" fields validatePropertyChainAxioms ++
  unknownFieldDiagnostics
    path
    "graph"
    ("id" ∷ "lbl" ∷ "meta" ∷ "nodes" ∷ "edges" ∷
     "equivalentNodesSets" ∷ "logicalDefinitionAxioms" ∷
     "domainRangeAxioms" ∷ "propertyChainAxioms" ∷ [])
    fields

validateGraphs : String → ℕ → List JSON.JsonValue → List SchemaDiagnostic
validateGraphs path n [] =
  []
validateGraphs path n (value ∷ values) with Decode.asObject value
... | present fields =
  validateGraph (indexPath path n) fields ++
  validateGraphs path (suc n) values
... | absent =
  schemaWarningAt (indexPath path n) "expected graph object" ∷
  validateGraphs path (suc n) values

schemaDiagnostics : JSON.JsonValue → List SchemaDiagnostic
schemaDiagnostics value with Decode.asObject value
... | absent =
  schemaErrorAt "$" "expected top-level object" ∷ []
... | present fields =
  duplicateFieldDiagnostics "$" fields ++
  expectObjectField "$" "meta" fields validateMetaFields ++
  validateGraphDocumentGraphs fields ++
  unknownFieldDiagnostics
    "$"
    "document"
    ("@context" ∷ "meta" ∷ "graphs" ∷ [])
    fields
  where
  validateGraphDocumentGraphs :
    List (String × JSON.JsonValue) → List SchemaDiagnostic
  validateGraphDocumentGraphs fields with Decode.lookupField "graphs" fields
  ... | absent =
    schemaWarningAt "$.graphs" "missing required top-level graphs array" ∷ []
  ... | present graphsValue with Decode.asArray graphsValue
  ...   | absent =
    schemaErrorAt "$.graphs" "expected top-level graphs array" ∷ []
  ...   | present graphs =
    validateGraphs "$.graphs" zero graphs

SchemaClean : JSON.JsonValue → Type₀
SchemaClean value =
  NoSchemaDiagnostics (schemaDiagnostics value)