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

module OWL2.Portable.Regularity where

open import Cubical.Data.Nat.Base using (zero; suc)
open import OWL2.Prelude
import OWL2.Data.String as String
import OWL2.Portable.ObjectPropertyKeys as Keys
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 [] =
    
  listCount (x ∷ xs) =
    suc (listCount xs)

  twoOrMoreToList : ∀ {A : Type₀} → P.TwoOrMore A → List A
  twoOrMoreToList xs =
    P.first xs ∷ P.second xs ∷ P.rest xs

objectPropertyBaseKey : P.ObjectPropertyExpression → String
objectPropertyBaseKey =
  Keys.portableObjectPropertyBaseKey

data CompositeObjectPropertyKind : Type₀ where
  topObjectPropertyComposite :
    CompositeObjectPropertyKind
  bottomObjectPropertyComposite :
    CompositeObjectPropertyKind
  propertyChainSuperPropertyComposite :
    CompositeObjectPropertyKind
  transitiveObjectPropertyComposite :
    CompositeObjectPropertyKind

record CompositeObjectPropertyFact : Type₀ where
  constructor compositeObjectPropertyFact
  field
    compositeObjectPropertyKey :
      String
    compositeObjectPropertyExpression :
      P.ObjectPropertyExpression
    compositeObjectPropertyKind :
      CompositeObjectPropertyKind
    compositeObjectPropertySource :
      Optional (P.Annotated P.Axiom)

open CompositeObjectPropertyFact public

topObjectPropertyCompositeFact : CompositeObjectPropertyFact
topObjectPropertyCompositeFact =
  compositeObjectPropertyFact
    (objectPropertyBaseKey P.topObjectProperty)
    P.topObjectProperty
    topObjectPropertyComposite
    absent

bottomObjectPropertyCompositeFact : CompositeObjectPropertyFact
bottomObjectPropertyCompositeFact =
  compositeObjectPropertyFact
    (objectPropertyBaseKey P.bottomObjectProperty)
    P.bottomObjectProperty
    bottomObjectPropertyComposite
    absent

compositeFactsForAnnotatedAxiom :
  P.Annotated P.Axiom → List CompositeObjectPropertyFact
compositeFactsForAnnotatedAxiom source with P.body source
... | P.subObjectPropertyOf (P.subObjectProperty property) super =
  []
... | P.subObjectPropertyOf (P.subObjectPropertyChain chain) super =
  compositeObjectPropertyFact
    (objectPropertyBaseKey super)
    super
    propertyChainSuperPropertyComposite
    (present source)
  ∷ []
... | P.transitiveObjectProperty property =
  compositeObjectPropertyFact
    (objectPropertyBaseKey property)
    property
    transitiveObjectPropertyComposite
    (present source)
  ∷ []
... | _ =
  []

compositeFactsForAnnotatedAxioms :
  List (P.Annotated P.Axiom) → List CompositeObjectPropertyFact
compositeFactsForAnnotatedAxioms =
  concatMap compositeFactsForAnnotatedAxiom

ontologyCompositeObjectPropertyFacts :
  P.Ontology → List CompositeObjectPropertyFact
ontologyCompositeObjectPropertyFacts ont =
  topObjectPropertyCompositeFact
  ∷
  bottomObjectPropertyCompositeFact
  ∷
  compositeFactsForAnnotatedAxioms (P.axioms ont)

ontologyDocumentCompositeObjectPropertyFacts :
  P.OntologyDocument → List CompositeObjectPropertyFact
ontologyDocumentCompositeObjectPropertyFacts document =
  ontologyCompositeObjectPropertyFacts (P.documentOntology document)

data PropertyHierarchyFactKind : Type₀ where
  subObjectPropertyHierarchy :
    PropertyHierarchyFactKind
  equivalentObjectPropertiesHierarchy :
    PropertyHierarchyFactKind
  inverseObjectPropertiesHierarchy :
    PropertyHierarchyFactKind

record PropertyHierarchyFact : Type₀ where
  constructor propertyHierarchyFact
  field
    propertyHierarchySubPropertyKey :
      String
    propertyHierarchySuperPropertyKey :
      String
    propertyHierarchySubProperty :
      P.ObjectPropertyExpression
    propertyHierarchySuperProperty :
      P.ObjectPropertyExpression
    propertyHierarchyFactKind :
      PropertyHierarchyFactKind
    propertyHierarchyFactSource :
      P.Annotated P.Axiom

open PropertyHierarchyFact public

propertyHierarchyFactFor :
  P.Annotated P.Axiom →
  PropertyHierarchyFactKind →
  P.ObjectPropertyExpression →
  P.ObjectPropertyExpression →
  PropertyHierarchyFact
propertyHierarchyFactFor source kind sub super =
  propertyHierarchyFact
    (objectPropertyBaseKey sub)
    (objectPropertyBaseKey super)
    sub
    super
    kind
    source

propertyHierarchyFactsFromPropertyToProperties :
  P.Annotated P.Axiom →
  PropertyHierarchyFactKind →
  P.ObjectPropertyExpression →
  List P.ObjectPropertyExpression →
  List PropertyHierarchyFact
propertyHierarchyFactsFromPropertyToProperties source kind property [] =
  []
propertyHierarchyFactsFromPropertyToProperties
  source
  kind
  property
  (target ∷ targets) =
  propertyHierarchyFactFor source kind property target
  ∷
  propertyHierarchyFactsFromPropertyToProperties
    source
    kind
    property
    targets

propertyHierarchyFactsForEquivalentPropertyListFrom :
  P.Annotated P.Axiom →
  List P.ObjectPropertyExpression →
  List P.ObjectPropertyExpression →
  List PropertyHierarchyFact
propertyHierarchyFactsForEquivalentPropertyListFrom source allProperties [] =
  []
propertyHierarchyFactsForEquivalentPropertyListFrom
  source
  allProperties
  (property ∷ properties) =
  propertyHierarchyFactsFromPropertyToProperties
    source
    equivalentObjectPropertiesHierarchy
    property
    allProperties
  ++
  propertyHierarchyFactsForEquivalentPropertyListFrom
    source
    allProperties
    properties

propertyHierarchyFactsForEquivalentProperties :
  P.Annotated P.Axiom →
  P.TwoOrMore P.ObjectPropertyExpression →
  List PropertyHierarchyFact
propertyHierarchyFactsForEquivalentProperties source properties =
  propertyHierarchyFactsForEquivalentPropertyListFrom
    source
    propertyList
    propertyList
  where
  propertyList : List P.ObjectPropertyExpression
  propertyList =
    twoOrMoreToList properties

propertyHierarchyFactsForAnnotatedAxiom :
  P.Annotated P.Axiom → List PropertyHierarchyFact
propertyHierarchyFactsForAnnotatedAxiom source with P.body source
... | P.subObjectPropertyOf (P.subObjectProperty sub) super =
  propertyHierarchyFactFor
    source
    subObjectPropertyHierarchy
    sub
    super
  ∷ []
... | P.subObjectPropertyOf (P.subObjectPropertyChain chain) super =
  []
... | P.equivalentObjectProperties properties =
  propertyHierarchyFactsForEquivalentProperties source properties
... | P.inverseObjectProperties left right =
  propertyHierarchyFactFor
    source
    inverseObjectPropertiesHierarchy
    left
    (P.objectInverseOf right)
  ∷
  propertyHierarchyFactFor
    source
    inverseObjectPropertiesHierarchy
    (P.objectInverseOf right)
    left
  ∷ []
... | _ =
  []

propertyHierarchyFactsForAnnotatedAxioms :
  List (P.Annotated P.Axiom) → List PropertyHierarchyFact
propertyHierarchyFactsForAnnotatedAxioms =
  concatMap propertyHierarchyFactsForAnnotatedAxiom

ontologyPropertyHierarchyFacts : P.Ontology → List PropertyHierarchyFact
ontologyPropertyHierarchyFacts ont =
  propertyHierarchyFactsForAnnotatedAxioms (P.axioms ont)

ontologyDocumentPropertyHierarchyFacts :
  P.OntologyDocument → List PropertyHierarchyFact
ontologyDocumentPropertyHierarchyFacts document =
  ontologyPropertyHierarchyFacts (P.documentOntology document)

mutual
  propertyKeyReachableWithin :
    ℕ →
    List PropertyHierarchyFact →
    String →
    String →
    Bool
  propertyKeyReachableWithin zero facts start target =
    String.stringEquality start target
  propertyKeyReachableWithin (suc fuel) facts start target
    with String.stringEquality start target
  ... | true =
    true
  ... | false =
    propertyKeyReachableThroughFacts fuel facts start target facts

  propertyKeyReachableThroughFacts :
    ℕ →
    List PropertyHierarchyFact →
    String →
    String →
    List PropertyHierarchyFact →
    Bool
  propertyKeyReachableThroughFacts fuel allFacts start target [] =
    false
  propertyKeyReachableThroughFacts
    fuel
    allFacts
    start
    target
    (fact ∷ facts)
    with String.stringEquality start (propertyHierarchySubPropertyKey fact)
  ... | true
    with propertyKeyReachableWithin
           fuel
           allFacts
           (propertyHierarchySuperPropertyKey fact)
           target
  ...   | true =
    true
  ...   | false =
    propertyKeyReachableThroughFacts fuel allFacts start target facts
  propertyKeyReachableThroughFacts fuel allFacts start target (fact ∷ facts)
      | false =
    propertyKeyReachableThroughFacts fuel allFacts start target facts

propertyKeyReachable :
  List PropertyHierarchyFact →
  String →
  String →
  Bool
propertyKeyReachable facts start target =
  propertyKeyReachableWithin (listCount facts) facts start target

data SimplePropertyUseKind : Type₀ where
  objectHasSelfUse :
    SimplePropertyUseKind
  objectMinCardinalityUse :
    ℕ → SimplePropertyUseKind
  objectMaxCardinalityUse :
    ℕ → SimplePropertyUseKind
  objectExactCardinalityUse :
    ℕ → SimplePropertyUseKind
  disjointObjectPropertiesUse :
    SimplePropertyUseKind
  functionalObjectPropertyUse :
    SimplePropertyUseKind
  inverseFunctionalObjectPropertyUse :
    SimplePropertyUseKind
  irreflexiveObjectPropertyUse :
    SimplePropertyUseKind
  asymmetricObjectPropertyUse :
    SimplePropertyUseKind

record SimplePropertyUse : Type₀ where
  constructor simplePropertyUse
  field
    simplePropertyUseSource :
      P.Annotated P.Axiom
    simplePropertyUseKind :
      SimplePropertyUseKind
    simplePropertyUseProperty :
      P.ObjectPropertyExpression
    simplePropertyUseKey :
      String

open SimplePropertyUse public

simplePropertyUseAt :
  P.Annotated P.Axiom →
  SimplePropertyUseKind →
  P.ObjectPropertyExpression →
  List SimplePropertyUse
simplePropertyUseAt source kind property =
  simplePropertyUse source kind property (objectPropertyBaseKey property) ∷ []

simplePropertyUsesForProperties :
  P.Annotated P.Axiom →
  SimplePropertyUseKind →
  List P.ObjectPropertyExpression →
  List SimplePropertyUse
simplePropertyUsesForProperties source kind [] =
  []
simplePropertyUsesForProperties source kind (property ∷ properties) =
  simplePropertyUseAt source kind property
  ++ simplePropertyUsesForProperties source kind properties

simplePropertyUsesForPropertiesTwoOrMore :
  P.Annotated P.Axiom →
  SimplePropertyUseKind →
  P.TwoOrMore P.ObjectPropertyExpression →
  List SimplePropertyUse
simplePropertyUsesForPropertiesTwoOrMore source kind properties =
  simplePropertyUseAt source kind (P.first properties)
  ++
  simplePropertyUseAt source kind (P.second properties)
  ++
  simplePropertyUsesForProperties source kind (P.rest properties)

mutual
  simplePropertyUsesForClassExpression :
    P.Annotated P.Axiom → P.ClassExpression → List SimplePropertyUse
  simplePropertyUsesForClassExpression source (P.namedClass c) =
    []
  simplePropertyUsesForClassExpression source P.owlThing =
    []
  simplePropertyUsesForClassExpression source P.owlNothing =
    []
  simplePropertyUsesForClassExpression source (P.objectIntersectionOf classes) =
    simplePropertyUsesForClassExpressionsTwoOrMore source classes
  simplePropertyUsesForClassExpression source (P.objectUnionOf classes) =
    simplePropertyUsesForClassExpressionsTwoOrMore source classes
  simplePropertyUsesForClassExpression source (P.objectComplementOf class) =
    simplePropertyUsesForClassExpression source class
  simplePropertyUsesForClassExpression source (P.objectOneOf individuals) =
    []
  simplePropertyUsesForClassExpression
    source
    (P.objectSomeValuesFrom property class) =
    simplePropertyUsesForClassExpression source class
  simplePropertyUsesForClassExpression
    source
    (P.objectAllValuesFrom property class) =
    simplePropertyUsesForClassExpression source class
  simplePropertyUsesForClassExpression
    source
    (P.objectHasValue property individual) =
    []
  simplePropertyUsesForClassExpression source (P.objectHasSelf property) =
    simplePropertyUseAt source objectHasSelfUse property
  simplePropertyUsesForClassExpression
    source
    (P.objectMinCardinality n property qualifier) =
    simplePropertyUseAt source (objectMinCardinalityUse n) property
    ++ simplePropertyUsesForOptionalClassExpression source qualifier
  simplePropertyUsesForClassExpression
    source
    (P.objectMaxCardinality n property qualifier) =
    simplePropertyUseAt source (objectMaxCardinalityUse n) property
    ++ simplePropertyUsesForOptionalClassExpression source qualifier
  simplePropertyUsesForClassExpression
    source
    (P.objectExactCardinality n property qualifier) =
    simplePropertyUseAt source (objectExactCardinalityUse n) property
    ++ simplePropertyUsesForOptionalClassExpression source qualifier
  simplePropertyUsesForClassExpression source (P.dataSomeValuesFrom p range) =
    []
  simplePropertyUsesForClassExpression source (P.dataAllValuesFrom p range) =
    []
  simplePropertyUsesForClassExpression source (P.dataHasValue p literal) =
    []
  simplePropertyUsesForClassExpression
    source
    (P.dataMinCardinality n property qualifier) =
    []
  simplePropertyUsesForClassExpression
    source
    (P.dataMaxCardinality n property qualifier) =
    []
  simplePropertyUsesForClassExpression
    source
    (P.dataExactCardinality n property qualifier) =
    []

  simplePropertyUsesForOptionalClassExpression :
    P.Annotated P.Axiom →
    Optional P.ClassExpression →
    List SimplePropertyUse
  simplePropertyUsesForOptionalClassExpression source absent =
    []
  simplePropertyUsesForOptionalClassExpression source (present class) =
    simplePropertyUsesForClassExpression source class

  simplePropertyUsesForClassExpressions :
    P.Annotated P.Axiom →
    List P.ClassExpression →
    List SimplePropertyUse
  simplePropertyUsesForClassExpressions source [] =
    []
  simplePropertyUsesForClassExpressions source (class ∷ classes) =
    simplePropertyUsesForClassExpression source class
    ++ simplePropertyUsesForClassExpressions source classes

  simplePropertyUsesForClassExpressionsTwoOrMore :
    P.Annotated P.Axiom →
    P.TwoOrMore P.ClassExpression →
    List SimplePropertyUse
  simplePropertyUsesForClassExpressionsTwoOrMore source classes =
    simplePropertyUsesForClassExpression source (P.first classes)
    ++
    simplePropertyUsesForClassExpression source (P.second classes)
    ++
    simplePropertyUsesForClassExpressions source (P.rest classes)

simplePropertyUsesForAxiom :
  P.Annotated P.Axiom → P.Axiom → List SimplePropertyUse
simplePropertyUsesForAxiom source (P.declaration entity) =
  []
simplePropertyUsesForAxiom source (P.subClassOf left right) =
  simplePropertyUsesForClassExpression source left
  ++ simplePropertyUsesForClassExpression source right
simplePropertyUsesForAxiom source (P.equivalentClasses classes) =
  simplePropertyUsesForClassExpressionsTwoOrMore source classes
simplePropertyUsesForAxiom source (P.disjointClasses classes) =
  simplePropertyUsesForClassExpressionsTwoOrMore source classes
simplePropertyUsesForAxiom source (P.disjointUnion class classes) =
  simplePropertyUsesForClassExpressionsTwoOrMore source classes
simplePropertyUsesForAxiom source (P.subObjectPropertyOf left right) =
  []
simplePropertyUsesForAxiom
  source
  (P.equivalentObjectProperties properties) =
  []
simplePropertyUsesForAxiom source (P.disjointObjectProperties properties) =
  simplePropertyUsesForPropertiesTwoOrMore
    source
    disjointObjectPropertiesUse
    properties
simplePropertyUsesForAxiom
  source
  (P.inverseObjectProperties left right) =
  []
simplePropertyUsesForAxiom source (P.objectPropertyDomain property class) =
  simplePropertyUsesForClassExpression source class
simplePropertyUsesForAxiom source (P.objectPropertyRange property class) =
  simplePropertyUsesForClassExpression source class
simplePropertyUsesForAxiom source (P.functionalObjectProperty property) =
  simplePropertyUseAt source functionalObjectPropertyUse property
simplePropertyUsesForAxiom
  source
  (P.inverseFunctionalObjectProperty property) =
  simplePropertyUseAt source inverseFunctionalObjectPropertyUse property
simplePropertyUsesForAxiom source (P.reflexiveObjectProperty property) =
  []
simplePropertyUsesForAxiom source (P.irreflexiveObjectProperty property) =
  simplePropertyUseAt source irreflexiveObjectPropertyUse property
simplePropertyUsesForAxiom source (P.symmetricObjectProperty property) =
  []
simplePropertyUsesForAxiom source (P.asymmetricObjectProperty property) =
  simplePropertyUseAt source asymmetricObjectPropertyUse property
simplePropertyUsesForAxiom source (P.transitiveObjectProperty property) =
  []
simplePropertyUsesForAxiom source (P.subDataPropertyOf left right) =
  []
simplePropertyUsesForAxiom
  source
  (P.equivalentDataProperties properties) =
  []
simplePropertyUsesForAxiom source (P.disjointDataProperties properties) =
  []
simplePropertyUsesForAxiom source (P.dataPropertyDomain property class) =
  simplePropertyUsesForClassExpression source class
simplePropertyUsesForAxiom source (P.dataPropertyRange property range) =
  []
simplePropertyUsesForAxiom source (P.functionalDataProperty property) =
  []
simplePropertyUsesForAxiom source (P.datatypeDefinition datatype range) =
  []
simplePropertyUsesForAxiom source (P.hasKey class key) =
  simplePropertyUsesForClassExpression source class
simplePropertyUsesForAxiom source (P.sameIndividual individuals) =
  []
simplePropertyUsesForAxiom source (P.differentIndividuals individuals) =
  []
simplePropertyUsesForAxiom source (P.classAssertion class individual) =
  simplePropertyUsesForClassExpression source class
simplePropertyUsesForAxiom
  source
  (P.objectPropertyAssertion property subject object) =
  []
simplePropertyUsesForAxiom
  source
  (P.negativeObjectPropertyAssertion property subject object) =
  []
simplePropertyUsesForAxiom
  source
  (P.dataPropertyAssertion property subject value) =
  []
simplePropertyUsesForAxiom
  source
  (P.negativeDataPropertyAssertion property subject value) =
  []
simplePropertyUsesForAxiom
  source
  (P.annotationAssertion property subject value) =
  []
simplePropertyUsesForAxiom
  source
  (P.subAnnotationPropertyOf left right) =
  []
simplePropertyUsesForAxiom
  source
  (P.annotationPropertyDomain property domain) =
  []
simplePropertyUsesForAxiom
  source
  (P.annotationPropertyRange property range) =
  []

simplePropertyUsesForAnnotatedAxiom :
  P.Annotated P.Axiom → List SimplePropertyUse
simplePropertyUsesForAnnotatedAxiom source =
  simplePropertyUsesForAxiom source (P.body source)

simplePropertyUsesForAnnotatedAxioms :
  List (P.Annotated P.Axiom) → List SimplePropertyUse
simplePropertyUsesForAnnotatedAxioms =
  concatMap simplePropertyUsesForAnnotatedAxiom

ontologySimplePropertyUses : P.Ontology → List SimplePropertyUse
ontologySimplePropertyUses ont =
  simplePropertyUsesForAnnotatedAxioms (P.axioms ont)

ontologyDocumentSimplePropertyUses :
  P.OntologyDocument → List SimplePropertyUse
ontologyDocumentSimplePropertyUses document =
  ontologySimplePropertyUses (P.documentOntology document)

data SimplePropertyViolationKind : Type₀ where
  nonCanonicalSimplePropertyUse :
    SimplePropertyViolationKind
  compositeSimplePropertyUse :
    CompositeObjectPropertyFact → SimplePropertyViolationKind
  compositeHierarchySimplePropertyUse :
    CompositeObjectPropertyFact → SimplePropertyViolationKind

record SimplePropertyViolation : Type₀ where
  constructor simplePropertyViolation
  field
    simplePropertyViolationUse :
      SimplePropertyUse
    simplePropertyViolationKind :
      SimplePropertyViolationKind

open SimplePropertyViolation public

canonicalForSimplePropertyUse : P.ObjectPropertyExpression → Bool
canonicalForSimplePropertyUse (P.objectProperty p) =
  true
canonicalForSimplePropertyUse P.topObjectProperty =
  true
canonicalForSimplePropertyUse P.bottomObjectProperty =
  true
canonicalForSimplePropertyUse (P.objectInverseOf (P.objectProperty p)) =
  true
canonicalForSimplePropertyUse (P.objectInverseOf p) =
  false

nonCanonicalViolationForUse :
  SimplePropertyUse → List SimplePropertyViolation
nonCanonicalViolationForUse use
  with canonicalForSimplePropertyUse (simplePropertyUseProperty use)
... | true =
  []
... | false =
  simplePropertyViolation use nonCanonicalSimplePropertyUse ∷ []

compositeViolationsForUse :
  List PropertyHierarchyFact →
  SimplePropertyUse →
  List CompositeObjectPropertyFact →
  List SimplePropertyViolation
compositeViolationsForUse hierarchyFacts use [] =
  []
compositeViolationsForUse hierarchyFacts use (fact ∷ facts)
  with String.stringEquality
        (simplePropertyUseKey use)
        (compositeObjectPropertyKey fact)
... | true =
  simplePropertyViolation use (compositeSimplePropertyUse fact)
  ∷ compositeViolationsForUse hierarchyFacts use facts
... | false
  with propertyKeyReachable
         hierarchyFacts
         (compositeObjectPropertyKey fact)
         (simplePropertyUseKey use)
...   | true =
  simplePropertyViolation use (compositeHierarchySimplePropertyUse fact)
  ∷ compositeViolationsForUse hierarchyFacts use facts
...   | false =
  compositeViolationsForUse hierarchyFacts use facts

simplePropertyViolationsForUse :
  List CompositeObjectPropertyFact →
  List PropertyHierarchyFact →
  SimplePropertyUse →
  List SimplePropertyViolation
simplePropertyViolationsForUse compositeFacts hierarchyFacts use =
  nonCanonicalViolationForUse use
  ++ compositeViolationsForUse hierarchyFacts use compositeFacts

simplePropertyViolationsForUses :
  List CompositeObjectPropertyFact →
  List PropertyHierarchyFact →
  List SimplePropertyUse →
  List SimplePropertyViolation
simplePropertyViolationsForUses compositeFacts hierarchyFacts =
  concatMap (simplePropertyViolationsForUse compositeFacts hierarchyFacts)

ontologyDocumentSimplePropertyViolations :
  P.OntologyDocument → List SimplePropertyViolation
ontologyDocumentSimplePropertyViolations document =
  simplePropertyViolationsForUses
    (ontologyDocumentCompositeObjectPropertyFacts document)
    (ontologyDocumentPropertyHierarchyFacts document)
    (ontologyDocumentSimplePropertyUses document)

record RegularityReport : Type₀ where
  constructor regularityReport
  field
    regularityReportDocument :
      P.OntologyDocument
    regularityReportCompositeObjectPropertyFacts :
      List CompositeObjectPropertyFact
    regularityReportPropertyHierarchyFacts :
      List PropertyHierarchyFact
    regularityReportSimplePropertyUses :
      List SimplePropertyUse
    regularityReportSimplePropertyViolations :
      List SimplePropertyViolation
    regularityReportCompositeObjectPropertyCount :
      ℕ
    regularityReportPropertyHierarchyCount :
      ℕ
    regularityReportSimplePropertyUseCount :
      ℕ
    regularityReportSimplePropertyViolationCount :
      ℕ

open RegularityReport public

reportRegularity : P.OntologyDocument → RegularityReport
reportRegularity document =
  regularityReport
    document
    compositeFacts
    hierarchyFacts
    simpleUses
    violations
    (listCount compositeFacts)
    (listCount hierarchyFacts)
    (listCount simpleUses)
    (listCount violations)
  where
  compositeFacts : List CompositeObjectPropertyFact
  compositeFacts =
    ontologyDocumentCompositeObjectPropertyFacts document

  hierarchyFacts : List PropertyHierarchyFact
  hierarchyFacts =
    ontologyDocumentPropertyHierarchyFacts document

  simpleUses : List SimplePropertyUse
  simpleUses =
    ontologyDocumentSimplePropertyUses document

  violations : List SimplePropertyViolation
  violations =
    simplePropertyViolationsForUses compositeFacts hierarchyFacts simpleUses

NoSimplePropertyViolations :
  List SimplePropertyViolation → Type₀
NoSimplePropertyViolations [] =
  Unit*
NoSimplePropertyViolations (_ ∷ _) =
  ⊥

NoReportSimplePropertyViolations : RegularityReport → Type₀
NoReportSimplePropertyViolations report =
  NoSimplePropertyViolations
    (regularityReportSimplePropertyViolations report)

PortableRegularityRestrictions : P.OntologyDocument → Type₀
PortableRegularityRestrictions document =
  NoReportSimplePropertyViolations (reportRegularity document)