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

module OWL2.Syntax.PropertyKinds where

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

data PropertyKind : Type₀ where
  objectPropertyKind dataPropertyKind annotationPropertyKind :
    PropertyKind

PropertyName :
  ∀ {ℓ} →
  Signature ℓ → PropertyKind → Type ℓ
PropertyName Sig objectPropertyKind =
  ObjectPropertyName Sig
PropertyName Sig dataPropertyKind =
  DataPropertyName Sig
PropertyName Sig annotationPropertyKind =
  AnnotationPropertyName Sig

propertyEntity :
  ∀ {ℓ} {Sig : Signature ℓ}
    (kind : PropertyKind) →
  PropertyName Sig kind → Entity Sig
propertyEntity objectPropertyKind p =
  objectPropertyEntity p
propertyEntity dataPropertyKind p =
  dataPropertyEntity p
propertyEntity annotationPropertyKind p =
  annotationPropertyEntity p

PropertyDeclared :
  ∀ {ℓ} {Sig : Signature ℓ} →
  DeclarationEnvironment Sig →
  (kind : PropertyKind) →
  PropertyName Sig kind → Type ℓ
PropertyDeclared Γ objectPropertyKind p =
  objectPropertyDeclared Γ p
PropertyDeclared Γ dataPropertyKind p =
  dataPropertyDeclared Γ p
PropertyDeclared Γ annotationPropertyKind p =
  annotationPropertyDeclared Γ p

data DeclaredProperty
  {ℓ : Level} {Sig : Signature ℓ}
  (Γ : DeclarationEnvironment Sig)
  : Type ℓ where
  declaredObjectProperty :
    (p : ObjectPropertyName Sig) →
    objectPropertyDeclared Γ p →
    DeclaredProperty Γ
  declaredDataProperty :
    (p : DataPropertyName Sig) →
    dataPropertyDeclared Γ p →
    DeclaredProperty Γ
  declaredAnnotationProperty :
    (p : AnnotationPropertyName Sig) →
    annotationPropertyDeclared Γ p →
    DeclaredProperty Γ

declaredPropertyKind :
  ∀ {ℓ} {Sig : Signature ℓ}
    {Γ : DeclarationEnvironment Sig} →
  DeclaredProperty Γ → PropertyKind
declaredPropertyKind (declaredObjectProperty p pΓ) =
  objectPropertyKind
declaredPropertyKind (declaredDataProperty p pΓ) =
  dataPropertyKind
declaredPropertyKind (declaredAnnotationProperty p pΓ) =
  annotationPropertyKind

declaredPropertyEntity :
  ∀ {ℓ} {Sig : Signature ℓ}
    {Γ : DeclarationEnvironment Sig} →
  DeclaredProperty Γ → Entity Sig
declaredPropertyEntity (declaredObjectProperty p pΓ) =
  objectPropertyEntity p
declaredPropertyEntity (declaredDataProperty p pΓ) =
  dataPropertyEntity p
declaredPropertyEntity (declaredAnnotationProperty p pΓ) =
  annotationPropertyEntity p