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

module OWL2.Portable.PropertyKinds where

open import OWL2.Prelude
import OWL2.Portable.Syntax as P

data EntityRole : Type₀ where
  classRole :
    EntityRole
  objectPropertyRole :
    EntityRole
  dataPropertyRole :
    EntityRole
  datatypeRole :
    EntityRole
  namedIndividualRole :
    EntityRole
  annotationPropertyRole :
    EntityRole

data DeclarationCollisionKind : Type₀ where
  propertyKindCollision :
    DeclarationCollisionKind
  classDatatypeCollision :
    DeclarationCollisionKind
  strictPunningCollision :
    DeclarationCollisionKind

iriKey : P.IRI → String
iriKey i =
  P.payload i

reservedIRIKey : P.ReservedIRI → String
reservedIRIKey P.owlThingIRI =
  "http://www.w3.org/2002/07/owl#Thing"
reservedIRIKey P.owlNothingIRI =
  "http://www.w3.org/2002/07/owl#Nothing"
reservedIRIKey P.owlTopObjectPropertyIRI =
  "http://www.w3.org/2002/07/owl#topObjectProperty"
reservedIRIKey P.owlBottomObjectPropertyIRI =
  "http://www.w3.org/2002/07/owl#bottomObjectProperty"
reservedIRIKey P.owlTopDataPropertyIRI =
  "http://www.w3.org/2002/07/owl#topDataProperty"
reservedIRIKey P.owlBottomDataPropertyIRI =
  "http://www.w3.org/2002/07/owl#bottomDataProperty"
reservedIRIKey P.rdfPlainLiteralIRI =
  "http://www.w3.org/1999/02/22-rdf-syntax-ns#PlainLiteral"
reservedIRIKey P.rdfsLiteralIRI =
  "http://www.w3.org/2000/01/rdf-schema#Literal"
reservedIRIKey P.xsdStringIRI =
  "http://www.w3.org/2001/XMLSchema#string"

nameKey : P.Name → String
nameKey (P.named i) =
  iriKey i
nameKey (P.reserved r) =
  reservedIRIKey r

entityKey : P.Entity → String
entityKey (P.classEntity c) =
  nameKey c
entityKey (P.objectPropertyEntity p) =
  nameKey p
entityKey (P.dataPropertyEntity p) =
  nameKey p
entityKey (P.datatypeEntity d) =
  nameKey d
entityKey (P.namedIndividualEntity i) =
  iriKey i
entityKey (P.annotationPropertyEntity p) =
  iriKey p

entityRole : P.Entity → EntityRole
entityRole (P.classEntity c) =
  classRole
entityRole (P.objectPropertyEntity p) =
  objectPropertyRole
entityRole (P.dataPropertyEntity p) =
  dataPropertyRole
entityRole (P.datatypeEntity d) =
  datatypeRole
entityRole (P.namedIndividualEntity i) =
  namedIndividualRole
entityRole (P.annotationPropertyEntity p) =
  annotationPropertyRole

record DeclarationFact : Type₀ where
  constructor declarationFact
  field
    key    : String
    role   : EntityRole
    source : P.Annotated P.Axiom

open DeclarationFact public

declarationFactFromAnnotated :
  P.Annotated P.Axiom → Optional DeclarationFact
declarationFactFromAnnotated ax with P.body ax
... | P.declaration e =
  present (declarationFact (entityKey e) (entityRole e) ax)
... | _ =
  absent

declarationFacts :
  List (P.Annotated P.Axiom) → List DeclarationFact
declarationFacts axioms =
  filterMap declarationFactFromAnnotated axioms

ontologyDeclarationFacts : P.Ontology → List DeclarationFact
ontologyDeclarationFacts ont =
  declarationFacts (P.axioms ont)

ontologyDocumentDeclarationFacts :
  P.OntologyDocument → List DeclarationFact
ontologyDocumentDeclarationFacts document =
  ontologyDeclarationFacts (P.documentOntology document)

record DeclarationCollision : Type₀ where
  constructor declarationCollision
  field
    collisionKey : String
    leftRole     : EntityRole
    rightRole    : EntityRole
    kind         : DeclarationCollisionKind
    leftSource   : P.Annotated P.Axiom
    rightSource  : P.Annotated P.Axiom

open DeclarationCollision public

owl2DLCollisionKind :
  EntityRole → EntityRole → Optional DeclarationCollisionKind
owl2DLCollisionKind classRole datatypeRole =
  present classDatatypeCollision
owl2DLCollisionKind datatypeRole classRole =
  present classDatatypeCollision
owl2DLCollisionKind objectPropertyRole dataPropertyRole =
  present propertyKindCollision
owl2DLCollisionKind dataPropertyRole objectPropertyRole =
  present propertyKindCollision
owl2DLCollisionKind objectPropertyRole annotationPropertyRole =
  present propertyKindCollision
owl2DLCollisionKind annotationPropertyRole objectPropertyRole =
  present propertyKindCollision
owl2DLCollisionKind dataPropertyRole annotationPropertyRole =
  present propertyKindCollision
owl2DLCollisionKind annotationPropertyRole dataPropertyRole =
  present propertyKindCollision
owl2DLCollisionKind _ _ =
  absent

sameEntityRole : EntityRole → EntityRole → Bool
sameEntityRole classRole classRole =
  true
sameEntityRole objectPropertyRole objectPropertyRole =
  true
sameEntityRole dataPropertyRole dataPropertyRole =
  true
sameEntityRole datatypeRole datatypeRole =
  true
sameEntityRole namedIndividualRole namedIndividualRole =
  true
sameEntityRole annotationPropertyRole annotationPropertyRole =
  true
sameEntityRole _ _ =
  false

strictPunningCollisionKind :
  EntityRole → EntityRole → Optional DeclarationCollisionKind
strictPunningCollisionKind left right with sameEntityRole left right
... | true =
  absent
... | false =
  present strictPunningCollision

maybeCollision :
  (EntityRole → EntityRole → Optional DeclarationCollisionKind) →
  DeclarationFact → DeclarationFact → Optional DeclarationCollision
maybeCollision classify left right
  with primStringEquality (key left) (key right) | classify (role left) (role right)
... | true | present collisionKind =
  present
    (declarationCollision
      (key left)
      (role left)
      (role right)
      collisionKind
      (source left)
      (source right))
... | _ | _ =
  absent

collisionsWith :
  (DeclarationFact → DeclarationFact → Optional DeclarationCollision) →
  DeclarationFact → List DeclarationFact → List DeclarationCollision
collisionsWith check left [] =
  []
collisionsWith check left (right ∷ facts) with check left right
... | present collision =
  collision ∷ collisionsWith check left facts
... | absent =
  collisionsWith check left facts

pairwiseCollisions :
  (DeclarationFact → DeclarationFact → Optional DeclarationCollision) →
  List DeclarationFact → List DeclarationCollision
pairwiseCollisions check [] =
  []
pairwiseCollisions check (fact ∷ facts) =
  collisionsWith check fact facts ++ pairwiseCollisions check facts

owl2DLDeclarationCollisions :
  List (P.Annotated P.Axiom) → List DeclarationCollision
owl2DLDeclarationCollisions axioms =
  pairwiseCollisions
    (maybeCollision owl2DLCollisionKind)
    (declarationFacts axioms)

owl2DLOntologyDeclarationCollisions :
  P.Ontology → List DeclarationCollision
owl2DLOntologyDeclarationCollisions ont =
  owl2DLDeclarationCollisions (P.axioms ont)

owl2DLOntologyDocumentDeclarationCollisions :
  P.OntologyDocument → List DeclarationCollision
owl2DLOntologyDocumentDeclarationCollisions document =
  owl2DLOntologyDeclarationCollisions (P.documentOntology document)

strictDeclarationPunningCollisions :
  List (P.Annotated P.Axiom) → List DeclarationCollision
strictDeclarationPunningCollisions axioms =
  pairwiseCollisions
    (maybeCollision strictPunningCollisionKind)
    (declarationFacts axioms)

strictOntologyDeclarationPunningCollisions :
  P.Ontology → List DeclarationCollision
strictOntologyDeclarationPunningCollisions ont =
  strictDeclarationPunningCollisions (P.axioms ont)

strictOntologyDocumentDeclarationPunningCollisions :
  P.OntologyDocument → List DeclarationCollision
strictOntologyDocumentDeclarationPunningCollisions document =
  strictOntologyDeclarationPunningCollisions (P.documentOntology document)

NoCollisions : List DeclarationCollision → Type₀
NoCollisions [] =
  Unit*
NoCollisions (_ ∷ _) =
  ⊥

OWL2DLDeclarationRolesConsistent : P.OntologyDocument → Type₀
OWL2DLDeclarationRolesConsistent document =
  NoCollisions (owl2DLOntologyDocumentDeclarationCollisions document)

StrictDeclarationRolesConsistent : P.OntologyDocument → Type₀
StrictDeclarationRolesConsistent document =
  NoCollisions (strictOntologyDocumentDeclarationPunningCollisions document)

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

  collectOptional :
    ∀ {A B : Type₀} → (A → List B) → Optional A → List B
  collectOptional f absent =
    []
  collectOptional f (present x) =
    f x

  collectOneOrMore :
    ∀ {A B : Type₀} → (A → List B) → P.OneOrMore A → List B
  collectOneOrMore f xs =
    f (P.head xs) ++ concatMap f (P.tail xs)

  collectTwoOrMore :
    ∀ {A B : Type₀} → (A → List B) → P.TwoOrMore A → List B
  collectTwoOrMore f xs =
    f (P.first xs) ++ f (P.second xs) ++ concatMap f (P.rest xs)

data PropertyUsageRole : Type₀ where
  objectPropertyUsageRole :
    PropertyUsageRole
  dataPropertyUsageRole :
    PropertyUsageRole
  annotationPropertyUsageRole :
    PropertyUsageRole

samePropertyUsageRole : PropertyUsageRole → PropertyUsageRole → Bool
samePropertyUsageRole objectPropertyUsageRole objectPropertyUsageRole =
  true
samePropertyUsageRole dataPropertyUsageRole dataPropertyUsageRole =
  true
samePropertyUsageRole annotationPropertyUsageRole annotationPropertyUsageRole =
  true
samePropertyUsageRole _ _ =
  false

record PropertyUsageFact : Type₀ where
  constructor propertyUsageFact
  field
    propertyUseKey    : String
    propertyUseRole   : PropertyUsageRole
    propertyUseSource : P.Annotated P.Axiom

open PropertyUsageFact public

objectPropertyUsageFact :
  P.Annotated P.Axiom → P.ObjectPropertyName → PropertyUsageFact
objectPropertyUsageFact source p =
  propertyUsageFact (nameKey p) objectPropertyUsageRole source

dataPropertyUsageFact :
  P.Annotated P.Axiom → P.DataPropertyName → PropertyUsageFact
dataPropertyUsageFact source p =
  propertyUsageFact (nameKey p) dataPropertyUsageRole source

annotationPropertyUsageFact :
  P.Annotated P.Axiom → P.AnnotationPropertyName → PropertyUsageFact
annotationPropertyUsageFact source p =
  propertyUsageFact (iriKey p) annotationPropertyUsageRole source

mutual
  propertyUsageFactsInAnnotation :
    P.Annotated P.Axiom → P.Annotation → List PropertyUsageFact
  propertyUsageFactsInAnnotation source (P.annotation annotations property value) =
    annotationPropertyUsageFact source property
    ∷ propertyUsageFactsInAnnotations source annotations

  propertyUsageFactsInAnnotations :
    P.Annotated P.Axiom → List P.Annotation → List PropertyUsageFact
  propertyUsageFactsInAnnotations source [] =
    []
  propertyUsageFactsInAnnotations source (ann ∷ annotations) =
    propertyUsageFactsInAnnotation source ann
    ++ propertyUsageFactsInAnnotations source annotations

propertyUsageFactsInObjectPropertyExpression :
  P.Annotated P.Axiom →
  P.ObjectPropertyExpression →
  List PropertyUsageFact
propertyUsageFactsInObjectPropertyExpression source (P.objectProperty p) =
  objectPropertyUsageFact source p ∷ []
propertyUsageFactsInObjectPropertyExpression source P.topObjectProperty =
  []
propertyUsageFactsInObjectPropertyExpression source P.bottomObjectProperty =
  []
propertyUsageFactsInObjectPropertyExpression source (P.objectInverseOf p) =
  propertyUsageFactsInObjectPropertyExpression source p

propertyUsageFactsInObjectPropertyChain :
  P.Annotated P.Axiom → P.ObjectPropertyChain → List PropertyUsageFact
propertyUsageFactsInObjectPropertyChain source (P.objectPropertyChain properties) =
  collectTwoOrMore
    (propertyUsageFactsInObjectPropertyExpression source)
    properties

propertyUsageFactsInSubObjectPropertyExpression :
  P.Annotated P.Axiom →
  P.SubObjectPropertyExpression →
  List PropertyUsageFact
propertyUsageFactsInSubObjectPropertyExpression source (P.subObjectProperty p) =
  propertyUsageFactsInObjectPropertyExpression source p
propertyUsageFactsInSubObjectPropertyExpression
  source
  (P.subObjectPropertyChain chain) =
  propertyUsageFactsInObjectPropertyChain source chain

propertyUsageFactsInDataPropertyExpression :
  P.Annotated P.Axiom →
  P.DataPropertyExpression →
  List PropertyUsageFact
propertyUsageFactsInDataPropertyExpression source (P.dataProperty p) =
  dataPropertyUsageFact source p ∷ []
propertyUsageFactsInDataPropertyExpression source P.topDataProperty =
  []
propertyUsageFactsInDataPropertyExpression source P.bottomDataProperty =
  []

propertyUsageFactsInPropertyKey :
  P.Annotated P.Axiom → P.PropertyKey → List PropertyUsageFact
propertyUsageFactsInPropertyKey source key =
  concatMap
    (propertyUsageFactsInObjectPropertyExpression source)
    (P.objectProperties key)
  ++
  concatMap
    (propertyUsageFactsInDataPropertyExpression source)
    (P.dataProperties key)

mutual
  propertyUsageFactsInClassExpression :
    P.Annotated P.Axiom → P.ClassExpression → List PropertyUsageFact
  propertyUsageFactsInClassExpression source (P.namedClass c) =
    []
  propertyUsageFactsInClassExpression source P.owlThing =
    []
  propertyUsageFactsInClassExpression source P.owlNothing =
    []
  propertyUsageFactsInClassExpression source (P.objectIntersectionOf cs) =
    propertyUsageFactsInClassExpressionsTwoOrMore source cs
  propertyUsageFactsInClassExpression source (P.objectUnionOf cs) =
    propertyUsageFactsInClassExpressionsTwoOrMore source cs
  propertyUsageFactsInClassExpression source (P.objectComplementOf c) =
    propertyUsageFactsInClassExpression source c
  propertyUsageFactsInClassExpression source (P.objectOneOf individuals) =
    []
  propertyUsageFactsInClassExpression
    source
    (P.objectSomeValuesFrom p c) =
    propertyUsageFactsInObjectPropertyExpression source p
    ++ propertyUsageFactsInClassExpression source c
  propertyUsageFactsInClassExpression
    source
    (P.objectAllValuesFrom p c) =
    propertyUsageFactsInObjectPropertyExpression source p
    ++ propertyUsageFactsInClassExpression source c
  propertyUsageFactsInClassExpression source (P.objectHasValue p individual) =
    propertyUsageFactsInObjectPropertyExpression source p
  propertyUsageFactsInClassExpression source (P.objectHasSelf p) =
    propertyUsageFactsInObjectPropertyExpression source p
  propertyUsageFactsInClassExpression
    source
    (P.objectMinCardinality n p qualifier) =
    propertyUsageFactsInObjectPropertyExpression source p
    ++ propertyUsageFactsInOptionalClassExpression source qualifier
  propertyUsageFactsInClassExpression
    source
    (P.objectMaxCardinality n p qualifier) =
    propertyUsageFactsInObjectPropertyExpression source p
    ++ propertyUsageFactsInOptionalClassExpression source qualifier
  propertyUsageFactsInClassExpression
    source
    (P.objectExactCardinality n p qualifier) =
    propertyUsageFactsInObjectPropertyExpression source p
    ++ propertyUsageFactsInOptionalClassExpression source qualifier
  propertyUsageFactsInClassExpression source (P.dataSomeValuesFrom p range) =
    propertyUsageFactsInDataPropertyExpression source p
  propertyUsageFactsInClassExpression source (P.dataAllValuesFrom p range) =
    propertyUsageFactsInDataPropertyExpression source p
  propertyUsageFactsInClassExpression source (P.dataHasValue p literal) =
    propertyUsageFactsInDataPropertyExpression source p
  propertyUsageFactsInClassExpression
    source
    (P.dataMinCardinality n p qualifier) =
    propertyUsageFactsInDataPropertyExpression source p
  propertyUsageFactsInClassExpression
    source
    (P.dataMaxCardinality n p qualifier) =
    propertyUsageFactsInDataPropertyExpression source p
  propertyUsageFactsInClassExpression
    source
    (P.dataExactCardinality n p qualifier) =
    propertyUsageFactsInDataPropertyExpression source p

  propertyUsageFactsInOptionalClassExpression :
    P.Annotated P.Axiom →
    Optional P.ClassExpression →
    List PropertyUsageFact
  propertyUsageFactsInOptionalClassExpression source absent =
    []
  propertyUsageFactsInOptionalClassExpression source (present c) =
    propertyUsageFactsInClassExpression source c

  propertyUsageFactsInClassExpressions :
    P.Annotated P.Axiom →
    List P.ClassExpression →
    List PropertyUsageFact
  propertyUsageFactsInClassExpressions source [] =
    []
  propertyUsageFactsInClassExpressions source (c ∷ cs) =
    propertyUsageFactsInClassExpression source c
    ++ propertyUsageFactsInClassExpressions source cs

  propertyUsageFactsInClassExpressionsTwoOrMore :
    P.Annotated P.Axiom →
    P.TwoOrMore P.ClassExpression →
    List PropertyUsageFact
  propertyUsageFactsInClassExpressionsTwoOrMore source cs =
    propertyUsageFactsInClassExpression source (P.first cs)
    ++
    propertyUsageFactsInClassExpression source (P.second cs)
    ++
    propertyUsageFactsInClassExpressions source (P.rest cs)

propertyUsageFactsInEntity :
  P.Annotated P.Axiom → P.Entity → List PropertyUsageFact
propertyUsageFactsInEntity source (P.classEntity c) =
  []
propertyUsageFactsInEntity source (P.objectPropertyEntity p) =
  objectPropertyUsageFact source p ∷ []
propertyUsageFactsInEntity source (P.dataPropertyEntity p) =
  dataPropertyUsageFact source p ∷ []
propertyUsageFactsInEntity source (P.datatypeEntity d) =
  []
propertyUsageFactsInEntity source (P.namedIndividualEntity i) =
  []
propertyUsageFactsInEntity source (P.annotationPropertyEntity p) =
  annotationPropertyUsageFact source p ∷ []

propertyUsageFactsInAxiom :
  P.Annotated P.Axiom → P.Axiom → List PropertyUsageFact
propertyUsageFactsInAxiom source (P.declaration e) =
  propertyUsageFactsInEntity source e
propertyUsageFactsInAxiom source (P.subClassOf c d) =
  propertyUsageFactsInClassExpression source c
  ++ propertyUsageFactsInClassExpression source d
propertyUsageFactsInAxiom source (P.equivalentClasses cs) =
  propertyUsageFactsInClassExpressionsTwoOrMore source cs
propertyUsageFactsInAxiom source (P.disjointClasses cs) =
  propertyUsageFactsInClassExpressionsTwoOrMore source cs
propertyUsageFactsInAxiom source (P.disjointUnion c cs) =
  propertyUsageFactsInClassExpressionsTwoOrMore source cs
propertyUsageFactsInAxiom source (P.subObjectPropertyOf p q) =
  propertyUsageFactsInSubObjectPropertyExpression source p
  ++ propertyUsageFactsInObjectPropertyExpression source q
propertyUsageFactsInAxiom source (P.equivalentObjectProperties ps) =
  collectTwoOrMore
    (propertyUsageFactsInObjectPropertyExpression source)
    ps
propertyUsageFactsInAxiom source (P.disjointObjectProperties ps) =
  collectTwoOrMore
    (propertyUsageFactsInObjectPropertyExpression source)
    ps
propertyUsageFactsInAxiom source (P.inverseObjectProperties p q) =
  propertyUsageFactsInObjectPropertyExpression source p
  ++ propertyUsageFactsInObjectPropertyExpression source q
propertyUsageFactsInAxiom source (P.objectPropertyDomain p c) =
  propertyUsageFactsInObjectPropertyExpression source p
  ++ propertyUsageFactsInClassExpression source c
propertyUsageFactsInAxiom source (P.objectPropertyRange p c) =
  propertyUsageFactsInObjectPropertyExpression source p
  ++ propertyUsageFactsInClassExpression source c
propertyUsageFactsInAxiom source (P.functionalObjectProperty p) =
  propertyUsageFactsInObjectPropertyExpression source p
propertyUsageFactsInAxiom source (P.inverseFunctionalObjectProperty p) =
  propertyUsageFactsInObjectPropertyExpression source p
propertyUsageFactsInAxiom source (P.reflexiveObjectProperty p) =
  propertyUsageFactsInObjectPropertyExpression source p
propertyUsageFactsInAxiom source (P.irreflexiveObjectProperty p) =
  propertyUsageFactsInObjectPropertyExpression source p
propertyUsageFactsInAxiom source (P.symmetricObjectProperty p) =
  propertyUsageFactsInObjectPropertyExpression source p
propertyUsageFactsInAxiom source (P.asymmetricObjectProperty p) =
  propertyUsageFactsInObjectPropertyExpression source p
propertyUsageFactsInAxiom source (P.transitiveObjectProperty p) =
  propertyUsageFactsInObjectPropertyExpression source p
propertyUsageFactsInAxiom source (P.subDataPropertyOf p q) =
  propertyUsageFactsInDataPropertyExpression source p
  ++ propertyUsageFactsInDataPropertyExpression source q
propertyUsageFactsInAxiom source (P.equivalentDataProperties ps) =
  collectTwoOrMore
    (propertyUsageFactsInDataPropertyExpression source)
    ps
propertyUsageFactsInAxiom source (P.disjointDataProperties ps) =
  collectTwoOrMore
    (propertyUsageFactsInDataPropertyExpression source)
    ps
propertyUsageFactsInAxiom source (P.dataPropertyDomain p c) =
  propertyUsageFactsInDataPropertyExpression source p
  ++ propertyUsageFactsInClassExpression source c
propertyUsageFactsInAxiom source (P.dataPropertyRange p range) =
  propertyUsageFactsInDataPropertyExpression source p
propertyUsageFactsInAxiom source (P.functionalDataProperty p) =
  propertyUsageFactsInDataPropertyExpression source p
propertyUsageFactsInAxiom source (P.datatypeDefinition datatype range) =
  []
propertyUsageFactsInAxiom source (P.hasKey c key) =
  propertyUsageFactsInClassExpression source c
  ++ propertyUsageFactsInPropertyKey source key
propertyUsageFactsInAxiom source (P.sameIndividual individuals) =
  []
propertyUsageFactsInAxiom source (P.differentIndividuals individuals) =
  []
propertyUsageFactsInAxiom source (P.classAssertion c individual) =
  propertyUsageFactsInClassExpression source c
propertyUsageFactsInAxiom source (P.objectPropertyAssertion p subject object) =
  propertyUsageFactsInObjectPropertyExpression source p
propertyUsageFactsInAxiom source (P.negativeObjectPropertyAssertion p subject object) =
  propertyUsageFactsInObjectPropertyExpression source p
propertyUsageFactsInAxiom source (P.dataPropertyAssertion p subject value) =
  propertyUsageFactsInDataPropertyExpression source p
propertyUsageFactsInAxiom source (P.negativeDataPropertyAssertion p subject value) =
  propertyUsageFactsInDataPropertyExpression source p
propertyUsageFactsInAxiom source (P.annotationAssertion p subject value) =
  annotationPropertyUsageFact source p ∷ []
propertyUsageFactsInAxiom source (P.subAnnotationPropertyOf p q) =
  annotationPropertyUsageFact source p
  ∷ annotationPropertyUsageFact source q
  ∷ []
propertyUsageFactsInAxiom source (P.annotationPropertyDomain p domain) =
  annotationPropertyUsageFact source p ∷ []
propertyUsageFactsInAxiom source (P.annotationPropertyRange p range) =
  annotationPropertyUsageFact source p ∷ []

propertyUsageFactsInAnnotated :
  P.Annotated P.Axiom → List PropertyUsageFact
propertyUsageFactsInAnnotated source =
  propertyUsageFactsInAnnotations source (P.annotations source)
  ++ propertyUsageFactsInAxiom source (P.body source)

propertyUsageFacts :
  List (P.Annotated P.Axiom) → List PropertyUsageFact
propertyUsageFacts axioms =
  concatMap propertyUsageFactsInAnnotated axioms

ontologyPropertyUsageFacts : P.Ontology → List PropertyUsageFact
ontologyPropertyUsageFacts ont =
  propertyUsageFacts (P.axioms ont)

ontologyDocumentPropertyUsageFacts :
  P.OntologyDocument → List PropertyUsageFact
ontologyDocumentPropertyUsageFacts document =
  ontologyPropertyUsageFacts (P.documentOntology document)

record PropertyUsageConflict : Type₀ where
  constructor propertyUsageConflict
  field
    propertyUsageConflictKey :
      String
    leftPropertyUsageRole :
      PropertyUsageRole
    rightPropertyUsageRole :
      PropertyUsageRole
    leftPropertyUsageSource :
      P.Annotated P.Axiom
    rightPropertyUsageSource :
      P.Annotated P.Axiom

open PropertyUsageConflict public

maybePropertyUsageConflict :
  PropertyUsageFact → PropertyUsageFact → Optional PropertyUsageConflict
maybePropertyUsageConflict left right
  with primStringEquality
        (propertyUseKey left)
        (propertyUseKey right)
     | samePropertyUsageRole
        (propertyUseRole left)
        (propertyUseRole right)
... | true | false =
  present
    (propertyUsageConflict
      (propertyUseKey left)
      (propertyUseRole left)
      (propertyUseRole right)
      (propertyUseSource left)
      (propertyUseSource right))
... | _ | _ =
  absent

propertyUsageConflictsWith :
  PropertyUsageFact →
  List PropertyUsageFact →
  List PropertyUsageConflict
propertyUsageConflictsWith left [] =
  []
propertyUsageConflictsWith left (right ∷ facts)
  with maybePropertyUsageConflict left right
... | present conflict =
  conflict ∷ propertyUsageConflictsWith left facts
... | absent =
  propertyUsageConflictsWith left facts

pairwisePropertyUsageConflicts :
  List PropertyUsageFact → List PropertyUsageConflict
pairwisePropertyUsageConflicts [] =
  []
pairwisePropertyUsageConflicts (fact ∷ facts) =
  propertyUsageConflictsWith fact facts
  ++ pairwisePropertyUsageConflicts facts

propertyRoleUsageConflicts :
  List (P.Annotated P.Axiom) → List PropertyUsageConflict
propertyRoleUsageConflicts axioms =
  pairwisePropertyUsageConflicts (propertyUsageFacts axioms)

ontologyPropertyRoleUsageConflicts :
  P.Ontology → List PropertyUsageConflict
ontologyPropertyRoleUsageConflicts ont =
  propertyRoleUsageConflicts (P.axioms ont)

ontologyDocumentPropertyRoleUsageConflicts :
  P.OntologyDocument → List PropertyUsageConflict
ontologyDocumentPropertyRoleUsageConflicts document =
  ontologyPropertyRoleUsageConflicts (P.documentOntology document)

NoPropertyUsageConflicts : List PropertyUsageConflict → Type₀
NoPropertyUsageConflicts [] =
  Unit*
NoPropertyUsageConflicts (_ ∷ _) =
  ⊥

PropertyRoleUsageConsistent : P.OntologyDocument → Type₀
PropertyRoleUsageConsistent document =
  NoPropertyUsageConflicts
    (ontologyDocumentPropertyRoleUsageConflicts document)