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

module OWL2.Profiles.QL 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 NonQLFeature : Type₀ where
  topObjectPropertyFeature :
    NonQLFeature
  bottomObjectPropertyFeature :
    NonQLFeature
  nonSimpleObjectInverseOfFeature :
    NonQLFeature
  objectPropertyChainFeature :
    NonQLFeature

  topDataPropertyFeature :
    NonQLFeature
  bottomDataPropertyFeature :
    NonQLFeature

  dataTopFeature :
    NonQLFeature
  dataBottomFeature :
    NonQLFeature
  dataComplementOfFeature :
    NonQLFeature
  dataUnionOfFeature :
    NonQLFeature
  dataOneOfFeature :
    NonQLFeature
  datatypeRestrictionFeature :
    NonQLFeature

  objectIntersectionOfSubClassFeature :
    NonQLFeature
  objectUnionOfFeature :
    NonQLFeature
  objectComplementOfSubClassFeature :
    NonQLFeature
  objectOneOfFeature :
    NonQLFeature
  objectSomeValuesFromSubClassFillerFeature :
    NonQLFeature
  objectSomeValuesFromSuperClassFillerFeature :
    NonQLFeature
  objectAllValuesFromFeature :
    NonQLFeature
  objectHasValueFeature :
    NonQLFeature
  objectHasSelfFeature :
    NonQLFeature
  objectMinCardinalityFeature :
    NonQLFeature
  objectMaxCardinalityFeature :
    NonQLFeature
  objectExactCardinalityFeature :
    NonQLFeature

  dataAllValuesFromFeature :
    NonQLFeature
  dataHasValueFeature :
    NonQLFeature
  dataMinCardinalityFeature :
    NonQLFeature
  dataMaxCardinalityFeature :
    NonQLFeature
  dataExactCardinalityFeature :
    NonQLFeature

  disjointUnionAxiomFeature :
    NonQLFeature
  functionalObjectPropertyAxiomFeature :
    NonQLFeature
  inverseFunctionalObjectPropertyAxiomFeature :
    NonQLFeature
  irreflexiveObjectPropertyAxiomFeature :
    NonQLFeature
  transitiveObjectPropertyAxiomFeature :
    NonQLFeature
  functionalDataPropertyAxiomFeature :
    NonQLFeature
  hasKeyAxiomFeature :
    NonQLFeature
  sameIndividualAxiomFeature :
    NonQLFeature
  negativeObjectPropertyAssertionAxiomFeature :
    NonQLFeature
  negativeDataPropertyAssertionAxiomFeature :
    NonQLFeature
  nonAtomicClassAssertionFeature :
    NonQLFeature
  anonymousIndividualFeature :
    NonQLFeature

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

NoNonQLFeatures : List NonQLFeature → Type₀
NoNonQLFeatures [] =
  Unit*
NoNonQLFeatures (_ ∷ _) =
  ⊥

objectPropertyExpressionNonQLFeatures :
  P.ObjectPropertyExpression → List NonQLFeature
objectPropertyExpressionNonQLFeatures (P.objectProperty p) =
  []
objectPropertyExpressionNonQLFeatures P.topObjectProperty =
  topObjectPropertyFeature ∷ []
objectPropertyExpressionNonQLFeatures P.bottomObjectProperty =
  bottomObjectPropertyFeature ∷ []
objectPropertyExpressionNonQLFeatures (P.objectInverseOf (P.objectProperty p)) =
  []
objectPropertyExpressionNonQLFeatures (P.objectInverseOf p) =
  nonSimpleObjectInverseOfFeature
  ∷ objectPropertyExpressionNonQLFeatures p

objectPropertyExpressionsNonQLFeatures :
  List P.ObjectPropertyExpression → List NonQLFeature
objectPropertyExpressionsNonQLFeatures =
  concatMap objectPropertyExpressionNonQLFeatures

objectPropertyExpressionTwoOrMoreNonQLFeatures :
  P.TwoOrMore P.ObjectPropertyExpression → List NonQLFeature
objectPropertyExpressionTwoOrMoreNonQLFeatures ps =
  objectPropertyExpressionNonQLFeatures (P.first ps)
  ++
  objectPropertyExpressionNonQLFeatures (P.second ps)
  ++
  objectPropertyExpressionsNonQLFeatures (P.rest ps)

objectPropertyChainNonQLFeatures :
  P.ObjectPropertyChain → List NonQLFeature
objectPropertyChainNonQLFeatures (P.objectPropertyChain ps) =
  objectPropertyExpressionTwoOrMoreNonQLFeatures ps

subObjectPropertyExpressionNonQLFeatures :
  P.SubObjectPropertyExpression → List NonQLFeature
subObjectPropertyExpressionNonQLFeatures (P.subObjectProperty p) =
  objectPropertyExpressionNonQLFeatures p
subObjectPropertyExpressionNonQLFeatures (P.subObjectPropertyChain chain) =
  objectPropertyChainFeature ∷ objectPropertyChainNonQLFeatures chain

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

dataPropertyExpressionsNonQLFeatures :
  List P.DataPropertyExpression → List NonQLFeature
dataPropertyExpressionsNonQLFeatures =
  concatMap dataPropertyExpressionNonQLFeatures

dataPropertyExpressionTwoOrMoreNonQLFeatures :
  P.TwoOrMore P.DataPropertyExpression → List NonQLFeature
dataPropertyExpressionTwoOrMoreNonQLFeatures ps =
  dataPropertyExpressionNonQLFeatures (P.first ps)
  ++
  dataPropertyExpressionNonQLFeatures (P.second ps)
  ++
  dataPropertyExpressionsNonQLFeatures (P.rest ps)

mutual
  dataRangeNonQLFeatures : P.DataRange → List NonQLFeature
  dataRangeNonQLFeatures (P.datatype d) =
    []
  dataRangeNonQLFeatures P.dataTop =
    dataTopFeature ∷ []
  dataRangeNonQLFeatures P.dataBottom =
    dataBottomFeature ∷ []
  dataRangeNonQLFeatures (P.dataComplementOf d) =
    dataComplementOfFeature ∷ dataRangeNonQLFeatures d
  dataRangeNonQLFeatures (P.dataIntersectionOf ds) =
    dataRangeTwoOrMoreNonQLFeatures ds
  dataRangeNonQLFeatures (P.dataUnionOf ds) =
    dataUnionOfFeature ∷ dataRangeTwoOrMoreNonQLFeatures ds
  dataRangeNonQLFeatures (P.dataOneOf xs) =
    dataOneOfFeature ∷ []
  dataRangeNonQLFeatures (P.datatypeRestriction d restrictions) =
    datatypeRestrictionFeature ∷ []

  dataRangesNonQLFeatures : List P.DataRange → List NonQLFeature
  dataRangesNonQLFeatures [] =
    []
  dataRangesNonQLFeatures (d ∷ ds) =
    dataRangeNonQLFeatures d ++ dataRangesNonQLFeatures ds

  dataRangeTwoOrMoreNonQLFeatures :
    P.TwoOrMore P.DataRange → List NonQLFeature
  dataRangeTwoOrMoreNonQLFeatures ds =
    dataRangeNonQLFeatures (P.first ds)
    ++
    dataRangeNonQLFeatures (P.second ds)
    ++
    dataRangesNonQLFeatures (P.rest ds)

  optionalDataRangeNonQLFeatures :
    Optional P.DataRange → List NonQLFeature
  optionalDataRangeNonQLFeatures absent =
    []
  optionalDataRangeNonQLFeatures (present d) =
    dataRangeNonQLFeatures d

individualNonQLFeatures : P.Individual → List NonQLFeature
individualNonQLFeatures (P.namedIndividual x) =
  []
individualNonQLFeatures (P.anonymousIndividual x) =
  anonymousIndividualFeature ∷ []

individualsNonQLFeatures : List P.Individual → List NonQLFeature
individualsNonQLFeatures =
  concatMap individualNonQLFeatures

individualOneOrMoreNonQLFeatures :
  P.OneOrMore P.Individual → List NonQLFeature
individualOneOrMoreNonQLFeatures xs =
  individualNonQLFeatures (P.head xs)
  ++
  individualsNonQLFeatures (P.tail xs)

individualTwoOrMoreNonQLFeatures :
  P.TwoOrMore P.Individual → List NonQLFeature
individualTwoOrMoreNonQLFeatures xs =
  individualNonQLFeatures (P.first xs)
  ++
  individualNonQLFeatures (P.second xs)
  ++
  individualsNonQLFeatures (P.rest xs)

mutual
  classExpressionNonQLFeatures :
    P.ClassExpression → List NonQLFeature
  classExpressionNonQLFeatures c =
    superClassExpressionNonQLFeatures c

  subClassExpressionNonQLFeatures :
    P.ClassExpression → List NonQLFeature
  subClassExpressionNonQLFeatures (P.namedClass c) =
    []
  subClassExpressionNonQLFeatures P.owlThing =
    []
  subClassExpressionNonQLFeatures P.owlNothing =
    []
  subClassExpressionNonQLFeatures (P.objectIntersectionOf cs) =
    objectIntersectionOfSubClassFeature
    ∷ classExpressionTwoOrMoreNonQLFeatures cs
  subClassExpressionNonQLFeatures (P.objectUnionOf cs) =
    objectUnionOfFeature ∷ classExpressionTwoOrMoreNonQLFeatures cs
  subClassExpressionNonQLFeatures (P.objectComplementOf c) =
    objectComplementOfSubClassFeature ∷ classExpressionNonQLFeatures c
  subClassExpressionNonQLFeatures (P.objectOneOf xs) =
    objectOneOfFeature ∷ individualOneOrMoreNonQLFeatures xs
  subClassExpressionNonQLFeatures (P.objectSomeValuesFrom p P.owlThing) =
    objectPropertyExpressionNonQLFeatures p
  subClassExpressionNonQLFeatures (P.objectSomeValuesFrom p c) =
    objectSomeValuesFromSubClassFillerFeature
    ∷
    objectPropertyExpressionNonQLFeatures p
    ++
    classExpressionNonQLFeatures c
  subClassExpressionNonQLFeatures (P.objectAllValuesFrom p c) =
    objectAllValuesFromFeature
    ∷
    objectPropertyExpressionNonQLFeatures p
    ++
    classExpressionNonQLFeatures c
  subClassExpressionNonQLFeatures (P.objectHasValue p x) =
    objectHasValueFeature ∷ objectPropertyExpressionNonQLFeatures p
  subClassExpressionNonQLFeatures (P.objectHasSelf p) =
    objectHasSelfFeature ∷ objectPropertyExpressionNonQLFeatures p
  subClassExpressionNonQLFeatures (P.objectMinCardinality n p c) =
    objectMinCardinalityFeature
    ∷
    objectPropertyExpressionNonQLFeatures p
    ++
    optionalClassExpressionNonQLFeatures c
  subClassExpressionNonQLFeatures (P.objectMaxCardinality n p c) =
    objectMaxCardinalityFeature
    ∷
    objectPropertyExpressionNonQLFeatures p
    ++
    optionalClassExpressionNonQLFeatures c
  subClassExpressionNonQLFeatures (P.objectExactCardinality n p c) =
    objectExactCardinalityFeature
    ∷
    objectPropertyExpressionNonQLFeatures p
    ++
    optionalClassExpressionNonQLFeatures c
  subClassExpressionNonQLFeatures (P.dataSomeValuesFrom p d) =
    dataPropertyExpressionNonQLFeatures p
    ++
    dataRangeNonQLFeatures d
  subClassExpressionNonQLFeatures (P.dataAllValuesFrom p d) =
    dataAllValuesFromFeature
    ∷
    dataPropertyExpressionNonQLFeatures p
    ++
    dataRangeNonQLFeatures d
  subClassExpressionNonQLFeatures (P.dataHasValue p literal) =
    dataHasValueFeature ∷ dataPropertyExpressionNonQLFeatures p
  subClassExpressionNonQLFeatures (P.dataMinCardinality n p d) =
    dataMinCardinalityFeature
    ∷
    dataPropertyExpressionNonQLFeatures p
    ++
    optionalDataRangeNonQLFeatures d
  subClassExpressionNonQLFeatures (P.dataMaxCardinality n p d) =
    dataMaxCardinalityFeature
    ∷
    dataPropertyExpressionNonQLFeatures p
    ++
    optionalDataRangeNonQLFeatures d
  subClassExpressionNonQLFeatures (P.dataExactCardinality n p d) =
    dataExactCardinalityFeature
    ∷
    dataPropertyExpressionNonQLFeatures p
    ++
    optionalDataRangeNonQLFeatures d

  superClassExpressionNonQLFeatures :
    P.ClassExpression → List NonQLFeature
  superClassExpressionNonQLFeatures (P.namedClass c) =
    []
  superClassExpressionNonQLFeatures P.owlThing =
    []
  superClassExpressionNonQLFeatures P.owlNothing =
    []
  superClassExpressionNonQLFeatures (P.objectIntersectionOf cs) =
    superClassExpressionTwoOrMoreNonQLFeatures cs
  superClassExpressionNonQLFeatures (P.objectUnionOf cs) =
    objectUnionOfFeature ∷ classExpressionTwoOrMoreNonQLFeatures cs
  superClassExpressionNonQLFeatures (P.objectComplementOf c) =
    subClassExpressionNonQLFeatures c
  superClassExpressionNonQLFeatures (P.objectOneOf xs) =
    objectOneOfFeature ∷ individualOneOrMoreNonQLFeatures xs
  superClassExpressionNonQLFeatures (P.objectSomeValuesFrom p (P.namedClass c)) =
    objectPropertyExpressionNonQLFeatures p
  superClassExpressionNonQLFeatures (P.objectSomeValuesFrom p P.owlThing) =
    objectPropertyExpressionNonQLFeatures p
  superClassExpressionNonQLFeatures (P.objectSomeValuesFrom p P.owlNothing) =
    objectPropertyExpressionNonQLFeatures p
  superClassExpressionNonQLFeatures (P.objectSomeValuesFrom p c) =
    objectSomeValuesFromSuperClassFillerFeature
    ∷
    objectPropertyExpressionNonQLFeatures p
    ++
    classExpressionNonQLFeatures c
  superClassExpressionNonQLFeatures (P.objectAllValuesFrom p c) =
    objectAllValuesFromFeature
    ∷
    objectPropertyExpressionNonQLFeatures p
    ++
    classExpressionNonQLFeatures c
  superClassExpressionNonQLFeatures (P.objectHasValue p x) =
    objectHasValueFeature ∷ objectPropertyExpressionNonQLFeatures p
  superClassExpressionNonQLFeatures (P.objectHasSelf p) =
    objectHasSelfFeature ∷ objectPropertyExpressionNonQLFeatures p
  superClassExpressionNonQLFeatures (P.objectMinCardinality n p c) =
    objectMinCardinalityFeature
    ∷
    objectPropertyExpressionNonQLFeatures p
    ++
    optionalClassExpressionNonQLFeatures c
  superClassExpressionNonQLFeatures (P.objectMaxCardinality n p c) =
    objectMaxCardinalityFeature
    ∷
    objectPropertyExpressionNonQLFeatures p
    ++
    optionalClassExpressionNonQLFeatures c
  superClassExpressionNonQLFeatures (P.objectExactCardinality n p c) =
    objectExactCardinalityFeature
    ∷
    objectPropertyExpressionNonQLFeatures p
    ++
    optionalClassExpressionNonQLFeatures c
  superClassExpressionNonQLFeatures (P.dataSomeValuesFrom p d) =
    dataPropertyExpressionNonQLFeatures p
    ++
    dataRangeNonQLFeatures d
  superClassExpressionNonQLFeatures (P.dataAllValuesFrom p d) =
    dataAllValuesFromFeature
    ∷
    dataPropertyExpressionNonQLFeatures p
    ++
    dataRangeNonQLFeatures d
  superClassExpressionNonQLFeatures (P.dataHasValue p literal) =
    dataHasValueFeature ∷ dataPropertyExpressionNonQLFeatures p
  superClassExpressionNonQLFeatures (P.dataMinCardinality n p d) =
    dataMinCardinalityFeature
    ∷
    dataPropertyExpressionNonQLFeatures p
    ++
    optionalDataRangeNonQLFeatures d
  superClassExpressionNonQLFeatures (P.dataMaxCardinality n p d) =
    dataMaxCardinalityFeature
    ∷
    dataPropertyExpressionNonQLFeatures p
    ++
    optionalDataRangeNonQLFeatures d
  superClassExpressionNonQLFeatures (P.dataExactCardinality n p d) =
    dataExactCardinalityFeature
    ∷
    dataPropertyExpressionNonQLFeatures p
    ++
    optionalDataRangeNonQLFeatures d

  classExpressionsNonQLFeatures :
    List P.ClassExpression → List NonQLFeature
  classExpressionsNonQLFeatures [] =
    []
  classExpressionsNonQLFeatures (c ∷ cs) =
    classExpressionNonQLFeatures c ++ classExpressionsNonQLFeatures cs

  classExpressionTwoOrMoreNonQLFeatures :
    P.TwoOrMore P.ClassExpression → List NonQLFeature
  classExpressionTwoOrMoreNonQLFeatures cs =
    classExpressionNonQLFeatures (P.first cs)
    ++
    classExpressionNonQLFeatures (P.second cs)
    ++
    classExpressionsNonQLFeatures (P.rest cs)

  subClassExpressionsNonQLFeatures :
    List P.ClassExpression → List NonQLFeature
  subClassExpressionsNonQLFeatures [] =
    []
  subClassExpressionsNonQLFeatures (c ∷ cs) =
    subClassExpressionNonQLFeatures c ++ subClassExpressionsNonQLFeatures cs

  subClassExpressionTwoOrMoreNonQLFeatures :
    P.TwoOrMore P.ClassExpression → List NonQLFeature
  subClassExpressionTwoOrMoreNonQLFeatures cs =
    subClassExpressionNonQLFeatures (P.first cs)
    ++
    subClassExpressionNonQLFeatures (P.second cs)
    ++
    subClassExpressionsNonQLFeatures (P.rest cs)

  superClassExpressionsNonQLFeatures :
    List P.ClassExpression → List NonQLFeature
  superClassExpressionsNonQLFeatures [] =
    []
  superClassExpressionsNonQLFeatures (c ∷ cs) =
    superClassExpressionNonQLFeatures c ++ superClassExpressionsNonQLFeatures cs

  superClassExpressionTwoOrMoreNonQLFeatures :
    P.TwoOrMore P.ClassExpression → List NonQLFeature
  superClassExpressionTwoOrMoreNonQLFeatures cs =
    superClassExpressionNonQLFeatures (P.first cs)
    ++
    superClassExpressionNonQLFeatures (P.second cs)
    ++
    superClassExpressionsNonQLFeatures (P.rest cs)

  optionalClassExpressionNonQLFeatures :
    Optional P.ClassExpression → List NonQLFeature
  optionalClassExpressionNonQLFeatures absent =
    []
  optionalClassExpressionNonQLFeatures (present c) =
    classExpressionNonQLFeatures c

atomicClassExpressionNonQLFeatures :
  P.ClassExpression → List NonQLFeature
atomicClassExpressionNonQLFeatures (P.namedClass c) =
  []
atomicClassExpressionNonQLFeatures P.owlThing =
  []
atomicClassExpressionNonQLFeatures P.owlNothing =
  []
atomicClassExpressionNonQLFeatures c =
  nonAtomicClassAssertionFeature ∷ classExpressionNonQLFeatures c

propertyKeyNonQLFeatures : P.PropertyKey → List NonQLFeature
propertyKeyNonQLFeatures key =
  objectPropertyExpressionsNonQLFeatures (P.objectProperties key)
  ++
  dataPropertyExpressionsNonQLFeatures (P.dataProperties key)

axiomNonQLFeatures : P.Axiom → List NonQLFeature
axiomNonQLFeatures (P.declaration e) =
  []
axiomNonQLFeatures (P.subClassOf c d) =
  subClassExpressionNonQLFeatures c ++ superClassExpressionNonQLFeatures d
axiomNonQLFeatures (P.equivalentClasses cs) =
  subClassExpressionTwoOrMoreNonQLFeatures cs
axiomNonQLFeatures (P.disjointClasses cs) =
  subClassExpressionTwoOrMoreNonQLFeatures cs
axiomNonQLFeatures (P.disjointUnion c cs) =
  disjointUnionAxiomFeature
  ∷ subClassExpressionTwoOrMoreNonQLFeatures cs
axiomNonQLFeatures (P.subObjectPropertyOf p q) =
  subObjectPropertyExpressionNonQLFeatures p
  ++
  objectPropertyExpressionNonQLFeatures q
axiomNonQLFeatures (P.equivalentObjectProperties ps) =
  objectPropertyExpressionTwoOrMoreNonQLFeatures ps
axiomNonQLFeatures (P.disjointObjectProperties ps) =
  objectPropertyExpressionTwoOrMoreNonQLFeatures ps
axiomNonQLFeatures (P.inverseObjectProperties p q) =
  objectPropertyExpressionNonQLFeatures p
  ++
  objectPropertyExpressionNonQLFeatures q
axiomNonQLFeatures (P.objectPropertyDomain p c) =
  objectPropertyExpressionNonQLFeatures p
  ++
  superClassExpressionNonQLFeatures c
axiomNonQLFeatures (P.objectPropertyRange p c) =
  objectPropertyExpressionNonQLFeatures p
  ++
  superClassExpressionNonQLFeatures c
axiomNonQLFeatures (P.functionalObjectProperty p) =
  functionalObjectPropertyAxiomFeature
  ∷ objectPropertyExpressionNonQLFeatures p
axiomNonQLFeatures (P.inverseFunctionalObjectProperty p) =
  inverseFunctionalObjectPropertyAxiomFeature
  ∷ objectPropertyExpressionNonQLFeatures p
axiomNonQLFeatures (P.reflexiveObjectProperty p) =
  objectPropertyExpressionNonQLFeatures p
axiomNonQLFeatures (P.irreflexiveObjectProperty p) =
  irreflexiveObjectPropertyAxiomFeature
  ∷ objectPropertyExpressionNonQLFeatures p
axiomNonQLFeatures (P.symmetricObjectProperty p) =
  objectPropertyExpressionNonQLFeatures p
axiomNonQLFeatures (P.asymmetricObjectProperty p) =
  objectPropertyExpressionNonQLFeatures p
axiomNonQLFeatures (P.transitiveObjectProperty p) =
  transitiveObjectPropertyAxiomFeature
  ∷ objectPropertyExpressionNonQLFeatures p
axiomNonQLFeatures (P.subDataPropertyOf p q) =
  dataPropertyExpressionNonQLFeatures p
  ++
  dataPropertyExpressionNonQLFeatures q
axiomNonQLFeatures (P.equivalentDataProperties ps) =
  dataPropertyExpressionTwoOrMoreNonQLFeatures ps
axiomNonQLFeatures (P.disjointDataProperties ps) =
  dataPropertyExpressionTwoOrMoreNonQLFeatures ps
axiomNonQLFeatures (P.dataPropertyDomain p c) =
  dataPropertyExpressionNonQLFeatures p
  ++
  superClassExpressionNonQLFeatures c
axiomNonQLFeatures (P.dataPropertyRange p d) =
  dataPropertyExpressionNonQLFeatures p
  ++
  dataRangeNonQLFeatures d
axiomNonQLFeatures (P.functionalDataProperty p) =
  functionalDataPropertyAxiomFeature
  ∷ dataPropertyExpressionNonQLFeatures p
axiomNonQLFeatures (P.datatypeDefinition d range) =
  dataRangeNonQLFeatures range
axiomNonQLFeatures (P.hasKey c key) =
  hasKeyAxiomFeature
  ∷
  classExpressionNonQLFeatures c
  ++
  propertyKeyNonQLFeatures key
axiomNonQLFeatures (P.sameIndividual xs) =
  sameIndividualAxiomFeature ∷ individualTwoOrMoreNonQLFeatures xs
axiomNonQLFeatures (P.differentIndividuals xs) =
  individualTwoOrMoreNonQLFeatures xs
axiomNonQLFeatures (P.classAssertion c x) =
  atomicClassExpressionNonQLFeatures c
  ++
  individualNonQLFeatures x
axiomNonQLFeatures (P.objectPropertyAssertion p x y) =
  objectPropertyExpressionNonQLFeatures p
  ++
  individualNonQLFeatures x
  ++
  individualNonQLFeatures y
axiomNonQLFeatures (P.negativeObjectPropertyAssertion p x y) =
  negativeObjectPropertyAssertionAxiomFeature
  ∷
  objectPropertyExpressionNonQLFeatures p
  ++
  individualNonQLFeatures x
  ++
  individualNonQLFeatures y
axiomNonQLFeatures (P.dataPropertyAssertion p x literal) =
  dataPropertyExpressionNonQLFeatures p
  ++
  individualNonQLFeatures x
axiomNonQLFeatures (P.negativeDataPropertyAssertion p x literal) =
  negativeDataPropertyAssertionAxiomFeature
  ∷
  dataPropertyExpressionNonQLFeatures p
  ++
  individualNonQLFeatures x
axiomNonQLFeatures (P.annotationAssertion p subject value) =
  []
axiomNonQLFeatures (P.subAnnotationPropertyOf p q) =
  []
axiomNonQLFeatures (P.annotationPropertyDomain p domainIRI) =
  []
axiomNonQLFeatures (P.annotationPropertyRange p rangeIRI) =
  []

annotatedAxiomNonQLFeatures :
  P.Annotated P.Axiom → List NonQLFeature
annotatedAxiomNonQLFeatures ax =
  axiomNonQLFeatures (P.body ax)

annotatedAxiomsNonQLFeatures :
  List (P.Annotated P.Axiom) → List NonQLFeature
annotatedAxiomsNonQLFeatures =
  concatMap annotatedAxiomNonQLFeatures

ontologyNonQLFeatures : P.Ontology → List NonQLFeature
ontologyNonQLFeatures ont =
  annotatedAxiomsNonQLFeatures (P.axioms ont)

ontologyDocumentNonQLFeatures :
  P.OntologyDocument → List NonQLFeature
ontologyDocumentNonQLFeatures document =
  ontologyNonQLFeatures (P.documentOntology document)

record QLReport : Type₀ where
  constructor qlReport
  field
    nonQLFeatures : List NonQLFeature

open QLReport public

classExpressionReport : P.ClassExpression → QLReport
classExpressionReport c =
  qlReport (classExpressionNonQLFeatures c)

subClassExpressionReport : P.ClassExpression → QLReport
subClassExpressionReport c =
  qlReport (subClassExpressionNonQLFeatures c)

superClassExpressionReport : P.ClassExpression → QLReport
superClassExpressionReport c =
  qlReport (superClassExpressionNonQLFeatures c)

axiomReport : P.Axiom → QLReport
axiomReport ax =
  qlReport (axiomNonQLFeatures ax)

ontologyReport : P.Ontology → QLReport
ontologyReport ont =
  qlReport (ontologyNonQLFeatures ont)

ontologyDocumentReport : P.OntologyDocument → QLReport
ontologyDocumentReport document =
  qlReport (ontologyDocumentNonQLFeatures document)

isQLObjectPropertyExpression : P.ObjectPropertyExpression → Bool
isQLObjectPropertyExpression p =
  isEmpty (objectPropertyExpressionNonQLFeatures p)

isQLSubObjectPropertyExpression : P.SubObjectPropertyExpression → Bool
isQLSubObjectPropertyExpression p =
  isEmpty (subObjectPropertyExpressionNonQLFeatures p)

isQLDataPropertyExpression : P.DataPropertyExpression → Bool
isQLDataPropertyExpression p =
  isEmpty (dataPropertyExpressionNonQLFeatures p)

isQLDataRange : P.DataRange → Bool
isQLDataRange d =
  isEmpty (dataRangeNonQLFeatures d)

isQLClassExpression : P.ClassExpression → Bool
isQLClassExpression c =
  isEmpty (classExpressionNonQLFeatures c)

isQLSubClassExpression : P.ClassExpression → Bool
isQLSubClassExpression c =
  isEmpty (subClassExpressionNonQLFeatures c)

isQLSuperClassExpression : P.ClassExpression → Bool
isQLSuperClassExpression c =
  isEmpty (superClassExpressionNonQLFeatures c)

isQLAxiom : P.Axiom → Bool
isQLAxiom ax =
  isEmpty (axiomNonQLFeatures ax)

isQLAnnotatedAxiom : P.Annotated P.Axiom → Bool
isQLAnnotatedAxiom ax =
  isEmpty (annotatedAxiomNonQLFeatures ax)

isQLOntology : P.Ontology → Bool
isQLOntology ont =
  isEmpty (ontologyNonQLFeatures ont)

isQLDocument : P.OntologyDocument → Bool
isQLDocument document =
  isEmpty (ontologyDocumentNonQLFeatures document)

QLObjectPropertyExpression : P.ObjectPropertyExpression → Type₀
QLObjectPropertyExpression p =
  NoNonQLFeatures (objectPropertyExpressionNonQLFeatures p)

QLSubObjectPropertyExpression : P.SubObjectPropertyExpression → Type₀
QLSubObjectPropertyExpression p =
  NoNonQLFeatures (subObjectPropertyExpressionNonQLFeatures p)

QLDataPropertyExpression : P.DataPropertyExpression → Type₀
QLDataPropertyExpression p =
  NoNonQLFeatures (dataPropertyExpressionNonQLFeatures p)

QLDataRange : P.DataRange → Type₀
QLDataRange d =
  NoNonQLFeatures (dataRangeNonQLFeatures d)

QLClassExpression : P.ClassExpression → Type₀
QLClassExpression c =
  NoNonQLFeatures (classExpressionNonQLFeatures c)

QLSubClassExpression : P.ClassExpression → Type₀
QLSubClassExpression c =
  NoNonQLFeatures (subClassExpressionNonQLFeatures c)

QLSuperClassExpression : P.ClassExpression → Type₀
QLSuperClassExpression c =
  NoNonQLFeatures (superClassExpressionNonQLFeatures c)

QLAxiom : P.Axiom → Type₀
QLAxiom ax =
  NoNonQLFeatures (axiomNonQLFeatures ax)

QLAnnotatedAxiom : P.Annotated P.Axiom → Type₀
QLAnnotatedAxiom ax =
  NoNonQLFeatures (annotatedAxiomNonQLFeatures ax)

QLOntology : P.Ontology → Type₀
QLOntology ont =
  NoNonQLFeatures (ontologyNonQLFeatures ont)

QLDocument : P.OntologyDocument → Type₀
QLDocument document =
  NoNonQLFeatures (ontologyDocumentNonQLFeatures document)