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

module OWL2.Portable.Declarations where

open import OWL2.Prelude
import OWL2.Portable.PropertyKinds as PK
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

data EntityUseSource : Type₀ where
  axiomSource :
    P.Annotated P.Axiom → EntityUseSource
  ontologyAnnotationSource :
    P.Annotation → EntityUseSource

record EntityUseFact : Type₀ where
  constructor entityUseFact
  field
    entityUseKey :
      String
    entityUseRole :
      PK.EntityRole
    entityUseSource :
      EntityUseSource

open EntityUseFact public

classUseFact : EntityUseSource → P.ClassName → EntityUseFact
classUseFact source c =
  entityUseFact (PK.nameKey c) PK.classRole source

objectPropertyUseFact :
  EntityUseSource → P.ObjectPropertyName → EntityUseFact
objectPropertyUseFact source p =
  entityUseFact (PK.nameKey p) PK.objectPropertyRole source

dataPropertyUseFact :
  EntityUseSource → P.DataPropertyName → EntityUseFact
dataPropertyUseFact source p =
  entityUseFact (PK.nameKey p) PK.dataPropertyRole source

datatypeUseFact : EntityUseSource → P.DatatypeName → EntityUseFact
datatypeUseFact source d =
  entityUseFact (PK.nameKey d) PK.datatypeRole source

namedIndividualUseFact :
  EntityUseSource → P.NamedIndividualName → EntityUseFact
namedIndividualUseFact source i =
  entityUseFact (PK.iriKey i) PK.namedIndividualRole source

annotationPropertyUseFact :
  EntityUseSource → P.AnnotationPropertyName → EntityUseFact
annotationPropertyUseFact source p =
  entityUseFact (PK.iriKey p) PK.annotationPropertyRole source

mutual
  entityUsesInAnnotationValue :
    EntityUseSource → P.AnnotationValue → List EntityUseFact
  entityUsesInAnnotationValue source (P.annotationValueIRI value) =
    []
  entityUsesInAnnotationValue source (P.annotationValueAnonymous value) =
    []
  entityUsesInAnnotationValue source (P.annotationValueLiteral literal) =
    entityUsesInLiteral source literal

  entityUsesInAnnotation :
    EntityUseSource → P.Annotation → List EntityUseFact
  entityUsesInAnnotation source (P.annotation annotations property value) =
    annotationPropertyUseFact source property
    ∷
    ( entityUsesInAnnotations source annotations
      ++ entityUsesInAnnotationValue source value )

  entityUsesInAnnotations :
    EntityUseSource → List P.Annotation → List EntityUseFact
  entityUsesInAnnotations source [] =
    []
  entityUsesInAnnotations source (ann ∷ annotations) =
    entityUsesInAnnotation source ann
    ++ entityUsesInAnnotations source annotations

  entityUsesInLiteral : EntityUseSource → P.Literal → List EntityUseFact
  entityUsesInLiteral source (P.typedLiteral lexical datatype) =
    datatypeUseFact source datatype ∷ []
  entityUsesInLiteral source (P.stringLiteral lexical) =
    []
  entityUsesInLiteral source (P.languageLiteral lexical language) =
    []

  entityUsesInLiterals :
    EntityUseSource → List P.Literal → List EntityUseFact
  entityUsesInLiterals source [] =
    []
  entityUsesInLiterals source (literal ∷ literals) =
    entityUsesInLiteral source literal
    ++ entityUsesInLiterals source literals

  entityUsesInLiteralsOneOrMore :
    EntityUseSource → P.OneOrMore P.Literal → List EntityUseFact
  entityUsesInLiteralsOneOrMore source literals =
    entityUsesInLiteral source (P.head literals)
    ++ entityUsesInLiterals source (P.tail literals)

  entityUsesInIndividual :
    EntityUseSource → P.Individual → List EntityUseFact
  entityUsesInIndividual source (P.namedIndividual i) =
    namedIndividualUseFact source i ∷ []
  entityUsesInIndividual source (P.anonymousIndividual bnode) =
    []

  entityUsesInIndividuals :
    EntityUseSource → List P.Individual → List EntityUseFact
  entityUsesInIndividuals source [] =
    []
  entityUsesInIndividuals source (individual ∷ individuals) =
    entityUsesInIndividual source individual
    ++ entityUsesInIndividuals source individuals

  entityUsesInIndividualsOneOrMore :
    EntityUseSource → P.OneOrMore P.Individual → List EntityUseFact
  entityUsesInIndividualsOneOrMore source individuals =
    entityUsesInIndividual source (P.head individuals)
    ++ entityUsesInIndividuals source (P.tail individuals)

  entityUsesInIndividualsTwoOrMore :
    EntityUseSource → P.TwoOrMore P.Individual → List EntityUseFact
  entityUsesInIndividualsTwoOrMore source individuals =
    entityUsesInIndividual source (P.first individuals)
    ++
    entityUsesInIndividual source (P.second individuals)
    ++
    entityUsesInIndividuals source (P.rest individuals)

  entityUsesInFacetRestriction :
    EntityUseSource → P.FacetRestriction → List EntityUseFact
  entityUsesInFacetRestriction source restriction =
    entityUsesInLiteral source (P.value restriction)

  entityUsesInFacetRestrictions :
    EntityUseSource → List P.FacetRestriction → List EntityUseFact
  entityUsesInFacetRestrictions source [] =
    []
  entityUsesInFacetRestrictions source (restriction ∷ restrictions) =
    entityUsesInFacetRestriction source restriction
    ++ entityUsesInFacetRestrictions source restrictions

  entityUsesInDataRange :
    EntityUseSource → P.DataRange → List EntityUseFact
  entityUsesInDataRange source (P.datatype d) =
    datatypeUseFact source d ∷ []
  entityUsesInDataRange source P.dataTop =
    []
  entityUsesInDataRange source P.dataBottom =
    []
  entityUsesInDataRange source (P.dataComplementOf range) =
    entityUsesInDataRange source range
  entityUsesInDataRange source (P.dataIntersectionOf ranges) =
    entityUsesInDataRangesTwoOrMore source ranges
  entityUsesInDataRange source (P.dataUnionOf ranges) =
    entityUsesInDataRangesTwoOrMore source ranges
  entityUsesInDataRange source (P.dataOneOf literals) =
    entityUsesInLiteralsOneOrMore source literals
  entityUsesInDataRange source (P.datatypeRestriction datatype restrictions) =
    datatypeUseFact source datatype
    ∷ entityUsesInFacetRestrictions source restrictions

  entityUsesInDataRanges :
    EntityUseSource → List P.DataRange → List EntityUseFact
  entityUsesInDataRanges source [] =
    []
  entityUsesInDataRanges source (range ∷ ranges) =
    entityUsesInDataRange source range
    ++ entityUsesInDataRanges source ranges

  entityUsesInDataRangesTwoOrMore :
    EntityUseSource → P.TwoOrMore P.DataRange → List EntityUseFact
  entityUsesInDataRangesTwoOrMore source ranges =
    entityUsesInDataRange source (P.first ranges)
    ++
    entityUsesInDataRange source (P.second ranges)
    ++
    entityUsesInDataRanges source (P.rest ranges)

  entityUsesInOptionalDataRange :
    EntityUseSource → Optional P.DataRange → List EntityUseFact
  entityUsesInOptionalDataRange source absent =
    []
  entityUsesInOptionalDataRange source (present range) =
    entityUsesInDataRange source range

  entityUsesInObjectPropertyExpression :
    EntityUseSource → P.ObjectPropertyExpression → List EntityUseFact
  entityUsesInObjectPropertyExpression source (P.objectProperty p) =
    objectPropertyUseFact source p ∷ []
  entityUsesInObjectPropertyExpression source P.topObjectProperty =
    []
  entityUsesInObjectPropertyExpression source P.bottomObjectProperty =
    []
  entityUsesInObjectPropertyExpression source (P.objectInverseOf p) =
    entityUsesInObjectPropertyExpression source p

  entityUsesInObjectPropertyExpressions :
    EntityUseSource →
    List P.ObjectPropertyExpression →
    List EntityUseFact
  entityUsesInObjectPropertyExpressions source [] =
    []
  entityUsesInObjectPropertyExpressions source (p ∷ ps) =
    entityUsesInObjectPropertyExpression source p
    ++ entityUsesInObjectPropertyExpressions source ps

  entityUsesInObjectPropertyExpressionsTwoOrMore :
    EntityUseSource →
    P.TwoOrMore P.ObjectPropertyExpression →
    List EntityUseFact
  entityUsesInObjectPropertyExpressionsTwoOrMore source properties =
    entityUsesInObjectPropertyExpression source (P.first properties)
    ++
    entityUsesInObjectPropertyExpression source (P.second properties)
    ++
    entityUsesInObjectPropertyExpressions source (P.rest properties)

  entityUsesInObjectPropertyChain :
    EntityUseSource → P.ObjectPropertyChain → List EntityUseFact
  entityUsesInObjectPropertyChain
    source
    (P.objectPropertyChain properties) =
    entityUsesInObjectPropertyExpressionsTwoOrMore source properties

  entityUsesInSubObjectPropertyExpression :
    EntityUseSource →
    P.SubObjectPropertyExpression →
    List EntityUseFact
  entityUsesInSubObjectPropertyExpression source (P.subObjectProperty p) =
    entityUsesInObjectPropertyExpression source p
  entityUsesInSubObjectPropertyExpression
    source
    (P.subObjectPropertyChain chain) =
    entityUsesInObjectPropertyChain source chain

  entityUsesInDataPropertyExpression :
    EntityUseSource → P.DataPropertyExpression → List EntityUseFact
  entityUsesInDataPropertyExpression source (P.dataProperty p) =
    dataPropertyUseFact source p ∷ []
  entityUsesInDataPropertyExpression source P.topDataProperty =
    []
  entityUsesInDataPropertyExpression source P.bottomDataProperty =
    []

  entityUsesInDataPropertyExpressions :
    EntityUseSource → List P.DataPropertyExpression → List EntityUseFact
  entityUsesInDataPropertyExpressions source [] =
    []
  entityUsesInDataPropertyExpressions source (p ∷ ps) =
    entityUsesInDataPropertyExpression source p
    ++ entityUsesInDataPropertyExpressions source ps

  entityUsesInDataPropertyExpressionsTwoOrMore :
    EntityUseSource → P.TwoOrMore P.DataPropertyExpression → List EntityUseFact
  entityUsesInDataPropertyExpressionsTwoOrMore source properties =
    entityUsesInDataPropertyExpression source (P.first properties)
    ++
    entityUsesInDataPropertyExpression source (P.second properties)
    ++
    entityUsesInDataPropertyExpressions source (P.rest properties)

  entityUsesInPropertyKey :
    EntityUseSource → P.PropertyKey → List EntityUseFact
  entityUsesInPropertyKey source key =
    entityUsesInObjectPropertyExpressions source (P.objectProperties key)
    ++
    entityUsesInDataPropertyExpressions source (P.dataProperties key)

  entityUsesInClassExpression :
    EntityUseSource → P.ClassExpression → List EntityUseFact
  entityUsesInClassExpression source (P.namedClass c) =
    classUseFact source c ∷ []
  entityUsesInClassExpression source P.owlThing =
    []
  entityUsesInClassExpression source P.owlNothing =
    []
  entityUsesInClassExpression source (P.objectIntersectionOf cs) =
    entityUsesInClassExpressionsTwoOrMore source cs
  entityUsesInClassExpression source (P.objectUnionOf cs) =
    entityUsesInClassExpressionsTwoOrMore source cs
  entityUsesInClassExpression source (P.objectComplementOf c) =
    entityUsesInClassExpression source c
  entityUsesInClassExpression source (P.objectOneOf individuals) =
    entityUsesInIndividualsOneOrMore source individuals
  entityUsesInClassExpression source (P.objectSomeValuesFrom p c) =
    entityUsesInObjectPropertyExpression source p
    ++ entityUsesInClassExpression source c
  entityUsesInClassExpression source (P.objectAllValuesFrom p c) =
    entityUsesInObjectPropertyExpression source p
    ++ entityUsesInClassExpression source c
  entityUsesInClassExpression source (P.objectHasValue p individual) =
    entityUsesInObjectPropertyExpression source p
    ++ entityUsesInIndividual source individual
  entityUsesInClassExpression source (P.objectHasSelf p) =
    entityUsesInObjectPropertyExpression source p
  entityUsesInClassExpression source (P.objectMinCardinality n p qualifier) =
    entityUsesInObjectPropertyExpression source p
    ++ entityUsesInOptionalClassExpression source qualifier
  entityUsesInClassExpression source (P.objectMaxCardinality n p qualifier) =
    entityUsesInObjectPropertyExpression source p
    ++ entityUsesInOptionalClassExpression source qualifier
  entityUsesInClassExpression source (P.objectExactCardinality n p qualifier) =
    entityUsesInObjectPropertyExpression source p
    ++ entityUsesInOptionalClassExpression source qualifier
  entityUsesInClassExpression source (P.dataSomeValuesFrom p range) =
    entityUsesInDataPropertyExpression source p
    ++ entityUsesInDataRange source range
  entityUsesInClassExpression source (P.dataAllValuesFrom p range) =
    entityUsesInDataPropertyExpression source p
    ++ entityUsesInDataRange source range
  entityUsesInClassExpression source (P.dataHasValue p literal) =
    entityUsesInDataPropertyExpression source p
    ++ entityUsesInLiteral source literal
  entityUsesInClassExpression source (P.dataMinCardinality n p qualifier) =
    entityUsesInDataPropertyExpression source p
    ++ entityUsesInOptionalDataRange source qualifier
  entityUsesInClassExpression source (P.dataMaxCardinality n p qualifier) =
    entityUsesInDataPropertyExpression source p
    ++ entityUsesInOptionalDataRange source qualifier
  entityUsesInClassExpression source (P.dataExactCardinality n p qualifier) =
    entityUsesInDataPropertyExpression source p
    ++ entityUsesInOptionalDataRange source qualifier

  entityUsesInClassExpressions :
    EntityUseSource → List P.ClassExpression → List EntityUseFact
  entityUsesInClassExpressions source [] =
    []
  entityUsesInClassExpressions source (c ∷ cs) =
    entityUsesInClassExpression source c
    ++ entityUsesInClassExpressions source cs

  entityUsesInClassExpressionsTwoOrMore :
    EntityUseSource → P.TwoOrMore P.ClassExpression → List EntityUseFact
  entityUsesInClassExpressionsTwoOrMore source cs =
    entityUsesInClassExpression source (P.first cs)
    ++
    entityUsesInClassExpression source (P.second cs)
    ++
    entityUsesInClassExpressions source (P.rest cs)

  entityUsesInOptionalClassExpression :
    EntityUseSource → Optional P.ClassExpression → List EntityUseFact
  entityUsesInOptionalClassExpression source absent =
    []
  entityUsesInOptionalClassExpression source (present c) =
    entityUsesInClassExpression source c

entityUsesInAxiom : EntityUseSource → P.Axiom → List EntityUseFact
entityUsesInAxiom source (P.declaration entity) =
  []
entityUsesInAxiom source (P.subClassOf c d) =
  entityUsesInClassExpression source c
  ++ entityUsesInClassExpression source d
entityUsesInAxiom source (P.equivalentClasses cs) =
  entityUsesInClassExpressionsTwoOrMore source cs
entityUsesInAxiom source (P.disjointClasses cs) =
  entityUsesInClassExpressionsTwoOrMore source cs
entityUsesInAxiom source (P.disjointUnion c cs) =
  classUseFact source c
  ∷ entityUsesInClassExpressionsTwoOrMore source cs
entityUsesInAxiom source (P.subObjectPropertyOf p q) =
  entityUsesInSubObjectPropertyExpression source p
  ++ entityUsesInObjectPropertyExpression source q
entityUsesInAxiom source (P.equivalentObjectProperties ps) =
  entityUsesInObjectPropertyExpressionsTwoOrMore source ps
entityUsesInAxiom source (P.disjointObjectProperties ps) =
  entityUsesInObjectPropertyExpressionsTwoOrMore source ps
entityUsesInAxiom source (P.inverseObjectProperties p q) =
  entityUsesInObjectPropertyExpression source p
  ++ entityUsesInObjectPropertyExpression source q
entityUsesInAxiom source (P.objectPropertyDomain p c) =
  entityUsesInObjectPropertyExpression source p
  ++ entityUsesInClassExpression source c
entityUsesInAxiom source (P.objectPropertyRange p c) =
  entityUsesInObjectPropertyExpression source p
  ++ entityUsesInClassExpression source c
entityUsesInAxiom source (P.functionalObjectProperty p) =
  entityUsesInObjectPropertyExpression source p
entityUsesInAxiom source (P.inverseFunctionalObjectProperty p) =
  entityUsesInObjectPropertyExpression source p
entityUsesInAxiom source (P.reflexiveObjectProperty p) =
  entityUsesInObjectPropertyExpression source p
entityUsesInAxiom source (P.irreflexiveObjectProperty p) =
  entityUsesInObjectPropertyExpression source p
entityUsesInAxiom source (P.symmetricObjectProperty p) =
  entityUsesInObjectPropertyExpression source p
entityUsesInAxiom source (P.asymmetricObjectProperty p) =
  entityUsesInObjectPropertyExpression source p
entityUsesInAxiom source (P.transitiveObjectProperty p) =
  entityUsesInObjectPropertyExpression source p
entityUsesInAxiom source (P.subDataPropertyOf p q) =
  entityUsesInDataPropertyExpression source p
  ++ entityUsesInDataPropertyExpression source q
entityUsesInAxiom source (P.equivalentDataProperties ps) =
  entityUsesInDataPropertyExpressionsTwoOrMore source ps
entityUsesInAxiom source (P.disjointDataProperties ps) =
  entityUsesInDataPropertyExpressionsTwoOrMore source ps
entityUsesInAxiom source (P.dataPropertyDomain p c) =
  entityUsesInDataPropertyExpression source p
  ++ entityUsesInClassExpression source c
entityUsesInAxiom source (P.dataPropertyRange p range) =
  entityUsesInDataPropertyExpression source p
  ++ entityUsesInDataRange source range
entityUsesInAxiom source (P.functionalDataProperty p) =
  entityUsesInDataPropertyExpression source p
entityUsesInAxiom source (P.datatypeDefinition datatype range) =
  datatypeUseFact source datatype
  ∷ entityUsesInDataRange source range
entityUsesInAxiom source (P.hasKey c key) =
  entityUsesInClassExpression source c
  ++ entityUsesInPropertyKey source key
entityUsesInAxiom source (P.sameIndividual individuals) =
  entityUsesInIndividualsTwoOrMore source individuals
entityUsesInAxiom source (P.differentIndividuals individuals) =
  entityUsesInIndividualsTwoOrMore source individuals
entityUsesInAxiom source (P.classAssertion c individual) =
  entityUsesInClassExpression source c
  ++ entityUsesInIndividual source individual
entityUsesInAxiom source (P.objectPropertyAssertion p subject object) =
  entityUsesInObjectPropertyExpression source p
  ++ entityUsesInIndividual source subject
  ++ entityUsesInIndividual source object
entityUsesInAxiom source (P.negativeObjectPropertyAssertion p subject object) =
  entityUsesInObjectPropertyExpression source p
  ++ entityUsesInIndividual source subject
  ++ entityUsesInIndividual source object
entityUsesInAxiom source (P.dataPropertyAssertion p subject value) =
  entityUsesInDataPropertyExpression source p
  ++ entityUsesInIndividual source subject
  ++ entityUsesInLiteral source value
entityUsesInAxiom source (P.negativeDataPropertyAssertion p subject value) =
  entityUsesInDataPropertyExpression source p
  ++ entityUsesInIndividual source subject
  ++ entityUsesInLiteral source value
entityUsesInAxiom source (P.annotationAssertion p subject value) =
  annotationPropertyUseFact source p
  ∷ entityUsesInAnnotationValue source value
entityUsesInAxiom source (P.subAnnotationPropertyOf p q) =
  annotationPropertyUseFact source p
  ∷ annotationPropertyUseFact source q
  ∷ []
entityUsesInAxiom source (P.annotationPropertyDomain p domain) =
  annotationPropertyUseFact source p ∷ []
entityUsesInAxiom source (P.annotationPropertyRange p range) =
  annotationPropertyUseFact source p ∷ []

entityUsesInAnnotated : P.Annotated P.Axiom → List EntityUseFact
entityUsesInAnnotated ax =
  entityUsesInAnnotations source (P.annotations ax)
  ++ entityUsesInAxiom source (P.body ax)
  where
  source : EntityUseSource
  source =
    axiomSource ax

entityUsesInOntologyAnnotation : P.Annotation → List EntityUseFact
entityUsesInOntologyAnnotation ann =
  entityUsesInAnnotation (ontologyAnnotationSource ann) ann

entityUsesInOntology : P.Ontology → List EntityUseFact
entityUsesInOntology ont =
  concatMap entityUsesInOntologyAnnotation (P.annotations ont)
  ++ concatMap entityUsesInAnnotated (P.axioms ont)

entityUses : List (P.Annotated P.Axiom) → List EntityUseFact
entityUses axioms =
  concatMap entityUsesInAnnotated axioms

ontologyDocumentEntityUses :
  P.OntologyDocument → List EntityUseFact
ontologyDocumentEntityUses document =
  entityUsesInOntology (P.documentOntology document)

record UndeclaredEntityUse : Type₀ where
  constructor undeclaredEntityUse
  field
    undeclaredUseKey :
      String
    undeclaredUseRole :
      PK.EntityRole
    undeclaredUseSource :
      EntityUseSource

open UndeclaredEntityUse public

declarationMatchesUse : PK.DeclarationFact → EntityUseFact → Bool
declarationMatchesUse declaration use
  with primStringEquality (PK.key declaration) (entityUseKey use)
     | PK.sameEntityRole (PK.role declaration) (entityUseRole use)
... | true | true =
  true
... | _ | _ =
  false

declaredUse : List PK.DeclarationFact → EntityUseFact → Bool
declaredUse [] use =
  false
declaredUse (declaration ∷ declarations) use
  with declarationMatchesUse declaration use
... | true =
  true
... | false =
  declaredUse declarations use

maybeUndeclaredUse :
  List PK.DeclarationFact → EntityUseFact → Optional UndeclaredEntityUse
maybeUndeclaredUse declarations use with declaredUse declarations use
... | true =
  absent
... | false =
  present
    (undeclaredEntityUse
      (entityUseKey use)
      (entityUseRole use)
      (entityUseSource use))

undeclaredEntityUsesFromFacts :
  List PK.DeclarationFact → List EntityUseFact → List UndeclaredEntityUse
undeclaredEntityUsesFromFacts declarations uses =
  filterMap (maybeUndeclaredUse declarations) uses

undeclaredEntityUses :
  List (P.Annotated P.Axiom) → List UndeclaredEntityUse
undeclaredEntityUses axioms =
  undeclaredEntityUsesFromFacts
    (PK.declarationFacts axioms)
    (entityUses axioms)

ontologyUndeclaredEntityUses :
  P.Ontology → List UndeclaredEntityUse
ontologyUndeclaredEntityUses ont =
  undeclaredEntityUsesFromFacts
    (PK.declarationFacts (P.axioms ont))
    (entityUsesInOntology ont)

ontologyDocumentUndeclaredEntityUses :
  P.OntologyDocument → List UndeclaredEntityUse
ontologyDocumentUndeclaredEntityUses document =
  ontologyUndeclaredEntityUses (P.documentOntology document)

NoUndeclaredEntityUses : List UndeclaredEntityUse → Type₀
NoUndeclaredEntityUses [] =
  Unit*
NoUndeclaredEntityUses (_ ∷ _) =
  ⊥

AllEntityUsesDeclared : P.OntologyDocument → Type₀
AllEntityUsesDeclared document =
  NoUndeclaredEntityUses (ontologyDocumentUndeclaredEntityUses document)