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

module OWL2.Examples.Punning where

open import OWL2.Prelude
open import OWL2.Syntax
open import OWL2.Syntax.Declarations
open import OWL2.Syntax.WellFormed
open import OWL2.Syntax.PropertyKinds
open import OWL2.Syntax.Punning
open import OWL2.Syntax.GlobalRestrictions
import OWL2.Examples.GlobalRestrictions as Global
import OWL2.Examples.PropertyChain as Chain
import OWL2.Examples.Regularity as Reg

data ChainIdentifier : Type₀ where
  personID parentID grandparentID dataPropertyID datatypeID :
    ChainIdentifier
  aliceID bobID carolID annotationID :
    ChainIdentifier

chainEntityIdentifier :
  EntityIdentifier Chain.ChainSignature
chainEntityIdentifier .Identifier =
  ChainIdentifier
chainEntityIdentifier .classIdentifier Chain.Person =
  personID
chainEntityIdentifier .objectPropertyIdentifier Chain.hasParent =
  parentID
chainEntityIdentifier .objectPropertyIdentifier Chain.hasGrandparent =
  grandparentID
chainEntityIdentifier .dataPropertyIdentifier Chain.noDataProperty =
  dataPropertyID
chainEntityIdentifier .datatypeIdentifier Chain.noDatatype =
  datatypeID
chainEntityIdentifier .individualIdentifier Chain.Alice =
  aliceID
chainEntityIdentifier .individualIdentifier Chain.Bob =
  bobID
chainEntityIdentifier .individualIdentifier Chain.Carol =
  carolID
chainEntityIdentifier .annotationPropertyIdentifier Chain.label =
  annotationID

chainTypedEnvironment :
  DeclarationEnvironment Chain.ChainSignature
chainTypedEnvironment =
  declarationEnvironment
    (λ _ → Unit*)
    (λ _ → Unit*)
    (λ _ → ⊥)
    (λ _ → ⊥)
    (λ _ → Unit*)
    (λ _ → ⊥)

declaredChainOntologyWellFormedInTypedEnvironment :
  OntologyWellFormed
    chainTypedEnvironment
    Global.declaredChainOntology
declaredChainOntologyWellFormedInTypedEnvironment =
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  ((tt* , (tt* , tt*)) , tt*) ,
  (tt* , (tt* , tt*)) ,
  (tt* , (tt* , tt*)) ,
  (tt* , (tt* , tt*)) ,
  tt*

declaredChainGlobalRestrictionsInTypedEnvironment :
  OntologyGlobalRestrictions
    chainTypedEnvironment
    Reg.chainRegularityContext
    Global.declaredChainOntology
declaredChainGlobalRestrictionsInTypedEnvironment .wellFormed =
  declaredChainOntologyWellFormedInTypedEnvironment
declaredChainGlobalRestrictionsInTypedEnvironment .contextualRegularity =
  Global.declaredChainContextualRegular

chainTypingConstraints :
  OWL2DLTypingConstraints
    chainEntityIdentifier
    chainTypedEnvironment
chainTypingConstraints .objectDataPropertiesDisjoint
  p Chain.noDataProperty pΓ qΓ sameIdentifier =
    qΓ
chainTypingConstraints .objectAnnotationPropertiesDisjoint
  p Chain.label pΓ qΓ sameIdentifier =
    qΓ
chainTypingConstraints .dataAnnotationPropertiesDisjoint
  Chain.noDataProperty q pΓ qΓ sameIdentifier =
    pΓ
chainTypingConstraints .classDatatypesDisjoint
  Chain.Person Chain.noDatatype cΓ dΓ sameIdentifier =
    dΓ

declaredParentProperty :
  DeclaredProperty chainTypedEnvironment
declaredParentProperty =
  declaredObjectProperty Chain.hasParent tt*

declaredParentPropertyKind :
  declaredPropertyKind declaredParentProperty ≡ objectPropertyKind
declaredParentPropertyKind =
  refl

declaredParentPropertyEntity :
  declaredPropertyEntity declaredParentProperty
  ≡
  objectPropertyEntity Chain.hasParent
declaredParentPropertyEntity =
  refl

declaredChainTypedGlobalRestrictions :
  OntologyTypedGlobalRestrictions
    chainEntityIdentifier
    chainTypedEnvironment
    Reg.chainRegularityContext
    Global.declaredChainOntology
declaredChainTypedGlobalRestrictions .globalRestrictions =
  declaredChainGlobalRestrictionsInTypedEnvironment
declaredChainTypedGlobalRestrictions .typingConstraints =
  chainTypingConstraints

CollisionSignature : Signature ℓ-zero
CollisionSignature .IRI =
  ⊥
CollisionSignature .ClassName =
  Unit
CollisionSignature .ObjectPropertyName =
  ⊥
CollisionSignature .DataPropertyName =
  ⊥
CollisionSignature .DatatypeName =
  Unit
CollisionSignature .IndividualName =
  ⊥
CollisionSignature .Literal =
  ⊥
CollisionSignature .FacetName =
  ⊥
CollisionSignature .AnnotationPropertyName =
  ⊥

data CollisionIdentifier : Type₀ where
  sharedID : CollisionIdentifier

collisionEntityIdentifier :
  EntityIdentifier CollisionSignature
collisionEntityIdentifier .Identifier =
  CollisionIdentifier
collisionEntityIdentifier .classIdentifier tt =
  sharedID
collisionEntityIdentifier .objectPropertyIdentifier ()
collisionEntityIdentifier .dataPropertyIdentifier ()
collisionEntityIdentifier .datatypeIdentifier tt =
  sharedID
collisionEntityIdentifier .individualIdentifier ()
collisionEntityIdentifier .annotationPropertyIdentifier ()

collisionEnvironment :
  DeclarationEnvironment CollisionSignature
collisionEnvironment =
  declarationEnvironment
    (λ _ → Unit*)
    (λ ())
    (λ ())
    (λ _ → Unit*)
    (λ ())
    (λ ())

collisionNoEntityPunningRejected :
  ¬ NoEntityPunning collisionEntityIdentifier collisionEnvironment
collisionNoEntityPunningRejected noEntityPunning =
  classDatatypeKindContradiction
    (NoEntityPunning.noPunning noEntityPunning
      (classEntity tt)
      (datatypeEntity tt)
      tt*
      tt*
      refl)

collisionOWL2DLTypingRejected :
  ¬ OWL2DLTypingConstraints
      collisionEntityIdentifier
      collisionEnvironment
collisionOWL2DLTypingRejected constraints =
  OWL2DLTypingConstraints.classDatatypesDisjoint
    constraints
    tt
    tt
    tt*
    tt*
    refl

ClassIndividualSignature : Signature ℓ-zero
ClassIndividualSignature .IRI =
  ⊥
ClassIndividualSignature .ClassName =
  Unit
ClassIndividualSignature .ObjectPropertyName =
  ⊥
ClassIndividualSignature .DataPropertyName =
  ⊥
ClassIndividualSignature .DatatypeName =
  ⊥
ClassIndividualSignature .IndividualName =
  Unit
ClassIndividualSignature .Literal =
  ⊥
ClassIndividualSignature .FacetName =
  ⊥
ClassIndividualSignature .AnnotationPropertyName =
  ⊥

classIndividualEntityIdentifier :
  EntityIdentifier ClassIndividualSignature
classIndividualEntityIdentifier .Identifier =
  CollisionIdentifier
classIndividualEntityIdentifier .classIdentifier tt =
  sharedID
classIndividualEntityIdentifier .objectPropertyIdentifier ()
classIndividualEntityIdentifier .dataPropertyIdentifier ()
classIndividualEntityIdentifier .datatypeIdentifier ()
classIndividualEntityIdentifier .individualIdentifier tt =
  sharedID
classIndividualEntityIdentifier .annotationPropertyIdentifier ()

classIndividualEnvironment :
  DeclarationEnvironment ClassIndividualSignature
classIndividualEnvironment =
  declarationEnvironment
    (λ _ → Unit*)
    (λ ())
    (λ ())
    (λ ())
    (λ _ → Unit*)
    (λ ())

classIndividualNoEntityPunningRejected :
  ¬ NoEntityPunning
      classIndividualEntityIdentifier
      classIndividualEnvironment
classIndividualNoEntityPunningRejected noEntityPunning =
  classIndividualKindContradiction
    (NoEntityPunning.noPunning noEntityPunning
      (classEntity tt)
      (individualEntity tt)
      tt*
      tt*
      refl)

classIndividualOWL2DLTypingAllowed :
  OWL2DLTypingConstraints
    classIndividualEntityIdentifier
    classIndividualEnvironment
classIndividualOWL2DLTypingAllowed .objectDataPropertiesDisjoint ()
classIndividualOWL2DLTypingAllowed .objectAnnotationPropertiesDisjoint ()
classIndividualOWL2DLTypingAllowed .dataAnnotationPropertiesDisjoint ()
classIndividualOWL2DLTypingAllowed .classDatatypesDisjoint c ()