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

module OWL2.Examples.Portable.PropertyKinds where

open import OWL2.Prelude
import OWL2.Check.Result as CheckResult
import OWL2.Portable.Check.Declarations as CheckDeclarations
import OWL2.Portable.Check.PropertyRoles as CheckPropertyRoles
import OWL2.Portable.Syntax as P
open import OWL2.Portable.PropertyKinds

name : String → P.Name
name text =
  P.named (P.iri text)

className : String → P.ClassName
className =
  name

objectPropertyName : String → P.ObjectPropertyName
objectPropertyName =
  name

dataPropertyName : String → P.DataPropertyName
dataPropertyName =
  name

datatypeName : String → P.DatatypeName
datatypeName =
  name

axiom : P.Axiom → P.Annotated P.Axiom
axiom body =
  P.annotated [] body

document : List (P.Annotated P.Axiom) → P.OntologyDocument
document axioms =
  P.ontologyDocument [] (P.ontology P.anonymousOntology [] [] axioms)

person : P.ClassName
person =
  className "https://example.org/portable#Person"

hasParent : P.ObjectPropertyName
hasParent =
  objectPropertyName "https://example.org/portable#hasParent"

age : P.DataPropertyName
age =
  dataPropertyName "https://example.org/portable#age"

integer : P.DatatypeName
integer =
  datatypeName "http://www.w3.org/2001/XMLSchema#integer"

aliceName : P.NamedIndividualName
aliceName =
  P.iri "https://example.org/portable#Alice"

cleanAxioms : List (P.Annotated P.Axiom)
cleanAxioms =
  axiom (P.declaration (P.classEntity person))
  ∷ axiom (P.declaration (P.objectPropertyEntity hasParent))
  ∷ axiom (P.declaration (P.dataPropertyEntity age))
  ∷ axiom (P.declaration (P.datatypeEntity integer))
  ∷ axiom (P.declaration (P.namedIndividualEntity aliceName))
  ∷ []

cleanDocument : P.OntologyDocument
cleanDocument =
  document cleanAxioms

cleanDeclarationRolesConsistent :
  OWL2DLDeclarationRolesConsistent cleanDocument
cleanDeclarationRolesConsistent =
  tt*

cleanPropertyRoleUsagesConsistent :
  PropertyRoleUsageConsistent cleanDocument
cleanPropertyRoleUsagesConsistent =
  tt*

cleanDeclarationCheckResult :
  CheckDeclarations.DeclarationCheckResult
cleanDeclarationCheckResult =
  CheckDeclarations.checkDeclarations cleanDocument

cleanDeclarationCheckDiagnostics :
  CheckResult.diagnostics cleanDeclarationCheckResult ≡ []
cleanDeclarationCheckDiagnostics =
  refl

cleanPropertyRoleCheckResult :
  CheckPropertyRoles.PropertyRoleCheckResult
cleanPropertyRoleCheckResult =
  CheckPropertyRoles.checkPropertyRoles cleanDocument

cleanPropertyRoleCheckDiagnostics :
  CheckResult.diagnostics cleanPropertyRoleCheckResult ≡ []
cleanPropertyRoleCheckDiagnostics =
  refl

sharedProperty : P.Name
sharedProperty =
  name "https://example.org/portable#sharedProperty"

propertyCollisionDocument : P.OntologyDocument
propertyCollisionDocument =
  document
    ( axiom (P.declaration (P.objectPropertyEntity sharedProperty))
    ∷ axiom (P.declaration (P.dataPropertyEntity sharedProperty))
    ∷ [] )

propertyCollisionRejected :
  ¬ OWL2DLDeclarationRolesConsistent propertyCollisionDocument
propertyCollisionRejected impossible =
  impossible

propertyCollisionDeclarationCheckResult :
  CheckDeclarations.DeclarationCheckResult
propertyCollisionDeclarationCheckResult =
  CheckDeclarations.checkDeclarations propertyCollisionDocument

propertyCollisionDeclarationCheckDiagnostics :
  CheckResult.diagnostics propertyCollisionDeclarationCheckResult ≡
  CheckDeclarations.declarationRoleCollisionDiagnostic
    (declarationCollision
      "https://example.org/portable#sharedProperty"
      objectPropertyRole
      dataPropertyRole
      propertyKindCollision
      (axiom (P.declaration (P.objectPropertyEntity sharedProperty)))
      (axiom (P.declaration (P.dataPropertyEntity sharedProperty))))
  ∷ []
propertyCollisionDeclarationCheckDiagnostics =
  refl

propertyCollisionDeclarationCheckUnclean :
  CheckResult.clean? propertyCollisionDeclarationCheckResult ≡ false
propertyCollisionDeclarationCheckUnclean =
  refl

propertyCollisionDeclarationCheckEvidenceUnavailable :
  CheckResult.evidence? propertyCollisionDeclarationCheckResult ≡ absent
propertyCollisionDeclarationCheckEvidenceUnavailable =
  refl

propertyCollisionRejectedByUsageScan :
  ¬ PropertyRoleUsageConsistent propertyCollisionDocument
propertyCollisionRejectedByUsageScan impossible =
  impossible

sharedClassDatatype : P.Name
sharedClassDatatype =
  name "https://example.org/portable#sharedClassDatatype"

classDatatypeCollisionDocument : P.OntologyDocument
classDatatypeCollisionDocument =
  document
    ( axiom (P.declaration (P.classEntity sharedClassDatatype))
    ∷ axiom (P.declaration (P.datatypeEntity sharedClassDatatype))
    ∷ [] )

classDatatypeCollisionRejected :
  ¬ OWL2DLDeclarationRolesConsistent classDatatypeCollisionDocument
classDatatypeCollisionRejected impossible =
  impossible

reservedClassDatatypeCollisionDocument : P.OntologyDocument
reservedClassDatatypeCollisionDocument =
  document
    ( axiom (P.declaration (P.classEntity (P.reserved P.owlThingIRI)))
    ∷ axiom
        (P.declaration
          (P.datatypeEntity
            (P.named (P.iri "http://www.w3.org/2002/07/owl#Thing"))))
    ∷ [] )

reservedClassDatatypeCollisionRejected :
  ¬ OWL2DLDeclarationRolesConsistent reservedClassDatatypeCollisionDocument
reservedClassDatatypeCollisionRejected impossible =
  impossible

classIndividualSharedIRI : P.IRI
classIndividualSharedIRI =
  P.iri "https://example.org/portable#ClassIndividualSharedIRI"

classIndividualPunningDocument : P.OntologyDocument
classIndividualPunningDocument =
  document
    ( axiom
        (P.declaration
          (P.classEntity (P.named classIndividualSharedIRI)))
    ∷ axiom
        (P.declaration
          (P.namedIndividualEntity classIndividualSharedIRI))
    ∷ [] )

classIndividualPunningAllowedByOWL2DL :
  OWL2DLDeclarationRolesConsistent classIndividualPunningDocument
classIndividualPunningAllowedByOWL2DL =
  tt*

classIndividualPunningRejectedByStrictPolicy :
  ¬ StrictDeclarationRolesConsistent classIndividualPunningDocument
classIndividualPunningRejectedByStrictPolicy impossible =
  impossible

usageOnlySharedProperty : P.Name
usageOnlySharedProperty =
  name "https://example.org/portable#usageOnlySharedProperty"

aliceIndividual : P.Individual
aliceIndividual =
  P.namedIndividual aliceName

usageOnlyConflictDocument : P.OntologyDocument
usageOnlyConflictDocument =
  document
    ( axiom
        (P.objectPropertyAssertion
          (P.objectProperty usageOnlySharedProperty)
          aliceIndividual
          aliceIndividual)
    ∷ axiom
        (P.dataPropertyAssertion
          (P.dataProperty usageOnlySharedProperty)
          aliceIndividual
          (P.stringLiteral "value"))
    ∷ [] )

usageOnlyDeclarationRolesConsistent :
  OWL2DLDeclarationRolesConsistent usageOnlyConflictDocument
usageOnlyDeclarationRolesConsistent =
  tt*

usageOnlyConflictRejectedByUsageScan :
  ¬ PropertyRoleUsageConsistent usageOnlyConflictDocument
usageOnlyConflictRejectedByUsageScan impossible =
  impossible

usageOnlyPropertyRoleCheckResult :
  CheckPropertyRoles.PropertyRoleCheckResult
usageOnlyPropertyRoleCheckResult =
  CheckPropertyRoles.checkPropertyRoles usageOnlyConflictDocument

usageOnlyPropertyRoleCheckDiagnostics :
  CheckResult.diagnostics usageOnlyPropertyRoleCheckResult ≡
  CheckPropertyRoles.propertyRoleUsageConflictDiagnostic
    (propertyUsageConflict
      "https://example.org/portable#usageOnlySharedProperty"
      objectPropertyUsageRole
      dataPropertyUsageRole
      (axiom
        (P.objectPropertyAssertion
          (P.objectProperty usageOnlySharedProperty)
          aliceIndividual
          aliceIndividual))
      (axiom
        (P.dataPropertyAssertion
          (P.dataProperty usageOnlySharedProperty)
          aliceIndividual
          (P.stringLiteral "value"))))
  ∷ []
usageOnlyPropertyRoleCheckDiagnostics =
  refl

usageOnlyPropertyRoleCheckUnclean :
  CheckResult.clean? usageOnlyPropertyRoleCheckResult ≡ false
usageOnlyPropertyRoleCheckUnclean =
  refl

usageOnlyPropertyRoleCheckEvidenceUnavailable :
  CheckResult.evidence? usageOnlyPropertyRoleCheckResult ≡ absent
usageOnlyPropertyRoleCheckEvidenceUnavailable =
  refl