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

module OWL2.Syntax.Punning where

open import OWL2.Prelude
open import OWL2.Syntax
open import OWL2.Syntax.Declarations
open import OWL2.Syntax.PropertyKinds

entityKind :
  ∀ {ℓ} {Sig : Signature ℓ} →
  Entity Sig → EntityKind
entityKind (classEntity c) =
  class
entityKind (objectPropertyEntity p) =
  objectProperty
entityKind (dataPropertyEntity p) =
  dataProperty
entityKind (datatypeEntity d) =
  datatype
entityKind (individualEntity x) =
  individual
entityKind (annotationPropertyEntity p) =
  annotationProperty

data SameEntityKind : EntityKind → EntityKind → Type₀ where
  sameClassKind :
    SameEntityKind class class
  sameObjectPropertyKind :
    SameEntityKind objectProperty objectProperty
  sameDataPropertyKind :
    SameEntityKind dataProperty dataProperty
  sameDatatypeKind :
    SameEntityKind datatype datatype
  sameIndividualKind :
    SameEntityKind individual individual
  sameAnnotationPropertyKind :
    SameEntityKind annotationProperty annotationProperty

propertyKindEntityKind :
  PropertyKind → EntityKind
propertyKindEntityKind objectPropertyKind =
  objectProperty
propertyKindEntityKind dataPropertyKind =
  dataProperty
propertyKindEntityKind annotationPropertyKind =
  annotationProperty

record EntityIdentifier
  {ℓ : Level}
  (Sig : Signature ℓ)
  : Type (ℓ-suc ℓ) where
  field
    Identifier :
      Type ℓ
    classIdentifier :
      ClassName Sig → Identifier
    objectPropertyIdentifier :
      ObjectPropertyName Sig → Identifier
    dataPropertyIdentifier :
      DataPropertyName Sig → Identifier
    datatypeIdentifier :
      DatatypeName Sig → Identifier
    individualIdentifier :
      IndividualName Sig → Identifier
    annotationPropertyIdentifier :
      AnnotationPropertyName Sig → Identifier

open EntityIdentifier public

entityIdentifier :
  ∀ {ℓ} {Sig : Signature ℓ}
    (ids : EntityIdentifier Sig) →
  Entity Sig → Identifier ids
entityIdentifier ids (classEntity c) =
  classIdentifier ids c
entityIdentifier ids (objectPropertyEntity p) =
  objectPropertyIdentifier ids p
entityIdentifier ids (dataPropertyEntity p) =
  dataPropertyIdentifier ids p
entityIdentifier ids (datatypeEntity d) =
  datatypeIdentifier ids d
entityIdentifier ids (individualEntity x) =
  individualIdentifier ids x
entityIdentifier ids (annotationPropertyEntity p) =
  annotationPropertyIdentifier ids p

record NoEntityPunning
  {ℓ : Level} {Sig : Signature ℓ}
  (ids : EntityIdentifier Sig)
  (Γ : DeclarationEnvironment Sig)
  : Type ℓ where
  field
    noPunning :
      ∀ e f →
      EntityDeclared Γ e →
      EntityDeclared Γ f →
      entityIdentifier ids e ≡ entityIdentifier ids f →
      SameEntityKind (entityKind e) (entityKind f)

open NoEntityPunning public

record OWL2DLTypingConstraints
  {ℓ : Level} {Sig : Signature ℓ}
  (ids : EntityIdentifier Sig)
  (Γ : DeclarationEnvironment Sig)
  : Type ℓ where
  field
    objectDataPropertiesDisjoint :
      ∀ p q →
      objectPropertyDeclared Γ p →
      dataPropertyDeclared Γ q →
      ¬ (objectPropertyIdentifier ids p ≡ dataPropertyIdentifier ids q)
    objectAnnotationPropertiesDisjoint :
      ∀ p q →
      objectPropertyDeclared Γ p →
      annotationPropertyDeclared Γ q →
      ¬ (objectPropertyIdentifier ids p ≡ annotationPropertyIdentifier ids q)
    dataAnnotationPropertiesDisjoint :
      ∀ p q →
      dataPropertyDeclared Γ p →
      annotationPropertyDeclared Γ q →
      ¬ (dataPropertyIdentifier ids p ≡ annotationPropertyIdentifier ids q)
    classDatatypesDisjoint :
      ∀ c d →
      classDeclared Γ c →
      datatypeDeclared Γ d →
      ¬ (classIdentifier ids c ≡ datatypeIdentifier ids d)

open OWL2DLTypingConstraints public

objectDataKindContradiction :
  SameEntityKind objectProperty dataProperty → ⊥
objectDataKindContradiction ()

objectAnnotationKindContradiction :
  SameEntityKind objectProperty annotationProperty → ⊥
objectAnnotationKindContradiction ()

dataAnnotationKindContradiction :
  SameEntityKind dataProperty annotationProperty → ⊥
dataAnnotationKindContradiction ()

classDatatypeKindContradiction :
  SameEntityKind class datatype → ⊥
classDatatypeKindContradiction ()

classIndividualKindContradiction :
  SameEntityKind class individual → ⊥
classIndividualKindContradiction ()

noEntityPunningImpliesOWL2DLTypingConstraints :
  ∀ {ℓ} {Sig : Signature ℓ}
    {ids : EntityIdentifier Sig}
    {Γ : DeclarationEnvironment Sig} →
  NoEntityPunning ids Γ →
  OWL2DLTypingConstraints ids Γ
noEntityPunningImpliesOWL2DLTypingConstraints noEntityPunning
  .objectDataPropertiesDisjoint p q pΓ qΓ sameIdentifier =
    objectDataKindContradiction
      (NoEntityPunning.noPunning noEntityPunning
        (objectPropertyEntity p)
        (dataPropertyEntity q)
        pΓ
        qΓ
        sameIdentifier)
noEntityPunningImpliesOWL2DLTypingConstraints noEntityPunning
  .objectAnnotationPropertiesDisjoint p q pΓ qΓ sameIdentifier =
    objectAnnotationKindContradiction
      (NoEntityPunning.noPunning noEntityPunning
        (objectPropertyEntity p)
        (annotationPropertyEntity q)
        pΓ
        qΓ
        sameIdentifier)
noEntityPunningImpliesOWL2DLTypingConstraints noEntityPunning
  .dataAnnotationPropertiesDisjoint p q pΓ qΓ sameIdentifier =
    dataAnnotationKindContradiction
      (NoEntityPunning.noPunning noEntityPunning
        (dataPropertyEntity p)
        (annotationPropertyEntity q)
        pΓ
        qΓ
        sameIdentifier)
noEntityPunningImpliesOWL2DLTypingConstraints noEntityPunning
  .classDatatypesDisjoint c d cΓ dΓ sameIdentifier =
    classDatatypeKindContradiction
      (NoEntityPunning.noPunning noEntityPunning
        (classEntity c)
        (datatypeEntity d)
        cΓ
        dΓ
        sameIdentifier)