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

module OWL2.Elab.SymbolTable where

open import OWL2.Prelude
open import OWL2.Foundation.Fin
open import OWL2.Foundation.List
open import OWL2.Raw
import OWL2.Kernel as K

sameRawIRI : RawIRI → RawIRI → Bool
sameRawIRI left right =
  primStringEquality (text left) (text right)

sameString : String → String → Bool
sameString =
  primStringEquality

lookupRawIRI : RawIRI → (iris : List RawIRI) → Optional (Fin (listCount iris))
lookupRawIRI =
  lookupFin sameRawIRI

lookupString : String → (values : List String) → Optional (Fin (listCount values))
lookupString =
  lookupFin sameString

record SymbolTable : Type₀ where
  constructor symbolTable
  field
    classIRIs :
      List RawIRI
    objectPropertyIRIs :
      List RawIRI
    dataPropertyIRIs :
      List RawIRI
    annotationPropertyIRIs :
      List RawIRI
    datatypeIRIs :
      List RawIRI
    facetIRIs :
      List RawIRI
    individualIRIs :
      List RawIRI
    annotationIRIs :
      List RawIRI
    annotationBlankNodes :
      List String
    punningPolicy :
      K.PunningPolicy

open SymbolTable public

symbolTableSignature : SymbolTable → K.Signature
symbolTableSignature table =
  K.signature
    (listCount (classIRIs table))
    (listCount (objectPropertyIRIs table))
    (listCount (dataPropertyIRIs table))
    (listCount (annotationPropertyIRIs table))
    (listCount (datatypeIRIs table))
    (listCount (facetIRIs table))
    (listCount (individualIRIs table))
    (listCount (annotationIRIs table))
    (listCount (annotationBlankNodes table))
    (punningPolicy table)

emptySymbolTable : SymbolTable
emptySymbolTable =
  symbolTable [] [] [] [] [] [] [] [] [] K.noPunning

appendSymbolTables :
  K.PunningPolicy →
  SymbolTable →
  SymbolTable →
  SymbolTable
appendSymbolTables policy left right =
  symbolTable
    (classIRIs left ++ classIRIs right)
    (objectPropertyIRIs left ++ objectPropertyIRIs right)
    (dataPropertyIRIs left ++ dataPropertyIRIs right)
    (annotationPropertyIRIs left ++ annotationPropertyIRIs right)
    (datatypeIRIs left ++ datatypeIRIs right)
    (facetIRIs left ++ facetIRIs right)
    (individualIRIs left ++ individualIRIs right)
    (annotationIRIs left ++ annotationIRIs right)
    (annotationBlankNodes left ++ annotationBlankNodes right)
    policy

leftSymbolTableMorphism :
  (policy : K.PunningPolicy) →
  (left right : SymbolTable) →
  K.SignatureMorphism
    (symbolTableSignature left)
    (symbolTableSignature (appendSymbolTables policy left right))
leftSymbolTableMorphism policy left right =
  K.signatureMorphism
    (λ name →
      K.className
        (injectLeftFin
          (classIRIs left)
          (classIRIs right)
          (K.symbol name)))
    (λ name →
      K.objectPropertyName
        (injectLeftFin
          (objectPropertyIRIs left)
          (objectPropertyIRIs right)
          (K.symbol name)))
    (λ name →
      K.dataPropertyName
        (injectLeftFin
          (dataPropertyIRIs left)
          (dataPropertyIRIs right)
          (K.symbol name)))
    (λ name →
      K.annotationPropertyName
        (injectLeftFin
          (annotationPropertyIRIs left)
          (annotationPropertyIRIs right)
          (K.symbol name)))
    (λ name →
      K.datatypeName
        (injectLeftFin
          (datatypeIRIs left)
          (datatypeIRIs right)
          (K.symbol name)))
    (λ name →
      K.facetName
        (injectLeftFin
          (facetIRIs left)
          (facetIRIs right)
          (K.symbol name)))
    (λ name →
      K.individualName
        (injectLeftFin
          (individualIRIs left)
          (individualIRIs right)
          (K.symbol name)))
    (λ name →
      K.iriName
        (injectLeftFin
          (annotationIRIs left)
          (annotationIRIs right)
          (K.symbol name)))
    (λ name →
      K.blankNodeName
        (injectLeftFin
          (annotationBlankNodes left)
          (annotationBlankNodes right)
          (K.symbol name)))
    (λ simple →
      let mapped =
            K.objectPropertyName
              (injectLeftFin
                (objectPropertyIRIs left)
                (objectPropertyIRIs right)
                (K.symbol (K.property simple)))
      in
      K.simpleObjectPropertyName
        mapped
        (K.trivialSimpleObjectProperty mapped))

rightSymbolTableMorphism :
  (policy : K.PunningPolicy) →
  (left right : SymbolTable) →
  K.SignatureMorphism
    (symbolTableSignature right)
    (symbolTableSignature (appendSymbolTables policy left right))
rightSymbolTableMorphism policy left right =
  K.signatureMorphism
    (λ name →
      K.className
        (injectRightFin
          (classIRIs left)
          (classIRIs right)
          (K.symbol name)))
    (λ name →
      K.objectPropertyName
        (injectRightFin
          (objectPropertyIRIs left)
          (objectPropertyIRIs right)
          (K.symbol name)))
    (λ name →
      K.dataPropertyName
        (injectRightFin
          (dataPropertyIRIs left)
          (dataPropertyIRIs right)
          (K.symbol name)))
    (λ name →
      K.annotationPropertyName
        (injectRightFin
          (annotationPropertyIRIs left)
          (annotationPropertyIRIs right)
          (K.symbol name)))
    (λ name →
      K.datatypeName
        (injectRightFin
          (datatypeIRIs left)
          (datatypeIRIs right)
          (K.symbol name)))
    (λ name →
      K.facetName
        (injectRightFin
          (facetIRIs left)
          (facetIRIs right)
          (K.symbol name)))
    (λ name →
      K.individualName
        (injectRightFin
          (individualIRIs left)
          (individualIRIs right)
          (K.symbol name)))
    (λ name →
      K.iriName
        (injectRightFin
          (annotationIRIs left)
          (annotationIRIs right)
          (K.symbol name)))
    (λ name →
      K.blankNodeName
        (injectRightFin
          (annotationBlankNodes left)
          (annotationBlankNodes right)
          (K.symbol name)))
    (λ simple →
      let mapped =
            K.objectPropertyName
              (injectRightFin
                (objectPropertyIRIs left)
                (objectPropertyIRIs right)
                (K.symbol (K.property simple)))
      in
      K.simpleObjectPropertyName
        mapped
        (K.trivialSimpleObjectProperty mapped))

classLookup :
  (table : SymbolTable) →
  RawIRI →
  Optional (K.ClassName (symbolTableSignature table))
classLookup table iri with lookupRawIRI iri (classIRIs table)
... | present index =
  present (K.className index)
... | absent =
  absent

objectPropertyLookup :
  (table : SymbolTable) →
  RawIRI →
  Optional (K.ObjectPropertyName (symbolTableSignature table))
objectPropertyLookup table iri with lookupRawIRI iri (objectPropertyIRIs table)
... | present index =
  present (K.objectPropertyName index)
... | absent =
  absent

dataPropertyLookup :
  (table : SymbolTable) →
  RawIRI →
  Optional (K.DataPropertyName (symbolTableSignature table))
dataPropertyLookup table iri with lookupRawIRI iri (dataPropertyIRIs table)
... | present index =
  present (K.dataPropertyName index)
... | absent =
  absent

annotationPropertyLookup :
  (table : SymbolTable) →
  RawIRI →
  Optional (K.AnnotationPropertyName (symbolTableSignature table))
annotationPropertyLookup table iri with
  lookupRawIRI iri (annotationPropertyIRIs table)
... | present index =
  present (K.annotationPropertyName index)
... | absent =
  absent

datatypeLookup :
  (table : SymbolTable) →
  RawIRI →
  Optional (K.DatatypeName (symbolTableSignature table))
datatypeLookup table iri with lookupRawIRI iri (datatypeIRIs table)
... | present index =
  present (K.datatypeName index)
... | absent =
  absent

facetLookup :
  (table : SymbolTable) →
  RawIRI →
  Optional (K.FacetName (symbolTableSignature table))
facetLookup table iri with lookupRawIRI iri (facetIRIs table)
... | present index =
  present (K.facetName index)
... | absent =
  absent

individualLookup :
  (table : SymbolTable) →
  RawIRI →
  Optional (K.IndividualName (symbolTableSignature table))
individualLookup table iri with lookupRawIRI iri (individualIRIs table)
... | present index =
  present (K.individualName index)
... | absent =
  absent

annotationIRILookup :
  (table : SymbolTable) →
  RawIRI →
  Optional (K.IRIName (symbolTableSignature table))
annotationIRILookup table iri with lookupRawIRI iri (annotationIRIs table)
... | present index =
  present (K.iriName index)
... | absent =
  absent

annotationBlankNodeLookup :
  (table : SymbolTable) →
  String →
  Optional (K.BlankNodeName (symbolTableSignature table))
annotationBlankNodeLookup table name with
  lookupString name (annotationBlankNodes table)
... | present index =
  present (K.blankNodeName index)
... | absent =
  absent

entityClassIRIs : RawEntity → List RawIRI
entityClassIRIs entity with kind entity
... | rawClass =
  iri entity ∷ []
... | rawObjectProperty =
  []
... | rawDataProperty =
  []
... | rawDatatype =
  []
... | rawIndividual =
  []
... | rawAnnotationProperty =
  []
... | rawUnknownEntityKind =
  []

entityObjectPropertyIRIs : RawEntity → List RawIRI
entityObjectPropertyIRIs entity with kind entity
... | rawClass =
  []
... | rawObjectProperty =
  iri entity ∷ []
... | rawDataProperty =
  []
... | rawDatatype =
  []
... | rawIndividual =
  []
... | rawAnnotationProperty =
  []
... | rawUnknownEntityKind =
  []

entityDataPropertyIRIs : RawEntity → List RawIRI
entityDataPropertyIRIs entity with kind entity
... | rawClass =
  []
... | rawObjectProperty =
  []
... | rawDataProperty =
  iri entity ∷ []
... | rawDatatype =
  []
... | rawIndividual =
  []
... | rawAnnotationProperty =
  []
... | rawUnknownEntityKind =
  []

entityAnnotationPropertyIRIs : RawEntity → List RawIRI
entityAnnotationPropertyIRIs entity with kind entity
... | rawClass =
  []
... | rawObjectProperty =
  []
... | rawDataProperty =
  []
... | rawDatatype =
  []
... | rawIndividual =
  []
... | rawAnnotationProperty =
  iri entity ∷ []
... | rawUnknownEntityKind =
  []

entityDatatypeIRIs : RawEntity → List RawIRI
entityDatatypeIRIs entity with kind entity
... | rawClass =
  []
... | rawObjectProperty =
  []
... | rawDataProperty =
  []
... | rawDatatype =
  iri entity ∷ []
... | rawIndividual =
  []
... | rawAnnotationProperty =
  []
... | rawUnknownEntityKind =
  []

entityIndividualIRIs : RawEntity → List RawIRI
entityIndividualIRIs entity with kind entity
... | rawClass =
  []
... | rawObjectProperty =
  []
... | rawDataProperty =
  []
... | rawDatatype =
  []
... | rawIndividual =
  iri entity ∷ []
... | rawAnnotationProperty =
  []
... | rawUnknownEntityKind =
  []

axiomEntity : RawAxiom → Optional RawEntity
axiomEntity (rawDeclaration entity) =
  present entity
axiomEntity (rawSubClassOf sub sup) =
  absent
axiomEntity (rawEquivalentClasses classes) =
  absent
axiomEntity (rawDisjointClasses classes) =
  absent
axiomEntity (rawDisjointUnion class classes) =
  absent
axiomEntity (rawSubObjectPropertyOf sub sup) =
  absent
axiomEntity (rawEquivalentObjectProperties properties) =
  absent
axiomEntity (rawDisjointObjectProperties properties) =
  absent
axiomEntity (rawInverseObjectProperties left right) =
  absent
axiomEntity (rawObjectPropertyDomain property class) =
  absent
axiomEntity (rawObjectPropertyRange property class) =
  absent
axiomEntity (rawFunctionalObjectProperty property) =
  absent
axiomEntity (rawInverseFunctionalObjectProperty property) =
  absent
axiomEntity (rawReflexiveObjectProperty property) =
  absent
axiomEntity (rawIrreflexiveObjectProperty property) =
  absent
axiomEntity (rawSymmetricObjectProperty property) =
  absent
axiomEntity (rawAsymmetricObjectProperty property) =
  absent
axiomEntity (rawTransitiveObjectProperty property) =
  absent
axiomEntity (rawSubDataPropertyOf sub sup) =
  absent
axiomEntity (rawEquivalentDataProperties properties) =
  absent
axiomEntity (rawDisjointDataProperties properties) =
  absent
axiomEntity (rawDataPropertyDomain property class) =
  absent
axiomEntity (rawDataPropertyRange property range) =
  absent
axiomEntity (rawFunctionalDataProperty property) =
  absent
axiomEntity (rawDatatypeDefinition datatype range) =
  absent
axiomEntity (rawHasKey class objectProperties dataProperties) =
  absent
axiomEntity (rawSameIndividual individuals) =
  absent
axiomEntity (rawDifferentIndividuals individuals) =
  absent
axiomEntity (rawClassAssertion class individual) =
  absent
axiomEntity (rawObjectPropertyAssertion property subject object) =
  absent
axiomEntity (rawNegativeObjectPropertyAssertion property subject object) =
  absent
axiomEntity (rawDataPropertyAssertion property subject literal) =
  absent
axiomEntity (rawNegativeDataPropertyAssertion property subject literal) =
  absent
axiomEntity (rawAnnotationAssertion property subject value) =
  absent
axiomEntity (rawSubAnnotationPropertyOf sub sup) =
  absent
axiomEntity (rawAnnotationPropertyDomain property iri) =
  absent
axiomEntity (rawAnnotationPropertyRange property iri) =
  absent
axiomEntity (rawUnsupportedAxiom reason) =
  absent

annotatedEntity : RawAnnotated RawAxiom → Optional RawEntity
annotatedEntity axiom =
  axiomEntity (body axiom)

rawAnnotationValueIRIs : RawAnnotationValue → List RawIRI
rawAnnotationValueIRIs (rawAnnotationValueIRI iri) =
  iri ∷ []
rawAnnotationValueIRIs (rawAnnotationValueAnonymous name) =
  []
rawAnnotationValueIRIs (rawAnnotationValueLiteral literal) =
  []

rawAnnotationSubjectIRIs : RawAnnotationSubject → List RawIRI
rawAnnotationSubjectIRIs (rawAnnotationSubjectIRI iri) =
  iri ∷ []
rawAnnotationSubjectIRIs (rawAnnotationSubjectAnonymous name) =
  []

mutual
  rawAnnotationIRIs : RawAnnotation → List RawIRI
  rawAnnotationIRIs (rawAnnotation annotations property value) =
    rawAnnotationsIRIs annotations ++ rawAnnotationValueIRIs value

  rawAnnotationsIRIs : List RawAnnotation → List RawIRI
  rawAnnotationsIRIs [] =
    []
  rawAnnotationsIRIs (annotation ∷ annotations) =
    rawAnnotationIRIs annotation ++ rawAnnotationsIRIs annotations

rawAnnotationValueBlankNodes : RawAnnotationValue → List String
rawAnnotationValueBlankNodes (rawAnnotationValueIRI iri) =
  []
rawAnnotationValueBlankNodes (rawAnnotationValueAnonymous name) =
  name ∷ []
rawAnnotationValueBlankNodes (rawAnnotationValueLiteral literal) =
  []

rawAnnotationSubjectBlankNodes : RawAnnotationSubject → List String
rawAnnotationSubjectBlankNodes (rawAnnotationSubjectIRI iri) =
  []
rawAnnotationSubjectBlankNodes (rawAnnotationSubjectAnonymous name) =
  name ∷ []

mutual
  rawAnnotationBlankNodes : RawAnnotation → List String
  rawAnnotationBlankNodes (rawAnnotation annotations property value) =
    rawAnnotationsBlankNodes annotations ++ rawAnnotationValueBlankNodes value

  rawAnnotationsBlankNodes : List RawAnnotation → List String
  rawAnnotationsBlankNodes [] =
    []
  rawAnnotationsBlankNodes (annotation ∷ annotations) =
    rawAnnotationBlankNodes annotation ++ rawAnnotationsBlankNodes annotations

rawFacetRestrictionIRIs : RawFacetRestriction → List RawIRI
rawFacetRestrictionIRIs restriction =
  facet restriction ∷ []

rawFacetRestrictionsIRIs : List RawFacetRestriction → List RawIRI
rawFacetRestrictionsIRIs [] =
  []
rawFacetRestrictionsIRIs (restriction ∷ restrictions) =
  rawFacetRestrictionIRIs restriction ++ rawFacetRestrictionsIRIs restrictions

mutual
  rawDataRangeFacetIRIs : RawDataRange → List RawIRI
  rawDataRangeFacetIRIs (rawDatatype iri) =
    []
  rawDataRangeFacetIRIs (rawDatatypeRestriction iri restrictions) =
    rawFacetRestrictionsIRIs restrictions
  rawDataRangeFacetIRIs rawDataTop =
    []
  rawDataRangeFacetIRIs rawDataBottom =
    []
  rawDataRangeFacetIRIs (rawDataComplementOf range) =
    rawDataRangeFacetIRIs range
  rawDataRangeFacetIRIs (rawDataIntersectionOf ranges) =
    rawDataRangesFacetIRIs ranges
  rawDataRangeFacetIRIs (rawDataUnionOf ranges) =
    rawDataRangesFacetIRIs ranges
  rawDataRangeFacetIRIs (rawDataOneOf literals) =
    []

  rawDataRangesFacetIRIs : List RawDataRange → List RawIRI
  rawDataRangesFacetIRIs [] =
    []
  rawDataRangesFacetIRIs (range ∷ ranges) =
    rawDataRangeFacetIRIs range ++ rawDataRangesFacetIRIs ranges

  optionalRawDataRangeFacetIRIs : Optional RawDataRange → List RawIRI
  optionalRawDataRangeFacetIRIs absent =
    []
  optionalRawDataRangeFacetIRIs (present range) =
    rawDataRangeFacetIRIs range

  rawClassExpressionFacetIRIs : RawClassExpression → List RawIRI
  rawClassExpressionFacetIRIs (rawNamedClass iri) =
    []
  rawClassExpressionFacetIRIs rawOwlThing =
    []
  rawClassExpressionFacetIRIs rawOwlNothing =
    []
  rawClassExpressionFacetIRIs (rawObjectIntersectionOf classes) =
    rawClassExpressionsFacetIRIs classes
  rawClassExpressionFacetIRIs (rawObjectUnionOf classes) =
    rawClassExpressionsFacetIRIs classes
  rawClassExpressionFacetIRIs (rawObjectComplementOf class) =
    rawClassExpressionFacetIRIs class
  rawClassExpressionFacetIRIs (rawObjectOneOf individuals) =
    []
  rawClassExpressionFacetIRIs (rawObjectSomeValuesFrom property class) =
    rawClassExpressionFacetIRIs class
  rawClassExpressionFacetIRIs (rawObjectAllValuesFrom property class) =
    rawClassExpressionFacetIRIs class
  rawClassExpressionFacetIRIs (rawObjectHasValue property individual) =
    []
  rawClassExpressionFacetIRIs (rawObjectHasSelf property) =
    []
  rawClassExpressionFacetIRIs
    (rawObjectMinCardinality n property class) =
    optionalRawClassExpressionFacetIRIs class
  rawClassExpressionFacetIRIs
    (rawObjectMaxCardinality n property class) =
    optionalRawClassExpressionFacetIRIs class
  rawClassExpressionFacetIRIs
    (rawObjectExactCardinality n property class) =
    optionalRawClassExpressionFacetIRIs class
  rawClassExpressionFacetIRIs (rawDataSomeValuesFrom property range) =
    rawDataRangeFacetIRIs range
  rawClassExpressionFacetIRIs (rawDataAllValuesFrom property range) =
    rawDataRangeFacetIRIs range
  rawClassExpressionFacetIRIs (rawDataHasValue property literal) =
    []
  rawClassExpressionFacetIRIs (rawDataMinCardinality n property range) =
    optionalRawDataRangeFacetIRIs range
  rawClassExpressionFacetIRIs (rawDataMaxCardinality n property range) =
    optionalRawDataRangeFacetIRIs range
  rawClassExpressionFacetIRIs (rawDataExactCardinality n property range) =
    optionalRawDataRangeFacetIRIs range

  rawClassExpressionsFacetIRIs : List RawClassExpression → List RawIRI
  rawClassExpressionsFacetIRIs [] =
    []
  rawClassExpressionsFacetIRIs (class ∷ classes) =
    rawClassExpressionFacetIRIs class ++
    rawClassExpressionsFacetIRIs classes

  optionalRawClassExpressionFacetIRIs :
    Optional RawClassExpression → List RawIRI
  optionalRawClassExpressionFacetIRIs absent =
    []
  optionalRawClassExpressionFacetIRIs (present class) =
    rawClassExpressionFacetIRIs class

axiomFacetIRIs : RawAxiom → List RawIRI
axiomFacetIRIs (rawDeclaration entity) =
  []
axiomFacetIRIs (rawSubClassOf sub sup) =
  rawClassExpressionFacetIRIs sub ++ rawClassExpressionFacetIRIs sup
axiomFacetIRIs (rawEquivalentClasses classes) =
  rawClassExpressionsFacetIRIs classes
axiomFacetIRIs (rawDisjointClasses classes) =
  rawClassExpressionsFacetIRIs classes
axiomFacetIRIs (rawDisjointUnion class classes) =
  rawClassExpressionsFacetIRIs classes
axiomFacetIRIs (rawSubObjectPropertyOf sub sup) =
  []
axiomFacetIRIs (rawEquivalentObjectProperties properties) =
  []
axiomFacetIRIs (rawDisjointObjectProperties properties) =
  []
axiomFacetIRIs (rawInverseObjectProperties left right) =
  []
axiomFacetIRIs (rawObjectPropertyDomain property class) =
  rawClassExpressionFacetIRIs class
axiomFacetIRIs (rawObjectPropertyRange property class) =
  rawClassExpressionFacetIRIs class
axiomFacetIRIs (rawFunctionalObjectProperty property) =
  []
axiomFacetIRIs (rawInverseFunctionalObjectProperty property) =
  []
axiomFacetIRIs (rawReflexiveObjectProperty property) =
  []
axiomFacetIRIs (rawIrreflexiveObjectProperty property) =
  []
axiomFacetIRIs (rawSymmetricObjectProperty property) =
  []
axiomFacetIRIs (rawAsymmetricObjectProperty property) =
  []
axiomFacetIRIs (rawTransitiveObjectProperty property) =
  []
axiomFacetIRIs (rawSubDataPropertyOf sub sup) =
  []
axiomFacetIRIs (rawEquivalentDataProperties properties) =
  []
axiomFacetIRIs (rawDisjointDataProperties properties) =
  []
axiomFacetIRIs (rawDataPropertyDomain property class) =
  rawClassExpressionFacetIRIs class
axiomFacetIRIs (rawDataPropertyRange property range) =
  rawDataRangeFacetIRIs range
axiomFacetIRIs (rawFunctionalDataProperty property) =
  []
axiomFacetIRIs (rawDatatypeDefinition datatype range) =
  rawDataRangeFacetIRIs range
axiomFacetIRIs (rawHasKey class objectProperties dataProperties) =
  rawClassExpressionFacetIRIs class
axiomFacetIRIs (rawSameIndividual individuals) =
  []
axiomFacetIRIs (rawDifferentIndividuals individuals) =
  []
axiomFacetIRIs (rawClassAssertion class individual) =
  rawClassExpressionFacetIRIs class
axiomFacetIRIs (rawObjectPropertyAssertion property subject object) =
  []
axiomFacetIRIs (rawNegativeObjectPropertyAssertion property subject object) =
  []
axiomFacetIRIs (rawDataPropertyAssertion property subject literal) =
  []
axiomFacetIRIs (rawNegativeDataPropertyAssertion property subject literal) =
  []
axiomFacetIRIs (rawAnnotationAssertion property subject value) =
  []
axiomFacetIRIs (rawSubAnnotationPropertyOf sub sup) =
  []
axiomFacetIRIs (rawAnnotationPropertyDomain property iri) =
  []
axiomFacetIRIs (rawAnnotationPropertyRange property iri) =
  []
axiomFacetIRIs (rawUnsupportedAxiom reason) =
  []

axiomAnnotationIRIs : RawAxiom → List RawIRI
axiomAnnotationIRIs (rawDeclaration entity) =
  []
axiomAnnotationIRIs (rawSubClassOf sub sup) =
  []
axiomAnnotationIRIs (rawEquivalentClasses classes) =
  []
axiomAnnotationIRIs (rawDisjointClasses classes) =
  []
axiomAnnotationIRIs (rawDisjointUnion class classes) =
  []
axiomAnnotationIRIs (rawSubObjectPropertyOf sub sup) =
  []
axiomAnnotationIRIs (rawEquivalentObjectProperties properties) =
  []
axiomAnnotationIRIs (rawDisjointObjectProperties properties) =
  []
axiomAnnotationIRIs (rawInverseObjectProperties left right) =
  []
axiomAnnotationIRIs (rawObjectPropertyDomain property class) =
  []
axiomAnnotationIRIs (rawObjectPropertyRange property class) =
  []
axiomAnnotationIRIs (rawFunctionalObjectProperty property) =
  []
axiomAnnotationIRIs (rawInverseFunctionalObjectProperty property) =
  []
axiomAnnotationIRIs (rawReflexiveObjectProperty property) =
  []
axiomAnnotationIRIs (rawIrreflexiveObjectProperty property) =
  []
axiomAnnotationIRIs (rawSymmetricObjectProperty property) =
  []
axiomAnnotationIRIs (rawAsymmetricObjectProperty property) =
  []
axiomAnnotationIRIs (rawTransitiveObjectProperty property) =
  []
axiomAnnotationIRIs (rawSubDataPropertyOf sub sup) =
  []
axiomAnnotationIRIs (rawEquivalentDataProperties properties) =
  []
axiomAnnotationIRIs (rawDisjointDataProperties properties) =
  []
axiomAnnotationIRIs (rawDataPropertyDomain property class) =
  []
axiomAnnotationIRIs (rawDataPropertyRange property range) =
  []
axiomAnnotationIRIs (rawFunctionalDataProperty property) =
  []
axiomAnnotationIRIs (rawDatatypeDefinition datatype range) =
  []
axiomAnnotationIRIs (rawHasKey class objectProperties dataProperties) =
  []
axiomAnnotationIRIs (rawSameIndividual individuals) =
  []
axiomAnnotationIRIs (rawDifferentIndividuals individuals) =
  []
axiomAnnotationIRIs (rawClassAssertion class individual) =
  []
axiomAnnotationIRIs (rawObjectPropertyAssertion property subject object) =
  []
axiomAnnotationIRIs (rawNegativeObjectPropertyAssertion property subject object) =
  []
axiomAnnotationIRIs (rawDataPropertyAssertion property subject literal) =
  []
axiomAnnotationIRIs (rawNegativeDataPropertyAssertion property subject literal) =
  []
axiomAnnotationIRIs (rawAnnotationAssertion property subject value) =
  rawAnnotationSubjectIRIs subject ++ rawAnnotationValueIRIs value
axiomAnnotationIRIs (rawSubAnnotationPropertyOf sub sup) =
  []
axiomAnnotationIRIs (rawAnnotationPropertyDomain property iri) =
  iri ∷ []
axiomAnnotationIRIs (rawAnnotationPropertyRange property iri) =
  iri ∷ []
axiomAnnotationIRIs (rawUnsupportedAxiom reason) =
  []

axiomAnnotationBlankNodes : RawAxiom → List String
axiomAnnotationBlankNodes (rawDeclaration entity) =
  []
axiomAnnotationBlankNodes (rawSubClassOf sub sup) =
  []
axiomAnnotationBlankNodes (rawEquivalentClasses classes) =
  []
axiomAnnotationBlankNodes (rawDisjointClasses classes) =
  []
axiomAnnotationBlankNodes (rawDisjointUnion class classes) =
  []
axiomAnnotationBlankNodes (rawSubObjectPropertyOf sub sup) =
  []
axiomAnnotationBlankNodes (rawEquivalentObjectProperties properties) =
  []
axiomAnnotationBlankNodes (rawDisjointObjectProperties properties) =
  []
axiomAnnotationBlankNodes (rawInverseObjectProperties left right) =
  []
axiomAnnotationBlankNodes (rawObjectPropertyDomain property class) =
  []
axiomAnnotationBlankNodes (rawObjectPropertyRange property class) =
  []
axiomAnnotationBlankNodes (rawFunctionalObjectProperty property) =
  []
axiomAnnotationBlankNodes (rawInverseFunctionalObjectProperty property) =
  []
axiomAnnotationBlankNodes (rawReflexiveObjectProperty property) =
  []
axiomAnnotationBlankNodes (rawIrreflexiveObjectProperty property) =
  []
axiomAnnotationBlankNodes (rawSymmetricObjectProperty property) =
  []
axiomAnnotationBlankNodes (rawAsymmetricObjectProperty property) =
  []
axiomAnnotationBlankNodes (rawTransitiveObjectProperty property) =
  []
axiomAnnotationBlankNodes (rawSubDataPropertyOf sub sup) =
  []
axiomAnnotationBlankNodes (rawEquivalentDataProperties properties) =
  []
axiomAnnotationBlankNodes (rawDisjointDataProperties properties) =
  []
axiomAnnotationBlankNodes (rawDataPropertyDomain property class) =
  []
axiomAnnotationBlankNodes (rawDataPropertyRange property range) =
  []
axiomAnnotationBlankNodes (rawFunctionalDataProperty property) =
  []
axiomAnnotationBlankNodes (rawDatatypeDefinition datatype range) =
  []
axiomAnnotationBlankNodes (rawHasKey class objectProperties dataProperties) =
  []
axiomAnnotationBlankNodes (rawSameIndividual individuals) =
  []
axiomAnnotationBlankNodes (rawDifferentIndividuals individuals) =
  []
axiomAnnotationBlankNodes (rawClassAssertion class individual) =
  []
axiomAnnotationBlankNodes (rawObjectPropertyAssertion property subject object) =
  []
axiomAnnotationBlankNodes
  (rawNegativeObjectPropertyAssertion property subject object) =
  []
axiomAnnotationBlankNodes (rawDataPropertyAssertion property subject literal) =
  []
axiomAnnotationBlankNodes (rawNegativeDataPropertyAssertion property subject literal) =
  []
axiomAnnotationBlankNodes (rawAnnotationAssertion property subject value) =
  rawAnnotationSubjectBlankNodes subject ++ rawAnnotationValueBlankNodes value
axiomAnnotationBlankNodes (rawSubAnnotationPropertyOf sub sup) =
  []
axiomAnnotationBlankNodes (rawAnnotationPropertyDomain property iri) =
  []
axiomAnnotationBlankNodes (rawAnnotationPropertyRange property iri) =
  []
axiomAnnotationBlankNodes (rawUnsupportedAxiom reason) =
  []

annotatedAnnotationIRIs : RawAnnotated RawAxiom → List RawIRI
annotatedAnnotationIRIs axiom =
  rawAnnotationsIRIs (annotations axiom) ++ axiomAnnotationIRIs (body axiom)

annotatedAnnotationBlankNodes : RawAnnotated RawAxiom → List String
annotatedAnnotationBlankNodes axiom =
  rawAnnotationsBlankNodes (annotations axiom) ++
  axiomAnnotationBlankNodes (body axiom)

annotatedFacetIRIs : RawAnnotated RawAxiom → List RawIRI
annotatedFacetIRIs axiom =
  axiomFacetIRIs (body axiom)

collectAnnotationIRIs : List (RawAnnotated RawAxiom) → List RawIRI
collectAnnotationIRIs [] =
  []
collectAnnotationIRIs (axiom ∷ axioms) =
  annotatedAnnotationIRIs axiom ++ collectAnnotationIRIs axioms

collectAnnotationBlankNodes : List (RawAnnotated RawAxiom) → List String
collectAnnotationBlankNodes [] =
  []
collectAnnotationBlankNodes (axiom ∷ axioms) =
  annotatedAnnotationBlankNodes axiom ++ collectAnnotationBlankNodes axioms

collectFacetIRIs : List (RawAnnotated RawAxiom) → List RawIRI
collectFacetIRIs [] =
  []
collectFacetIRIs (axiom ∷ axioms) =
  annotatedFacetIRIs axiom ++ collectFacetIRIs axioms

collectWith : (RawEntity → List RawIRI) → List (RawAnnotated RawAxiom) → List RawIRI
collectWith select [] =
  []
collectWith select (axiom ∷ axioms) with annotatedEntity axiom
... | present entity =
  select entity ++ collectWith select axioms
... | absent =
  collectWith select axioms

symbolTableFromRaw : RawOntology → SymbolTable
symbolTableFromRaw raw =
  symbolTable
    (collectWith entityClassIRIs (axioms raw))
    (collectWith entityObjectPropertyIRIs (axioms raw))
    (collectWith entityDataPropertyIRIs (axioms raw))
    (collectWith entityAnnotationPropertyIRIs (axioms raw))
    (collectWith entityDatatypeIRIs (axioms raw))
    (collectFacetIRIs (axioms raw))
    (collectWith entityIndividualIRIs (axioms raw))
    (rawAnnotationsIRIs (annotations raw) ++ collectAnnotationIRIs (axioms raw))
    (rawAnnotationsBlankNodes (annotations raw) ++
     collectAnnotationBlankNodes (axioms raw))
    K.noPunning