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

module OWL2.Syntax.Declarations where

open import OWL2.Prelude
open import OWL2.Syntax

private
  AnyList :
    ∀ {ℓA ℓP} {A : Type ℓA} →
    List A → (A → Type ℓP) → Type (ℓ-max ℓA ℓP)
  AnyList [] P =
    ⊥*
  AnyList (x ∷ xs) P =
    P x ⊎ AnyList xs P

record DeclarationEnvironment {ℓ : Level} (Sig : Signature ℓ) : Type (ℓ-suc ℓ) where
  constructor declarationEnvironment
  field
    classDeclared :
      ClassName Sig → Type ℓ
    objectPropertyDeclared :
      ObjectPropertyName Sig → Type ℓ
    dataPropertyDeclared :
      DataPropertyName Sig → Type ℓ
    datatypeDeclared :
      DatatypeName Sig → Type ℓ
    individualDeclared :
      IndividualName Sig → Type ℓ
    annotationPropertyDeclared :
      AnnotationPropertyName Sig → Type ℓ

open DeclarationEnvironment public

EntityDeclared :
  ∀ {ℓ} {Sig : Signature ℓ} →
  DeclarationEnvironment Sig → Entity Sig → Type ℓ
EntityDeclared Γ (classEntity c) =
  classDeclared Γ c
EntityDeclared Γ (objectPropertyEntity p) =
  objectPropertyDeclared Γ p
EntityDeclared Γ (dataPropertyEntity p) =
  dataPropertyDeclared Γ p
EntityDeclared Γ (datatypeEntity d) =
  datatypeDeclared Γ d
EntityDeclared Γ (individualEntity x) =
  individualDeclared Γ x
EntityDeclared Γ (annotationPropertyEntity p) =
  annotationPropertyDeclared Γ p

emptyDeclarationEnvironment :
  ∀ {ℓ} {Sig : Signature ℓ} →
  DeclarationEnvironment Sig
emptyDeclarationEnvironment =
  declarationEnvironment
    (λ _ → ⊥*)
    (λ _ → ⊥*)
    (λ _ → ⊥*)
    (λ _ → ⊥*)
    (λ _ → ⊥*)
    (λ _ → ⊥*)

fullDeclarationEnvironment :
  ∀ {ℓ} {Sig : Signature ℓ} →
  DeclarationEnvironment Sig
fullDeclarationEnvironment =
  declarationEnvironment
    (λ _ → Unit*)
    (λ _ → Unit*)
    (λ _ → Unit*)
    (λ _ → Unit*)
    (λ _ → Unit*)
    (λ _ → Unit*)

_⊆ᵈ_ :
  ∀ {ℓ} {Sig : Signature ℓ} →
  DeclarationEnvironment Sig →
  DeclarationEnvironment Sig →
  Type ℓ
Γ ⊆ᵈ Δ =
  (∀ c → classDeclared Γ c → classDeclared Δ c)
  ×
  (∀ p → objectPropertyDeclared Γ p → objectPropertyDeclared Δ p)
  ×
  (∀ p → dataPropertyDeclared Γ p → dataPropertyDeclared Δ p)
  ×
  (∀ d → datatypeDeclared Γ d → datatypeDeclared Δ d)
  ×
  (∀ x → individualDeclared Γ x → individualDeclared Δ x)
  ×
  (∀ p → annotationPropertyDeclared Γ p → annotationPropertyDeclared Δ p)

declarationEnvironmentRefl :
  ∀ {ℓ} {Sig : Signature ℓ}
    {Γ : DeclarationEnvironment Sig} →
  Γ ⊆ᵈ Γ
declarationEnvironmentRefl =
  (λ _ x → x) ,
  (λ _ x → x) ,
  (λ _ x → x) ,
  (λ _ x → x) ,
  (λ _ x → x) ,
  (λ _ x → x)

declarationEnvironmentTrans :
  ∀ {ℓ} {Sig : Signature ℓ}
    {Γ Δ E : DeclarationEnvironment Sig} →
  Γ ⊆ᵈ Δ → Δ ⊆ᵈ E → Γ ⊆ᵈ E
declarationEnvironmentTrans ΓΔ ΔΕ =
  (λ c cΓ → fst ΔΕ c (fst ΓΔ c cΓ)) ,
  (λ p pΓ → fst (snd ΔΕ) p (fst (snd ΓΔ) p pΓ)) ,
  (λ p pΓ → fst (snd (snd ΔΕ)) p (fst (snd (snd ΓΔ)) p pΓ)) ,
  (λ d dΓ →
    fst (snd (snd (snd ΔΕ))) d
      (fst (snd (snd (snd ΓΔ))) d dΓ)) ,
  (λ x xΓ →
    fst (snd (snd (snd (snd ΔΕ)))) x
      (fst (snd (snd (snd (snd ΓΔ)))) x xΓ)) ,
  (λ p pΓ →
    snd (snd (snd (snd (snd ΔΕ)))) p
      (snd (snd (snd (snd (snd ΓΔ)))) p pΓ))

data DeclaresEntityInAxiom
  {ℓ : Level} {Sig : Signature ℓ}
  : Entity Sig → Axiom Sig → Type ℓ where
  declaredInDeclaration :
    ∀ {e : Entity Sig} →
    DeclaresEntityInAxiom e (declaration e)

DeclaredInAxioms :
  ∀ {ℓ} {Sig : Signature ℓ} →
  Entity Sig → List (Axiom Sig) → Type ℓ
DeclaredInAxioms e axioms =
  AnyList axioms (DeclaresEntityInAxiom e)

declaredAtHead :
  ∀ {ℓ} {Sig : Signature ℓ}
    {e : Entity Sig}
    {axioms : List (Axiom Sig)} →
  DeclaredInAxioms e (declaration e ∷ axioms)
declaredAtHead =
  inl declaredInDeclaration

declaredLater :
  ∀ {ℓ} {Sig : Signature ℓ}
    {e : Entity Sig}
    {axiom : Axiom Sig}
    {axioms : List (Axiom Sig)} →
  DeclaredInAxioms e axioms →
  DeclaredInAxioms e (axiom ∷ axioms)
declaredLater =
  inr

ontologyDeclarationEnvironment :
  ∀ {ℓ} {Sig : Signature ℓ} →
  Ontology Sig → DeclarationEnvironment Sig
ontologyDeclarationEnvironment O =
  declarationEnvironment
    (λ c → DeclaredInAxioms (classEntity c) (axioms O))
    (λ p → DeclaredInAxioms (objectPropertyEntity p) (axioms O))
    (λ p → DeclaredInAxioms (dataPropertyEntity p) (axioms O))
    (λ d → DeclaredInAxioms (datatypeEntity d) (axioms O))
    (λ x → DeclaredInAxioms (individualEntity x) (axioms O))
    (λ p → DeclaredInAxioms (annotationPropertyEntity p) (axioms O))