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

module OWL2.Examples.WebProtege.KeyRestrictions where

open import OWL2.Prelude
import OWL2.Examples.WebProtege.Annotations as A
import OWL2.Portable.Declarations as Decl
import OWL2.Portable.KeyRestrictions as KR
import OWL2.Portable.PropertyKinds as PK
import OWL2.Portable.Syntax as P
import OWL2.Profiles.EL as EL
import OWL2.Profiles.QL as QL
import OWL2.Profiles.RL as RL

axiom : P.Axiom → P.Annotated P.Axiom
axiom =
  A.axiom

document : List (P.Annotated P.Axiom) → P.OntologyDocument
document axioms =
  P.ontologyDocument
    (A.webProtegePrefix ∷ [])
    (P.ontology
      (P.ontologyIRI A.webProtegeOntologyIRI absent)
      []
      []
      axioms)

dataPropertyName : String → P.DataPropertyName
dataPropertyName text =
  P.named (P.iri text)

accession : P.DataPropertyName
accession =
  dataPropertyName "https://example.org/webprotege#accession"

Accession : P.DataPropertyExpression
Accession =
  P.dataProperty accession

keyDeclarationAxioms : List (P.Annotated P.Axiom)
keyDeclarationAxioms =
  A.declarationAxioms
  ++ (axiom (P.declaration (P.dataPropertyEntity accession)) ∷ [])

curatedDatasetKey : P.PropertyKey
curatedDatasetKey =
  P.propertyKey (A.HasCurator ∷ []) (Accession ∷ [])

acceptedKeyAxiom : P.Annotated P.Axiom
acceptedKeyAxiom =
  axiom (P.hasKey A.CuratedDatasetC curatedDatasetKey)

acceptedKeyDocument : P.OntologyDocument
acceptedKeyDocument =
  document (keyDeclarationAxioms ++ (acceptedKeyAxiom ∷ []))

acceptedKeyReport : KR.KeyRestrictionsReport
acceptedKeyReport =
  KR.reportKeyRestrictions acceptedKeyDocument

acceptedKeyStructuralViolations :
  KR.keyRestrictionStructuralViolations acceptedKeyReport ≡ []
acceptedKeyStructuralViolations =
  refl

acceptedKeyDeclarationCoverageGaps :
  KR.keyRestrictionDeclarationCoverageGaps acceptedKeyReport ≡ []
acceptedKeyDeclarationCoverageGaps =
  refl

acceptedKeyPropertyRoleConflicts :
  KR.keyRestrictionPropertyRoleUsageConflicts acceptedKeyReport ≡ []
acceptedKeyPropertyRoleConflicts =
  refl

acceptedKeyStructuralViolationCount :
  KR.keyRestrictionStructuralViolationCount acceptedKeyReport ≡ 
acceptedKeyStructuralViolationCount =
  refl

acceptedKeyDeclarationCoverageGapCount :
  KR.keyRestrictionDeclarationCoverageGapCount acceptedKeyReport ≡ 
acceptedKeyDeclarationCoverageGapCount =
  refl

acceptedKeyPropertyRoleConflictCount :
  KR.keyRestrictionPropertyRoleUsageConflictCount acceptedKeyReport ≡ 
acceptedKeyPropertyRoleConflictCount =
  refl

acceptedKeyNoRestrictions :
  KR.NoKeyRestrictionViolations acceptedKeyDocument
acceptedKeyNoRestrictions =
  KR.noKeyRestrictionViolations tt* tt* tt*

acceptedKeyNonELFeatures :
  EL.ontologyDocumentNonELFeatures acceptedKeyDocument ≡
  EL.hasKeyAxiomFeature ∷ []
acceptedKeyNonELFeatures =
  refl

acceptedKeyRejectedByELProfile :
  ¬ EL.ELDocument acceptedKeyDocument
acceptedKeyRejectedByELProfile impossible =
  impossible

acceptedKeyNonQLFeatures :
  QL.ontologyDocumentNonQLFeatures acceptedKeyDocument ≡
  QL.hasKeyAxiomFeature ∷ []
acceptedKeyNonQLFeatures =
  refl

acceptedKeyRejectedByQLProfile :
  ¬ QL.QLDocument acceptedKeyDocument
acceptedKeyRejectedByQLProfile impossible =
  impossible

acceptedKeyNonRLFeatures :
  RL.ontologyDocumentNonRLFeatures acceptedKeyDocument ≡ []
acceptedKeyNonRLFeatures =
  refl

acceptedKeyAcceptedByRLProfile :
  RL.RLDocument acceptedKeyDocument
acceptedKeyAcceptedByRLProfile =
  tt*

undeclaredKeyClass : P.ClassName
undeclaredKeyClass =
  P.named (P.iri "https://example.org/webprotege#UndeclaredKeyClass")

UndeclaredKeyClassC : P.ClassExpression
UndeclaredKeyClassC =
  P.namedClass undeclaredKeyClass

undeclaredKeyClassAxiom : P.Annotated P.Axiom
undeclaredKeyClassAxiom =
  axiom (P.hasKey UndeclaredKeyClassC curatedDatasetKey)

undeclaredKeyClassDocument : P.OntologyDocument
undeclaredKeyClassDocument =
  document (keyDeclarationAxioms ++ (undeclaredKeyClassAxiom ∷ []))

undeclaredKeyClassReport : KR.KeyRestrictionsReport
undeclaredKeyClassReport =
  KR.reportKeyRestrictions undeclaredKeyClassDocument

undeclaredKeyClassDeclarationCoverageGaps :
  KR.keyRestrictionDeclarationCoverageGaps undeclaredKeyClassReport ≡
  Decl.undeclaredEntityUse
    (PK.nameKey undeclaredKeyClass)
    PK.classRole
    (Decl.axiomSource undeclaredKeyClassAxiom)
  ∷ []
undeclaredKeyClassDeclarationCoverageGaps =
  refl

undeclaredKeyClassDeclarationCoverageGapCount :
  KR.keyRestrictionDeclarationCoverageGapCount undeclaredKeyClassReport ≡ 
undeclaredKeyClassDeclarationCoverageGapCount =
  refl

undeclaredKeyClassRejectedByPackagedPredicate :
  ¬ KR.NoKeyRestrictionViolations undeclaredKeyClassDocument
undeclaredKeyClassRejectedByPackagedPredicate impossible =
  KR.noKeyRestrictionDeclarationCoverageGaps impossible

undeclaredKeyDataProperty : P.DataPropertyName
undeclaredKeyDataProperty =
  dataPropertyName
    "https://example.org/webprotege#undeclaredKeyDataProperty"

UndeclaredKeyDataProperty : P.DataPropertyExpression
UndeclaredKeyDataProperty =
  P.dataProperty undeclaredKeyDataProperty

undeclaredDataPropertyKey : P.PropertyKey
undeclaredDataPropertyKey =
  P.propertyKey [] (UndeclaredKeyDataProperty ∷ [])

undeclaredDataPropertyKeyAxiom : P.Annotated P.Axiom
undeclaredDataPropertyKeyAxiom =
  axiom (P.hasKey A.CuratedDatasetC undeclaredDataPropertyKey)

undeclaredDataPropertyKeyDocument : P.OntologyDocument
undeclaredDataPropertyKeyDocument =
  document (A.declarationAxioms ++ (undeclaredDataPropertyKeyAxiom ∷ []))

undeclaredDataPropertyKeyReport : KR.KeyRestrictionsReport
undeclaredDataPropertyKeyReport =
  KR.reportKeyRestrictions undeclaredDataPropertyKeyDocument

undeclaredDataPropertyKeyDeclarationCoverageGaps :
  KR.keyRestrictionDeclarationCoverageGaps
    undeclaredDataPropertyKeyReport
  ≡
  Decl.undeclaredEntityUse
    (PK.nameKey undeclaredKeyDataProperty)
    PK.dataPropertyRole
    (Decl.axiomSource undeclaredDataPropertyKeyAxiom)
  ∷ []
undeclaredDataPropertyKeyDeclarationCoverageGaps =
  refl

undeclaredDataPropertyKeyDeclarationCoverageGapCount :
  KR.keyRestrictionDeclarationCoverageGapCount
    undeclaredDataPropertyKeyReport
  ≡ 
undeclaredDataPropertyKeyDeclarationCoverageGapCount =
  refl

undeclaredDataPropertyKeyRejectedByPackagedPredicate :
  ¬ KR.NoKeyRestrictionViolations undeclaredDataPropertyKeyDocument
undeclaredDataPropertyKeyRejectedByPackagedPredicate impossible =
  KR.noKeyRestrictionDeclarationCoverageGaps impossible

inverseCuratorKey : P.PropertyKey
inverseCuratorKey =
  P.propertyKey (P.objectInverseOf A.HasCurator ∷ []) []

objectKeyRejectedAxiom : P.Annotated P.Axiom
objectKeyRejectedAxiom =
  axiom (P.hasKey A.CuratedDatasetC inverseCuratorKey)

objectKeyRejectedDocument : P.OntologyDocument
objectKeyRejectedDocument =
  document (keyDeclarationAxioms ++ (objectKeyRejectedAxiom ∷ []))

objectKeyRejectedReport : KR.KeyRestrictionsReport
objectKeyRejectedReport =
  KR.reportKeyRestrictions objectKeyRejectedDocument

objectKeyRejectedStructuralViolations :
  KR.keyRestrictionStructuralViolations objectKeyRejectedReport ≡
  KR.objectKeyPropertyExpressionNotNamed
    objectKeyRejectedAxiom
    (P.objectInverseOf A.HasCurator)
  ∷ []
objectKeyRejectedStructuralViolations =
  refl

objectKeyRejectedByPackagedPredicate :
  ¬ KR.NoKeyRestrictionViolations objectKeyRejectedDocument
objectKeyRejectedByPackagedPredicate impossible =
  KR.noKeyRestrictionStructuralViolations impossible

topDataPropertyKey : P.PropertyKey
topDataPropertyKey =
  P.propertyKey [] (P.topDataProperty ∷ [])

dataKeyRejectedAxiom : P.Annotated P.Axiom
dataKeyRejectedAxiom =
  axiom (P.hasKey A.CuratedDatasetC topDataPropertyKey)

dataKeyRejectedDocument : P.OntologyDocument
dataKeyRejectedDocument =
  document (keyDeclarationAxioms ++ (dataKeyRejectedAxiom ∷ []))

dataKeyRejectedReport : KR.KeyRestrictionsReport
dataKeyRejectedReport =
  KR.reportKeyRestrictions dataKeyRejectedDocument

dataKeyRejectedStructuralViolations :
  KR.keyRestrictionStructuralViolations dataKeyRejectedReport ≡
  KR.dataKeyPropertyExpressionNotNamed
    dataKeyRejectedAxiom
    P.topDataProperty
  ∷ []
dataKeyRejectedStructuralViolations =
  refl

dataKeyRejectedByPackagedPredicate :
  ¬ KR.NoKeyRestrictionViolations dataKeyRejectedDocument
dataKeyRejectedByPackagedPredicate impossible =
  KR.noKeyRestrictionStructuralViolations impossible

dataRoleMismatchKey : P.PropertyKey
dataRoleMismatchKey =
  P.propertyKey [] (P.dataProperty A.hasCurator ∷ [])

dataRoleMismatchAxiom : P.Annotated P.Axiom
dataRoleMismatchAxiom =
  axiom (P.hasKey A.CuratedDatasetC dataRoleMismatchKey)

dataRoleMismatchDocument : P.OntologyDocument
dataRoleMismatchDocument =
  document (A.declarationAxioms ++ (dataRoleMismatchAxiom ∷ []))

dataRoleMismatchReport : KR.KeyRestrictionsReport
dataRoleMismatchReport =
  KR.reportKeyRestrictions dataRoleMismatchDocument

dataRoleMismatchStructuralViolations :
  KR.keyRestrictionStructuralViolations dataRoleMismatchReport ≡ []
dataRoleMismatchStructuralViolations =
  refl

dataRoleMismatchDeclarationCoverageGapCount :
  KR.keyRestrictionDeclarationCoverageGapCount
    dataRoleMismatchReport
  ≡ 
dataRoleMismatchDeclarationCoverageGapCount =
  refl

dataRoleMismatchPropertyRoleConflictCount :
  KR.keyRestrictionPropertyRoleUsageConflictCount
    dataRoleMismatchReport
  ≡ 
dataRoleMismatchPropertyRoleConflictCount =
  refl

dataRoleMismatchRejectedByPackagedPredicate :
  ¬ KR.NoKeyRestrictionViolations dataRoleMismatchDocument
dataRoleMismatchRejectedByPackagedPredicate impossible =
  KR.noKeyRestrictionPropertyRoleUsageConflicts impossible