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

module OWL2.Import.OBOGraph.Policy where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
open import OWL2.Elab.Policy
open import OWL2.Foundation.Maybe
open import OWL2.OBOGraph.Syntax

private
  policyCode : String → DiagnosticCode
  policyCode name =
    mkDiagnosticCode "obograph.policy" name

  atNode : SourcePath
  atNode =
    sourcePath (fieldSegment "graphs" ∷ opaqueSegment "nodes" ∷ [])

  atPropertyValue : SourcePath
  atPropertyValue =
    sourcePath
      (fieldSegment "graphs" ∷
       opaqueSegment "meta" ∷
       opaqueSegment "basicPropertyValues" ∷ [])

  xsdAnyURI : String
  xsdAnyURI =
    "http://www.w3.org/2001/XMLSchema#anyURI"

  compactXSDAnyURI : String
  compactXSDAnyURI =
    "xsd:anyURI"

missingPropertyTypeDiagnostic : Node → Diagnostic
missingPropertyTypeDiagnostic n =
  diagnostic
    (policyCode "missing-property-type")
    severityError
    atNode
    (nodeId n)

unknownPropertyTypeDiagnostic : Node → Diagnostic
unknownPropertyTypeDiagnostic n =
  diagnostic
    (policyCode "unknown-property-type")
    severityError
    atNode
    (nodeId n)

lossyPropertyValueTypeDiagnostic : PropertyValue → String → Diagnostic
lossyPropertyValueTypeDiagnostic value valueType =
  diagnostic
    (policyCode "lossy-property-value-type")
    severityError
    atPropertyValue
    valueType

propertyTypeDiagnostics : ImportPolicy → Node → Optional PropertyType → Diagnostics
propertyTypeDiagnostics policy n absent with allowUnknownPropertyKinds policy
... | true =
  noDiagnostics
... | false =
  singleDiagnostic (missingPropertyTypeDiagnostic n)
propertyTypeDiagnostics policy n (present unknownProperty) with
  allowUnknownPropertyKinds policy
... | true =
  noDiagnostics
... | false =
  singleDiagnostic (unknownPropertyTypeDiagnostic n)
propertyTypeDiagnostics policy n (present objectProperty) =
  noDiagnostics
propertyTypeDiagnostics policy n (present annotationProperty) =
  noDiagnostics
propertyTypeDiagnostics policy n (present dataProperty) =
  noDiagnostics

propertyValueTypeDiagnostics : ImportPolicy → PropertyValue → Diagnostics
propertyValueTypeDiagnostics policy value with propertyValueType value
... | absent =
  noDiagnostics
... | present valueType with primStringEquality valueType xsdAnyURI
...   | true =
  noDiagnostics
...   | false with primStringEquality valueType compactXSDAnyURI
...     | true =
  noDiagnostics
...     | false with allowLossyMappings policy
...       | true =
  noDiagnostics
...       | false =
  singleDiagnostic (lossyPropertyValueTypeDiagnostic value valueType)

propertyValuesPolicyDiagnostics :
  ImportPolicy →
  List PropertyValue →
  Diagnostics
propertyValuesPolicyDiagnostics policy [] =
  noDiagnostics
propertyValuesPolicyDiagnostics policy (value ∷ values) =
  propertyValueTypeDiagnostics policy value ++
  propertyValuesPolicyDiagnostics policy values

metaPolicyDiagnostics : ImportPolicy → Meta → Diagnostics
metaPolicyDiagnostics policy m =
  propertyValuesPolicyDiagnostics policy (basicPropertyValues m)

nodePolicyDiagnostics : ImportPolicy → Node → Diagnostics
nodePolicyDiagnostics policy n with nodeType n
... | propertyNode =
  propertyTypeDiagnostics policy n (nodePropertyType n) ++
  metaPolicyDiagnostics policy (nodeMeta n)
... | classNode =
  metaPolicyDiagnostics policy (nodeMeta n)
... | individualNode =
  metaPolicyDiagnostics policy (nodeMeta n)
... | unknownNode =
  metaPolicyDiagnostics policy (nodeMeta n)

nodesPolicyDiagnostics : ImportPolicy → List Node → Diagnostics
nodesPolicyDiagnostics policy [] =
  noDiagnostics
nodesPolicyDiagnostics policy (n ∷ nodes) =
  nodePolicyDiagnostics policy n ++ nodesPolicyDiagnostics policy nodes

edgePolicyDiagnostics : ImportPolicy → Edge → Diagnostics
edgePolicyDiagnostics policy e =
  metaPolicyDiagnostics policy (edgeMeta e)

edgesPolicyDiagnostics : ImportPolicy → List Edge → Diagnostics
edgesPolicyDiagnostics policy [] =
  noDiagnostics
edgesPolicyDiagnostics policy (e ∷ edges) =
  edgePolicyDiagnostics policy e ++ edgesPolicyDiagnostics policy edges

equivalentNodesSetPolicyDiagnostics :
  ImportPolicy →
  EquivalentNodesSet →
  Diagnostics
equivalentNodesSetPolicyDiagnostics policy set =
  metaPolicyDiagnostics policy (equivalentMeta set)

equivalentNodesSetsPolicyDiagnostics :
  ImportPolicy →
  List EquivalentNodesSet →
  Diagnostics
equivalentNodesSetsPolicyDiagnostics policy [] =
  noDiagnostics
equivalentNodesSetsPolicyDiagnostics policy (set ∷ sets) =
  equivalentNodesSetPolicyDiagnostics policy set ++
  equivalentNodesSetsPolicyDiagnostics policy sets

graphPolicyDiagnostics : ImportPolicy → Graph → Diagnostics
graphPolicyDiagnostics policy g =
  metaPolicyDiagnostics policy (graphMeta g) ++
  nodesPolicyDiagnostics policy (nodes g) ++
  edgesPolicyDiagnostics policy (edges g) ++
  equivalentNodesSetsPolicyDiagnostics policy (equivalentNodesSets g)

graphsPolicyDiagnostics : ImportPolicy → List Graph → Diagnostics
graphsPolicyDiagnostics policy [] =
  noDiagnostics
graphsPolicyDiagnostics policy (g ∷ graphs) =
  graphPolicyDiagnostics policy g ++ graphsPolicyDiagnostics policy graphs

policyDiagnostics : ImportPolicy → GraphDocument → Diagnostics
policyDiagnostics policy doc =
  graphsPolicyDiagnostics policy (graphs doc)

record OBOGraphPolicyEvidence
  (policy : ImportPolicy)
  (doc : GraphDocument)
  : Type₀ where
  constructor obographPolicyEvidence
  field
    obographImportPolicyEvidence :
      ImportPolicyEvidence policy

open OBOGraphPolicyEvidence public

OBOGraphPolicyMeaning :
  (policy : ImportPolicy) →
  (doc : GraphDocument) →
  OBOGraphPolicyEvidence policy doc →
  Type₀
OBOGraphPolicyMeaning policy doc evidence =
  Unit

policyEvidence? :
  (policy : ImportPolicy) →
  (doc : GraphDocument) →
  Diagnostics →
  Optional (OBOGraphPolicyEvidence policy doc)
policyEvidence? policy doc [] =
  present (obographPolicyEvidence (trivialPolicyEvidence policy))
policyEvidence? policy doc (d ∷ diagnostics) =
  absent

policyCleanEvidence :
  (policy : ImportPolicy) →
  (doc : GraphDocument) →
  (diagnostics : Diagnostics) →
  CleanDiagnostics diagnostics →
  Present (policyEvidence? policy doc diagnostics)
policyCleanEvidence policy doc [] clean =
  presentWitness (obographPolicyEvidence (trivialPolicyEvidence policy))
policyCleanEvidence policy doc (d ∷ diagnostics) ()

policySound :
  (policy : ImportPolicy) →
  (doc : GraphDocument) →
  (diagnostics : Diagnostics) →
  (proof : Present (policyEvidence? policy doc diagnostics)) →
  OBOGraphPolicyMeaning policy doc (presentValue proof)
policySound policy doc diagnostics proof =
  tt

checkOBOGraphPolicy :
  (policy : ImportPolicy) →
  GraphDocument →
  CheckResult
    GraphDocument
    (OBOGraphPolicyEvidence policy)
    (OBOGraphPolicyMeaning policy)
checkOBOGraphPolicy policy doc =
  let diagnostics = policyDiagnostics policy doc in
  record
    { input =
        doc
    ; diagnostics =
        diagnostics
    ; clean? =
        diagnosticsClean? diagnostics
    ; evidence? =
        policyEvidence? policy doc diagnostics
    ; cleanEvidence =
        policyCleanEvidence policy doc diagnostics
    ; sound =
        policySound policy doc diagnostics
    }

checkOBOGraphStrictPolicy :
  GraphDocument →
  CheckResult
    GraphDocument
    (OBOGraphPolicyEvidence strictPolicy)
    (OBOGraphPolicyMeaning strictPolicy)
checkOBOGraphStrictPolicy =
  checkOBOGraphPolicy strictPolicy

checkOBOGraphCompatibilityPolicy :
  GraphDocument →
  CheckResult
    GraphDocument
    (OBOGraphPolicyEvidence compatibilityPolicy)
    (OBOGraphPolicyMeaning compatibilityPolicy)
checkOBOGraphCompatibilityPolicy =
  checkOBOGraphPolicy compatibilityPolicy