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

module OWL2.Profiles.RL 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 NonRLFeature : Type₀ where
  objectInverseOfFeature :
    NonRLFeature
  objectPropertyChainFeature :
    NonRLFeature
  topObjectPropertyFeature :
    NonRLFeature
  bottomObjectPropertyFeature :
    NonRLFeature

  topDataPropertyFeature :
    NonRLFeature
  bottomDataPropertyFeature :
    NonRLFeature

  dataComplementOfFeature :
    NonRLFeature
  dataIntersectionOfFeature :
    NonRLFeature
  dataUnionOfFeature :
    NonRLFeature
  dataOneOfFeature :
    NonRLFeature
  datatypeRestrictionFeature :
    NonRLFeature

  objectUnionOfFeature :
    NonRLFeature
  objectComplementOfFeature :
    NonRLFeature
  objectOneOfFeature :
    NonRLFeature
  objectSomeValuesFromFeature :
    NonRLFeature
  objectAllValuesFromFeature :
    NonRLFeature
  objectHasValueFeature :
    NonRLFeature
  objectHasSelfFeature :
    NonRLFeature
  objectMinCardinalityFeature :
    NonRLFeature
  objectMaxCardinalityFeature :
    NonRLFeature
  objectExactCardinalityFeature :
    NonRLFeature

  dataSomeValuesFromFeature :
    NonRLFeature
  dataAllValuesFromFeature :
    NonRLFeature
  dataHasValueFeature :
    NonRLFeature
  dataMinCardinalityFeature :
    NonRLFeature
  dataMaxCardinalityFeature :
    NonRLFeature
  dataExactCardinalityFeature :
    NonRLFeature

  disjointUnionAxiomFeature :
    NonRLFeature
  datatypeDefinitionAxiomFeature :
    NonRLFeature

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

NoNonRLFeatures : List NonRLFeature → Type₀
NoNonRLFeatures [] =
  Unit*
NoNonRLFeatures (_ ∷ _) =
  ⊥

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

objectPropertyExpressionsNonRLFeatures :
  List P.ObjectPropertyExpression → List NonRLFeature
objectPropertyExpressionsNonRLFeatures =
  concatMap objectPropertyExpressionNonRLFeatures

objectPropertyExpressionTwoOrMoreNonRLFeatures :
  P.TwoOrMore P.ObjectPropertyExpression → List NonRLFeature
objectPropertyExpressionTwoOrMoreNonRLFeatures ps =
  objectPropertyExpressionNonRLFeatures (P.first ps)
  ++
  objectPropertyExpressionNonRLFeatures (P.second ps)
  ++
  objectPropertyExpressionsNonRLFeatures (P.rest ps)

objectPropertyChainNonRLFeatures :
  P.ObjectPropertyChain → List NonRLFeature
objectPropertyChainNonRLFeatures (P.objectPropertyChain ps) =
  objectPropertyChainFeature
  ∷ objectPropertyExpressionTwoOrMoreNonRLFeatures ps

subObjectPropertyExpressionNonRLFeatures :
  P.SubObjectPropertyExpression → List NonRLFeature
subObjectPropertyExpressionNonRLFeatures (P.subObjectProperty p) =
  objectPropertyExpressionNonRLFeatures p
subObjectPropertyExpressionNonRLFeatures (P.subObjectPropertyChain chain) =
  objectPropertyChainNonRLFeatures chain

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

dataPropertyExpressionsNonRLFeatures :
  List P.DataPropertyExpression → List NonRLFeature
dataPropertyExpressionsNonRLFeatures =
  concatMap dataPropertyExpressionNonRLFeatures

dataPropertyExpressionTwoOrMoreNonRLFeatures :
  P.TwoOrMore P.DataPropertyExpression → List NonRLFeature
dataPropertyExpressionTwoOrMoreNonRLFeatures ps =
  dataPropertyExpressionNonRLFeatures (P.first ps)
  ++
  dataPropertyExpressionNonRLFeatures (P.second ps)
  ++
  dataPropertyExpressionsNonRLFeatures (P.rest ps)

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

  dataRangesNonRLFeatures : List P.DataRange → List NonRLFeature
  dataRangesNonRLFeatures [] =
    []
  dataRangesNonRLFeatures (d ∷ ds) =
    dataRangeNonRLFeatures d ++ dataRangesNonRLFeatures ds

  dataRangeTwoOrMoreNonRLFeatures :
    P.TwoOrMore P.DataRange → List NonRLFeature
  dataRangeTwoOrMoreNonRLFeatures ds =
    dataRangeNonRLFeatures (P.first ds)
    ++
    dataRangeNonRLFeatures (P.second ds)
    ++
    dataRangesNonRLFeatures (P.rest ds)

  optionalDataRangeNonRLFeatures :
    Optional P.DataRange → List NonRLFeature
  optionalDataRangeNonRLFeatures absent =
    []
  optionalDataRangeNonRLFeatures (present d) =
    dataRangeNonRLFeatures d

mutual
  classExpressionNonRLFeatures :
    P.ClassExpression → List NonRLFeature
  classExpressionNonRLFeatures (P.namedClass c) =
    []
  classExpressionNonRLFeatures P.owlThing =
    []
  classExpressionNonRLFeatures P.owlNothing =
    []
  classExpressionNonRLFeatures (P.objectIntersectionOf cs) =
    classExpressionTwoOrMoreNonRLFeatures cs
  classExpressionNonRLFeatures (P.objectUnionOf cs) =
    objectUnionOfFeature ∷ classExpressionTwoOrMoreNonRLFeatures cs
  classExpressionNonRLFeatures (P.objectComplementOf c) =
    objectComplementOfFeature ∷ classExpressionNonRLFeatures c
  classExpressionNonRLFeatures (P.objectOneOf xs) =
    objectOneOfFeature ∷ []
  classExpressionNonRLFeatures (P.objectSomeValuesFrom p c) =
    objectSomeValuesFromFeature
    ∷
    objectPropertyExpressionNonRLFeatures p
    ++
    classExpressionNonRLFeatures c
  classExpressionNonRLFeatures (P.objectAllValuesFrom p c) =
    objectAllValuesFromFeature
    ∷
    objectPropertyExpressionNonRLFeatures p
    ++
    classExpressionNonRLFeatures c
  classExpressionNonRLFeatures (P.objectHasValue p x) =
    objectHasValueFeature ∷ objectPropertyExpressionNonRLFeatures p
  classExpressionNonRLFeatures (P.objectHasSelf p) =
    objectHasSelfFeature ∷ objectPropertyExpressionNonRLFeatures p
  classExpressionNonRLFeatures (P.objectMinCardinality n p c) =
    objectMinCardinalityFeature
    ∷
    objectPropertyExpressionNonRLFeatures p
    ++
    optionalClassExpressionNonRLFeatures c
  classExpressionNonRLFeatures (P.objectMaxCardinality n p c) =
    objectMaxCardinalityFeature
    ∷
    objectPropertyExpressionNonRLFeatures p
    ++
    optionalClassExpressionNonRLFeatures c
  classExpressionNonRLFeatures (P.objectExactCardinality n p c) =
    objectExactCardinalityFeature
    ∷
    objectPropertyExpressionNonRLFeatures p
    ++
    optionalClassExpressionNonRLFeatures c
  classExpressionNonRLFeatures (P.dataSomeValuesFrom p d) =
    dataSomeValuesFromFeature
    ∷
    dataPropertyExpressionNonRLFeatures p
    ++
    dataRangeNonRLFeatures d
  classExpressionNonRLFeatures (P.dataAllValuesFrom p d) =
    dataAllValuesFromFeature
    ∷
    dataPropertyExpressionNonRLFeatures p
    ++
    dataRangeNonRLFeatures d
  classExpressionNonRLFeatures (P.dataHasValue p literal) =
    dataHasValueFeature ∷ dataPropertyExpressionNonRLFeatures p
  classExpressionNonRLFeatures (P.dataMinCardinality n p d) =
    dataMinCardinalityFeature
    ∷
    dataPropertyExpressionNonRLFeatures p
    ++
    optionalDataRangeNonRLFeatures d
  classExpressionNonRLFeatures (P.dataMaxCardinality n p d) =
    dataMaxCardinalityFeature
    ∷
    dataPropertyExpressionNonRLFeatures p
    ++
    optionalDataRangeNonRLFeatures d
  classExpressionNonRLFeatures (P.dataExactCardinality n p d) =
    dataExactCardinalityFeature
    ∷
    dataPropertyExpressionNonRLFeatures p
    ++
    optionalDataRangeNonRLFeatures d

  classExpressionsNonRLFeatures :
    List P.ClassExpression → List NonRLFeature
  classExpressionsNonRLFeatures [] =
    []
  classExpressionsNonRLFeatures (c ∷ cs) =
    classExpressionNonRLFeatures c ++ classExpressionsNonRLFeatures cs

  classExpressionTwoOrMoreNonRLFeatures :
    P.TwoOrMore P.ClassExpression → List NonRLFeature
  classExpressionTwoOrMoreNonRLFeatures cs =
    classExpressionNonRLFeatures (P.first cs)
    ++
    classExpressionNonRLFeatures (P.second cs)
    ++
    classExpressionsNonRLFeatures (P.rest cs)

  optionalClassExpressionNonRLFeatures :
    Optional P.ClassExpression → List NonRLFeature
  optionalClassExpressionNonRLFeatures absent =
    []
  optionalClassExpressionNonRLFeatures (present c) =
    classExpressionNonRLFeatures c

mutual
  subClassExpressionNonRLFeatures :
    P.ClassExpression → List NonRLFeature
  subClassExpressionNonRLFeatures (P.namedClass c) =
    []
  subClassExpressionNonRLFeatures P.owlThing =
    []
  subClassExpressionNonRLFeatures P.owlNothing =
    []
  subClassExpressionNonRLFeatures (P.objectIntersectionOf cs) =
    subClassExpressionTwoOrMoreNonRLFeatures cs
  subClassExpressionNonRLFeatures (P.objectUnionOf cs) =
    objectUnionOfFeature ∷ subClassExpressionTwoOrMoreNonRLFeatures cs
  subClassExpressionNonRLFeatures (P.objectComplementOf c) =
    objectComplementOfFeature ∷ subClassExpressionNonRLFeatures c
  subClassExpressionNonRLFeatures (P.objectOneOf xs) =
    objectOneOfFeature ∷ []
  subClassExpressionNonRLFeatures (P.objectSomeValuesFrom p c) =
    objectPropertyExpressionNonRLFeatures p
    ++
    subClassExpressionNonRLFeatures c
  subClassExpressionNonRLFeatures (P.objectAllValuesFrom p c) =
    objectAllValuesFromFeature
    ∷
    objectPropertyExpressionNonRLFeatures p
    ++
    subClassExpressionNonRLFeatures c
  subClassExpressionNonRLFeatures (P.objectHasValue p x) =
    objectPropertyExpressionNonRLFeatures p
  subClassExpressionNonRLFeatures (P.objectHasSelf p) =
    objectHasSelfFeature ∷ objectPropertyExpressionNonRLFeatures p
  subClassExpressionNonRLFeatures (P.objectMinCardinality n p c) =
    objectMinCardinalityFeature
    ∷
    objectPropertyExpressionNonRLFeatures p
    ++
    optionalSubClassExpressionNonRLFeatures c
  subClassExpressionNonRLFeatures (P.objectMaxCardinality n p c) =
    objectMaxCardinalityFeature
    ∷
    objectPropertyExpressionNonRLFeatures p
    ++
    optionalSubClassExpressionNonRLFeatures c
  subClassExpressionNonRLFeatures (P.objectExactCardinality n p c) =
    objectExactCardinalityFeature
    ∷
    objectPropertyExpressionNonRLFeatures p
    ++
    optionalSubClassExpressionNonRLFeatures c
  subClassExpressionNonRLFeatures (P.dataSomeValuesFrom p d) =
    dataPropertyExpressionNonRLFeatures p
    ++
    dataRangeNonRLFeatures d
  subClassExpressionNonRLFeatures (P.dataAllValuesFrom p d) =
    dataAllValuesFromFeature
    ∷
    dataPropertyExpressionNonRLFeatures p
    ++
    dataRangeNonRLFeatures d
  subClassExpressionNonRLFeatures (P.dataHasValue p literal) =
    dataPropertyExpressionNonRLFeatures p
  subClassExpressionNonRLFeatures (P.dataMinCardinality n p d) =
    dataMinCardinalityFeature
    ∷
    dataPropertyExpressionNonRLFeatures p
    ++
    optionalDataRangeNonRLFeatures d
  subClassExpressionNonRLFeatures (P.dataMaxCardinality n p d) =
    dataMaxCardinalityFeature
    ∷
    dataPropertyExpressionNonRLFeatures p
    ++
    optionalDataRangeNonRLFeatures d
  subClassExpressionNonRLFeatures (P.dataExactCardinality n p d) =
    dataExactCardinalityFeature
    ∷
    dataPropertyExpressionNonRLFeatures p
    ++
    optionalDataRangeNonRLFeatures d

  subClassExpressionsNonRLFeatures :
    List P.ClassExpression → List NonRLFeature
  subClassExpressionsNonRLFeatures [] =
    []
  subClassExpressionsNonRLFeatures (c ∷ cs) =
    subClassExpressionNonRLFeatures c ++ subClassExpressionsNonRLFeatures cs

  subClassExpressionTwoOrMoreNonRLFeatures :
    P.TwoOrMore P.ClassExpression → List NonRLFeature
  subClassExpressionTwoOrMoreNonRLFeatures cs =
    subClassExpressionNonRLFeatures (P.first cs)
    ++
    subClassExpressionNonRLFeatures (P.second cs)
    ++
    subClassExpressionsNonRLFeatures (P.rest cs)

  optionalSubClassExpressionNonRLFeatures :
    Optional P.ClassExpression → List NonRLFeature
  optionalSubClassExpressionNonRLFeatures absent =
    []
  optionalSubClassExpressionNonRLFeatures (present c) =
    subClassExpressionNonRLFeatures c

mutual
  superClassExpressionNonRLFeatures :
    P.ClassExpression → List NonRLFeature
  superClassExpressionNonRLFeatures (P.namedClass c) =
    []
  superClassExpressionNonRLFeatures P.owlThing =
    []
  superClassExpressionNonRLFeatures P.owlNothing =
    []
  superClassExpressionNonRLFeatures (P.objectIntersectionOf cs) =
    superClassExpressionTwoOrMoreNonRLFeatures cs
  superClassExpressionNonRLFeatures (P.objectUnionOf cs) =
    objectUnionOfFeature ∷ superClassExpressionTwoOrMoreNonRLFeatures cs
  superClassExpressionNonRLFeatures (P.objectComplementOf c) =
    objectComplementOfFeature ∷ subClassExpressionNonRLFeatures c
  superClassExpressionNonRLFeatures (P.objectOneOf xs) =
    objectOneOfFeature ∷ []
  superClassExpressionNonRLFeatures (P.objectSomeValuesFrom p c) =
    objectSomeValuesFromFeature
    ∷
    objectPropertyExpressionNonRLFeatures p
    ++
    superClassExpressionNonRLFeatures c
  superClassExpressionNonRLFeatures (P.objectAllValuesFrom p c) =
    objectPropertyExpressionNonRLFeatures p
    ++
    superClassExpressionNonRLFeatures c
  superClassExpressionNonRLFeatures (P.objectHasValue p x) =
    objectPropertyExpressionNonRLFeatures p
  superClassExpressionNonRLFeatures (P.objectHasSelf p) =
    objectHasSelfFeature ∷ objectPropertyExpressionNonRLFeatures p
  superClassExpressionNonRLFeatures (P.objectMinCardinality n p c) =
    objectMinCardinalityFeature
    ∷
    objectPropertyExpressionNonRLFeatures p
    ++
    optionalSuperClassExpressionNonRLFeatures c
  superClassExpressionNonRLFeatures (P.objectMaxCardinality n p c) =
    objectMaxCardinalityFeature
    ∷
    objectPropertyExpressionNonRLFeatures p
    ++
    optionalSuperClassExpressionNonRLFeatures c
  superClassExpressionNonRLFeatures (P.objectExactCardinality n p c) =
    objectExactCardinalityFeature
    ∷
    objectPropertyExpressionNonRLFeatures p
    ++
    optionalSuperClassExpressionNonRLFeatures c
  superClassExpressionNonRLFeatures (P.dataSomeValuesFrom p d) =
    dataSomeValuesFromFeature
    ∷
    dataPropertyExpressionNonRLFeatures p
    ++
    dataRangeNonRLFeatures d
  superClassExpressionNonRLFeatures (P.dataAllValuesFrom p d) =
    dataPropertyExpressionNonRLFeatures p
    ++
    dataRangeNonRLFeatures d
  superClassExpressionNonRLFeatures (P.dataHasValue p literal) =
    dataPropertyExpressionNonRLFeatures p
  superClassExpressionNonRLFeatures (P.dataMinCardinality n p d) =
    dataMinCardinalityFeature
    ∷
    dataPropertyExpressionNonRLFeatures p
    ++
    optionalDataRangeNonRLFeatures d
  superClassExpressionNonRLFeatures (P.dataMaxCardinality n p d) =
    dataMaxCardinalityFeature
    ∷
    dataPropertyExpressionNonRLFeatures p
    ++
    optionalDataRangeNonRLFeatures d
  superClassExpressionNonRLFeatures (P.dataExactCardinality n p d) =
    dataExactCardinalityFeature
    ∷
    dataPropertyExpressionNonRLFeatures p
    ++
    optionalDataRangeNonRLFeatures d

  superClassExpressionsNonRLFeatures :
    List P.ClassExpression → List NonRLFeature
  superClassExpressionsNonRLFeatures [] =
    []
  superClassExpressionsNonRLFeatures (c ∷ cs) =
    superClassExpressionNonRLFeatures c
    ++
    superClassExpressionsNonRLFeatures cs

  superClassExpressionTwoOrMoreNonRLFeatures :
    P.TwoOrMore P.ClassExpression → List NonRLFeature
  superClassExpressionTwoOrMoreNonRLFeatures cs =
    superClassExpressionNonRLFeatures (P.first cs)
    ++
    superClassExpressionNonRLFeatures (P.second cs)
    ++
    superClassExpressionsNonRLFeatures (P.rest cs)

  optionalSuperClassExpressionNonRLFeatures :
    Optional P.ClassExpression → List NonRLFeature
  optionalSuperClassExpressionNonRLFeatures absent =
    []
  optionalSuperClassExpressionNonRLFeatures (present c) =
    superClassExpressionNonRLFeatures c

propertyKeyNonRLFeatures : P.PropertyKey → List NonRLFeature
propertyKeyNonRLFeatures key =
  objectPropertyExpressionsNonRLFeatures (P.objectProperties key)
  ++
  dataPropertyExpressionsNonRLFeatures (P.dataProperties key)

axiomNonRLFeatures : P.Axiom → List NonRLFeature
axiomNonRLFeatures (P.declaration e) =
  []
axiomNonRLFeatures (P.subClassOf c d) =
  subClassExpressionNonRLFeatures c ++ superClassExpressionNonRLFeatures d
axiomNonRLFeatures (P.equivalentClasses cs) =
  classExpressionTwoOrMoreNonRLFeatures cs
axiomNonRLFeatures (P.disjointClasses cs) =
  classExpressionTwoOrMoreNonRLFeatures cs
axiomNonRLFeatures (P.disjointUnion c cs) =
  disjointUnionAxiomFeature
  ∷ classExpressionTwoOrMoreNonRLFeatures cs
axiomNonRLFeatures (P.subObjectPropertyOf p q) =
  subObjectPropertyExpressionNonRLFeatures p
  ++
  objectPropertyExpressionNonRLFeatures q
axiomNonRLFeatures (P.equivalentObjectProperties ps) =
  objectPropertyExpressionTwoOrMoreNonRLFeatures ps
axiomNonRLFeatures (P.disjointObjectProperties ps) =
  objectPropertyExpressionTwoOrMoreNonRLFeatures ps
axiomNonRLFeatures (P.inverseObjectProperties p q) =
  objectPropertyExpressionNonRLFeatures p
  ++
  objectPropertyExpressionNonRLFeatures q
axiomNonRLFeatures (P.objectPropertyDomain p c) =
  objectPropertyExpressionNonRLFeatures p
  ++
  superClassExpressionNonRLFeatures c
axiomNonRLFeatures (P.objectPropertyRange p c) =
  objectPropertyExpressionNonRLFeatures p
  ++
  superClassExpressionNonRLFeatures c
axiomNonRLFeatures (P.functionalObjectProperty p) =
  objectPropertyExpressionNonRLFeatures p
axiomNonRLFeatures (P.inverseFunctionalObjectProperty p) =
  objectPropertyExpressionNonRLFeatures p
axiomNonRLFeatures (P.reflexiveObjectProperty p) =
  objectPropertyExpressionNonRLFeatures p
axiomNonRLFeatures (P.irreflexiveObjectProperty p) =
  objectPropertyExpressionNonRLFeatures p
axiomNonRLFeatures (P.symmetricObjectProperty p) =
  objectPropertyExpressionNonRLFeatures p
axiomNonRLFeatures (P.asymmetricObjectProperty p) =
  objectPropertyExpressionNonRLFeatures p
axiomNonRLFeatures (P.transitiveObjectProperty p) =
  objectPropertyExpressionNonRLFeatures p
axiomNonRLFeatures (P.subDataPropertyOf p q) =
  dataPropertyExpressionNonRLFeatures p
  ++
  dataPropertyExpressionNonRLFeatures q
axiomNonRLFeatures (P.equivalentDataProperties ps) =
  dataPropertyExpressionTwoOrMoreNonRLFeatures ps
axiomNonRLFeatures (P.disjointDataProperties ps) =
  dataPropertyExpressionTwoOrMoreNonRLFeatures ps
axiomNonRLFeatures (P.dataPropertyDomain p c) =
  dataPropertyExpressionNonRLFeatures p
  ++
  superClassExpressionNonRLFeatures c
axiomNonRLFeatures (P.dataPropertyRange p d) =
  dataPropertyExpressionNonRLFeatures p
  ++
  dataRangeNonRLFeatures d
axiomNonRLFeatures (P.functionalDataProperty p) =
  dataPropertyExpressionNonRLFeatures p
axiomNonRLFeatures (P.datatypeDefinition d range) =
  datatypeDefinitionAxiomFeature ∷ dataRangeNonRLFeatures range
axiomNonRLFeatures (P.hasKey c key) =
  classExpressionNonRLFeatures c ++ propertyKeyNonRLFeatures key
axiomNonRLFeatures (P.sameIndividual xs) =
  []
axiomNonRLFeatures (P.differentIndividuals xs) =
  []
axiomNonRLFeatures (P.classAssertion c x) =
  classExpressionNonRLFeatures c
axiomNonRLFeatures (P.objectPropertyAssertion p x y) =
  objectPropertyExpressionNonRLFeatures p
axiomNonRLFeatures (P.negativeObjectPropertyAssertion p x y) =
  objectPropertyExpressionNonRLFeatures p
axiomNonRLFeatures (P.dataPropertyAssertion p x literal) =
  dataPropertyExpressionNonRLFeatures p
axiomNonRLFeatures (P.negativeDataPropertyAssertion p x literal) =
  dataPropertyExpressionNonRLFeatures p
axiomNonRLFeatures (P.annotationAssertion p subject value) =
  []
axiomNonRLFeatures (P.subAnnotationPropertyOf p q) =
  []
axiomNonRLFeatures (P.annotationPropertyDomain p domainIRI) =
  []
axiomNonRLFeatures (P.annotationPropertyRange p rangeIRI) =
  []

annotatedAxiomNonRLFeatures :
  P.Annotated P.Axiom → List NonRLFeature
annotatedAxiomNonRLFeatures ax =
  axiomNonRLFeatures (P.body ax)

annotatedAxiomsNonRLFeatures :
  List (P.Annotated P.Axiom) → List NonRLFeature
annotatedAxiomsNonRLFeatures =
  concatMap annotatedAxiomNonRLFeatures

ontologyNonRLFeatures : P.Ontology → List NonRLFeature
ontologyNonRLFeatures ont =
  annotatedAxiomsNonRLFeatures (P.axioms ont)

ontologyDocumentNonRLFeatures :
  P.OntologyDocument → List NonRLFeature
ontologyDocumentNonRLFeatures document =
  ontologyNonRLFeatures (P.documentOntology document)

record RLReport : Type₀ where
  constructor rlReport
  field
    nonRLFeatures : List NonRLFeature

open RLReport public

classExpressionReport : P.ClassExpression → RLReport
classExpressionReport c =
  rlReport (classExpressionNonRLFeatures c)

axiomReport : P.Axiom → RLReport
axiomReport ax =
  rlReport (axiomNonRLFeatures ax)

ontologyReport : P.Ontology → RLReport
ontologyReport ont =
  rlReport (ontologyNonRLFeatures ont)

ontologyDocumentReport : P.OntologyDocument → RLReport
ontologyDocumentReport document =
  rlReport (ontologyDocumentNonRLFeatures document)

isRLObjectPropertyExpression : P.ObjectPropertyExpression → Bool
isRLObjectPropertyExpression p =
  isEmpty (objectPropertyExpressionNonRLFeatures p)

isRLDataPropertyExpression : P.DataPropertyExpression → Bool
isRLDataPropertyExpression p =
  isEmpty (dataPropertyExpressionNonRLFeatures p)

isRLDataRange : P.DataRange → Bool
isRLDataRange d =
  isEmpty (dataRangeNonRLFeatures d)

isRLClassExpression : P.ClassExpression → Bool
isRLClassExpression c =
  isEmpty (classExpressionNonRLFeatures c)

isRLSubClassExpression : P.ClassExpression → Bool
isRLSubClassExpression c =
  isEmpty (subClassExpressionNonRLFeatures c)

isRLSuperClassExpression : P.ClassExpression → Bool
isRLSuperClassExpression c =
  isEmpty (superClassExpressionNonRLFeatures c)

isRLAxiom : P.Axiom → Bool
isRLAxiom ax =
  isEmpty (axiomNonRLFeatures ax)

isRLAnnotatedAxiom : P.Annotated P.Axiom → Bool
isRLAnnotatedAxiom ax =
  isEmpty (annotatedAxiomNonRLFeatures ax)

isRLOntology : P.Ontology → Bool
isRLOntology ont =
  isEmpty (ontologyNonRLFeatures ont)

isRLDocument : P.OntologyDocument → Bool
isRLDocument document =
  isEmpty (ontologyDocumentNonRLFeatures document)

RLObjectPropertyExpression : P.ObjectPropertyExpression → Type₀
RLObjectPropertyExpression p =
  NoNonRLFeatures (objectPropertyExpressionNonRLFeatures p)

RLDataPropertyExpression : P.DataPropertyExpression → Type₀
RLDataPropertyExpression p =
  NoNonRLFeatures (dataPropertyExpressionNonRLFeatures p)

RLDataRange : P.DataRange → Type₀
RLDataRange d =
  NoNonRLFeatures (dataRangeNonRLFeatures d)

RLClassExpression : P.ClassExpression → Type₀
RLClassExpression c =
  NoNonRLFeatures (classExpressionNonRLFeatures c)

RLSubClassExpression : P.ClassExpression → Type₀
RLSubClassExpression c =
  NoNonRLFeatures (subClassExpressionNonRLFeatures c)

RLSuperClassExpression : P.ClassExpression → Type₀
RLSuperClassExpression c =
  NoNonRLFeatures (superClassExpressionNonRLFeatures c)

RLAxiom : P.Axiom → Type₀
RLAxiom ax =
  NoNonRLFeatures (axiomNonRLFeatures ax)

RLAnnotatedAxiom : P.Annotated P.Axiom → Type₀
RLAnnotatedAxiom ax =
  NoNonRLFeatures (annotatedAxiomNonRLFeatures ax)

RLOntology : P.Ontology → Type₀
RLOntology ont =
  NoNonRLFeatures (ontologyNonRLFeatures ont)

RLDocument : P.OntologyDocument → Type₀
RLDocument document =
  NoNonRLFeatures (ontologyDocumentNonRLFeatures document)