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

module OWL2.OBOGraph.Policy where

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

open import OWL2.Prelude
open import OWL2.OBOGraph.Syntax

infixr  _<>_

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

policyShowNat : ℕ → String
policyShowNat =
  primShowNat

policyIndexPath : String → ℕ → String
policyIndexPath path n =
  path <> "[" <> policyShowNat n <> "]"

policyFieldPath : String → String → String
policyFieldPath path name =
  path <> "." <> name

data PolicySeverity : Type₀ where
  policyWarning : PolicySeverity

record PolicyDiagnostic : Type₀ where
  constructor policyDiagnostic
  field
    policyDiagnosticSeverity : PolicySeverity
    policyDiagnosticPath     : String
    policyDiagnosticMessage  : String

open PolicyDiagnostic public

policyWarningAt : String → String → PolicyDiagnostic
policyWarningAt =
  policyDiagnostic policyWarning

policyDiagnosticCount : List PolicyDiagnostic → ℕ
policyDiagnosticCount [] =
  zero
policyDiagnosticCount (x ∷ xs) =
  suc (policyDiagnosticCount xs)

NoPolicyDiagnostics : List PolicyDiagnostic → Type₀
NoPolicyDiagnostics diagnostics =
  diagnostics ≡ []

nodeTypePolicyDiagnostics : String → Node → List PolicyDiagnostic
nodeTypePolicyDiagnostics path n with nodeType n
... | unknownNode =
  policyWarningAt
    (policyFieldPath path "type")
    "node has unknown type after decode" ∷
  []
... | classNode =
  []
... | individualNode =
  []
... | propertyNode =
  []

nodePropertyTypeValueDiagnostics : String → Node → List PolicyDiagnostic
nodePropertyTypeValueDiagnostics path n with nodePropertyType n
... | present unknownProperty =
  policyWarningAt
    (policyFieldPath path "propertyType")
    "propertyType decoded as unknown property kind" ∷
  []
... | present objectProperty =
  []
... | present dataProperty =
  []
... | present annotationProperty =
  []
... | absent =
  []

nodePropertyTypePresenceDiagnostics : String → Node → List PolicyDiagnostic
nodePropertyTypePresenceDiagnostics path n with nodeType n | nodePropertyType n
... | propertyNode | absent =
  policyWarningAt
    (policyFieldPath path "propertyType")
    "property node has no explicit propertyType" ∷
  []
... | propertyNode | present propertyType =
  []
... | classNode | absent =
  []
... | classNode | present propertyType =
  policyWarningAt
    (policyFieldPath path "propertyType")
    "non-property node has propertyType" ∷
  []
... | individualNode | absent =
  []
... | individualNode | present propertyType =
  policyWarningAt
    (policyFieldPath path "propertyType")
    "non-property node has propertyType" ∷
  []
... | unknownNode | propertyType =
  []

nodePolicyDiagnostics : String → Node → List PolicyDiagnostic
nodePolicyDiagnostics path n =
  nodeTypePolicyDiagnostics path n ++
  nodePropertyTypeValueDiagnostics path n ++
  nodePropertyTypePresenceDiagnostics path n

nodesPolicyDiagnostics :
  String → ℕ → List Node → List PolicyDiagnostic
nodesPolicyDiagnostics path n [] =
  []
nodesPolicyDiagnostics path n (x ∷ nodes) =
  nodePolicyDiagnostics (policyIndexPath path n) x ++
  nodesPolicyDiagnostics path (suc n) nodes

graphPolicyDiagnostics : String → Graph → List PolicyDiagnostic
graphPolicyDiagnostics path g =
  nodesPolicyDiagnostics (policyFieldPath path "nodes") zero (nodes g)

graphsPolicyDiagnostics :
  String → ℕ → List Graph → List PolicyDiagnostic
graphsPolicyDiagnostics path n [] =
  []
graphsPolicyDiagnostics path n (g ∷ graphs) =
  graphPolicyDiagnostics (policyIndexPath path n) g ++
  graphsPolicyDiagnostics path (suc n) graphs

policyDiagnosticsInDocument : GraphDocument → List PolicyDiagnostic
policyDiagnosticsInDocument (graphDocument graphs) =
  graphsPolicyDiagnostics "$.graphs" zero graphs

PolicyClean : GraphDocument → Type₀
PolicyClean doc =
  NoPolicyDiagnostics (policyDiagnosticsInDocument doc)