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

module OWL2.Syntax.GlobalRestrictions where

open import OWL2.Prelude
open import OWL2.Syntax
open import OWL2.Syntax.Declarations
open import OWL2.Syntax.WellFormed
open import OWL2.Syntax.Regularity
open import OWL2.Syntax.Punning

record OntologyGlobalRestrictions
  {ℓ : Level} {Sig : Signature ℓ}
  (Γ : DeclarationEnvironment Sig)
  (context : RegularityContext Sig)
  (O : Ontology Sig)
  : Type (ℓ-suc ℓ) where
  field
    wellFormed :
      OntologyWellFormed Γ O
    contextualRegularity :
      ContextualOntologyRegular context O

open OntologyGlobalRestrictions public

OntologySelfContainedGlobalRestrictions :
  ∀ {ℓ} {Sig : Signature ℓ} →
  RegularityContext Sig → Ontology Sig → Type (ℓ-suc ℓ)
OntologySelfContainedGlobalRestrictions context O =
  OntologyGlobalRestrictions
    (ontologyDeclarationEnvironment O)
    context
    O

OntologyAxiomDerivedGlobalRestrictions :
  ∀ {ℓ} {Sig : Signature ℓ} →
  Ontology Sig → Type (ℓ-suc ℓ)
OntologyAxiomDerivedGlobalRestrictions O =
  OntologySelfContainedGlobalRestrictions
    (axiomRegularityContext (axioms O))
    O

ontologyGlobalRestrictionsSelfContained :
  ∀ {ℓ} {Sig : Signature ℓ}
    {context : RegularityContext Sig}
    {O : Ontology Sig} →
  OntologyGlobalRestrictions
    (ontologyDeclarationEnvironment O)
    context
    O →
  OntologySelfContainedGlobalRestrictions context O
ontologyGlobalRestrictionsSelfContained restrictions =
  restrictions

ontologyGlobalRestrictionsWellFormed :
  ∀ {ℓ} {Sig : Signature ℓ}
    {Γ : DeclarationEnvironment Sig}
    {context : RegularityContext Sig}
    {O : Ontology Sig} →
  OntologyGlobalRestrictions Γ context O →
  OntologyWellFormed Γ O
ontologyGlobalRestrictionsWellFormed restrictions =
  OntologyGlobalRestrictions.wellFormed restrictions

ontologyGlobalRestrictionsRegular :
  ∀ {ℓ} {Sig : Signature ℓ}
    {Γ : DeclarationEnvironment Sig}
    {context : RegularityContext Sig}
    {O : Ontology Sig} →
  OntologyGlobalRestrictions Γ context O →
  ContextualOntologyRegular context O
ontologyGlobalRestrictionsRegular restrictions =
  OntologyGlobalRestrictions.contextualRegularity restrictions

record OntologyTypedGlobalRestrictions
  {ℓ : Level} {Sig : Signature ℓ}
  (ids : EntityIdentifier Sig)
  (Γ : DeclarationEnvironment Sig)
  (context : RegularityContext Sig)
  (O : Ontology Sig)
  : Type (ℓ-suc ℓ) where
  field
    globalRestrictions :
      OntologyGlobalRestrictions Γ context O
    typingConstraints :
      OWL2DLTypingConstraints ids Γ

open OntologyTypedGlobalRestrictions public

OntologySelfContainedTypedGlobalRestrictions :
  ∀ {ℓ} {Sig : Signature ℓ} →
  EntityIdentifier Sig →
  RegularityContext Sig → Ontology Sig → Type (ℓ-suc ℓ)
OntologySelfContainedTypedGlobalRestrictions ids context O =
  OntologyTypedGlobalRestrictions
    ids
    (ontologyDeclarationEnvironment O)
    context
    O

ontologyTypedGlobalRestrictionsWellFormed :
  ∀ {ℓ} {Sig : Signature ℓ}
    {ids : EntityIdentifier Sig}
    {Γ : DeclarationEnvironment Sig}
    {context : RegularityContext Sig}
    {O : Ontology Sig} →
  OntologyTypedGlobalRestrictions ids Γ context O →
  OntologyWellFormed Γ O
ontologyTypedGlobalRestrictionsWellFormed restrictions =
  ontologyGlobalRestrictionsWellFormed
    (OntologyTypedGlobalRestrictions.globalRestrictions restrictions)

ontologyTypedGlobalRestrictionsRegular :
  ∀ {ℓ} {Sig : Signature ℓ}
    {ids : EntityIdentifier Sig}
    {Γ : DeclarationEnvironment Sig}
    {context : RegularityContext Sig}
    {O : Ontology Sig} →
  OntologyTypedGlobalRestrictions ids Γ context O →
  ContextualOntologyRegular context O
ontologyTypedGlobalRestrictionsRegular restrictions =
  ontologyGlobalRestrictionsRegular
    (OntologyTypedGlobalRestrictions.globalRestrictions restrictions)