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

module OWL2.Portable.KeyRestrictions where

open import Cubical.Data.Nat.Base using (zero; suc)
open import OWL2.Prelude
import OWL2.Portable.Declarations as Decl
import OWL2.Portable.PropertyKinds as PK
import OWL2.Portable.Syntax as P

private
  concatMap : ∀ {A B : Type₀} → (A → List B) → List A → List B
  concatMap f [] =
    []
  concatMap f (x ∷ xs) =
    f x ++ concatMap f xs

  listCount : ∀ {ℓ} {A : Type ℓ} → List A → ℕ
  listCount [] =
    zero
  listCount (x ∷ xs) =
    suc (listCount xs)

data KeyRestrictionViolation : Type₀ where
  nonClassifiableKeyClassExpression :
    P.Annotated P.Axiom →
    P.ClassExpression →
    KeyRestrictionViolation
  objectKeyPropertyExpressionNotNamed :
    P.Annotated P.Axiom →
    P.ObjectPropertyExpression →
    KeyRestrictionViolation
  dataKeyPropertyExpressionNotNamed :
    P.Annotated P.Axiom →
    P.DataPropertyExpression →
    KeyRestrictionViolation

keyClassExpressionViolations :
  P.Annotated P.Axiom →
  P.ClassExpression →
  List KeyRestrictionViolation
keyClassExpressionViolations source (P.namedClass c) =
  []
keyClassExpressionViolations source P.owlThing =
  []
keyClassExpressionViolations source P.owlNothing =
  []
keyClassExpressionViolations source c =
  nonClassifiableKeyClassExpression source c ∷ []

objectKeyPropertyExpressionViolations :
  P.Annotated P.Axiom →
  P.ObjectPropertyExpression →
  List KeyRestrictionViolation
objectKeyPropertyExpressionViolations source (P.objectProperty p) =
  []
objectKeyPropertyExpressionViolations source p =
  objectKeyPropertyExpressionNotNamed source p ∷ []

objectKeyPropertyExpressionsViolations :
  P.Annotated P.Axiom →
  List P.ObjectPropertyExpression →
  List KeyRestrictionViolation
objectKeyPropertyExpressionsViolations source [] =
  []
objectKeyPropertyExpressionsViolations source (p ∷ ps) =
  objectKeyPropertyExpressionViolations source p
  ++ objectKeyPropertyExpressionsViolations source ps

dataKeyPropertyExpressionViolations :
  P.Annotated P.Axiom →
  P.DataPropertyExpression →
  List KeyRestrictionViolation
dataKeyPropertyExpressionViolations source (P.dataProperty p) =
  []
dataKeyPropertyExpressionViolations source p =
  dataKeyPropertyExpressionNotNamed source p ∷ []

dataKeyPropertyExpressionsViolations :
  P.Annotated P.Axiom →
  List P.DataPropertyExpression →
  List KeyRestrictionViolation
dataKeyPropertyExpressionsViolations source [] =
  []
dataKeyPropertyExpressionsViolations source (p ∷ ps) =
  dataKeyPropertyExpressionViolations source p
  ++ dataKeyPropertyExpressionsViolations source ps

propertyKeyViolations :
  P.Annotated P.Axiom →
  P.PropertyKey →
  List KeyRestrictionViolation
propertyKeyViolations source key =
  objectKeyPropertyExpressionsViolations source (P.objectProperties key)
  ++ dataKeyPropertyExpressionsViolations source (P.dataProperties key)

keyRestrictionViolationsInAxiom :
  P.Annotated P.Axiom →
  P.Axiom →
  List KeyRestrictionViolation
keyRestrictionViolationsInAxiom source (P.hasKey c key) =
  keyClassExpressionViolations source c
  ++ propertyKeyViolations source key
keyRestrictionViolationsInAxiom source _ =
  []

keyRestrictionViolationsInAnnotated :
  P.Annotated P.Axiom →
  List KeyRestrictionViolation
keyRestrictionViolationsInAnnotated ax =
  keyRestrictionViolationsInAxiom ax (P.body ax)

keyRestrictionViolations :
  List (P.Annotated P.Axiom) →
  List KeyRestrictionViolation
keyRestrictionViolations axioms =
  concatMap keyRestrictionViolationsInAnnotated axioms

ontologyKeyRestrictionViolations :
  P.Ontology →
  List KeyRestrictionViolation
ontologyKeyRestrictionViolations ont =
  keyRestrictionViolations (P.axioms ont)

ontologyDocumentKeyRestrictionViolations :
  P.OntologyDocument →
  List KeyRestrictionViolation
ontologyDocumentKeyRestrictionViolations document =
  ontologyKeyRestrictionViolations (P.documentOntology document)

keyComponentEntityUsesInAxiom :
  P.Annotated P.Axiom →
  P.Axiom →
  List Decl.EntityUseFact
keyComponentEntityUsesInAxiom source (P.hasKey c key) =
  Decl.entityUsesInAxiom (Decl.axiomSource source) (P.hasKey c key)
keyComponentEntityUsesInAxiom source _ =
  []

keyComponentEntityUsesInAnnotated :
  P.Annotated P.Axiom →
  List Decl.EntityUseFact
keyComponentEntityUsesInAnnotated ax =
  keyComponentEntityUsesInAxiom ax (P.body ax)

keyComponentEntityUses :
  List (P.Annotated P.Axiom) →
  List Decl.EntityUseFact
keyComponentEntityUses axioms =
  concatMap keyComponentEntityUsesInAnnotated axioms

keyDeclarationCoverageGaps :
  List (P.Annotated P.Axiom) →
  List Decl.UndeclaredEntityUse
keyDeclarationCoverageGaps axioms =
  Decl.undeclaredEntityUsesFromFacts
    (PK.declarationFacts axioms)
    (keyComponentEntityUses axioms)

ontologyKeyDeclarationCoverageGaps :
  P.Ontology →
  List Decl.UndeclaredEntityUse
ontologyKeyDeclarationCoverageGaps ont =
  keyDeclarationCoverageGaps (P.axioms ont)

ontologyDocumentKeyDeclarationCoverageGaps :
  P.OntologyDocument →
  List Decl.UndeclaredEntityUse
ontologyDocumentKeyDeclarationCoverageGaps document =
  ontologyKeyDeclarationCoverageGaps (P.documentOntology document)

isHasKeyAxiom : P.Axiom → Bool
isHasKeyAxiom (P.hasKey c key) =
  true
isHasKeyAxiom _ =
  false

isHasKeySource : P.Annotated P.Axiom → Bool
isHasKeySource ax =
  isHasKeyAxiom (P.body ax)

propertyRoleUsageConflictInvolvesHasKey :
  PK.PropertyUsageConflict → Bool
propertyRoleUsageConflictInvolvesHasKey conflict
  with isHasKeySource (PK.leftPropertyUsageSource conflict)
     | isHasKeySource (PK.rightPropertyUsageSource conflict)
... | true | _ =
  true
... | _ | true =
  true
... | false | false =
  false

maybeKeyPropertyRoleUsageConflict :
  PK.PropertyUsageConflict → Optional PK.PropertyUsageConflict
maybeKeyPropertyRoleUsageConflict conflict
  with propertyRoleUsageConflictInvolvesHasKey conflict
... | true =
  present conflict
... | false =
  absent

keyPropertyRoleUsageConflicts :
  P.OntologyDocument →
  List PK.PropertyUsageConflict
keyPropertyRoleUsageConflicts document =
  filterMap
    maybeKeyPropertyRoleUsageConflict
    (PK.ontologyDocumentPropertyRoleUsageConflicts document)

record KeyRestrictionsReport : Type₀ where
  constructor keyRestrictionsReport
  field
    keyRestrictionsReportDocument :
      P.OntologyDocument
    keyRestrictionStructuralViolations :
      List KeyRestrictionViolation
    keyRestrictionDeclarationCoverageGaps :
      List Decl.UndeclaredEntityUse
    keyRestrictionPropertyRoleUsageConflicts :
      List PK.PropertyUsageConflict
    keyRestrictionStructuralViolationCount :
      ℕ
    keyRestrictionDeclarationCoverageGapCount :
      ℕ
    keyRestrictionPropertyRoleUsageConflictCount :
      ℕ

open KeyRestrictionsReport public

reportKeyRestrictions : P.OntologyDocument → KeyRestrictionsReport
reportKeyRestrictions document =
  keyRestrictionsReport
    document
    structuralViolations
    declarationCoverageGaps
    propertyRoleConflicts
    (listCount structuralViolations)
    (listCount declarationCoverageGaps)
    (listCount propertyRoleConflicts)
  where
  structuralViolations : List KeyRestrictionViolation
  structuralViolations =
    ontologyDocumentKeyRestrictionViolations document

  declarationCoverageGaps : List Decl.UndeclaredEntityUse
  declarationCoverageGaps =
    ontologyDocumentKeyDeclarationCoverageGaps document

  propertyRoleConflicts : List PK.PropertyUsageConflict
  propertyRoleConflicts =
    keyPropertyRoleUsageConflicts document

NoKeyRestrictionViolationRecords :
  List KeyRestrictionViolation → Type₀
NoKeyRestrictionViolationRecords [] =
  Unit*
NoKeyRestrictionViolationRecords (_ ∷ _) =
  ⊥

NoReportKeyRestrictionStructuralViolations :
  KeyRestrictionsReport → Type₀
NoReportKeyRestrictionStructuralViolations report =
  NoKeyRestrictionViolationRecords
    (keyRestrictionStructuralViolations report)

NoReportKeyDeclarationCoverageGaps :
  KeyRestrictionsReport → Type₀
NoReportKeyDeclarationCoverageGaps report =
  Decl.NoUndeclaredEntityUses
    (keyRestrictionDeclarationCoverageGaps report)

NoReportKeyPropertyRoleUsageConflicts :
  KeyRestrictionsReport → Type₀
NoReportKeyPropertyRoleUsageConflicts report =
  PK.NoPropertyUsageConflicts
    (keyRestrictionPropertyRoleUsageConflicts report)

NoKeyRestrictionStructuralViolations :
  P.OntologyDocument → Type₀
NoKeyRestrictionStructuralViolations document =
  NoReportKeyRestrictionStructuralViolations
    (reportKeyRestrictions document)

NoKeyRestrictionDeclarationCoverageGaps :
  P.OntologyDocument → Type₀
NoKeyRestrictionDeclarationCoverageGaps document =
  NoReportKeyDeclarationCoverageGaps
    (reportKeyRestrictions document)

NoKeyRestrictionPropertyRoleUsageConflicts :
  P.OntologyDocument → Type₀
NoKeyRestrictionPropertyRoleUsageConflicts document =
  NoReportKeyPropertyRoleUsageConflicts
    (reportKeyRestrictions document)

record NoKeyRestrictionViolations
  (document : P.OntologyDocument) : Type₀ where
  constructor noKeyRestrictionViolations
  field
    noKeyRestrictionStructuralViolations :
      NoKeyRestrictionStructuralViolations document
    noKeyRestrictionDeclarationCoverageGaps :
      NoKeyRestrictionDeclarationCoverageGaps document
    noKeyRestrictionPropertyRoleUsageConflicts :
      NoKeyRestrictionPropertyRoleUsageConflicts document

open NoKeyRestrictionViolations public