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

module OWL2.Portable.CardinalityRestrictions where

open import Cubical.Data.Nat.Base using (zero; suc)
open import OWL2.Prelude
import OWL2.Portable.Syntax as P

private
  concatMap : ∀ {A B : Type₀} → (A → List B) → List A → List B
  concatMap f [] =
    []
  concatMap f (x ∷ xs) =
    f x ++ concatMap f xs

  listCount : ∀ {ℓ} {A : Type ℓ} → List A → ℕ
  listCount [] =
    zero
  listCount (x ∷ xs) =
    suc (listCount xs)

data CardinalityRestrictionSource : Type₀ where
  axiomBodySource :
    P.Annotated P.Axiom → CardinalityRestrictionSource

data ObjectCardinalityRestriction : Type₀ where
  objectMinCardinalityRestriction :
    CardinalityRestrictionSource →
    ℕ →
    P.ObjectPropertyExpression →
    Optional P.ClassExpression →
    ObjectCardinalityRestriction
  objectMaxCardinalityRestriction :
    CardinalityRestrictionSource →
    ℕ →
    P.ObjectPropertyExpression →
    Optional P.ClassExpression →
    ObjectCardinalityRestriction
  objectExactCardinalityRestriction :
    CardinalityRestrictionSource →
    ℕ →
    P.ObjectPropertyExpression →
    Optional P.ClassExpression →
    ObjectCardinalityRestriction

data DataCardinalityRestriction : Type₀ where
  dataMinCardinalityRestriction :
    CardinalityRestrictionSource →
    ℕ →
    P.DataPropertyExpression →
    Optional P.DataRange →
    DataCardinalityRestriction
  dataMaxCardinalityRestriction :
    CardinalityRestrictionSource →
    ℕ →
    P.DataPropertyExpression →
    Optional P.DataRange →
    DataCardinalityRestriction
  dataExactCardinalityRestriction :
    CardinalityRestrictionSource →
    ℕ →
    P.DataPropertyExpression →
    Optional P.DataRange →
    DataCardinalityRestriction

data CardinalityRestriction : Type₀ where
  objectCardinalityRestriction :
    ObjectCardinalityRestriction → CardinalityRestriction
  dataCardinalityRestriction :
    DataCardinalityRestriction → CardinalityRestriction

objectCardinalityRestrictionSource :
  ObjectCardinalityRestriction → CardinalityRestrictionSource
objectCardinalityRestrictionSource
  (objectMinCardinalityRestriction source n property qualifier) =
  source
objectCardinalityRestrictionSource
  (objectMaxCardinalityRestriction source n property qualifier) =
  source
objectCardinalityRestrictionSource
  (objectExactCardinalityRestriction source n property qualifier) =
  source

objectCardinalityRestrictionNumber : ObjectCardinalityRestriction → ℕ
objectCardinalityRestrictionNumber
  (objectMinCardinalityRestriction source n property qualifier) =
  n
objectCardinalityRestrictionNumber
  (objectMaxCardinalityRestriction source n property qualifier) =
  n
objectCardinalityRestrictionNumber
  (objectExactCardinalityRestriction source n property qualifier) =
  n

objectCardinalityRestrictionProperty :
  ObjectCardinalityRestriction → P.ObjectPropertyExpression
objectCardinalityRestrictionProperty
  (objectMinCardinalityRestriction source n property qualifier) =
  property
objectCardinalityRestrictionProperty
  (objectMaxCardinalityRestriction source n property qualifier) =
  property
objectCardinalityRestrictionProperty
  (objectExactCardinalityRestriction source n property qualifier) =
  property

objectCardinalityRestrictionQualifier :
  ObjectCardinalityRestriction → Optional P.ClassExpression
objectCardinalityRestrictionQualifier
  (objectMinCardinalityRestriction source n property qualifier) =
  qualifier
objectCardinalityRestrictionQualifier
  (objectMaxCardinalityRestriction source n property qualifier) =
  qualifier
objectCardinalityRestrictionQualifier
  (objectExactCardinalityRestriction source n property qualifier) =
  qualifier

dataCardinalityRestrictionSource :
  DataCardinalityRestriction → CardinalityRestrictionSource
dataCardinalityRestrictionSource
  (dataMinCardinalityRestriction source n property range) =
  source
dataCardinalityRestrictionSource
  (dataMaxCardinalityRestriction source n property range) =
  source
dataCardinalityRestrictionSource
  (dataExactCardinalityRestriction source n property range) =
  source

dataCardinalityRestrictionNumber : DataCardinalityRestriction → ℕ
dataCardinalityRestrictionNumber
  (dataMinCardinalityRestriction source n property range) =
  n
dataCardinalityRestrictionNumber
  (dataMaxCardinalityRestriction source n property range) =
  n
dataCardinalityRestrictionNumber
  (dataExactCardinalityRestriction source n property range) =
  n

dataCardinalityRestrictionProperty :
  DataCardinalityRestriction → P.DataPropertyExpression
dataCardinalityRestrictionProperty
  (dataMinCardinalityRestriction source n property range) =
  property
dataCardinalityRestrictionProperty
  (dataMaxCardinalityRestriction source n property range) =
  property
dataCardinalityRestrictionProperty
  (dataExactCardinalityRestriction source n property range) =
  property

dataCardinalityRestrictionRange :
  DataCardinalityRestriction → Optional P.DataRange
dataCardinalityRestrictionRange
  (dataMinCardinalityRestriction source n property range) =
  range
dataCardinalityRestrictionRange
  (dataMaxCardinalityRestriction source n property range) =
  range
dataCardinalityRestrictionRange
  (dataExactCardinalityRestriction source n property range) =
  range

objectCardinalityRestrictionsAsCardinalityRestrictions :
  List ObjectCardinalityRestriction → List CardinalityRestriction
objectCardinalityRestrictionsAsCardinalityRestrictions =
  map objectCardinalityRestriction

dataCardinalityRestrictionsAsCardinalityRestrictions :
  List DataCardinalityRestriction → List CardinalityRestriction
dataCardinalityRestrictionsAsCardinalityRestrictions =
  map dataCardinalityRestriction

cardinalityRestrictions :
  List ObjectCardinalityRestriction →
  List DataCardinalityRestriction →
  List CardinalityRestriction
cardinalityRestrictions objectRestrictions dataRestrictions =
  objectCardinalityRestrictionsAsCardinalityRestrictions objectRestrictions
  ++ dataCardinalityRestrictionsAsCardinalityRestrictions dataRestrictions

mutual
  objectCardinalityRestrictionsInClassExpression :
    CardinalityRestrictionSource →
    P.ClassExpression →
    List ObjectCardinalityRestriction
  objectCardinalityRestrictionsInClassExpression source (P.namedClass c) =
    []
  objectCardinalityRestrictionsInClassExpression source P.owlThing =
    []
  objectCardinalityRestrictionsInClassExpression source P.owlNothing =
    []
  objectCardinalityRestrictionsInClassExpression
    source
    (P.objectIntersectionOf classes) =
    objectCardinalityRestrictionsInClassExpressionsTwoOrMore source classes
  objectCardinalityRestrictionsInClassExpression
    source
    (P.objectUnionOf classes) =
    objectCardinalityRestrictionsInClassExpressionsTwoOrMore source classes
  objectCardinalityRestrictionsInClassExpression
    source
    (P.objectComplementOf class) =
    objectCardinalityRestrictionsInClassExpression source class
  objectCardinalityRestrictionsInClassExpression
    source
    (P.objectOneOf individuals) =
    []
  objectCardinalityRestrictionsInClassExpression
    source
    (P.objectSomeValuesFrom property class) =
    objectCardinalityRestrictionsInClassExpression source class
  objectCardinalityRestrictionsInClassExpression
    source
    (P.objectAllValuesFrom property class) =
    objectCardinalityRestrictionsInClassExpression source class
  objectCardinalityRestrictionsInClassExpression
    source
    (P.objectHasValue property individual) =
    []
  objectCardinalityRestrictionsInClassExpression
    source
    (P.objectHasSelf property) =
    []
  objectCardinalityRestrictionsInClassExpression
    source
    (P.objectMinCardinality n property qualifier) =
    objectMinCardinalityRestriction source n property qualifier
    ∷ objectCardinalityRestrictionsInOptionalClassExpression source qualifier
  objectCardinalityRestrictionsInClassExpression
    source
    (P.objectMaxCardinality n property qualifier) =
    objectMaxCardinalityRestriction source n property qualifier
    ∷ objectCardinalityRestrictionsInOptionalClassExpression source qualifier
  objectCardinalityRestrictionsInClassExpression
    source
    (P.objectExactCardinality n property qualifier) =
    objectExactCardinalityRestriction source n property qualifier
    ∷ objectCardinalityRestrictionsInOptionalClassExpression source qualifier
  objectCardinalityRestrictionsInClassExpression
    source
    (P.dataSomeValuesFrom property range) =
    []
  objectCardinalityRestrictionsInClassExpression
    source
    (P.dataAllValuesFrom property range) =
    []
  objectCardinalityRestrictionsInClassExpression
    source
    (P.dataHasValue property literal) =
    []
  objectCardinalityRestrictionsInClassExpression
    source
    (P.dataMinCardinality n property range) =
    []
  objectCardinalityRestrictionsInClassExpression
    source
    (P.dataMaxCardinality n property range) =
    []
  objectCardinalityRestrictionsInClassExpression
    source
    (P.dataExactCardinality n property range) =
    []

  objectCardinalityRestrictionsInClassExpressions :
    CardinalityRestrictionSource →
    List P.ClassExpression →
    List ObjectCardinalityRestriction
  objectCardinalityRestrictionsInClassExpressions source [] =
    []
  objectCardinalityRestrictionsInClassExpressions source (class ∷ classes) =
    objectCardinalityRestrictionsInClassExpression source class
    ++ objectCardinalityRestrictionsInClassExpressions source classes

  objectCardinalityRestrictionsInClassExpressionsTwoOrMore :
    CardinalityRestrictionSource →
    P.TwoOrMore P.ClassExpression →
    List ObjectCardinalityRestriction
  objectCardinalityRestrictionsInClassExpressionsTwoOrMore source classes =
    objectCardinalityRestrictionsInClassExpression source (P.first classes)
    ++
    objectCardinalityRestrictionsInClassExpression source (P.second classes)
    ++
    objectCardinalityRestrictionsInClassExpressions source (P.rest classes)

  objectCardinalityRestrictionsInOptionalClassExpression :
    CardinalityRestrictionSource →
    Optional P.ClassExpression →
    List ObjectCardinalityRestriction
  objectCardinalityRestrictionsInOptionalClassExpression source absent =
    []
  objectCardinalityRestrictionsInOptionalClassExpression source (present class) =
    objectCardinalityRestrictionsInClassExpression source class

mutual
  dataCardinalityRestrictionsInClassExpression :
    CardinalityRestrictionSource →
    P.ClassExpression →
    List DataCardinalityRestriction
  dataCardinalityRestrictionsInClassExpression source (P.namedClass c) =
    []
  dataCardinalityRestrictionsInClassExpression source P.owlThing =
    []
  dataCardinalityRestrictionsInClassExpression source P.owlNothing =
    []
  dataCardinalityRestrictionsInClassExpression
    source
    (P.objectIntersectionOf classes) =
    dataCardinalityRestrictionsInClassExpressionsTwoOrMore source classes
  dataCardinalityRestrictionsInClassExpression
    source
    (P.objectUnionOf classes) =
    dataCardinalityRestrictionsInClassExpressionsTwoOrMore source classes
  dataCardinalityRestrictionsInClassExpression
    source
    (P.objectComplementOf class) =
    dataCardinalityRestrictionsInClassExpression source class
  dataCardinalityRestrictionsInClassExpression
    source
    (P.objectOneOf individuals) =
    []
  dataCardinalityRestrictionsInClassExpression
    source
    (P.objectSomeValuesFrom property class) =
    dataCardinalityRestrictionsInClassExpression source class
  dataCardinalityRestrictionsInClassExpression
    source
    (P.objectAllValuesFrom property class) =
    dataCardinalityRestrictionsInClassExpression source class
  dataCardinalityRestrictionsInClassExpression
    source
    (P.objectHasValue property individual) =
    []
  dataCardinalityRestrictionsInClassExpression
    source
    (P.objectHasSelf property) =
    []
  dataCardinalityRestrictionsInClassExpression
    source
    (P.objectMinCardinality n property qualifier) =
    dataCardinalityRestrictionsInOptionalClassExpression source qualifier
  dataCardinalityRestrictionsInClassExpression
    source
    (P.objectMaxCardinality n property qualifier) =
    dataCardinalityRestrictionsInOptionalClassExpression source qualifier
  dataCardinalityRestrictionsInClassExpression
    source
    (P.objectExactCardinality n property qualifier) =
    dataCardinalityRestrictionsInOptionalClassExpression source qualifier
  dataCardinalityRestrictionsInClassExpression
    source
    (P.dataSomeValuesFrom property range) =
    []
  dataCardinalityRestrictionsInClassExpression
    source
    (P.dataAllValuesFrom property range) =
    []
  dataCardinalityRestrictionsInClassExpression
    source
    (P.dataHasValue property literal) =
    []
  dataCardinalityRestrictionsInClassExpression
    source
    (P.dataMinCardinality n property range) =
    dataMinCardinalityRestriction source n property range ∷ []
  dataCardinalityRestrictionsInClassExpression
    source
    (P.dataMaxCardinality n property range) =
    dataMaxCardinalityRestriction source n property range ∷ []
  dataCardinalityRestrictionsInClassExpression
    source
    (P.dataExactCardinality n property range) =
    dataExactCardinalityRestriction source n property range ∷ []

  dataCardinalityRestrictionsInClassExpressions :
    CardinalityRestrictionSource →
    List P.ClassExpression →
    List DataCardinalityRestriction
  dataCardinalityRestrictionsInClassExpressions source [] =
    []
  dataCardinalityRestrictionsInClassExpressions source (class ∷ classes) =
    dataCardinalityRestrictionsInClassExpression source class
    ++ dataCardinalityRestrictionsInClassExpressions source classes

  dataCardinalityRestrictionsInClassExpressionsTwoOrMore :
    CardinalityRestrictionSource →
    P.TwoOrMore P.ClassExpression →
    List DataCardinalityRestriction
  dataCardinalityRestrictionsInClassExpressionsTwoOrMore source classes =
    dataCardinalityRestrictionsInClassExpression source (P.first classes)
    ++
    dataCardinalityRestrictionsInClassExpression source (P.second classes)
    ++
    dataCardinalityRestrictionsInClassExpressions source (P.rest classes)

  dataCardinalityRestrictionsInOptionalClassExpression :
    CardinalityRestrictionSource →
    Optional P.ClassExpression →
    List DataCardinalityRestriction
  dataCardinalityRestrictionsInOptionalClassExpression source absent =
    []
  dataCardinalityRestrictionsInOptionalClassExpression source (present class) =
    dataCardinalityRestrictionsInClassExpression source class

objectCardinalityRestrictionsInAxiom :
  CardinalityRestrictionSource →
  P.Axiom →
  List ObjectCardinalityRestriction
objectCardinalityRestrictionsInAxiom source (P.declaration entity) =
  []
objectCardinalityRestrictionsInAxiom source (P.subClassOf subclass superclass) =
  objectCardinalityRestrictionsInClassExpression source subclass
  ++ objectCardinalityRestrictionsInClassExpression source superclass
objectCardinalityRestrictionsInAxiom source (P.equivalentClasses classes) =
  objectCardinalityRestrictionsInClassExpressionsTwoOrMore source classes
objectCardinalityRestrictionsInAxiom source (P.disjointClasses classes) =
  objectCardinalityRestrictionsInClassExpressionsTwoOrMore source classes
objectCardinalityRestrictionsInAxiom source (P.disjointUnion class classes) =
  objectCardinalityRestrictionsInClassExpressionsTwoOrMore source classes
objectCardinalityRestrictionsInAxiom source (P.subObjectPropertyOf left right) =
  []
objectCardinalityRestrictionsInAxiom
  source
  (P.equivalentObjectProperties properties) =
  []
objectCardinalityRestrictionsInAxiom
  source
  (P.disjointObjectProperties properties) =
  []
objectCardinalityRestrictionsInAxiom
  source
  (P.inverseObjectProperties left right) =
  []
objectCardinalityRestrictionsInAxiom source (P.objectPropertyDomain property class) =
  objectCardinalityRestrictionsInClassExpression source class
objectCardinalityRestrictionsInAxiom source (P.objectPropertyRange property class) =
  objectCardinalityRestrictionsInClassExpression source class
objectCardinalityRestrictionsInAxiom source (P.functionalObjectProperty property) =
  []
objectCardinalityRestrictionsInAxiom
  source
  (P.inverseFunctionalObjectProperty property) =
  []
objectCardinalityRestrictionsInAxiom source (P.reflexiveObjectProperty property) =
  []
objectCardinalityRestrictionsInAxiom source (P.irreflexiveObjectProperty property) =
  []
objectCardinalityRestrictionsInAxiom source (P.symmetricObjectProperty property) =
  []
objectCardinalityRestrictionsInAxiom source (P.asymmetricObjectProperty property) =
  []
objectCardinalityRestrictionsInAxiom source (P.transitiveObjectProperty property) =
  []
objectCardinalityRestrictionsInAxiom source (P.subDataPropertyOf left right) =
  []
objectCardinalityRestrictionsInAxiom
  source
  (P.equivalentDataProperties properties) =
  []
objectCardinalityRestrictionsInAxiom
  source
  (P.disjointDataProperties properties) =
  []
objectCardinalityRestrictionsInAxiom source (P.dataPropertyDomain property class) =
  objectCardinalityRestrictionsInClassExpression source class
objectCardinalityRestrictionsInAxiom source (P.dataPropertyRange property range) =
  []
objectCardinalityRestrictionsInAxiom source (P.functionalDataProperty property) =
  []
objectCardinalityRestrictionsInAxiom source (P.datatypeDefinition datatype range) =
  []
objectCardinalityRestrictionsInAxiom source (P.hasKey class key) =
  objectCardinalityRestrictionsInClassExpression source class
objectCardinalityRestrictionsInAxiom source (P.sameIndividual individuals) =
  []
objectCardinalityRestrictionsInAxiom source (P.differentIndividuals individuals) =
  []
objectCardinalityRestrictionsInAxiom source (P.classAssertion class individual) =
  objectCardinalityRestrictionsInClassExpression source class
objectCardinalityRestrictionsInAxiom
  source
  (P.objectPropertyAssertion property subject object) =
  []
objectCardinalityRestrictionsInAxiom
  source
  (P.negativeObjectPropertyAssertion property subject object) =
  []
objectCardinalityRestrictionsInAxiom
  source
  (P.dataPropertyAssertion property subject value) =
  []
objectCardinalityRestrictionsInAxiom
  source
  (P.negativeDataPropertyAssertion property subject value) =
  []
objectCardinalityRestrictionsInAxiom
  source
  (P.annotationAssertion property subject value) =
  []
objectCardinalityRestrictionsInAxiom
  source
  (P.subAnnotationPropertyOf left right) =
  []
objectCardinalityRestrictionsInAxiom source (P.annotationPropertyDomain property domain) =
  []
objectCardinalityRestrictionsInAxiom source (P.annotationPropertyRange property range) =
  []

dataCardinalityRestrictionsInAxiom :
  CardinalityRestrictionSource →
  P.Axiom →
  List DataCardinalityRestriction
dataCardinalityRestrictionsInAxiom source (P.declaration entity) =
  []
dataCardinalityRestrictionsInAxiom source (P.subClassOf subclass superclass) =
  dataCardinalityRestrictionsInClassExpression source subclass
  ++ dataCardinalityRestrictionsInClassExpression source superclass
dataCardinalityRestrictionsInAxiom source (P.equivalentClasses classes) =
  dataCardinalityRestrictionsInClassExpressionsTwoOrMore source classes
dataCardinalityRestrictionsInAxiom source (P.disjointClasses classes) =
  dataCardinalityRestrictionsInClassExpressionsTwoOrMore source classes
dataCardinalityRestrictionsInAxiom source (P.disjointUnion class classes) =
  dataCardinalityRestrictionsInClassExpressionsTwoOrMore source classes
dataCardinalityRestrictionsInAxiom source (P.subObjectPropertyOf left right) =
  []
dataCardinalityRestrictionsInAxiom
  source
  (P.equivalentObjectProperties properties) =
  []
dataCardinalityRestrictionsInAxiom
  source
  (P.disjointObjectProperties properties) =
  []
dataCardinalityRestrictionsInAxiom
  source
  (P.inverseObjectProperties left right) =
  []
dataCardinalityRestrictionsInAxiom source (P.objectPropertyDomain property class) =
  dataCardinalityRestrictionsInClassExpression source class
dataCardinalityRestrictionsInAxiom source (P.objectPropertyRange property class) =
  dataCardinalityRestrictionsInClassExpression source class
dataCardinalityRestrictionsInAxiom source (P.functionalObjectProperty property) =
  []
dataCardinalityRestrictionsInAxiom
  source
  (P.inverseFunctionalObjectProperty property) =
  []
dataCardinalityRestrictionsInAxiom source (P.reflexiveObjectProperty property) =
  []
dataCardinalityRestrictionsInAxiom source (P.irreflexiveObjectProperty property) =
  []
dataCardinalityRestrictionsInAxiom source (P.symmetricObjectProperty property) =
  []
dataCardinalityRestrictionsInAxiom source (P.asymmetricObjectProperty property) =
  []
dataCardinalityRestrictionsInAxiom source (P.transitiveObjectProperty property) =
  []
dataCardinalityRestrictionsInAxiom source (P.subDataPropertyOf left right) =
  []
dataCardinalityRestrictionsInAxiom
  source
  (P.equivalentDataProperties properties) =
  []
dataCardinalityRestrictionsInAxiom
  source
  (P.disjointDataProperties properties) =
  []
dataCardinalityRestrictionsInAxiom source (P.dataPropertyDomain property class) =
  dataCardinalityRestrictionsInClassExpression source class
dataCardinalityRestrictionsInAxiom source (P.dataPropertyRange property range) =
  []
dataCardinalityRestrictionsInAxiom source (P.functionalDataProperty property) =
  []
dataCardinalityRestrictionsInAxiom source (P.datatypeDefinition datatype range) =
  []
dataCardinalityRestrictionsInAxiom source (P.hasKey class key) =
  dataCardinalityRestrictionsInClassExpression source class
dataCardinalityRestrictionsInAxiom source (P.sameIndividual individuals) =
  []
dataCardinalityRestrictionsInAxiom source (P.differentIndividuals individuals) =
  []
dataCardinalityRestrictionsInAxiom source (P.classAssertion class individual) =
  dataCardinalityRestrictionsInClassExpression source class
dataCardinalityRestrictionsInAxiom
  source
  (P.objectPropertyAssertion property subject object) =
  []
dataCardinalityRestrictionsInAxiom
  source
  (P.negativeObjectPropertyAssertion property subject object) =
  []
dataCardinalityRestrictionsInAxiom
  source
  (P.dataPropertyAssertion property subject value) =
  []
dataCardinalityRestrictionsInAxiom
  source
  (P.negativeDataPropertyAssertion property subject value) =
  []
dataCardinalityRestrictionsInAxiom
  source
  (P.annotationAssertion property subject value) =
  []
dataCardinalityRestrictionsInAxiom
  source
  (P.subAnnotationPropertyOf left right) =
  []
dataCardinalityRestrictionsInAxiom source (P.annotationPropertyDomain property domain) =
  []
dataCardinalityRestrictionsInAxiom source (P.annotationPropertyRange property range) =
  []

objectCardinalityRestrictionsInAnnotatedAxiom :
  P.Annotated P.Axiom → List ObjectCardinalityRestriction
objectCardinalityRestrictionsInAnnotatedAxiom axiom =
  objectCardinalityRestrictionsInAxiom
    (axiomBodySource axiom)
    (P.body axiom)

dataCardinalityRestrictionsInAnnotatedAxiom :
  P.Annotated P.Axiom → List DataCardinalityRestriction
dataCardinalityRestrictionsInAnnotatedAxiom axiom =
  dataCardinalityRestrictionsInAxiom
    (axiomBodySource axiom)
    (P.body axiom)

objectCardinalityRestrictionsInAxioms :
  List (P.Annotated P.Axiom) → List ObjectCardinalityRestriction
objectCardinalityRestrictionsInAxioms =
  concatMap objectCardinalityRestrictionsInAnnotatedAxiom

dataCardinalityRestrictionsInAxioms :
  List (P.Annotated P.Axiom) → List DataCardinalityRestriction
dataCardinalityRestrictionsInAxioms =
  concatMap dataCardinalityRestrictionsInAnnotatedAxiom

ontologyObjectCardinalityRestrictions :
  P.Ontology → List ObjectCardinalityRestriction
ontologyObjectCardinalityRestrictions ont =
  objectCardinalityRestrictionsInAxioms (P.axioms ont)

ontologyDataCardinalityRestrictions :
  P.Ontology → List DataCardinalityRestriction
ontologyDataCardinalityRestrictions ont =
  dataCardinalityRestrictionsInAxioms (P.axioms ont)

ontologyCardinalityRestrictions :
  P.Ontology → List CardinalityRestriction
ontologyCardinalityRestrictions ont =
  cardinalityRestrictions
    (ontologyObjectCardinalityRestrictions ont)
    (ontologyDataCardinalityRestrictions ont)

ontologyDocumentObjectCardinalityRestrictions :
  P.OntologyDocument → List ObjectCardinalityRestriction
ontologyDocumentObjectCardinalityRestrictions document =
  ontologyObjectCardinalityRestrictions (P.documentOntology document)

ontologyDocumentDataCardinalityRestrictions :
  P.OntologyDocument → List DataCardinalityRestriction
ontologyDocumentDataCardinalityRestrictions document =
  ontologyDataCardinalityRestrictions (P.documentOntology document)

ontologyDocumentCardinalityRestrictions :
  P.OntologyDocument → List CardinalityRestriction
ontologyDocumentCardinalityRestrictions document =
  cardinalityRestrictions
    (ontologyDocumentObjectCardinalityRestrictions document)
    (ontologyDocumentDataCardinalityRestrictions document)

data CardinalityRestrictionSafetyIssue : Type₀ where
  topObjectPropertyCardinalityRestriction :
    ObjectCardinalityRestriction → CardinalityRestrictionSafetyIssue
  bottomObjectPropertyCardinalityRestriction :
    ObjectCardinalityRestriction → CardinalityRestrictionSafetyIssue
  complexObjectCardinalityQualifier :
    ObjectCardinalityRestriction →
    P.ClassExpression →
    CardinalityRestrictionSafetyIssue
  topDataPropertyCardinalityRestriction :
    DataCardinalityRestriction → CardinalityRestrictionSafetyIssue
  bottomDataPropertyCardinalityRestriction :
    DataCardinalityRestriction → CardinalityRestrictionSafetyIssue
  complexDataCardinalityRange :
    DataCardinalityRestriction →
    P.DataRange →
    CardinalityRestrictionSafetyIssue

objectPropertySafetyIssues :
  ObjectCardinalityRestriction →
  P.ObjectPropertyExpression →
  List CardinalityRestrictionSafetyIssue
objectPropertySafetyIssues restriction (P.objectProperty property) =
  []
objectPropertySafetyIssues restriction P.topObjectProperty =
  topObjectPropertyCardinalityRestriction restriction ∷ []
objectPropertySafetyIssues restriction P.bottomObjectProperty =
  bottomObjectPropertyCardinalityRestriction restriction ∷ []
objectPropertySafetyIssues restriction (P.objectInverseOf property) =
  objectPropertySafetyIssues restriction property

objectQualifierSafetyIssues :
  ObjectCardinalityRestriction →
  Optional P.ClassExpression →
  List CardinalityRestrictionSafetyIssue
objectQualifierSafetyIssues restriction absent =
  []
objectQualifierSafetyIssues restriction (present (P.namedClass class)) =
  []
objectQualifierSafetyIssues restriction (present P.owlThing) =
  []
objectQualifierSafetyIssues restriction (present P.owlNothing) =
  []
objectQualifierSafetyIssues restriction (present qualifier) =
  complexObjectCardinalityQualifier restriction qualifier ∷ []

objectCardinalityRestrictionSafetyIssues :
  ObjectCardinalityRestriction → List CardinalityRestrictionSafetyIssue
objectCardinalityRestrictionSafetyIssues restriction =
  objectPropertySafetyIssues
    restriction
    (objectCardinalityRestrictionProperty restriction)
  ++
  objectQualifierSafetyIssues
    restriction
    (objectCardinalityRestrictionQualifier restriction)

dataPropertySafetyIssues :
  DataCardinalityRestriction →
  P.DataPropertyExpression →
  List CardinalityRestrictionSafetyIssue
dataPropertySafetyIssues restriction (P.dataProperty property) =
  []
dataPropertySafetyIssues restriction P.topDataProperty =
  topDataPropertyCardinalityRestriction restriction ∷ []
dataPropertySafetyIssues restriction P.bottomDataProperty =
  bottomDataPropertyCardinalityRestriction restriction ∷ []

dataRangeSafetyIssues :
  DataCardinalityRestriction →
  Optional P.DataRange →
  List CardinalityRestrictionSafetyIssue
dataRangeSafetyIssues restriction absent =
  []
dataRangeSafetyIssues restriction (present (P.datatype datatype)) =
  []
dataRangeSafetyIssues restriction (present P.dataTop) =
  []
dataRangeSafetyIssues restriction (present P.dataBottom) =
  []
dataRangeSafetyIssues restriction (present range) =
  complexDataCardinalityRange restriction range ∷ []

dataCardinalityRestrictionSafetyIssues :
  DataCardinalityRestriction → List CardinalityRestrictionSafetyIssue
dataCardinalityRestrictionSafetyIssues restriction =
  dataPropertySafetyIssues
    restriction
    (dataCardinalityRestrictionProperty restriction)
  ++
  dataRangeSafetyIssues
    restriction
    (dataCardinalityRestrictionRange restriction)

record ObjectCardinalityRestrictionClassification : Type₀ where
  constructor objectCardinalityRestrictionClassification
  field
    classifiedObjectCardinalityRestriction :
      ObjectCardinalityRestriction
    classifiedObjectCardinalityRestrictionIssues :
      List CardinalityRestrictionSafetyIssue

open ObjectCardinalityRestrictionClassification public

record DataCardinalityRestrictionClassification : Type₀ where
  constructor dataCardinalityRestrictionClassification
  field
    classifiedDataCardinalityRestriction :
      DataCardinalityRestriction
    classifiedDataCardinalityRestrictionIssues :
      List CardinalityRestrictionSafetyIssue

open DataCardinalityRestrictionClassification public

classifyObjectCardinalityRestriction :
  ObjectCardinalityRestriction →
  ObjectCardinalityRestrictionClassification
classifyObjectCardinalityRestriction restriction =
  objectCardinalityRestrictionClassification
    restriction
    (objectCardinalityRestrictionSafetyIssues restriction)

classifyDataCardinalityRestriction :
  DataCardinalityRestriction →
  DataCardinalityRestrictionClassification
classifyDataCardinalityRestriction restriction =
  dataCardinalityRestrictionClassification
    restriction
    (dataCardinalityRestrictionSafetyIssues restriction)

classifyObjectCardinalityRestrictions :
  List ObjectCardinalityRestriction →
  List ObjectCardinalityRestrictionClassification
classifyObjectCardinalityRestrictions =
  map classifyObjectCardinalityRestriction

classifyDataCardinalityRestrictions :
  List DataCardinalityRestriction →
  List DataCardinalityRestrictionClassification
classifyDataCardinalityRestrictions =
  map classifyDataCardinalityRestriction

objectCardinalityRestrictionsFromClassifications :
  List ObjectCardinalityRestrictionClassification →
  List ObjectCardinalityRestriction
objectCardinalityRestrictionsFromClassifications [] =
  []
objectCardinalityRestrictionsFromClassifications (classification ∷ rest) =
  classifiedObjectCardinalityRestriction classification
  ∷ objectCardinalityRestrictionsFromClassifications rest

dataCardinalityRestrictionsFromClassifications :
  List DataCardinalityRestrictionClassification →
  List DataCardinalityRestriction
dataCardinalityRestrictionsFromClassifications [] =
  []
dataCardinalityRestrictionsFromClassifications (classification ∷ rest) =
  classifiedDataCardinalityRestriction classification
  ∷ dataCardinalityRestrictionsFromClassifications rest

unsafeObjectCardinalityRestrictionIssues :
  List ObjectCardinalityRestrictionClassification →
  List CardinalityRestrictionSafetyIssue
unsafeObjectCardinalityRestrictionIssues [] =
  []
unsafeObjectCardinalityRestrictionIssues (classification ∷ rest) =
  classifiedObjectCardinalityRestrictionIssues classification
  ++ unsafeObjectCardinalityRestrictionIssues rest

unsafeDataCardinalityRestrictionIssues :
  List DataCardinalityRestrictionClassification →
  List CardinalityRestrictionSafetyIssue
unsafeDataCardinalityRestrictionIssues [] =
  []
unsafeDataCardinalityRestrictionIssues (classification ∷ rest) =
  classifiedDataCardinalityRestrictionIssues classification
  ++ unsafeDataCardinalityRestrictionIssues rest

record CardinalityRestrictionsReport : Type₀ where
  constructor cardinalityRestrictionsReport
  field
    cardinalityRestrictionsReportDocument :
      P.OntologyDocument
    reportObjectCardinalityRestrictions :
      List ObjectCardinalityRestriction
    reportDataCardinalityRestrictions :
      List DataCardinalityRestriction
    reportAllCardinalityRestrictions :
      List CardinalityRestriction
    reportObjectCardinalityRestrictionClassifications :
      List ObjectCardinalityRestrictionClassification
    reportDataCardinalityRestrictionClassifications :
      List DataCardinalityRestrictionClassification
    reportUnsafeCardinalityRestrictionIssues :
      List CardinalityRestrictionSafetyIssue
    reportObjectCardinalityRestrictionCount :
      ℕ
    reportDataCardinalityRestrictionCount :
      ℕ
    reportCardinalityRestrictionCount :
      ℕ
    reportUnsafeCardinalityRestrictionIssueCount :
      ℕ

open CardinalityRestrictionsReport public

reportCardinalityRestrictions :
  P.OntologyDocument → CardinalityRestrictionsReport
reportCardinalityRestrictions document =
  cardinalityRestrictionsReport
    document
    objectRestrictions
    dataRestrictions
    allRestrictions
    objectClassifications
    dataClassifications
    unsafeIssues
    (listCount objectRestrictions)
    (listCount dataRestrictions)
    (listCount allRestrictions)
    (listCount unsafeIssues)
  where
  objectRestrictions : List ObjectCardinalityRestriction
  objectRestrictions =
    ontologyDocumentObjectCardinalityRestrictions document

  dataRestrictions : List DataCardinalityRestriction
  dataRestrictions =
    ontologyDocumentDataCardinalityRestrictions document

  allRestrictions : List CardinalityRestriction
  allRestrictions =
    cardinalityRestrictions objectRestrictions dataRestrictions

  objectClassifications :
    List ObjectCardinalityRestrictionClassification
  objectClassifications =
    classifyObjectCardinalityRestrictions objectRestrictions

  dataClassifications :
    List DataCardinalityRestrictionClassification
  dataClassifications =
    classifyDataCardinalityRestrictions dataRestrictions

  unsafeIssues : List CardinalityRestrictionSafetyIssue
  unsafeIssues =
    unsafeObjectCardinalityRestrictionIssues objectClassifications
    ++ unsafeDataCardinalityRestrictionIssues dataClassifications

NoCardinalityRestrictionUses : List CardinalityRestriction → Type₀
NoCardinalityRestrictionUses [] =
  Unit*
NoCardinalityRestrictionUses (_ ∷ _) =
  ⊥

NoCardinalityRestrictionsInReport :
  CardinalityRestrictionsReport → Type₀
NoCardinalityRestrictionsInReport report =
  NoCardinalityRestrictionUses (reportAllCardinalityRestrictions report)

NoCardinalityRestrictions : P.OntologyDocument → Type₀
NoCardinalityRestrictions document =
  NoCardinalityRestrictionsInReport
    (reportCardinalityRestrictions document)

NoUnsafeCardinalityRestrictionIssues :
  List CardinalityRestrictionSafetyIssue → Type₀
NoUnsafeCardinalityRestrictionIssues [] =
  Unit*
NoUnsafeCardinalityRestrictionIssues (_ ∷ _) =
  ⊥

NoUnsafeCardinalityRestrictionsInReport :
  CardinalityRestrictionsReport → Type₀
NoUnsafeCardinalityRestrictionsInReport report =
  NoUnsafeCardinalityRestrictionIssues
    (reportUnsafeCardinalityRestrictionIssues report)

NoUnsafeCardinalityRestrictions : P.OntologyDocument → Type₀
NoUnsafeCardinalityRestrictions document =
  NoUnsafeCardinalityRestrictionsInReport
    (reportCardinalityRestrictions document)

objectClassificationsCoverRestrictions :
  (restrictions : List ObjectCardinalityRestriction) →
  objectCardinalityRestrictionsFromClassifications
    (classifyObjectCardinalityRestrictions restrictions)
  ≡ restrictions
objectClassificationsCoverRestrictions [] =
  refl
objectClassificationsCoverRestrictions (restriction ∷ restrictions) =
  cong
    (λ rest → restriction ∷ rest)
    (objectClassificationsCoverRestrictions restrictions)

dataClassificationsCoverRestrictions :
  (restrictions : List DataCardinalityRestriction) →
  dataCardinalityRestrictionsFromClassifications
    (classifyDataCardinalityRestrictions restrictions)
  ≡ restrictions
dataClassificationsCoverRestrictions [] =
  refl
dataClassificationsCoverRestrictions (restriction ∷ restrictions) =
  cong
    (λ rest → restriction ∷ rest)
    (dataClassificationsCoverRestrictions restrictions)

record CardinalityRestrictionsExplicitlyClassified
  (document : P.OntologyDocument) : Type₀ where
  constructor cardinalityRestrictionsExplicitlyClassified
  field
    objectCardinalityRestrictionsClassified :
      objectCardinalityRestrictionsFromClassifications
        (reportObjectCardinalityRestrictionClassifications
          (reportCardinalityRestrictions document))
      ≡ ontologyDocumentObjectCardinalityRestrictions document
    dataCardinalityRestrictionsClassified :
      dataCardinalityRestrictionsFromClassifications
        (reportDataCardinalityRestrictionClassifications
          (reportCardinalityRestrictions document))
      ≡ ontologyDocumentDataCardinalityRestrictions document

open CardinalityRestrictionsExplicitlyClassified public

cardinalityRestrictionsExplicitlyClassifiedProof :
  (document : P.OntologyDocument) →
  CardinalityRestrictionsExplicitlyClassified document
cardinalityRestrictionsExplicitlyClassifiedProof document =
  cardinalityRestrictionsExplicitlyClassified
    (objectClassificationsCoverRestrictions
      (ontologyDocumentObjectCardinalityRestrictions document))
    (dataClassificationsCoverRestrictions
      (ontologyDocumentDataCardinalityRestrictions document))