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

module OWL2.Syntax.WellFormed where

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

mutual
  ObjectPropertyExpressionWellFormed :
    ∀ {ℓ} {Sig : Signature ℓ} →
    DeclarationEnvironment Sig →
    ObjectPropertyExpression Sig → Type ℓ
  ObjectPropertyExpressionWellFormed Γ (objectProperty p) =
    objectPropertyDeclared Γ p
  ObjectPropertyExpressionWellFormed Γ topObjectProperty =
    Unit*
  ObjectPropertyExpressionWellFormed Γ bottomObjectProperty =
    Unit*
  ObjectPropertyExpressionWellFormed Γ (objectInverseOf p) =
    ObjectPropertyExpressionWellFormed Γ p

  ObjectPropertyExpressionsWellFormed :
    ∀ {ℓ} {Sig : Signature ℓ} →
    DeclarationEnvironment Sig →
    List (ObjectPropertyExpression Sig) → Type ℓ
  ObjectPropertyExpressionsWellFormed Γ [] =
    Unit*
  ObjectPropertyExpressionsWellFormed Γ (p ∷ ps) =
    ObjectPropertyExpressionWellFormed Γ p
    ×
    ObjectPropertyExpressionsWellFormed Γ ps

  SubObjectPropertyExpressionWellFormed :
    ∀ {ℓ} {Sig : Signature ℓ} →
    DeclarationEnvironment Sig →
    SubObjectPropertyExpression Sig → Type ℓ
  SubObjectPropertyExpressionWellFormed Γ (subObjectProperty p) =
    ObjectPropertyExpressionWellFormed Γ p
  SubObjectPropertyExpressionWellFormed Γ (subObjectPropertyChain p q ps) =
    ObjectPropertyExpressionWellFormed Γ p
    ×
    ObjectPropertyExpressionWellFormed Γ q
    ×
    ObjectPropertyExpressionsWellFormed Γ ps

  DataPropertyExpressionWellFormed :
    ∀ {ℓ} {Sig : Signature ℓ} →
    DeclarationEnvironment Sig →
    DataPropertyExpression Sig → Type ℓ
  DataPropertyExpressionWellFormed Γ (dataProperty p) =
    dataPropertyDeclared Γ p
  DataPropertyExpressionWellFormed Γ topDataProperty =
    Unit*
  DataPropertyExpressionWellFormed Γ bottomDataProperty =
    Unit*

  DataPropertyExpressionsWellFormed :
    ∀ {ℓ} {Sig : Signature ℓ} →
    DeclarationEnvironment Sig →
    List (DataPropertyExpression Sig) → Type ℓ
  DataPropertyExpressionsWellFormed Γ [] =
    Unit*
  DataPropertyExpressionsWellFormed Γ (p ∷ ps) =
    DataPropertyExpressionWellFormed Γ p
    ×
    DataPropertyExpressionsWellFormed Γ ps

  DataRangeWellFormed :
    ∀ {ℓ} {Sig : Signature ℓ} →
    DeclarationEnvironment Sig →
    DataRange Sig → Type ℓ
  DataRangeWellFormed Γ (datatype d) =
    datatypeDeclared Γ d
  DataRangeWellFormed Γ (datatypeRestriction d facets) =
    datatypeDeclared Γ d
  DataRangeWellFormed Γ dataTop =
    Unit*
  DataRangeWellFormed Γ dataBottom =
    Unit*
  DataRangeWellFormed Γ (dataComplementOf d) =
    DataRangeWellFormed Γ d
  DataRangeWellFormed Γ (dataIntersectionOf ds) =
    DataRangesWellFormed Γ ds
  DataRangeWellFormed Γ (dataUnionOf ds) =
    DataRangesWellFormed Γ ds
  DataRangeWellFormed Γ (dataOneOf xs) =
    Unit*

  DataRangesWellFormed :
    ∀ {ℓ} {Sig : Signature ℓ} →
    DeclarationEnvironment Sig →
    List (DataRange Sig) → Type ℓ
  DataRangesWellFormed Γ [] =
    Unit*
  DataRangesWellFormed Γ (d ∷ ds) =
    DataRangeWellFormed Γ d
    ×
    DataRangesWellFormed Γ ds

  ClassExpressionWellFormed :
    ∀ {ℓ} {Sig : Signature ℓ} →
    DeclarationEnvironment Sig →
    ClassExpression Sig → Type ℓ
  ClassExpressionWellFormed Γ (namedClass c) =
    classDeclared Γ c
  ClassExpressionWellFormed Γ owlThing =
    Unit*
  ClassExpressionWellFormed Γ owlNothing =
    Unit*
  ClassExpressionWellFormed Γ (objectIntersectionOf cs) =
    ClassExpressionsWellFormed Γ cs
  ClassExpressionWellFormed Γ (objectUnionOf cs) =
    ClassExpressionsWellFormed Γ cs
  ClassExpressionWellFormed Γ (objectComplementOf c) =
    ClassExpressionWellFormed Γ c
  ClassExpressionWellFormed Γ (objectOneOf xs) =
    IndividualsWellFormed Γ xs
  ClassExpressionWellFormed Γ (objectSomeValuesFrom p c) =
    ObjectPropertyExpressionWellFormed Γ p
    ×
    ClassExpressionWellFormed Γ c
  ClassExpressionWellFormed Γ (objectAllValuesFrom p c) =
    ObjectPropertyExpressionWellFormed Γ p
    ×
    ClassExpressionWellFormed Γ c
  ClassExpressionWellFormed Γ (objectHasValue p x) =
    ObjectPropertyExpressionWellFormed Γ p
    ×
    individualDeclared Γ x
  ClassExpressionWellFormed Γ (objectHasSelf p) =
    ObjectPropertyExpressionWellFormed Γ p
  ClassExpressionWellFormed Γ (objectMinCardinality n p c) =
    ObjectPropertyExpressionWellFormed Γ p
    ×
    OptionalClassExpressionWellFormed Γ c
  ClassExpressionWellFormed Γ (objectMaxCardinality n p c) =
    ObjectPropertyExpressionWellFormed Γ p
    ×
    OptionalClassExpressionWellFormed Γ c
  ClassExpressionWellFormed Γ (objectExactCardinality n p c) =
    ObjectPropertyExpressionWellFormed Γ p
    ×
    OptionalClassExpressionWellFormed Γ c
  ClassExpressionWellFormed Γ (dataSomeValuesFrom p d) =
    DataPropertyExpressionWellFormed Γ p
    ×
    DataRangeWellFormed Γ d
  ClassExpressionWellFormed Γ (dataAllValuesFrom p d) =
    DataPropertyExpressionWellFormed Γ p
    ×
    DataRangeWellFormed Γ d
  ClassExpressionWellFormed Γ (dataHasValue p lit) =
    DataPropertyExpressionWellFormed Γ p
  ClassExpressionWellFormed Γ (dataMinCardinality n p d) =
    DataPropertyExpressionWellFormed Γ p
    ×
    OptionalDataRangeWellFormed Γ d
  ClassExpressionWellFormed Γ (dataMaxCardinality n p d) =
    DataPropertyExpressionWellFormed Γ p
    ×
    OptionalDataRangeWellFormed Γ d
  ClassExpressionWellFormed Γ (dataExactCardinality n p d) =
    DataPropertyExpressionWellFormed Γ p
    ×
    OptionalDataRangeWellFormed Γ d

  ClassExpressionsWellFormed :
    ∀ {ℓ} {Sig : Signature ℓ} →
    DeclarationEnvironment Sig →
    List (ClassExpression Sig) → Type ℓ
  ClassExpressionsWellFormed Γ [] =
    Unit*
  ClassExpressionsWellFormed Γ (c ∷ cs) =
    ClassExpressionWellFormed Γ c
    ×
    ClassExpressionsWellFormed Γ cs

  OptionalClassExpressionWellFormed :
    ∀ {ℓ} {Sig : Signature ℓ} →
    DeclarationEnvironment Sig →
    Optional (ClassExpression Sig) → Type ℓ
  OptionalClassExpressionWellFormed Γ absent =
    Unit*
  OptionalClassExpressionWellFormed Γ (present c) =
    ClassExpressionWellFormed Γ c

  OptionalDataRangeWellFormed :
    ∀ {ℓ} {Sig : Signature ℓ} →
    DeclarationEnvironment Sig →
    Optional (DataRange Sig) → Type ℓ
  OptionalDataRangeWellFormed Γ absent =
    Unit*
  OptionalDataRangeWellFormed Γ (present d) =
    DataRangeWellFormed Γ d

  IndividualsWellFormed :
    ∀ {ℓ} {Sig : Signature ℓ} →
    DeclarationEnvironment Sig →
    List (IndividualName Sig) → Type ℓ
  IndividualsWellFormed Γ [] =
    Unit*
  IndividualsWellFormed Γ (x ∷ xs) =
    individualDeclared Γ x
    ×
    IndividualsWellFormed Γ xs

PropertyKeyWellFormed :
  ∀ {ℓ} {Sig : Signature ℓ} →
  DeclarationEnvironment Sig →
  PropertyKey Sig → Type ℓ
PropertyKeyWellFormed Γ key =
  ObjectPropertyExpressionsWellFormed Γ (objectProperties key)
  ×
  DataPropertyExpressionsWellFormed Γ (dataProperties key)

AxiomWellFormed :
  ∀ {ℓ} {Sig : Signature ℓ} →
  DeclarationEnvironment Sig → Axiom Sig → Type ℓ
AxiomWellFormed Γ (declaration e) =
  Unit*
AxiomWellFormed Γ (subClassOf c d) =
  ClassExpressionWellFormed Γ c × ClassExpressionWellFormed Γ d
AxiomWellFormed Γ (equivalentClasses cs) =
  ClassExpressionsWellFormed Γ cs
AxiomWellFormed Γ (disjointClasses cs) =
  ClassExpressionsWellFormed Γ cs
AxiomWellFormed Γ (subObjectPropertyOf p q) =
  SubObjectPropertyExpressionWellFormed Γ p
  ×
  ObjectPropertyExpressionWellFormed Γ q
AxiomWellFormed Γ (equivalentObjectProperties ps) =
  ObjectPropertyExpressionsWellFormed Γ ps
AxiomWellFormed Γ (disjointObjectProperties ps) =
  ObjectPropertyExpressionsWellFormed Γ ps
AxiomWellFormed Γ (objectPropertyDomain p c) =
  ObjectPropertyExpressionWellFormed Γ p × ClassExpressionWellFormed Γ c
AxiomWellFormed Γ (objectPropertyRange p c) =
  ObjectPropertyExpressionWellFormed Γ p × ClassExpressionWellFormed Γ c
AxiomWellFormed Γ (functionalObjectProperty p) =
  ObjectPropertyExpressionWellFormed Γ p
AxiomWellFormed Γ (inverseFunctionalObjectProperty p) =
  ObjectPropertyExpressionWellFormed Γ p
AxiomWellFormed Γ (reflexiveObjectProperty p) =
  ObjectPropertyExpressionWellFormed Γ p
AxiomWellFormed Γ (irreflexiveObjectProperty p) =
  ObjectPropertyExpressionWellFormed Γ p
AxiomWellFormed Γ (symmetricObjectProperty p) =
  ObjectPropertyExpressionWellFormed Γ p
AxiomWellFormed Γ (asymmetricObjectProperty p) =
  ObjectPropertyExpressionWellFormed Γ p
AxiomWellFormed Γ (transitiveObjectProperty p) =
  ObjectPropertyExpressionWellFormed Γ p
AxiomWellFormed Γ (subDataPropertyOf p q) =
  DataPropertyExpressionWellFormed Γ p × DataPropertyExpressionWellFormed Γ q
AxiomWellFormed Γ (equivalentDataProperties ps) =
  DataPropertyExpressionsWellFormed Γ ps
AxiomWellFormed Γ (disjointDataProperties ps) =
  DataPropertyExpressionsWellFormed Γ ps
AxiomWellFormed Γ (dataPropertyDomain p c) =
  DataPropertyExpressionWellFormed Γ p × ClassExpressionWellFormed Γ c
AxiomWellFormed Γ (dataPropertyRange p d) =
  DataPropertyExpressionWellFormed Γ p × DataRangeWellFormed Γ d
AxiomWellFormed Γ (functionalDataProperty p) =
  DataPropertyExpressionWellFormed Γ p
AxiomWellFormed Γ (datatypeDefinition d r) =
  datatypeDeclared Γ d × DataRangeWellFormed Γ r
AxiomWellFormed Γ (hasKey c key) =
  ClassExpressionWellFormed Γ c × PropertyKeyWellFormed Γ key
AxiomWellFormed Γ (sameIndividual xs) =
  IndividualsWellFormed Γ xs
AxiomWellFormed Γ (differentIndividuals xs) =
  IndividualsWellFormed Γ xs
AxiomWellFormed Γ (classAssertion c x) =
  ClassExpressionWellFormed Γ c × individualDeclared Γ x
AxiomWellFormed Γ (objectPropertyAssertion p x y) =
  ObjectPropertyExpressionWellFormed Γ p
  ×
  individualDeclared Γ x
  ×
  individualDeclared Γ y
AxiomWellFormed Γ (negativeObjectPropertyAssertion p x y) =
  ObjectPropertyExpressionWellFormed Γ p
  ×
  individualDeclared Γ x
  ×
  individualDeclared Γ y
AxiomWellFormed Γ (dataPropertyAssertion p x lit) =
  DataPropertyExpressionWellFormed Γ p × individualDeclared Γ x
AxiomWellFormed Γ (negativeDataPropertyAssertion p x lit) =
  DataPropertyExpressionWellFormed Γ p × individualDeclared Γ x

AxiomsWellFormed :
  ∀ {ℓ} {Sig : Signature ℓ} →
  DeclarationEnvironment Sig → List (Axiom Sig) → Type ℓ
AxiomsWellFormed Γ [] =
  Unit*
AxiomsWellFormed Γ (a ∷ axioms) =
  AxiomWellFormed Γ a
  ×
  AxiomsWellFormed Γ axioms

OntologyWellFormed :
  ∀ {ℓ} {Sig : Signature ℓ} →
  DeclarationEnvironment Sig → Ontology Sig → Type ℓ
OntologyWellFormed Γ O =
  AxiomsWellFormed Γ (axioms O)

OntologySelfContained :
  ∀ {ℓ} {Sig : Signature ℓ} →
  Ontology Sig → Type ℓ
OntologySelfContained O =
  OntologyWellFormed (ontologyDeclarationEnvironment O) O