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

module OWL2.Portable.Check.Declarations where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
import OWL2.Portable.Check.Core as Core
import OWL2.Portable.Declarations as Declarations
import OWL2.Portable.PropertyKinds as PropertyKinds
import OWL2.Portable.Syntax as P

record DeclarationEvidence (document : P.OntologyDocument) : Type₀ where
  constructor declarationEvidence
  field
    sourceDocument :
      P.OntologyDocument
    sourcePreserved :
      sourceDocument ≡ document
    declarationFacts :
      List PropertyKinds.DeclarationFact
    entityUses :
      List Declarations.EntityUseFact
    owl2DLDeclarationCollisions :
      List PropertyKinds.DeclarationCollision
    strictDeclarationPunningCollisions :
      List PropertyKinds.DeclarationCollision
    undeclaredEntityUses :
      List Declarations.UndeclaredEntityUse

open DeclarationEvidence public

record DeclarationCheckMeaning
  (document : P.OntologyDocument)
  (evidence : DeclarationEvidence document)
  : Type₀ where
  constructor declarationCheckMeaning
  field
    declarationSourcePreserved :
      sourceDocument evidence ≡ document
    declarationFactsRecorded :
      declarationFacts evidence ≡
      PropertyKinds.ontologyDocumentDeclarationFacts document
    entityUsesRecorded :
      entityUses evidence ≡
      Declarations.ontologyDocumentEntityUses document
    owl2DLDeclarationCollisionsRecorded :
      owl2DLDeclarationCollisions evidence ≡
      PropertyKinds.owl2DLOntologyDocumentDeclarationCollisions document
    strictDeclarationPunningCollisionsRecorded :
      strictDeclarationPunningCollisions evidence ≡
      PropertyKinds.strictOntologyDocumentDeclarationPunningCollisions document
    undeclaredEntityUsesRecorded :
      undeclaredEntityUses evidence ≡
      Declarations.ontologyDocumentUndeclaredEntityUses document

open DeclarationCheckMeaning public

DeclarationCheckResult : Type₀
DeclarationCheckResult =
  CheckResult
    P.OntologyDocument
    DeclarationEvidence
    DeclarationCheckMeaning

declarationDiagnosticNamespace : String
declarationDiagnosticNamespace =
  "owl2.portable.declarations"

undeclaredEntityUseCode declarationRoleCollisionCode :
  DiagnosticCode
undeclaredEntityUseCode =
  mkDiagnosticCode
    declarationDiagnosticNamespace
    "undeclaredEntityUse"
declarationRoleCollisionCode =
  mkDiagnosticCode
    declarationDiagnosticNamespace
    "declarationRoleCollision"

undeclaredEntityUseDiagnostic :
  Declarations.UndeclaredEntityUse →
  Diagnostic
undeclaredEntityUseDiagnostic use =
  diagnostic
    undeclaredEntityUseCode
    severityError
    rootSourcePath
    "entity use has no matching declaration"

declarationRoleCollisionDiagnostic :
  PropertyKinds.DeclarationCollision →
  Diagnostic
declarationRoleCollisionDiagnostic collision =
  diagnostic
    declarationRoleCollisionCode
    severityError
    rootSourcePath
    "entity IRI is declared in incompatible OWL 2 DL roles"

undeclaredEntityUseDiagnostics :
  List Declarations.UndeclaredEntityUse →
  Diagnostics
undeclaredEntityUseDiagnostics [] =
  []
undeclaredEntityUseDiagnostics (use ∷ uses) =
  undeclaredEntityUseDiagnostic use
  ∷ undeclaredEntityUseDiagnostics uses

declarationRoleCollisionDiagnostics :
  List PropertyKinds.DeclarationCollision →
  Diagnostics
declarationRoleCollisionDiagnostics [] =
  []
declarationRoleCollisionDiagnostics (collision ∷ collisions) =
  declarationRoleCollisionDiagnostic collision
  ∷ declarationRoleCollisionDiagnostics collisions

declarationDiagnostics : P.OntologyDocument → Diagnostics
declarationDiagnostics document =
  undeclaredEntityUseDiagnostics
    (Declarations.ontologyDocumentUndeclaredEntityUses document)
  ++
  declarationRoleCollisionDiagnostics
    (PropertyKinds.owl2DLOntologyDocumentDeclarationCollisions document)

declarationEvidenceFor :
  (document : P.OntologyDocument) →
  DeclarationEvidence document
declarationEvidenceFor document =
  declarationEvidence
    document
    refl
    (PropertyKinds.ontologyDocumentDeclarationFacts document)
    (Declarations.ontologyDocumentEntityUses document)
    (PropertyKinds.owl2DLOntologyDocumentDeclarationCollisions document)
    (PropertyKinds.strictOntologyDocumentDeclarationPunningCollisions document)
    (Declarations.ontologyDocumentUndeclaredEntityUses document)

declarationMeaningFor :
  (document : P.OntologyDocument) →
  (evidence : DeclarationEvidence document) →
  sourceDocument evidence ≡ document →
  declarationFacts evidence ≡
    PropertyKinds.ontologyDocumentDeclarationFacts document →
  entityUses evidence ≡
    Declarations.ontologyDocumentEntityUses document →
  owl2DLDeclarationCollisions evidence ≡
    PropertyKinds.owl2DLOntologyDocumentDeclarationCollisions document →
  strictDeclarationPunningCollisions evidence ≡
    PropertyKinds.strictOntologyDocumentDeclarationPunningCollisions document →
  undeclaredEntityUses evidence ≡
    Declarations.ontologyDocumentUndeclaredEntityUses document →
  DeclarationCheckMeaning document evidence
declarationMeaningFor document evidence preserved facts uses dl strict undeclared =
  declarationCheckMeaning preserved facts uses dl strict undeclared

checkDeclarations : P.OntologyDocument → DeclarationCheckResult
checkDeclarations document =
  Core.successfulResultWithDiagnostics
    (declarationDiagnostics document)
    document
    evidence
    (declarationMeaningFor
      document
      evidence
      refl
      refl
      refl
      refl
      refl
      refl)
  where
  evidence : DeclarationEvidence document
  evidence =
    declarationEvidenceFor document