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

module OWL2.Syntax.Regularity where

open import OWL2.Prelude
open import OWL2.Syntax

data Member {ℓ : Level} {A : Type ℓ} (x : A) : List A → Type ℓ where
  here :
    ∀ {xs} →
    Member x (x ∷ xs)
  there :
    ∀ {y xs} →
    Member x xs → Member x (y ∷ xs)

ListAll :
  ∀ {ℓA ℓP} {A : Type ℓA} →
  List A → (A → Type ℓP) → Type (ℓ-max ℓA ℓP)
ListAll [] P =
  Unit*
ListAll (x ∷ xs) P =
  P x × ListAll xs P

listAllAppend :
  ∀ {ℓA ℓP} {A : Type ℓA} {P : A → Type ℓP} {xs ys : List A} →
  ListAll xs P →
  ListAll ys P →
  ListAll (xs ++ ys) P
listAllAppend {xs = []} pxs pys =
  pys
listAllAppend {P = P} {xs = x ∷ xs} (px , pxs) pys =
  px , listAllAppend {P = P} {xs = xs} pxs pys

listAllAppendLeft :
  ∀ {ℓA ℓP} {A : Type ℓA} {P : A → Type ℓP} {xs ys : List A} →
  ListAll (xs ++ ys) P →
  ListAll xs P
listAllAppendLeft {xs = []} pxs++ys =
  tt*
listAllAppendLeft {P = P} {xs = x ∷ xs} (px , pxs++ys) =
  px , listAllAppendLeft {P = P} {xs = xs} pxs++ys

listAllAppendRight :
  ∀ {ℓA ℓP} {A : Type ℓA} {P : A → Type ℓP} {xs ys : List A} →
  ListAll (xs ++ ys) P →
  ListAll ys P
listAllAppendRight {xs = []} pxs++ys =
  pxs++ys
listAllAppendRight {P = P} {xs = x ∷ xs} (px , pxs++ys) =
  listAllAppendRight {P = P} {xs = xs} pxs++ys

listAllAppendSplit :
  ∀ {ℓA ℓP} {A : Type ℓA} {P : A → Type ℓP} {xs ys : List A} →
  ListAll (xs ++ ys) P →
  ListAll xs P × ListAll ys P
listAllAppendSplit {P = P} {xs = xs} {ys = ys} pxs++ys =
  listAllAppendLeft {P = P} {xs = xs} {ys = ys} pxs++ys ,
  listAllAppendRight {P = P} {xs = xs} {ys = ys} pxs++ys

inverseObjectPropertyExpression :
  ∀ {ℓ} {Sig : Signature ℓ} →
  ObjectPropertyExpression Sig → ObjectPropertyExpression Sig
inverseObjectPropertyExpression (objectProperty p) =
  objectInverseOf (objectProperty p)
inverseObjectPropertyExpression topObjectProperty =
  topObjectProperty
inverseObjectPropertyExpression bottomObjectProperty =
  bottomObjectProperty
inverseObjectPropertyExpression (objectInverseOf p) =
  p

data CanonicalObjectPropertyExpression
  {ℓ : Level} {Sig : Signature ℓ}
  : ObjectPropertyExpression Sig → Type ℓ where
  canonicalObjectProperty :
    ∀ {p} →
    CanonicalObjectPropertyExpression (objectProperty p)
  canonicalTopObjectProperty :
    CanonicalObjectPropertyExpression topObjectProperty
  canonicalBottomObjectProperty :
    CanonicalObjectPropertyExpression bottomObjectProperty
  canonicalObjectInverseOf :
    ∀ {p} →
    CanonicalObjectPropertyExpression
      (objectInverseOf (objectProperty p))

record RegularityContext
  {ℓ : Level}
  (Sig : Signature ℓ)
  : Type (ℓ-suc ℓ) where
  field
    Composite :
      ObjectPropertyExpression Sig → Type ℓ
    HierarchyStep :
      ObjectPropertyExpression Sig →
      ObjectPropertyExpression Sig → Type ℓ

open RegularityContext public

data AxiomCompositeObjectPropertyExpression
  {ℓ : Level} {Sig : Signature ℓ}
  (axioms : List (Axiom Sig))
  : ObjectPropertyExpression Sig → Type ℓ where
  compositeTop :
    AxiomCompositeObjectPropertyExpression axioms topObjectProperty
  compositeBottom :
    AxiomCompositeObjectPropertyExpression axioms bottomObjectProperty
  compositeChain :
    ∀ {p q ps super} →
    Member
      (subObjectPropertyOf (subObjectPropertyChain p q ps) super)
      axioms →
    AxiomCompositeObjectPropertyExpression axioms super
  compositeChainInverse :
    ∀ {p q ps super} →
    Member
      (subObjectPropertyOf
        (subObjectPropertyChain p q ps)
        (inverseObjectPropertyExpression super))
      axioms →
    AxiomCompositeObjectPropertyExpression axioms super
  compositeTransitive :
    ∀ {p} →
    Member (transitiveObjectProperty p) axioms →
    AxiomCompositeObjectPropertyExpression axioms p
  compositeTransitiveInverse :
    ∀ {p} →
    Member
      (transitiveObjectProperty (inverseObjectPropertyExpression p))
      axioms →
    AxiomCompositeObjectPropertyExpression axioms p

data AxiomPropertyHierarchyStep
  {ℓ : Level} {Sig : Signature ℓ}
  (axioms : List (Axiom Sig))
  : ObjectPropertyExpression Sig →
    ObjectPropertyExpression Sig →
    Type ℓ where
  hierarchySubObjectProperty :
    ∀ {p q} →
    Member (subObjectPropertyOf (subObjectProperty p) q) axioms →
    AxiomPropertyHierarchyStep axioms p q
  hierarchyEquivalentObjectProperties :
    ∀ {ps p q} →
    Member (equivalentObjectProperties ps) axioms →
    Member p ps →
    Member q ps →
    AxiomPropertyHierarchyStep axioms p q
  hierarchySymmetricObjectProperty :
    ∀ {p} →
    Member (symmetricObjectProperty p) axioms →
    AxiomPropertyHierarchyStep axioms p (inverseObjectPropertyExpression p)
  hierarchyInverseClosure :
    ∀ {p q} →
    AxiomPropertyHierarchyStep axioms p q →
    AxiomPropertyHierarchyStep axioms
      (inverseObjectPropertyExpression p)
      (inverseObjectPropertyExpression q)

axiomRegularityContext :
  ∀ {ℓ} {Sig : Signature ℓ} →
  List (Axiom Sig) → RegularityContext Sig
axiomRegularityContext axioms .Composite =
  AxiomCompositeObjectPropertyExpression axioms
axiomRegularityContext axioms .HierarchyStep =
  AxiomPropertyHierarchyStep axioms

data PropertyHierarchyPath
  {ℓ : Level} {Sig : Signature ℓ}
  (context : RegularityContext Sig)
  : ObjectPropertyExpression Sig →
    ObjectPropertyExpression Sig →
    Type ℓ where
  hierarchyRefl :
    ∀ {p} →
    PropertyHierarchyPath context p p
  hierarchyTrans :
    ∀ {p q r} →
    HierarchyStep context p q →
    PropertyHierarchyPath context q r →
    PropertyHierarchyPath context p r

SimpleObjectPropertyExpression :
  ∀ {ℓ} {Sig : Signature ℓ} →
  RegularityContext Sig →
  ObjectPropertyExpression Sig → Type ℓ
SimpleObjectPropertyExpression context p =
  CanonicalObjectPropertyExpression p
  ×
  (∀ q →
    PropertyHierarchyPath context q p →
    ¬ Composite context q)

NonSimpleObjectPropertyExpression :
  ∀ {ℓ} {Sig : Signature ℓ} →
  RegularityContext Sig →
  ObjectPropertyExpression Sig → Type ℓ
NonSimpleObjectPropertyExpression {Sig = Sig} context p =
  Σ (ObjectPropertyExpression Sig)
    (λ q →
      PropertyHierarchyPath context q p
      ×
      Composite context q)

nonSimpleContradictsSimple :
  ∀ {ℓ} {Sig : Signature ℓ}
    {context : RegularityContext Sig}
    {p : ObjectPropertyExpression Sig} →
  NonSimpleObjectPropertyExpression context p →
  SimpleObjectPropertyExpression context p →
  ⊥
nonSimpleContradictsSimple (q , path , composite) (canonical , simple) =
  simple q path composite

ObjectPropertyExpressionsSimple :
  ∀ {ℓ} {Sig : Signature ℓ} →
  RegularityContext Sig →
  List (ObjectPropertyExpression Sig) → Type ℓ
ObjectPropertyExpressionsSimple context [] =
  Unit*
ObjectPropertyExpressionsSimple context (p ∷ ps) =
  SimpleObjectPropertyExpression context p
  ×
  ObjectPropertyExpressionsSimple context ps

mutual
  ClassExpressionUsesOnlySimpleObjectProperties :
    ∀ {ℓ} {Sig : Signature ℓ} →
    RegularityContext Sig →
    ClassExpression Sig → Type ℓ
  ClassExpressionUsesOnlySimpleObjectProperties context (namedClass c) =
    Unit*
  ClassExpressionUsesOnlySimpleObjectProperties context owlThing =
    Unit*
  ClassExpressionUsesOnlySimpleObjectProperties context owlNothing =
    Unit*
  ClassExpressionUsesOnlySimpleObjectProperties context (objectIntersectionOf cs) =
    ClassExpressionsUseOnlySimpleObjectProperties context cs
  ClassExpressionUsesOnlySimpleObjectProperties context (objectUnionOf cs) =
    ClassExpressionsUseOnlySimpleObjectProperties context cs
  ClassExpressionUsesOnlySimpleObjectProperties context (objectComplementOf c) =
    ClassExpressionUsesOnlySimpleObjectProperties context c
  ClassExpressionUsesOnlySimpleObjectProperties context (objectOneOf xs) =
    Unit*
  ClassExpressionUsesOnlySimpleObjectProperties context (objectSomeValuesFrom p c) =
    ClassExpressionUsesOnlySimpleObjectProperties context c
  ClassExpressionUsesOnlySimpleObjectProperties context (objectAllValuesFrom p c) =
    ClassExpressionUsesOnlySimpleObjectProperties context c
  ClassExpressionUsesOnlySimpleObjectProperties context (objectHasValue p x) =
    Unit*
  ClassExpressionUsesOnlySimpleObjectProperties context (objectHasSelf p) =
    SimpleObjectPropertyExpression context p
  ClassExpressionUsesOnlySimpleObjectProperties context (objectMinCardinality n p c) =
    SimpleObjectPropertyExpression context p
    ×
    OptionalClassExpressionUsesOnlySimpleObjectProperties context c
  ClassExpressionUsesOnlySimpleObjectProperties context (objectMaxCardinality n p c) =
    SimpleObjectPropertyExpression context p
    ×
    OptionalClassExpressionUsesOnlySimpleObjectProperties context c
  ClassExpressionUsesOnlySimpleObjectProperties context (objectExactCardinality n p c) =
    SimpleObjectPropertyExpression context p
    ×
    OptionalClassExpressionUsesOnlySimpleObjectProperties context c
  ClassExpressionUsesOnlySimpleObjectProperties context (dataSomeValuesFrom p d) =
    Unit*
  ClassExpressionUsesOnlySimpleObjectProperties context (dataAllValuesFrom p d) =
    Unit*
  ClassExpressionUsesOnlySimpleObjectProperties context (dataHasValue p lit) =
    Unit*
  ClassExpressionUsesOnlySimpleObjectProperties context (dataMinCardinality n p d) =
    Unit*
  ClassExpressionUsesOnlySimpleObjectProperties context (dataMaxCardinality n p d) =
    Unit*
  ClassExpressionUsesOnlySimpleObjectProperties context (dataExactCardinality n p d) =
    Unit*

  ClassExpressionsUseOnlySimpleObjectProperties :
    ∀ {ℓ} {Sig : Signature ℓ} →
    RegularityContext Sig →
    List (ClassExpression Sig) → Type ℓ
  ClassExpressionsUseOnlySimpleObjectProperties context [] =
    Unit*
  ClassExpressionsUseOnlySimpleObjectProperties context (c ∷ cs) =
    ClassExpressionUsesOnlySimpleObjectProperties context c
    ×
    ClassExpressionsUseOnlySimpleObjectProperties context cs

  OptionalClassExpressionUsesOnlySimpleObjectProperties :
    ∀ {ℓ} {Sig : Signature ℓ} →
    RegularityContext Sig →
    Optional (ClassExpression Sig) → Type ℓ
  OptionalClassExpressionUsesOnlySimpleObjectProperties context absent =
    Unit*
  OptionalClassExpressionUsesOnlySimpleObjectProperties context (present c) =
    ClassExpressionUsesOnlySimpleObjectProperties context c

AxiomUsesOnlySimpleObjectProperties :
  ∀ {ℓ} {Sig : Signature ℓ} →
  RegularityContext Sig →
  Axiom Sig → Type ℓ
AxiomUsesOnlySimpleObjectProperties context (declaration e) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (subClassOf c d) =
  ClassExpressionUsesOnlySimpleObjectProperties context c
  ×
  ClassExpressionUsesOnlySimpleObjectProperties context d
AxiomUsesOnlySimpleObjectProperties context (equivalentClasses cs) =
  ClassExpressionsUseOnlySimpleObjectProperties context cs
AxiomUsesOnlySimpleObjectProperties context (disjointClasses cs) =
  ClassExpressionsUseOnlySimpleObjectProperties context cs
AxiomUsesOnlySimpleObjectProperties context (subObjectPropertyOf p q) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (equivalentObjectProperties ps) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (disjointObjectProperties ps) =
  ObjectPropertyExpressionsSimple context ps
AxiomUsesOnlySimpleObjectProperties context (objectPropertyDomain p c) =
  ClassExpressionUsesOnlySimpleObjectProperties context c
AxiomUsesOnlySimpleObjectProperties context (objectPropertyRange p c) =
  ClassExpressionUsesOnlySimpleObjectProperties context c
AxiomUsesOnlySimpleObjectProperties context (functionalObjectProperty p) =
  SimpleObjectPropertyExpression context p
AxiomUsesOnlySimpleObjectProperties context (inverseFunctionalObjectProperty p) =
  SimpleObjectPropertyExpression context p
AxiomUsesOnlySimpleObjectProperties context (reflexiveObjectProperty p) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (irreflexiveObjectProperty p) =
  SimpleObjectPropertyExpression context p
AxiomUsesOnlySimpleObjectProperties context (symmetricObjectProperty p) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (asymmetricObjectProperty p) =
  SimpleObjectPropertyExpression context p
AxiomUsesOnlySimpleObjectProperties context (transitiveObjectProperty p) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (subDataPropertyOf p q) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (equivalentDataProperties ps) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (disjointDataProperties ps) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (dataPropertyDomain p c) =
  ClassExpressionUsesOnlySimpleObjectProperties context c
AxiomUsesOnlySimpleObjectProperties context (dataPropertyRange p d) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (functionalDataProperty p) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (datatypeDefinition d r) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (hasKey c key) =
  ClassExpressionUsesOnlySimpleObjectProperties context c
AxiomUsesOnlySimpleObjectProperties context (sameIndividual xs) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (differentIndividuals xs) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (classAssertion c x) =
  ClassExpressionUsesOnlySimpleObjectProperties context c
AxiomUsesOnlySimpleObjectProperties context (objectPropertyAssertion p x y) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (negativeObjectPropertyAssertion p x y) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (dataPropertyAssertion p x lit) =
  Unit*
AxiomUsesOnlySimpleObjectProperties context (negativeDataPropertyAssertion p x lit) =
  Unit*

AxiomsUseOnlySimpleObjectProperties :
  ∀ {ℓ} {Sig : Signature ℓ} →
  RegularityContext Sig →
  List (Axiom Sig) → Type ℓ
AxiomsUseOnlySimpleObjectProperties context [] =
  Unit*
AxiomsUseOnlySimpleObjectProperties context (a ∷ axioms) =
  AxiomUsesOnlySimpleObjectProperties context a
  ×
  AxiomsUseOnlySimpleObjectProperties context axioms

axiomsUseOnlySimpleObjectPropertiesAppend :
  ∀ {ℓ} {Sig : Signature ℓ} {context : RegularityContext Sig}
    {left right : List (Axiom Sig)} →
  AxiomsUseOnlySimpleObjectProperties context left →
  AxiomsUseOnlySimpleObjectProperties context right →
  AxiomsUseOnlySimpleObjectProperties context (left ++ right)
axiomsUseOnlySimpleObjectPropertiesAppend {left = []} leftProof rightProof =
  rightProof
axiomsUseOnlySimpleObjectPropertiesAppend
  {left = axiom ∷ left}
  (axiomProof , leftProof)
  rightProof =
  axiomProof ,
  axiomsUseOnlySimpleObjectPropertiesAppend
    {left = left}
    leftProof
    rightProof

OntologyUsesOnlySimpleObjectProperties :
  ∀ {ℓ} {Sig : Signature ℓ} →
  Ontology Sig → Type ℓ
OntologyUsesOnlySimpleObjectProperties O =
  AxiomsUseOnlySimpleObjectProperties
    (axiomRegularityContext (axioms O))
    (axioms O)

ObjectPropertyExpressionsLessThan :
  ∀ {ℓ} {Sig : Signature ℓ} →
  (ObjectPropertyExpression Sig → ObjectPropertyExpression Sig → Type ℓ) →
  List (ObjectPropertyExpression Sig) →
  ObjectPropertyExpression Sig → Type ℓ
ObjectPropertyExpressionsLessThan _<_ [] super =
  Unit*
ObjectPropertyExpressionsLessThan _<_ (p ∷ ps) super =
  p < super
  ×
  ObjectPropertyExpressionsLessThan _<_ ps super

data RightRecursivePropertyChain
  {ℓ : Level} {Sig : Signature ℓ}
  (_<_ : ObjectPropertyExpression Sig → ObjectPropertyExpression Sig → Type ℓ)
  : ObjectPropertyExpression Sig →
    ObjectPropertyExpression Sig →
    List (ObjectPropertyExpression Sig) →
    ObjectPropertyExpression Sig →
    Type ℓ where
  rightRecursiveTwo :
    ∀ {p super} →
    p < super →
    RightRecursivePropertyChain _<_ p super [] super
  rightRecursiveMore :
    ∀ {p q r ps super} →
    p < super →
    RightRecursivePropertyChain _<_ q r ps super →
    RightRecursivePropertyChain _<_ p q (r ∷ ps) super

data RegularPropertyChain
  {ℓ : Level} {Sig : Signature ℓ}
  (_<_ : ObjectPropertyExpression Sig → ObjectPropertyExpression Sig → Type ℓ)
  : ObjectPropertyExpression Sig →
    ObjectPropertyExpression Sig →
    List (ObjectPropertyExpression Sig) →
    ObjectPropertyExpression Sig →
    Type ℓ where
  regularPropertyChainToTop :
    ∀ {p q ps} →
    RegularPropertyChain _<_ p q ps topObjectProperty
  regularTransitivePropertyChain :
    ∀ {p} →
    RegularPropertyChain _<_ p p [] p
  regularStrictPropertyChain :
    ∀ {p q ps super} →
    p < super →
    q < super →
    ObjectPropertyExpressionsLessThan _<_ ps super →
    RegularPropertyChain _<_ p q ps super
  regularLeftRecursivePropertyChain :
    ∀ {super q ps} →
    q < super →
    ObjectPropertyExpressionsLessThan _<_ ps super →
    RegularPropertyChain _<_ super q ps super
  regularRightRecursivePropertyChain :
    ∀ {p q ps super} →
    RightRecursivePropertyChain _<_ p q ps super →
    RegularPropertyChain _<_ p q ps super

SubObjectPropertyExpressionRegular :
  ∀ {ℓ} {Sig : Signature ℓ} →
  (ObjectPropertyExpression Sig → ObjectPropertyExpression Sig → Type ℓ) →
  SubObjectPropertyExpression Sig →
  ObjectPropertyExpression Sig → Type ℓ
SubObjectPropertyExpressionRegular _<_ (subObjectProperty p) super =
  Unit*
SubObjectPropertyExpressionRegular _<_ (subObjectPropertyChain p q ps) super =
  RegularPropertyChain _<_ p q ps super

AxiomPropertyChainRegular :
  ∀ {ℓ} {Sig : Signature ℓ} →
  (ObjectPropertyExpression Sig → ObjectPropertyExpression Sig → Type ℓ) →
  Axiom Sig → Type ℓ
AxiomPropertyChainRegular _<_ (subObjectPropertyOf sub super) =
  SubObjectPropertyExpressionRegular _<_ sub super
AxiomPropertyChainRegular _<_ axiom =
  Unit*

AxiomsPropertyChainsRegular :
  ∀ {ℓ} {Sig : Signature ℓ} →
  (ObjectPropertyExpression Sig → ObjectPropertyExpression Sig → Type ℓ) →
  List (Axiom Sig) → Type ℓ
AxiomsPropertyChainsRegular _<_ axioms =
  ListAll axioms (AxiomPropertyChainRegular _<_)

axiomsPropertyChainsRegularAppend :
  ∀ {ℓ} {Sig : Signature ℓ}
    {_<_ : ObjectPropertyExpression Sig → ObjectPropertyExpression Sig → Type ℓ}
    {left right : List (Axiom Sig)} →
  AxiomsPropertyChainsRegular _<_ left →
  AxiomsPropertyChainsRegular _<_ right →
  AxiomsPropertyChainsRegular _<_ (left ++ right)
axiomsPropertyChainsRegularAppend {left = []} leftProof rightProof =
  rightProof
axiomsPropertyChainsRegularAppend
  {left = axiom ∷ left}
  (axiomProof , leftProof)
  rightProof =
  axiomProof ,
  axiomsPropertyChainsRegularAppend
    {left = left}
    leftProof
    rightProof

record StrictChainOrder
  {ℓ : Level}
  (Sig : Signature ℓ)
  (axioms : List (Axiom Sig))
  : Type (ℓ-suc ℓ) where
  field
    _<_ :
      ObjectPropertyExpression Sig →
      ObjectPropertyExpression Sig → Type ℓ
    irrefl :
      ∀ p → ¬ (p < p)
    trans :
      ∀ {p q r} → p < q → q < r → p < r
    inversePreserves :
      ∀ {p q} →
      p < q →
      inverseObjectPropertyExpression p
      <
      inverseObjectPropertyExpression q
    chainsRegular :
      AxiomsPropertyChainsRegular _<_ axioms

open StrictChainOrder public

record HierarchyCompatibleChainOrder
  {ℓ : Level}
  (Sig : Signature ℓ)
  (context : RegularityContext Sig)
  (axioms : List (Axiom Sig))
  : Type (ℓ-suc ℓ) where
  field
    strictChainOrder :
      StrictChainOrder Sig axioms
    noBackHierarchy :
      ∀ {p q} →
      StrictChainOrder._<_ strictChainOrder p q →
      ¬ PropertyHierarchyPath context q p

open HierarchyCompatibleChainOrder public

record OntologyRegular
  {ℓ : Level} {Sig : Signature ℓ}
  (O : Ontology Sig)
  : Type (ℓ-suc ℓ) where
  field
    simpleObjectPropertyUses :
      OntologyUsesOnlySimpleObjectProperties O
    strictChainOrder :
      StrictChainOrder Sig (axioms O)

open OntologyRegular public

record ContextualOntologyRegular
  {ℓ : Level} {Sig : Signature ℓ}
  (context : RegularityContext Sig)
  (O : Ontology Sig)
  : Type (ℓ-suc ℓ) where
  field
    simpleObjectPropertyUses :
      AxiomsUseOnlySimpleObjectProperties context (axioms O)
    hierarchyCompatibleChainOrder :
      HierarchyCompatibleChainOrder Sig context (axioms O)

open ContextualOntologyRegular public