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

module OWL2.Profiles.EL where

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

data NonELFeature : Type₀ where
  objectInverseOfFeature :
    NonELFeature
  topObjectPropertyFeature :
    NonELFeature
  bottomObjectPropertyFeature :
    NonELFeature

  topDataPropertyFeature :
    NonELFeature
  bottomDataPropertyFeature :
    NonELFeature

  dataComplementOfFeature :
    NonELFeature
  dataIntersectionOfFeature :
    NonELFeature
  dataUnionOfFeature :
    NonELFeature
  dataOneOfFeature :
    NonELFeature
  datatypeRestrictionFeature :
    NonELFeature

  objectUnionOfFeature :
    NonELFeature
  objectComplementOfFeature :
    NonELFeature
  objectOneOfFeature :
    NonELFeature
  objectAllValuesFromFeature :
    NonELFeature
  objectHasSelfFeature :
    NonELFeature
  objectMinCardinalityFeature :
    NonELFeature
  objectMaxCardinalityFeature :
    NonELFeature
  objectExactCardinalityFeature :
    NonELFeature

  dataSomeValuesFromFeature :
    NonELFeature
  dataAllValuesFromFeature :
    NonELFeature
  dataHasValueFeature :
    NonELFeature
  dataMinCardinalityFeature :
    NonELFeature
  dataMaxCardinalityFeature :
    NonELFeature
  dataExactCardinalityFeature :
    NonELFeature

  disjointClassesAxiomFeature :
    NonELFeature
  disjointUnionAxiomFeature :
    NonELFeature
  equivalentObjectPropertiesAxiomFeature :
    NonELFeature
  disjointObjectPropertiesAxiomFeature :
    NonELFeature
  inverseObjectPropertiesAxiomFeature :
    NonELFeature
  functionalObjectPropertyAxiomFeature :
    NonELFeature
  inverseFunctionalObjectPropertyAxiomFeature :
    NonELFeature
  reflexiveObjectPropertyAxiomFeature :
    NonELFeature
  irreflexiveObjectPropertyAxiomFeature :
    NonELFeature
  symmetricObjectPropertyAxiomFeature :
    NonELFeature
  asymmetricObjectPropertyAxiomFeature :
    NonELFeature

  subDataPropertyOfAxiomFeature :
    NonELFeature
  equivalentDataPropertiesAxiomFeature :
    NonELFeature
  disjointDataPropertiesAxiomFeature :
    NonELFeature
  dataPropertyDomainAxiomFeature :
    NonELFeature
  dataPropertyRangeAxiomFeature :
    NonELFeature
  functionalDataPropertyAxiomFeature :
    NonELFeature
  datatypeDefinitionAxiomFeature :
    NonELFeature

  hasKeyAxiomFeature :
    NonELFeature
  sameIndividualAxiomFeature :
    NonELFeature
  differentIndividualsAxiomFeature :
    NonELFeature
  negativeObjectPropertyAssertionAxiomFeature :
    NonELFeature
  dataPropertyAssertionAxiomFeature :
    NonELFeature
  negativeDataPropertyAssertionAxiomFeature :
    NonELFeature

isEmpty : ∀ {A : Type₀} → List A → Bool
isEmpty [] =
  true
isEmpty (_ ∷ _) =
  false

NoNonELFeatures : List NonELFeature → Type₀
NoNonELFeatures [] =
  Unit*
NoNonELFeatures (_ ∷ _) =
  ⊥

objectPropertyExpressionNonELFeatures :
  P.ObjectPropertyExpression → List NonELFeature
objectPropertyExpressionNonELFeatures (P.objectProperty p) =
  []
objectPropertyExpressionNonELFeatures P.topObjectProperty =
  topObjectPropertyFeature ∷ []
objectPropertyExpressionNonELFeatures P.bottomObjectProperty =
  bottomObjectPropertyFeature ∷ []
objectPropertyExpressionNonELFeatures (P.objectInverseOf p) =
  objectInverseOfFeature ∷ objectPropertyExpressionNonELFeatures p

objectPropertyExpressionsNonELFeatures :
  List P.ObjectPropertyExpression → List NonELFeature
objectPropertyExpressionsNonELFeatures =
  concatMap objectPropertyExpressionNonELFeatures

objectPropertyExpressionTwoOrMoreNonELFeatures :
  P.TwoOrMore P.ObjectPropertyExpression → List NonELFeature
objectPropertyExpressionTwoOrMoreNonELFeatures ps =
  objectPropertyExpressionNonELFeatures (P.first ps)
  ++
  objectPropertyExpressionNonELFeatures (P.second ps)
  ++
  objectPropertyExpressionsNonELFeatures (P.rest ps)

objectPropertyChainNonELFeatures :
  P.ObjectPropertyChain → List NonELFeature
objectPropertyChainNonELFeatures (P.objectPropertyChain ps) =
  objectPropertyExpressionTwoOrMoreNonELFeatures ps

subObjectPropertyExpressionNonELFeatures :
  P.SubObjectPropertyExpression → List NonELFeature
subObjectPropertyExpressionNonELFeatures (P.subObjectProperty p) =
  objectPropertyExpressionNonELFeatures p
subObjectPropertyExpressionNonELFeatures (P.subObjectPropertyChain chain) =
  objectPropertyChainNonELFeatures chain

dataPropertyExpressionNonELFeatures :
  P.DataPropertyExpression → List NonELFeature
dataPropertyExpressionNonELFeatures (P.dataProperty p) =
  []
dataPropertyExpressionNonELFeatures P.topDataProperty =
  topDataPropertyFeature ∷ []
dataPropertyExpressionNonELFeatures P.bottomDataProperty =
  bottomDataPropertyFeature ∷ []

dataPropertyExpressionsNonELFeatures :
  List P.DataPropertyExpression → List NonELFeature
dataPropertyExpressionsNonELFeatures =
  concatMap dataPropertyExpressionNonELFeatures

dataPropertyExpressionTwoOrMoreNonELFeatures :
  P.TwoOrMore P.DataPropertyExpression → List NonELFeature
dataPropertyExpressionTwoOrMoreNonELFeatures ps =
  dataPropertyExpressionNonELFeatures (P.first ps)
  ++
  dataPropertyExpressionNonELFeatures (P.second ps)
  ++
  dataPropertyExpressionsNonELFeatures (P.rest ps)

mutual
  dataRangeNonELFeatures : P.DataRange → List NonELFeature
  dataRangeNonELFeatures (P.datatype d) =
    []
  dataRangeNonELFeatures P.dataTop =
    []
  dataRangeNonELFeatures P.dataBottom =
    []
  dataRangeNonELFeatures (P.dataComplementOf d) =
    dataComplementOfFeature ∷ dataRangeNonELFeatures d
  dataRangeNonELFeatures (P.dataIntersectionOf ds) =
    dataIntersectionOfFeature ∷ dataRangeTwoOrMoreNonELFeatures ds
  dataRangeNonELFeatures (P.dataUnionOf ds) =
    dataUnionOfFeature ∷ dataRangeTwoOrMoreNonELFeatures ds
  dataRangeNonELFeatures (P.dataOneOf xs) =
    dataOneOfFeature ∷ []
  dataRangeNonELFeatures (P.datatypeRestriction d restrictions) =
    datatypeRestrictionFeature ∷ []

  dataRangesNonELFeatures : List P.DataRange → List NonELFeature
  dataRangesNonELFeatures [] =
    []
  dataRangesNonELFeatures (d ∷ ds) =
    dataRangeNonELFeatures d ++ dataRangesNonELFeatures ds

  dataRangeTwoOrMoreNonELFeatures :
    P.TwoOrMore P.DataRange → List NonELFeature
  dataRangeTwoOrMoreNonELFeatures ds =
    dataRangeNonELFeatures (P.first ds)
    ++
    dataRangeNonELFeatures (P.second ds)
    ++
    dataRangesNonELFeatures (P.rest ds)

  optionalDataRangeNonELFeatures :
    Optional P.DataRange → List NonELFeature
  optionalDataRangeNonELFeatures absent =
    []
  optionalDataRangeNonELFeatures (present d) =
    dataRangeNonELFeatures d

mutual
  classExpressionNonELFeatures :
    P.ClassExpression → List NonELFeature
  classExpressionNonELFeatures (P.namedClass c) =
    []
  classExpressionNonELFeatures P.owlThing =
    []
  classExpressionNonELFeatures P.owlNothing =
    []
  classExpressionNonELFeatures (P.objectIntersectionOf cs) =
    classExpressionTwoOrMoreNonELFeatures cs
  classExpressionNonELFeatures (P.objectUnionOf cs) =
    objectUnionOfFeature ∷ classExpressionTwoOrMoreNonELFeatures cs
  classExpressionNonELFeatures (P.objectComplementOf c) =
    objectComplementOfFeature ∷ classExpressionNonELFeatures c
  classExpressionNonELFeatures (P.objectOneOf xs) =
    objectOneOfFeature ∷ []
  classExpressionNonELFeatures (P.objectSomeValuesFrom p c) =
    objectPropertyExpressionNonELFeatures p
    ++
    classExpressionNonELFeatures c
  classExpressionNonELFeatures (P.objectAllValuesFrom p c) =
    objectAllValuesFromFeature
    ∷
    objectPropertyExpressionNonELFeatures p
    ++
    classExpressionNonELFeatures c
  classExpressionNonELFeatures (P.objectHasValue p x) =
    objectPropertyExpressionNonELFeatures p
  classExpressionNonELFeatures (P.objectHasSelf p) =
    objectHasSelfFeature ∷ objectPropertyExpressionNonELFeatures p
  classExpressionNonELFeatures (P.objectMinCardinality n p c) =
    objectMinCardinalityFeature
    ∷
    objectPropertyExpressionNonELFeatures p
    ++
    optionalClassExpressionNonELFeatures c
  classExpressionNonELFeatures (P.objectMaxCardinality n p c) =
    objectMaxCardinalityFeature
    ∷
    objectPropertyExpressionNonELFeatures p
    ++
    optionalClassExpressionNonELFeatures c
  classExpressionNonELFeatures (P.objectExactCardinality n p c) =
    objectExactCardinalityFeature
    ∷
    objectPropertyExpressionNonELFeatures p
    ++
    optionalClassExpressionNonELFeatures c
  classExpressionNonELFeatures (P.dataSomeValuesFrom p d) =
    dataSomeValuesFromFeature
    ∷
    dataPropertyExpressionNonELFeatures p
    ++
    dataRangeNonELFeatures d
  classExpressionNonELFeatures (P.dataAllValuesFrom p d) =
    dataAllValuesFromFeature
    ∷
    dataPropertyExpressionNonELFeatures p
    ++
    dataRangeNonELFeatures d
  classExpressionNonELFeatures (P.dataHasValue p literal) =
    dataHasValueFeature ∷ dataPropertyExpressionNonELFeatures p
  classExpressionNonELFeatures (P.dataMinCardinality n p d) =
    dataMinCardinalityFeature
    ∷
    dataPropertyExpressionNonELFeatures p
    ++
    optionalDataRangeNonELFeatures d
  classExpressionNonELFeatures (P.dataMaxCardinality n p d) =
    dataMaxCardinalityFeature
    ∷
    dataPropertyExpressionNonELFeatures p
    ++
    optionalDataRangeNonELFeatures d
  classExpressionNonELFeatures (P.dataExactCardinality n p d) =
    dataExactCardinalityFeature
    ∷
    dataPropertyExpressionNonELFeatures p
    ++
    optionalDataRangeNonELFeatures d

  classExpressionsNonELFeatures :
    List P.ClassExpression → List NonELFeature
  classExpressionsNonELFeatures [] =
    []
  classExpressionsNonELFeatures (c ∷ cs) =
    classExpressionNonELFeatures c ++ classExpressionsNonELFeatures cs

  classExpressionTwoOrMoreNonELFeatures :
    P.TwoOrMore P.ClassExpression → List NonELFeature
  classExpressionTwoOrMoreNonELFeatures cs =
    classExpressionNonELFeatures (P.first cs)
    ++
    classExpressionNonELFeatures (P.second cs)
    ++
    classExpressionsNonELFeatures (P.rest cs)

  optionalClassExpressionNonELFeatures :
    Optional P.ClassExpression → List NonELFeature
  optionalClassExpressionNonELFeatures absent =
    []
  optionalClassExpressionNonELFeatures (present c) =
    classExpressionNonELFeatures c

propertyKeyNonELFeatures : P.PropertyKey → List NonELFeature
propertyKeyNonELFeatures key =
  objectPropertyExpressionsNonELFeatures (P.objectProperties key)
  ++
  dataPropertyExpressionsNonELFeatures (P.dataProperties key)

axiomNonELFeatures : P.Axiom → List NonELFeature
axiomNonELFeatures (P.declaration e) =
  []
axiomNonELFeatures (P.subClassOf c d) =
  classExpressionNonELFeatures c ++ classExpressionNonELFeatures d
axiomNonELFeatures (P.equivalentClasses cs) =
  classExpressionTwoOrMoreNonELFeatures cs
axiomNonELFeatures (P.disjointClasses cs) =
  disjointClassesAxiomFeature
  ∷ classExpressionTwoOrMoreNonELFeatures cs
axiomNonELFeatures (P.disjointUnion c cs) =
  disjointUnionAxiomFeature
  ∷ classExpressionTwoOrMoreNonELFeatures cs
axiomNonELFeatures (P.subObjectPropertyOf p q) =
  subObjectPropertyExpressionNonELFeatures p
  ++
  objectPropertyExpressionNonELFeatures q
axiomNonELFeatures (P.equivalentObjectProperties ps) =
  equivalentObjectPropertiesAxiomFeature
  ∷ objectPropertyExpressionTwoOrMoreNonELFeatures ps
axiomNonELFeatures (P.disjointObjectProperties ps) =
  disjointObjectPropertiesAxiomFeature
  ∷ objectPropertyExpressionTwoOrMoreNonELFeatures ps
axiomNonELFeatures (P.inverseObjectProperties p q) =
  inverseObjectPropertiesAxiomFeature
  ∷
  objectPropertyExpressionNonELFeatures p
  ++
  objectPropertyExpressionNonELFeatures q
axiomNonELFeatures (P.objectPropertyDomain p c) =
  objectPropertyExpressionNonELFeatures p
  ++
  classExpressionNonELFeatures c
axiomNonELFeatures (P.objectPropertyRange p c) =
  objectPropertyExpressionNonELFeatures p
  ++
  classExpressionNonELFeatures c
axiomNonELFeatures (P.functionalObjectProperty p) =
  functionalObjectPropertyAxiomFeature
  ∷ objectPropertyExpressionNonELFeatures p
axiomNonELFeatures (P.inverseFunctionalObjectProperty p) =
  inverseFunctionalObjectPropertyAxiomFeature
  ∷ objectPropertyExpressionNonELFeatures p
axiomNonELFeatures (P.reflexiveObjectProperty p) =
  reflexiveObjectPropertyAxiomFeature
  ∷ objectPropertyExpressionNonELFeatures p
axiomNonELFeatures (P.irreflexiveObjectProperty p) =
  irreflexiveObjectPropertyAxiomFeature
  ∷ objectPropertyExpressionNonELFeatures p
axiomNonELFeatures (P.symmetricObjectProperty p) =
  symmetricObjectPropertyAxiomFeature
  ∷ objectPropertyExpressionNonELFeatures p
axiomNonELFeatures (P.asymmetricObjectProperty p) =
  asymmetricObjectPropertyAxiomFeature
  ∷ objectPropertyExpressionNonELFeatures p
axiomNonELFeatures (P.transitiveObjectProperty p) =
  objectPropertyExpressionNonELFeatures p
axiomNonELFeatures (P.subDataPropertyOf p q) =
  subDataPropertyOfAxiomFeature
  ∷
  dataPropertyExpressionNonELFeatures p
  ++
  dataPropertyExpressionNonELFeatures q
axiomNonELFeatures (P.equivalentDataProperties ps) =
  equivalentDataPropertiesAxiomFeature
  ∷ dataPropertyExpressionTwoOrMoreNonELFeatures ps
axiomNonELFeatures (P.disjointDataProperties ps) =
  disjointDataPropertiesAxiomFeature
  ∷ dataPropertyExpressionTwoOrMoreNonELFeatures ps
axiomNonELFeatures (P.dataPropertyDomain p c) =
  dataPropertyDomainAxiomFeature
  ∷
  dataPropertyExpressionNonELFeatures p
  ++
  classExpressionNonELFeatures c
axiomNonELFeatures (P.dataPropertyRange p d) =
  dataPropertyRangeAxiomFeature
  ∷
  dataPropertyExpressionNonELFeatures p
  ++
  dataRangeNonELFeatures d
axiomNonELFeatures (P.functionalDataProperty p) =
  functionalDataPropertyAxiomFeature
  ∷ dataPropertyExpressionNonELFeatures p
axiomNonELFeatures (P.datatypeDefinition d range) =
  datatypeDefinitionAxiomFeature ∷ dataRangeNonELFeatures range
axiomNonELFeatures (P.hasKey c key) =
  hasKeyAxiomFeature
  ∷
  classExpressionNonELFeatures c
  ++
  propertyKeyNonELFeatures key
axiomNonELFeatures (P.sameIndividual xs) =
  sameIndividualAxiomFeature ∷ []
axiomNonELFeatures (P.differentIndividuals xs) =
  differentIndividualsAxiomFeature ∷ []
axiomNonELFeatures (P.classAssertion c x) =
  classExpressionNonELFeatures c
axiomNonELFeatures (P.objectPropertyAssertion p x y) =
  objectPropertyExpressionNonELFeatures p
axiomNonELFeatures (P.negativeObjectPropertyAssertion p x y) =
  negativeObjectPropertyAssertionAxiomFeature
  ∷ objectPropertyExpressionNonELFeatures p
axiomNonELFeatures (P.dataPropertyAssertion p x literal) =
  dataPropertyAssertionAxiomFeature
  ∷ dataPropertyExpressionNonELFeatures p
axiomNonELFeatures (P.negativeDataPropertyAssertion p x literal) =
  negativeDataPropertyAssertionAxiomFeature
  ∷ dataPropertyExpressionNonELFeatures p
axiomNonELFeatures (P.annotationAssertion p subject value) =
  []
axiomNonELFeatures (P.subAnnotationPropertyOf p q) =
  []
axiomNonELFeatures (P.annotationPropertyDomain p domainIRI) =
  []
axiomNonELFeatures (P.annotationPropertyRange p rangeIRI) =
  []

annotatedAxiomNonELFeatures :
  P.Annotated P.Axiom → List NonELFeature
annotatedAxiomNonELFeatures ax =
  axiomNonELFeatures (P.body ax)

annotatedAxiomsNonELFeatures :
  List (P.Annotated P.Axiom) → List NonELFeature
annotatedAxiomsNonELFeatures =
  concatMap annotatedAxiomNonELFeatures

ontologyNonELFeatures : P.Ontology → List NonELFeature
ontologyNonELFeatures ont =
  annotatedAxiomsNonELFeatures (P.axioms ont)

ontologyDocumentNonELFeatures :
  P.OntologyDocument → List NonELFeature
ontologyDocumentNonELFeatures document =
  ontologyNonELFeatures (P.documentOntology document)

record ELReport : Type₀ where
  constructor elReport
  field
    nonELFeatures : List NonELFeature

open ELReport public

classExpressionReport : P.ClassExpression → ELReport
classExpressionReport c =
  elReport (classExpressionNonELFeatures c)

axiomReport : P.Axiom → ELReport
axiomReport ax =
  elReport (axiomNonELFeatures ax)

ontologyReport : P.Ontology → ELReport
ontologyReport ont =
  elReport (ontologyNonELFeatures ont)

ontologyDocumentReport : P.OntologyDocument → ELReport
ontologyDocumentReport document =
  elReport (ontologyDocumentNonELFeatures document)

isELObjectPropertyExpression : P.ObjectPropertyExpression → Bool
isELObjectPropertyExpression p =
  isEmpty (objectPropertyExpressionNonELFeatures p)

isELDataPropertyExpression : P.DataPropertyExpression → Bool
isELDataPropertyExpression p =
  isEmpty (dataPropertyExpressionNonELFeatures p)

isELDataRange : P.DataRange → Bool
isELDataRange d =
  isEmpty (dataRangeNonELFeatures d)

isELClassExpression : P.ClassExpression → Bool
isELClassExpression c =
  isEmpty (classExpressionNonELFeatures c)

isELAxiom : P.Axiom → Bool
isELAxiom ax =
  isEmpty (axiomNonELFeatures ax)

isELAnnotatedAxiom : P.Annotated P.Axiom → Bool
isELAnnotatedAxiom ax =
  isEmpty (annotatedAxiomNonELFeatures ax)

isELOntology : P.Ontology → Bool
isELOntology ont =
  isEmpty (ontologyNonELFeatures ont)

isELDocument : P.OntologyDocument → Bool
isELDocument document =
  isEmpty (ontologyDocumentNonELFeatures document)

ELObjectPropertyExpression : P.ObjectPropertyExpression → Type₀
ELObjectPropertyExpression p =
  NoNonELFeatures (objectPropertyExpressionNonELFeatures p)

ELDataPropertyExpression : P.DataPropertyExpression → Type₀
ELDataPropertyExpression p =
  NoNonELFeatures (dataPropertyExpressionNonELFeatures p)

ELDataRange : P.DataRange → Type₀
ELDataRange d =
  NoNonELFeatures (dataRangeNonELFeatures d)

ELClassExpression : P.ClassExpression → Type₀
ELClassExpression c =
  NoNonELFeatures (classExpressionNonELFeatures c)

ELAxiom : P.Axiom → Type₀
ELAxiom ax =
  NoNonELFeatures (axiomNonELFeatures ax)

ELAnnotatedAxiom : P.Annotated P.Axiom → Type₀
ELAnnotatedAxiom ax =
  NoNonELFeatures (annotatedAxiomNonELFeatures ax)

ELOntology : P.Ontology → Type₀
ELOntology ont =
  NoNonELFeatures (ontologyNonELFeatures ont)

ELDocument : P.OntologyDocument → Type₀
ELDocument document =
  NoNonELFeatures (ontologyDocumentNonELFeatures document)