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

module OWL2.Elab.Structural where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
open import OWL2.Elab.CheckedImport
open import OWL2.Elab.Declarations
open import OWL2.Elab.Policy
open import OWL2.Elab.Punning
open import OWL2.Elab.Regularity
open import OWL2.Elab.Result
open import OWL2.Elab.SymbolTable
open import OWL2.Foundation.Maybe
open import OWL2.Raw hiding (SourcePath; sourcePath; rootPath; fieldPath; indexPath)
import OWL2.Kernel as K

private
  elabCode : String → DiagnosticCode
  elabCode name =
    mkDiagnosticCode "elab.structural" name

  importsPath : SourcePath
  importsPath =
    sourcePath (fieldSegment "imports" ∷ [])

  ontologyIRIPath : SourcePath
  ontologyIRIPath =
    sourcePath (fieldSegment "ontologyIRI" ∷ [])

  versionIRIPath : SourcePath
  versionIRIPath =
    sourcePath (fieldSegment "versionIRI" ∷ [])

  axiomsPath : SourcePath
  axiomsPath =
    sourcePath (fieldSegment "axioms" ∷ [])

  classExpressionPath : SourcePath
  classExpressionPath =
    sourcePath (fieldSegment "classExpression" ∷ [])

  objectPropertyExpressionPath : SourcePath
  objectPropertyExpressionPath =
    sourcePath (fieldSegment "objectPropertyExpression" ∷ [])

  dataPropertyExpressionPath : SourcePath
  dataPropertyExpressionPath =
    sourcePath (fieldSegment "dataPropertyExpression" ∷ [])

  annotationPropertyPath : SourcePath
  annotationPropertyPath =
    sourcePath (fieldSegment "annotationProperty" ∷ [])

  annotationIRIPath : SourcePath
  annotationIRIPath =
    sourcePath (fieldSegment "annotationIRI" ∷ [])

  annotationBlankNodePath : SourcePath
  annotationBlankNodePath =
    sourcePath (fieldSegment "annotationBlankNode" ∷ [])

  dataRangePath : SourcePath
  dataRangePath =
    sourcePath (fieldSegment "dataRange" ∷ [])

  literalPath : SourcePath
  literalPath =
    sourcePath (fieldSegment "literal" ∷ [])

  subObjectPropertyExpressionPath : SourcePath
  subObjectPropertyExpressionPath =
    sourcePath (fieldSegment "subObjectPropertyExpression" ∷ [])

  individualPath : SourcePath
  individualPath =
    sourcePath (fieldSegment "individual" ∷ [])

structuralUnsupportedImportDiagnostic : Diagnostic
structuralUnsupportedImportDiagnostic =
  diagnostic
    (elabCode "unsupported-import")
    severityError
    importsPath
    "The structural elaborator accepts only raw ontologies without imports."

structuralUnsupportedOntologyIRIDiagnostic : Diagnostic
structuralUnsupportedOntologyIRIDiagnostic =
  diagnostic
    (elabCode "unsupported-ontology-iri")
    severityError
    ontologyIRIPath
    "The structural elaborator does not erase ontology IRIs."

structuralUnsupportedVersionIRIDiagnostic : Diagnostic
structuralUnsupportedVersionIRIDiagnostic =
  diagnostic
    (elabCode "unsupported-version-iri")
    severityError
    versionIRIPath
    "The structural elaborator does not erase version IRIs."

structuralUnsupportedAxiomDiagnostic : Diagnostic
structuralUnsupportedAxiomDiagnostic =
  diagnostic
    (elabCode "unsupported-axiom")
    severityError
    axiomsPath
    "This structural elaborator does not yet support this axiom."

unsupportedClassExpressionDiagnostic : Diagnostic
unsupportedClassExpressionDiagnostic =
  diagnostic
    (elabCode "unsupported-class-expression")
    severityError
    classExpressionPath
    "This class expression is outside the current structural elaborator fragment."

undeclaredClassDiagnostic : RawIRI → Diagnostic
undeclaredClassDiagnostic iri =
  diagnostic
    (elabCode "undeclared-class")
    severityError
    classExpressionPath
    (text iri)

undeclaredObjectPropertyDiagnostic : RawIRI → Diagnostic
undeclaredObjectPropertyDiagnostic iri =
  diagnostic
    (elabCode "undeclared-object-property")
    severityError
    objectPropertyExpressionPath
    (text iri)

undeclaredDataPropertyDiagnostic : RawIRI → Diagnostic
undeclaredDataPropertyDiagnostic iri =
  diagnostic
    (elabCode "undeclared-data-property")
    severityError
    dataPropertyExpressionPath
    (text iri)

undeclaredAnnotationPropertyDiagnostic : RawIRI → Diagnostic
undeclaredAnnotationPropertyDiagnostic iri =
  diagnostic
    (elabCode "undeclared-annotation-property")
    severityError
    annotationPropertyPath
    (text iri)

untrackedAnnotationIRIDiagnostic : RawIRI → Diagnostic
untrackedAnnotationIRIDiagnostic iri =
  diagnostic
    (elabCode "untracked-annotation-iri")
    severityError
    annotationIRIPath
    (text iri)

untrackedAnnotationBlankNodeDiagnostic : String → Diagnostic
untrackedAnnotationBlankNodeDiagnostic name =
  diagnostic
    (elabCode "untracked-annotation-blank-node")
    severityError
    annotationBlankNodePath
    name

undeclaredDatatypeDiagnostic : RawIRI → Diagnostic
undeclaredDatatypeDiagnostic iri =
  diagnostic
    (elabCode "undeclared-datatype")
    severityError
    dataRangePath
    (text iri)

missingLiteralDatatypeDiagnostic : Diagnostic
missingLiteralDatatypeDiagnostic =
  diagnostic
    (elabCode "missing-literal-datatype")
    severityError
    literalPath
    "Literal imports must specify an explicit datatype IRI."

unsupportedLanguageTaggedLiteralDiagnostic : String → Diagnostic
unsupportedLanguageTaggedLiteralDiagnostic tag =
  diagnostic
    (elabCode "unsupported-language-tagged-literal")
    severityError
    literalPath
    tag

unsupportedDataRangeDiagnostic : Diagnostic
unsupportedDataRangeDiagnostic =
  diagnostic
    (elabCode "unsupported-data-range")
    severityError
    dataRangePath
    "This data range is outside the current structural elaborator fragment."

unsupportedSimpleObjectPropertyExpressionDiagnostic : Diagnostic
unsupportedSimpleObjectPropertyExpressionDiagnostic =
  diagnostic
    (elabCode "unsupported-simple-object-property-expression")
    severityError
    objectPropertyExpressionPath
    "Simple object property positions currently accept only named object properties."

unsupportedPropertyChainRegularityDiagnostic : Diagnostic
unsupportedPropertyChainRegularityDiagnostic =
  diagnostic
    (elabCode "unsupported-property-chain-regularity")
    severityError
    subObjectPropertyExpressionPath
    "Property-chain axioms require a checked global regularity certificate."

nonSimpleObjectPropertyDiagnostic : RawIRI → Diagnostic
nonSimpleObjectPropertyDiagnostic iri =
  diagnostic
    (elabCode "non-simple-object-property")
    severityError
    objectPropertyExpressionPath
    (text iri)

undeclaredIndividualDiagnostic : RawIRI → Diagnostic
undeclaredIndividualDiagnostic iri =
  diagnostic
    (elabCode "undeclared-individual")
    severityError
    individualPath
    (text iri)

unsupportedAnonymousIndividualDiagnostic : String → Diagnostic
unsupportedAnonymousIndividualDiagnostic name =
  diagnostic
    (elabCode "unsupported-anonymous-individual")
    severityError
    individualPath
    name

emptyClassExpressionListDiagnostic : Diagnostic
emptyClassExpressionListDiagnostic =
  diagnostic
    (elabCode "empty-class-expression-list")
    severityError
    classExpressionPath
    "This class expression list must contain at least one expression."

emptyIndividualListDiagnostic : Diagnostic
emptyIndividualListDiagnostic =
  diagnostic
    (elabCode "empty-individual-list")
    severityError
    individualPath
    "This individual list must contain at least one individual."

tooFewIndividualsDiagnostic : Diagnostic
tooFewIndividualsDiagnostic =
  diagnostic
    (elabCode "too-few-individuals")
    severityError
    individualPath
    "This individual axiom must contain at least two individuals."

tooFewDataPropertyExpressionsDiagnostic : Diagnostic
tooFewDataPropertyExpressionsDiagnostic =
  diagnostic
    (elabCode "too-few-data-property-expressions")
    severityError
    dataPropertyExpressionPath
    "This data property axiom must contain at least two property expressions."

tooFewObjectPropertyExpressionsDiagnostic : Diagnostic
tooFewObjectPropertyExpressionsDiagnostic =
  diagnostic
    (elabCode "too-few-object-property-expressions")
    severityError
    objectPropertyExpressionPath
    "This object property axiom must contain at least two property expressions."

tooFewSimpleObjectPropertyExpressionsDiagnostic : Diagnostic
tooFewSimpleObjectPropertyExpressionsDiagnostic =
  diagnostic
    (elabCode "too-few-simple-object-property-expressions")
    severityError
    objectPropertyExpressionPath
    "This simple object property axiom must contain at least two named properties."

emptyDataRangeListDiagnostic : Diagnostic
emptyDataRangeListDiagnostic =
  diagnostic
    (elabCode "empty-data-range-list")
    severityError
    dataRangePath
    "This data range list must contain at least one data range."

emptyLiteralListDiagnostic : Diagnostic
emptyLiteralListDiagnostic =
  diagnostic
    (elabCode "empty-literal-list")
    severityError
    literalPath
    "This literal list must contain at least one literal."

tooFewClassExpressionsDiagnostic : Diagnostic
tooFewClassExpressionsDiagnostic =
  diagnostic
    (elabCode "too-few-class-expressions")
    severityError
    classExpressionPath
    "This class axiom must contain at least two class expressions."

objectPropertyExpressionDiagnostics :
  SymbolTable →
  RawObjectPropertyExpression →
  Diagnostics
objectPropertyExpressionDiagnostics table (rawObjectProperty iri) with
  objectPropertyLookup table iri
... | present name =
  noDiagnostics
... | absent =
  singleDiagnostic (undeclaredObjectPropertyDiagnostic iri)
objectPropertyExpressionDiagnostics table rawTopObjectProperty =
  noDiagnostics
objectPropertyExpressionDiagnostics table rawBottomObjectProperty =
  noDiagnostics
objectPropertyExpressionDiagnostics table (rawObjectInverseOf property) =
  objectPropertyExpressionDiagnostics table property

simpleObjectPropertyExpressionDiagnostics :
  (table : SymbolTable) →
  K.RegularityContext (symbolTableSignature table) →
  RawObjectPropertyExpression →
  Diagnostics
simpleObjectPropertyExpressionDiagnostics table context (rawObjectProperty iri)
  with objectPropertyLookup table iri
... | absent =
  singleDiagnostic (undeclaredObjectPropertyDiagnostic iri)
... | present name with K.simpleObjectProperty? context name
...   | true =
  noDiagnostics
...   | false =
  singleDiagnostic (nonSimpleObjectPropertyDiagnostic iri)
simpleObjectPropertyExpressionDiagnostics table context rawTopObjectProperty =
  singleDiagnostic unsupportedSimpleObjectPropertyExpressionDiagnostic
simpleObjectPropertyExpressionDiagnostics table context rawBottomObjectProperty =
  singleDiagnostic unsupportedSimpleObjectPropertyExpressionDiagnostic
simpleObjectPropertyExpressionDiagnostics
  table
  context
  (rawObjectInverseOf property) =
  singleDiagnostic unsupportedSimpleObjectPropertyExpressionDiagnostic

objectPropertyExpressionListDiagnostics :
  SymbolTable →
  List RawObjectPropertyExpression →
  Diagnostics
objectPropertyExpressionListDiagnostics table [] =
  noDiagnostics
objectPropertyExpressionListDiagnostics table (property ∷ properties) =
  objectPropertyExpressionDiagnostics table property ++
  objectPropertyExpressionListDiagnostics table properties

atLeastTwoObjectPropertyExpressionListDiagnostics :
  SymbolTable →
  List RawObjectPropertyExpression →
  Diagnostics
atLeastTwoObjectPropertyExpressionListDiagnostics table [] =
  singleDiagnostic tooFewObjectPropertyExpressionsDiagnostic
atLeastTwoObjectPropertyExpressionListDiagnostics table (property ∷ []) =
  objectPropertyExpressionDiagnostics table property ++
  singleDiagnostic tooFewObjectPropertyExpressionsDiagnostic
atLeastTwoObjectPropertyExpressionListDiagnostics table properties =
  objectPropertyExpressionListDiagnostics table properties

subObjectPropertyExpressionDiagnostics :
  SymbolTable →
  RawSubObjectPropertyExpression →
  Diagnostics
subObjectPropertyExpressionDiagnostics table (rawSubObjectProperty property) =
  objectPropertyExpressionDiagnostics table property
subObjectPropertyExpressionDiagnostics table (rawSubObjectPropertyChain []) =
  singleDiagnostic tooFewObjectPropertyExpressionsDiagnostic
subObjectPropertyExpressionDiagnostics
  table
  (rawSubObjectPropertyChain (property ∷ [])) =
  objectPropertyExpressionDiagnostics table property ++
  singleDiagnostic tooFewObjectPropertyExpressionsDiagnostic
subObjectPropertyExpressionDiagnostics
  table
  (rawSubObjectPropertyChain properties) =
  objectPropertyExpressionListDiagnostics table properties ++
  singleDiagnostic unsupportedPropertyChainRegularityDiagnostic

simpleObjectPropertyExpressionListDiagnostics :
  (table : SymbolTable) →
  K.RegularityContext (symbolTableSignature table) →
  List RawObjectPropertyExpression →
  Diagnostics
simpleObjectPropertyExpressionListDiagnostics table context [] =
  noDiagnostics
simpleObjectPropertyExpressionListDiagnostics
  table
  context
  (property ∷ properties) =
  simpleObjectPropertyExpressionDiagnostics table context property ++
  simpleObjectPropertyExpressionListDiagnostics table context properties

atLeastTwoSimpleObjectPropertyExpressionListDiagnostics :
  (table : SymbolTable) →
  K.RegularityContext (symbolTableSignature table) →
  List RawObjectPropertyExpression →
  Diagnostics
atLeastTwoSimpleObjectPropertyExpressionListDiagnostics table context [] =
  singleDiagnostic tooFewSimpleObjectPropertyExpressionsDiagnostic
atLeastTwoSimpleObjectPropertyExpressionListDiagnostics
  table
  context
  (property ∷ []) =
  simpleObjectPropertyExpressionDiagnostics table context property ++
  singleDiagnostic tooFewSimpleObjectPropertyExpressionsDiagnostic
atLeastTwoSimpleObjectPropertyExpressionListDiagnostics
  table
  context
  properties =
  simpleObjectPropertyExpressionListDiagnostics table context properties

dataPropertyExpressionDiagnostics :
  SymbolTable →
  RawDataPropertyExpression →
  Diagnostics
dataPropertyExpressionDiagnostics table (rawDataProperty iri) with
  dataPropertyLookup table iri
... | present name =
  noDiagnostics
... | absent =
  singleDiagnostic (undeclaredDataPropertyDiagnostic iri)
dataPropertyExpressionDiagnostics table rawTopDataProperty =
  noDiagnostics
dataPropertyExpressionDiagnostics table rawBottomDataProperty =
  noDiagnostics

dataPropertyExpressionListDiagnostics :
  SymbolTable →
  List RawDataPropertyExpression →
  Diagnostics
dataPropertyExpressionListDiagnostics table [] =
  noDiagnostics
dataPropertyExpressionListDiagnostics table (property ∷ properties) =
  dataPropertyExpressionDiagnostics table property ++
  dataPropertyExpressionListDiagnostics table properties

atLeastTwoDataPropertyExpressionListDiagnostics :
  SymbolTable →
  List RawDataPropertyExpression →
  Diagnostics
atLeastTwoDataPropertyExpressionListDiagnostics table [] =
  singleDiagnostic tooFewDataPropertyExpressionsDiagnostic
atLeastTwoDataPropertyExpressionListDiagnostics table (property ∷ []) =
  dataPropertyExpressionDiagnostics table property ++
  singleDiagnostic tooFewDataPropertyExpressionsDiagnostic
atLeastTwoDataPropertyExpressionListDiagnostics table properties =
  dataPropertyExpressionListDiagnostics table properties

mutual
  literalDiagnostics : SymbolTable → RawLiteral → Diagnostics
  literalDiagnostics table literal with
    datatypeIRI literal | languageTag literal
  ... | absent | absent =
    singleDiagnostic missingLiteralDatatypeDiagnostic
  ... | absent | present tag =
    singleDiagnostic (unsupportedLanguageTaggedLiteralDiagnostic tag)
  ... | present iri | present tag =
    singleDiagnostic (unsupportedLanguageTaggedLiteralDiagnostic tag)
  ... | present iri | absent with datatypeLookup table iri
  ...   | present name =
    noDiagnostics
  ...   | absent =
    singleDiagnostic (undeclaredDatatypeDiagnostic iri)

  literalListDiagnostics :
    SymbolTable →
    List RawLiteral →
    Diagnostics
  literalListDiagnostics table [] =
    noDiagnostics
  literalListDiagnostics table (literal ∷ literals) =
    literalDiagnostics table literal ++
    literalListDiagnostics table literals

  nonEmptyLiteralListDiagnostics :
    SymbolTable →
    List RawLiteral →
    Diagnostics
  nonEmptyLiteralListDiagnostics table [] =
    singleDiagnostic emptyLiteralListDiagnostic
  nonEmptyLiteralListDiagnostics table literals =
    literalListDiagnostics table literals

  facetRestrictionDiagnostics :
    SymbolTable →
    RawFacetRestriction →
    Diagnostics
  facetRestrictionDiagnostics table restriction =
    literalDiagnostics table (value restriction)

  facetRestrictionListDiagnostics :
    SymbolTable →
    List RawFacetRestriction →
    Diagnostics
  facetRestrictionListDiagnostics table [] =
    noDiagnostics
  facetRestrictionListDiagnostics table (restriction ∷ restrictions) =
    facetRestrictionDiagnostics table restriction ++
    facetRestrictionListDiagnostics table restrictions

  dataRangeListDiagnostics :
    SymbolTable →
    List RawDataRange →
    Diagnostics
  dataRangeListDiagnostics table [] =
    noDiagnostics
  dataRangeListDiagnostics table (range ∷ ranges) =
    dataRangeDiagnostics table range ++
    dataRangeListDiagnostics table ranges

  nonEmptyDataRangeListDiagnostics :
    SymbolTable →
    List RawDataRange →
    Diagnostics
  nonEmptyDataRangeListDiagnostics table [] =
    singleDiagnostic emptyDataRangeListDiagnostic
  nonEmptyDataRangeListDiagnostics table ranges =
    dataRangeListDiagnostics table ranges

  dataRangeDiagnostics : SymbolTable → RawDataRange → Diagnostics
  dataRangeDiagnostics table (rawDatatype iri) with datatypeLookup table iri
  ... | present name =
    noDiagnostics
  ... | absent =
    singleDiagnostic (undeclaredDatatypeDiagnostic iri)
  dataRangeDiagnostics table (rawDatatypeRestriction iri restrictions) =
    dataRangeDiagnostics table (rawDatatype iri) ++
    facetRestrictionListDiagnostics table restrictions
  dataRangeDiagnostics table rawDataTop =
    noDiagnostics
  dataRangeDiagnostics table rawDataBottom =
    noDiagnostics
  dataRangeDiagnostics table (rawDataComplementOf range) =
    dataRangeDiagnostics table range
  dataRangeDiagnostics table (rawDataIntersectionOf ranges) =
    nonEmptyDataRangeListDiagnostics table ranges
  dataRangeDiagnostics table (rawDataUnionOf ranges) =
    nonEmptyDataRangeListDiagnostics table ranges
  dataRangeDiagnostics table (rawDataOneOf literals) =
    nonEmptyLiteralListDiagnostics table literals

optionalDataRangeDiagnostics :
  SymbolTable →
  Optional RawDataRange →
  Diagnostics
optionalDataRangeDiagnostics table absent =
  noDiagnostics
optionalDataRangeDiagnostics table (present range) =
  dataRangeDiagnostics table range

individualDiagnostics : SymbolTable → RawIndividual → Diagnostics
individualDiagnostics table (rawNamedIndividual iri) with
  individualLookup table iri
... | present name =
  noDiagnostics
... | absent =
  singleDiagnostic (undeclaredIndividualDiagnostic iri)
individualDiagnostics table (rawAnonymousIndividual name) =
  singleDiagnostic (unsupportedAnonymousIndividualDiagnostic name)

individualListDiagnostics :
  SymbolTable →
  List RawIndividual →
  Diagnostics
individualListDiagnostics table [] =
  noDiagnostics
individualListDiagnostics table (individual ∷ individuals) =
  individualDiagnostics table individual ++
  individualListDiagnostics table individuals

nonEmptyIndividualListDiagnostics :
  SymbolTable →
  List RawIndividual →
  Diagnostics
nonEmptyIndividualListDiagnostics table [] =
  singleDiagnostic emptyIndividualListDiagnostic
nonEmptyIndividualListDiagnostics table individuals =
  individualListDiagnostics table individuals

atLeastTwoIndividualListDiagnostics :
  SymbolTable →
  List RawIndividual →
  Diagnostics
atLeastTwoIndividualListDiagnostics table [] =
  singleDiagnostic tooFewIndividualsDiagnostic
atLeastTwoIndividualListDiagnostics table (individual ∷ []) =
  individualDiagnostics table individual ++
  singleDiagnostic tooFewIndividualsDiagnostic
atLeastTwoIndividualListDiagnostics table individuals =
  individualListDiagnostics table individuals

mutual
  classExpressionListDiagnostics :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    List RawClassExpression →
    Diagnostics
  classExpressionListDiagnostics table context [] =
    noDiagnostics
  classExpressionListDiagnostics table context (class ∷ classes) =
    classExpressionDiagnostics table context class ++
    classExpressionListDiagnostics table context classes

  nonEmptyClassExpressionListDiagnostics :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    List RawClassExpression →
    Diagnostics
  nonEmptyClassExpressionListDiagnostics table context [] =
    singleDiagnostic emptyClassExpressionListDiagnostic
  nonEmptyClassExpressionListDiagnostics table context classes =
    classExpressionListDiagnostics table context classes

  atLeastTwoClassExpressionListDiagnostics :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    List RawClassExpression →
    Diagnostics
  atLeastTwoClassExpressionListDiagnostics table context [] =
    singleDiagnostic tooFewClassExpressionsDiagnostic
  atLeastTwoClassExpressionListDiagnostics table context (class ∷ []) =
    classExpressionDiagnostics table context class ++
    singleDiagnostic tooFewClassExpressionsDiagnostic
  atLeastTwoClassExpressionListDiagnostics table context classes =
    classExpressionListDiagnostics table context classes

  optionalClassExpressionDiagnostics :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    Optional RawClassExpression →
    Diagnostics
  optionalClassExpressionDiagnostics table context absent =
    noDiagnostics
  optionalClassExpressionDiagnostics table context (present class) =
    classExpressionDiagnostics table context class

  classExpressionDiagnostics :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    RawClassExpression →
    Diagnostics
  classExpressionDiagnostics table context (rawNamedClass iri)
    with classLookup table iri
  ... | present name =
    noDiagnostics
  ... | absent =
    singleDiagnostic (undeclaredClassDiagnostic iri)
  classExpressionDiagnostics table context rawOwlThing =
    noDiagnostics
  classExpressionDiagnostics table context rawOwlNothing =
    noDiagnostics
  classExpressionDiagnostics table context (rawObjectIntersectionOf classes) =
    nonEmptyClassExpressionListDiagnostics table context classes
  classExpressionDiagnostics table context (rawObjectUnionOf classes) =
    nonEmptyClassExpressionListDiagnostics table context classes
  classExpressionDiagnostics table context (rawObjectOneOf individuals) =
    nonEmptyIndividualListDiagnostics table individuals
  classExpressionDiagnostics table context (rawObjectComplementOf class) =
    classExpressionDiagnostics table context class
  classExpressionDiagnostics
    table
    context
    (rawObjectSomeValuesFrom property class) =
    objectPropertyExpressionDiagnostics table property ++
    classExpressionDiagnostics table context class
  classExpressionDiagnostics
    table
    context
    (rawObjectAllValuesFrom property class) =
    objectPropertyExpressionDiagnostics table property ++
    classExpressionDiagnostics table context class
  classExpressionDiagnostics table context (rawObjectHasValue property individual) =
    objectPropertyExpressionDiagnostics table property ++
    individualDiagnostics table individual
  classExpressionDiagnostics table context (rawObjectHasSelf property) =
    simpleObjectPropertyExpressionDiagnostics table context property
  classExpressionDiagnostics
    table
    context
    (rawObjectMinCardinality n property class) =
    simpleObjectPropertyExpressionDiagnostics table context property ++
    optionalClassExpressionDiagnostics table context class
  classExpressionDiagnostics
    table
    context
    (rawObjectMaxCardinality n property class) =
    simpleObjectPropertyExpressionDiagnostics table context property ++
    optionalClassExpressionDiagnostics table context class
  classExpressionDiagnostics
    table
    context
    (rawObjectExactCardinality n property class) =
    simpleObjectPropertyExpressionDiagnostics table context property ++
    optionalClassExpressionDiagnostics table context class
  classExpressionDiagnostics table context (rawDataSomeValuesFrom property range) =
    dataPropertyExpressionDiagnostics table property ++
    dataRangeDiagnostics table range
  classExpressionDiagnostics table context (rawDataAllValuesFrom property range) =
    dataPropertyExpressionDiagnostics table property ++
    dataRangeDiagnostics table range
  classExpressionDiagnostics table context (rawDataHasValue property literal) =
    dataPropertyExpressionDiagnostics table property ++
    literalDiagnostics table literal
  classExpressionDiagnostics
    table
    context
    (rawDataMinCardinality n property range) =
    dataPropertyExpressionDiagnostics table property ++
    optionalDataRangeDiagnostics table range
  classExpressionDiagnostics
    table
    context
    (rawDataMaxCardinality n property range) =
    dataPropertyExpressionDiagnostics table property ++
    optionalDataRangeDiagnostics table range
  classExpressionDiagnostics
    table
    context
    (rawDataExactCardinality n property range) =
    dataPropertyExpressionDiagnostics table property ++
    optionalDataRangeDiagnostics table range

annotationPropertyDiagnostics : SymbolTable → RawIRI → Diagnostics
annotationPropertyDiagnostics table iri with annotationPropertyLookup table iri
... | present name =
  noDiagnostics
... | absent =
  singleDiagnostic (undeclaredAnnotationPropertyDiagnostic iri)

annotationIRIDiagnostics : SymbolTable → RawIRI → Diagnostics
annotationIRIDiagnostics table iri with annotationIRILookup table iri
... | present name =
  noDiagnostics
... | absent =
  singleDiagnostic (untrackedAnnotationIRIDiagnostic iri)

annotationBlankNodeDiagnostics : SymbolTable → String → Diagnostics
annotationBlankNodeDiagnostics table name with annotationBlankNodeLookup table name
... | present blankNode =
  noDiagnostics
... | absent =
  singleDiagnostic (untrackedAnnotationBlankNodeDiagnostic name)

annotationSubjectDiagnostics :
  SymbolTable →
  RawAnnotationSubject →
  Diagnostics
annotationSubjectDiagnostics table (rawAnnotationSubjectIRI iri) =
  annotationIRIDiagnostics table iri
annotationSubjectDiagnostics table (rawAnnotationSubjectAnonymous name) =
  annotationBlankNodeDiagnostics table name

annotationValueDiagnostics :
  SymbolTable →
  RawAnnotationValue →
  Diagnostics
annotationValueDiagnostics table (rawAnnotationValueIRI iri) =
  annotationIRIDiagnostics table iri
annotationValueDiagnostics table (rawAnnotationValueAnonymous name) =
  annotationBlankNodeDiagnostics table name
annotationValueDiagnostics table (rawAnnotationValueLiteral literal) =
  literalDiagnostics table literal

mutual
  annotationDiagnostics :
    SymbolTable →
    RawAnnotation →
    Diagnostics
  annotationDiagnostics table (rawAnnotation annotations property value) =
    annotationsDiagnostics table annotations ++
    annotationPropertyDiagnostics table property ++
    annotationValueDiagnostics table value

  annotationsDiagnostics :
    SymbolTable →
    List RawAnnotation →
    Diagnostics
  annotationsDiagnostics table [] =
    noDiagnostics
  annotationsDiagnostics table (annotation ∷ annotations) =
    annotationDiagnostics table annotation ++
    annotationsDiagnostics table annotations

structuralAxiomDiagnostics :
  (table : SymbolTable) →
  K.RegularityContext (symbolTableSignature table) →
  RawAxiom →
  Diagnostics
structuralAxiomDiagnostics table context (rawDeclaration entity) =
  declarationAxiomDiagnostics (rawDeclaration entity)
structuralAxiomDiagnostics table context (rawSubClassOf sub sup) =
  classExpressionDiagnostics table context sub ++
  classExpressionDiagnostics table context sup
structuralAxiomDiagnostics table context (rawEquivalentClasses classes) =
  atLeastTwoClassExpressionListDiagnostics table context classes
structuralAxiomDiagnostics table context (rawDisjointClasses classes) =
  atLeastTwoClassExpressionListDiagnostics table context classes
structuralAxiomDiagnostics table context (rawDisjointUnion class classes) =
  classExpressionDiagnostics table context (rawNamedClass class) ++
  atLeastTwoClassExpressionListDiagnostics table context classes
structuralAxiomDiagnostics table context (rawSubObjectPropertyOf sub sup) =
  subObjectPropertyExpressionDiagnostics table sub ++
  objectPropertyExpressionDiagnostics table sup
structuralAxiomDiagnostics table context (rawEquivalentObjectProperties properties) =
  atLeastTwoObjectPropertyExpressionListDiagnostics table properties
structuralAxiomDiagnostics table context (rawDisjointObjectProperties properties) =
  atLeastTwoSimpleObjectPropertyExpressionListDiagnostics table context properties
structuralAxiomDiagnostics table context (rawInverseObjectProperties left right) =
  objectPropertyExpressionDiagnostics table left ++
  objectPropertyExpressionDiagnostics table right
structuralAxiomDiagnostics table context (rawObjectPropertyDomain property class) =
  objectPropertyExpressionDiagnostics table property ++
  classExpressionDiagnostics table context class
structuralAxiomDiagnostics table context (rawObjectPropertyRange property class) =
  objectPropertyExpressionDiagnostics table property ++
  classExpressionDiagnostics table context class
structuralAxiomDiagnostics table context (rawFunctionalObjectProperty property) =
  simpleObjectPropertyExpressionDiagnostics table context property
structuralAxiomDiagnostics
  table
  context
  (rawInverseFunctionalObjectProperty property) =
  simpleObjectPropertyExpressionDiagnostics table context property
structuralAxiomDiagnostics table context (rawReflexiveObjectProperty property) =
  objectPropertyExpressionDiagnostics table property
structuralAxiomDiagnostics table context (rawIrreflexiveObjectProperty property) =
  simpleObjectPropertyExpressionDiagnostics table context property
structuralAxiomDiagnostics table context (rawSymmetricObjectProperty property) =
  objectPropertyExpressionDiagnostics table property
structuralAxiomDiagnostics table context (rawAsymmetricObjectProperty property) =
  simpleObjectPropertyExpressionDiagnostics table context property
structuralAxiomDiagnostics table context (rawTransitiveObjectProperty property) =
  objectPropertyExpressionDiagnostics table property
structuralAxiomDiagnostics table context (rawSubDataPropertyOf sub sup) =
  dataPropertyExpressionDiagnostics table sub ++
  dataPropertyExpressionDiagnostics table sup
structuralAxiomDiagnostics table context (rawEquivalentDataProperties properties) =
  atLeastTwoDataPropertyExpressionListDiagnostics table properties
structuralAxiomDiagnostics table context (rawDisjointDataProperties properties) =
  atLeastTwoDataPropertyExpressionListDiagnostics table properties
structuralAxiomDiagnostics table context (rawDataPropertyDomain property class) =
  dataPropertyExpressionDiagnostics table property ++
  classExpressionDiagnostics table context class
structuralAxiomDiagnostics table context (rawDataPropertyRange property range) =
  dataPropertyExpressionDiagnostics table property ++
  dataRangeDiagnostics table range
structuralAxiomDiagnostics table context (rawFunctionalDataProperty property) =
  dataPropertyExpressionDiagnostics table property
structuralAxiomDiagnostics table context (rawDatatypeDefinition datatype range) =
  dataRangeDiagnostics table (rawDatatype datatype) ++
  dataRangeDiagnostics table range
structuralAxiomDiagnostics
  table
  context
  (rawHasKey class objectProperties dataProperties) =
  classExpressionDiagnostics table context class ++
  simpleObjectPropertyExpressionListDiagnostics
    table
    context
    objectProperties ++
  dataPropertyExpressionListDiagnostics table dataProperties
structuralAxiomDiagnostics table context (rawSameIndividual individuals) =
  atLeastTwoIndividualListDiagnostics table individuals
structuralAxiomDiagnostics table context (rawDifferentIndividuals individuals) =
  atLeastTwoIndividualListDiagnostics table individuals
structuralAxiomDiagnostics table context (rawClassAssertion class individual) =
  classExpressionDiagnostics table context class ++
  individualDiagnostics table individual
structuralAxiomDiagnostics
  table
  context
  (rawObjectPropertyAssertion property subject object) =
  objectPropertyExpressionDiagnostics table property ++
  individualDiagnostics table subject ++
  individualDiagnostics table object
structuralAxiomDiagnostics
  table
  context
  (rawNegativeObjectPropertyAssertion property subject object) =
  objectPropertyExpressionDiagnostics table property ++
  individualDiagnostics table subject ++
  individualDiagnostics table object
structuralAxiomDiagnostics
  table
  context
  (rawDataPropertyAssertion property subject literal) =
  dataPropertyExpressionDiagnostics table property ++
  individualDiagnostics table subject ++
  literalDiagnostics table literal
structuralAxiomDiagnostics
  table
  context
  (rawNegativeDataPropertyAssertion property subject literal) =
  dataPropertyExpressionDiagnostics table property ++
  individualDiagnostics table subject ++
  literalDiagnostics table literal
structuralAxiomDiagnostics
  table
  context
  (rawAnnotationAssertion property subject value) =
  annotationPropertyDiagnostics table property ++
  annotationSubjectDiagnostics table subject ++
  annotationValueDiagnostics table value
structuralAxiomDiagnostics table context (rawSubAnnotationPropertyOf sub sup) =
  annotationPropertyDiagnostics table sub ++
  annotationPropertyDiagnostics table sup
structuralAxiomDiagnostics table context (rawAnnotationPropertyDomain property iri) =
  annotationPropertyDiagnostics table property ++
  annotationIRIDiagnostics table iri
structuralAxiomDiagnostics table context (rawAnnotationPropertyRange property iri) =
  annotationPropertyDiagnostics table property ++
  annotationIRIDiagnostics table iri
structuralAxiomDiagnostics table context (rawUnsupportedAxiom reason) =
  singleDiagnostic structuralUnsupportedAxiomDiagnostic

annotatedStructuralDiagnostics :
  (table : SymbolTable) →
  K.RegularityContext (symbolTableSignature table) →
  RawAnnotated RawAxiom →
  Diagnostics
annotatedStructuralDiagnostics table context axiom =
  annotationsDiagnostics table (annotations axiom) ++
  structuralAxiomDiagnostics table context (body axiom)

structuralAxiomsDiagnostics :
  (table : SymbolTable) →
  K.RegularityContext (symbolTableSignature table) →
  List (RawAnnotated RawAxiom) →
  Diagnostics
structuralAxiomsDiagnostics table context [] =
  noDiagnostics
structuralAxiomsDiagnostics table context (axiom ∷ axioms) =
  annotatedStructuralDiagnostics table context axiom ++
  structuralAxiomsDiagnostics table context axioms

structuralImportsDiagnostics : List RawIRI → Diagnostics
structuralImportsDiagnostics [] =
  noDiagnostics
structuralImportsDiagnostics (iri ∷ imports) =
  singleDiagnostic structuralUnsupportedImportDiagnostic

structuralImportsDiagnosticsClosed :
  (rawImports : List RawIRI) →
  CleanDiagnostics (structuralImportsDiagnostics rawImports) →
  rawImports ≡ []
structuralImportsDiagnosticsClosed [] clean =
  refl
structuralImportsDiagnosticsClosed (iri ∷ imports) ()

structuralOntologyIRIDiagnostics : Optional RawIRI → Diagnostics
structuralOntologyIRIDiagnostics absent =
  noDiagnostics
structuralOntologyIRIDiagnostics (present iri) =
  singleDiagnostic structuralUnsupportedOntologyIRIDiagnostic

structuralVersionIRIDiagnostics : Optional RawIRI → Diagnostics
structuralVersionIRIDiagnostics absent =
  noDiagnostics
structuralVersionIRIDiagnostics (present iri) =
  singleDiagnostic structuralUnsupportedVersionIRIDiagnostic

structuralElaborationDiagnostics : RawOntology → Diagnostics
structuralElaborationDiagnostics raw =
  structuralImportsDiagnostics (imports raw) ++
  structuralOntologyIRIDiagnostics (ontologyIRI raw) ++
  structuralVersionIRIDiagnostics (versionIRI raw) ++
  annotationsDiagnostics table (annotations raw) ++
  rawPunningDiagnosticsFromSymbolTable table ++
  structuralAxiomsDiagnostics table context (axioms raw)
  where
  table : SymbolTable
  table =
    symbolTableFromRaw raw

  context : K.RegularityContext (symbolTableSignature table)
  context =
    structuralRegularityContext table (axioms raw)

structuralRawImportsClosed :
  (raw : RawOntology) →
  CleanDiagnostics (structuralElaborationDiagnostics raw) →
  imports raw ≡ []
structuralRawImportsClosed raw clean =
  structuralImportsDiagnosticsClosed
    (imports raw)
    (cleanAppendLeft
      (structuralImportsDiagnostics (imports raw))
      (structuralOntologyIRIDiagnostics (ontologyIRI raw) ++
       structuralVersionIRIDiagnostics (versionIRI raw) ++
       annotationsDiagnostics table (annotations raw) ++
       rawPunningDiagnosticsFromSymbolTable table ++
       structuralAxiomsDiagnostics table context (axioms raw))
      clean)
  where
  table : SymbolTable
  table =
    symbolTableFromRaw raw

  context : K.RegularityContext (symbolTableSignature table)
  context =
    structuralRegularityContext table (axioms raw)

private
  structuralObjectPropertyExpression :
    (table : SymbolTable) →
    RawObjectPropertyExpression →
    Optional (K.ObjectPropertyExpression (symbolTableSignature table))
  structuralObjectPropertyExpression table (rawObjectProperty iri) with
    objectPropertyLookup table iri
  ... | present name =
    present (K.objectProperty name)
  ... | absent =
    absent
  structuralObjectPropertyExpression table rawTopObjectProperty =
    present K.topObjectProperty
  structuralObjectPropertyExpression table rawBottomObjectProperty =
    present K.bottomObjectProperty
  structuralObjectPropertyExpression table (rawObjectInverseOf property) with
    structuralObjectPropertyExpression table property
  ... | present property′ =
    present (K.objectInverseOf property′)
  ... | absent =
    absent

  simpleObjectPropertyNameFromEvidence :
    {table : SymbolTable} →
    (name : K.ObjectPropertyName (symbolTableSignature table)) →
    Optional (K.SimpleObjectProperty (symbolTableSignature table) name) →
    Optional (K.SimpleObjectPropertyName (symbolTableSignature table))
  simpleObjectPropertyNameFromEvidence name (present simple) =
    present (K.simpleObjectPropertyName name simple)
  simpleObjectPropertyNameFromEvidence name absent =
    absent

  structuralSimpleObjectPropertyName :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    RawObjectPropertyExpression →
    Optional (K.SimpleObjectPropertyName (symbolTableSignature table))
  structuralSimpleObjectPropertyName table context (rawObjectProperty iri) with
    objectPropertyLookup table iri
  ... | present name =
    simpleObjectPropertyNameFromEvidence
      name
      (K.simpleObjectPropertyEvidence? context name)
  ... | absent =
    absent
  structuralSimpleObjectPropertyName table context rawTopObjectProperty =
    absent
  structuralSimpleObjectPropertyName table context rawBottomObjectProperty =
    absent
  structuralSimpleObjectPropertyName table context (rawObjectInverseOf property) =
    absent

  structuralObjectPropertyExpressionList :
    (table : SymbolTable) →
    List RawObjectPropertyExpression →
    Optional (List (K.ObjectPropertyExpression (symbolTableSignature table)))
  structuralObjectPropertyExpressionList table [] =
    present []
  structuralObjectPropertyExpressionList table (property ∷ properties) with
    structuralObjectPropertyExpression table property |
    structuralObjectPropertyExpressionList table properties
  ... | present property′ | present properties′ =
    present (property′ ∷ properties′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent

  structuralAtLeastTwoObjectPropertyExpressionList :
    (table : SymbolTable) →
    List RawObjectPropertyExpression →
    Optional
      (K.AtLeastTwo (K.ObjectPropertyExpression (symbolTableSignature table)))
  structuralAtLeastTwoObjectPropertyExpressionList table [] =
    absent
  structuralAtLeastTwoObjectPropertyExpressionList table (property ∷ []) =
    absent
  structuralAtLeastTwoObjectPropertyExpressionList
    table
    (first ∷ second ∷ rest) with
    structuralObjectPropertyExpression table first |
    structuralObjectPropertyExpression table second |
    structuralObjectPropertyExpressionList table rest
  ... | present first′ | present second′ | present rest′ =
    present (K.atLeastTwo first′ second′ rest′)
  ... | absent | _ | _ =
    absent
  ... | _ | absent | _ =
    absent
  ... | _ | _ | absent =
    absent

  structuralSimpleObjectPropertyNameList :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    List RawObjectPropertyExpression →
    Optional (List (K.SimpleObjectPropertyName (symbolTableSignature table)))
  structuralSimpleObjectPropertyNameList table context [] =
    present []
  structuralSimpleObjectPropertyNameList table context (property ∷ properties) with
    structuralSimpleObjectPropertyName table context property |
    structuralSimpleObjectPropertyNameList table context properties
  ... | present property′ | present properties′ =
    present (property′ ∷ properties′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent

  structuralAtLeastTwoSimpleObjectPropertyNameList :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    List RawObjectPropertyExpression →
    Optional
      (K.AtLeastTwo (K.SimpleObjectPropertyName (symbolTableSignature table)))
  structuralAtLeastTwoSimpleObjectPropertyNameList table context [] =
    absent
  structuralAtLeastTwoSimpleObjectPropertyNameList table context (property ∷ []) =
    absent
  structuralAtLeastTwoSimpleObjectPropertyNameList
    table
    context
    (first ∷ second ∷ rest) with
    structuralSimpleObjectPropertyName table context first |
    structuralSimpleObjectPropertyName table context second |
    structuralSimpleObjectPropertyNameList table context rest
  ... | present first′ | present second′ | present rest′ =
    present (K.atLeastTwo first′ second′ rest′)
  ... | absent | _ | _ =
    absent
  ... | _ | absent | _ =
    absent
  ... | _ | _ | absent =
    absent

  structuralSubObjectPropertyExpression :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    RawSubObjectPropertyExpression →
    Optional (K.SubObjectPropertyExpression (symbolTableSignature table))
  structuralSubObjectPropertyExpression
    table
    context
    (rawSubObjectProperty property) with
    structuralObjectPropertyExpression table property
  ... | present property′ =
    present (K.subObjectProperty property′)
  ... | absent =
    absent
  structuralSubObjectPropertyExpression
    table
    context
    (rawSubObjectPropertyChain properties) with
    structuralAtLeastTwoObjectPropertyExpressionList table properties
  ... | present properties′ =
    present
      (K.subObjectPropertyChain (K.objectPropertyChain properties′))
  ... | absent =
    absent

  structuralDataPropertyExpression :
    (table : SymbolTable) →
    RawDataPropertyExpression →
    Optional (K.DataPropertyExpression (symbolTableSignature table))
  structuralDataPropertyExpression table (rawDataProperty iri) with
    dataPropertyLookup table iri
  ... | present name =
    present (K.dataProperty name)
  ... | absent =
    absent
  structuralDataPropertyExpression table rawTopDataProperty =
    present K.topDataProperty
  structuralDataPropertyExpression table rawBottomDataProperty =
    present K.bottomDataProperty

  structuralDataPropertyExpressionList :
    (table : SymbolTable) →
    List RawDataPropertyExpression →
    Optional (List (K.DataPropertyExpression (symbolTableSignature table)))
  structuralDataPropertyExpressionList table [] =
    present []
  structuralDataPropertyExpressionList table (property ∷ properties) with
    structuralDataPropertyExpression table property |
    structuralDataPropertyExpressionList table properties
  ... | present property′ | present properties′ =
    present (property′ ∷ properties′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent

  structuralAtLeastTwoDataPropertyExpressionList :
    (table : SymbolTable) →
    List RawDataPropertyExpression →
    Optional (K.AtLeastTwo (K.DataPropertyExpression (symbolTableSignature table)))
  structuralAtLeastTwoDataPropertyExpressionList table [] =
    absent
  structuralAtLeastTwoDataPropertyExpressionList table (property ∷ []) =
    absent
  structuralAtLeastTwoDataPropertyExpressionList table (first ∷ second ∷ rest) with
    structuralDataPropertyExpression table first |
    structuralDataPropertyExpression table second |
    structuralDataPropertyExpressionList table rest
  ... | present first′ | present second′ | present rest′ =
    present (K.atLeastTwo first′ second′ rest′)
  ... | absent | _ | _ =
    absent
  ... | _ | absent | _ =
    absent
  ... | _ | _ | absent =
    absent

  structuralTypedLiteral :
    (table : SymbolTable) →
    String →
    RawIRI →
    Optional (K.Literal (symbolTableSignature table))
  structuralTypedLiteral table lexical iri with datatypeLookup table iri
  ... | present name =
    present (K.typedLiteral lexical name (K.trivialLiteralSupported name))
  ... | absent =
    absent

  structuralLiteral :
    (table : SymbolTable) →
    RawLiteral →
    Optional (K.Literal (symbolTableSignature table))
  structuralLiteral table literal with datatypeIRI literal | languageTag literal
  ... | present iri | absent =
    structuralTypedLiteral table (lexicalForm literal) iri
  ... | _ | _ =
    absent

  structuralLiteralList :
    (table : SymbolTable) →
    List RawLiteral →
    Optional (List (K.Literal (symbolTableSignature table)))
  structuralLiteralList table [] =
    present []
  structuralLiteralList table (literal ∷ literals) with
    structuralLiteral table literal |
    structuralLiteralList table literals
  ... | present literal′ | present literals′ =
    present (literal′ ∷ literals′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent

  structuralNonEmptyLiteralList :
    (table : SymbolTable) →
    List RawLiteral →
    Optional (K.NonEmpty (K.Literal (symbolTableSignature table)))
  structuralNonEmptyLiteralList table [] =
    absent
  structuralNonEmptyLiteralList table (literal ∷ literals) with
    structuralLiteral table literal |
    structuralLiteralList table literals
  ... | present literal′ | present literals′ =
    present (K.nonEmpty literal′ literals′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent

  structuralFacetRestriction :
    (table : SymbolTable) →
    RawFacetRestriction →
    Optional (K.FacetRestriction (symbolTableSignature table))
  structuralFacetRestriction table restriction with
    facetLookup table (facet restriction) |
    structuralLiteral table (value restriction)
  ... | present facet′ | present value′ =
    present (K.facetRestriction facet′ value′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent

  structuralFacetRestrictions :
    (table : SymbolTable) →
    List RawFacetRestriction →
    Optional (List (K.FacetRestriction (symbolTableSignature table)))
  structuralFacetRestrictions table [] =
    present []
  structuralFacetRestrictions table (restriction ∷ restrictions) with
    structuralFacetRestriction table restriction |
    structuralFacetRestrictions table restrictions
  ... | present restriction′ | present restrictions′ =
    present (restriction′ ∷ restrictions′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent

  structuralAnnotationSubject :
    (table : SymbolTable) →
    RawAnnotationSubject →
    Optional (K.AnnotationSubject (symbolTableSignature table))
  structuralAnnotationSubject table (rawAnnotationSubjectIRI iri) with
    annotationIRILookup table iri
  ... | present iri′ =
    present (K.annotationSubjectIRI iri′)
  ... | absent =
    absent
  structuralAnnotationSubject table (rawAnnotationSubjectAnonymous name) with
    annotationBlankNodeLookup table name
  ... | present name′ =
    present (K.annotationSubjectAnonymous name′)
  ... | absent =
    absent

  structuralAnnotationValue :
    (table : SymbolTable) →
    RawAnnotationValue →
    Optional (K.AnnotationValue (symbolTableSignature table))
  structuralAnnotationValue table (rawAnnotationValueIRI iri) with
    annotationIRILookup table iri
  ... | present iri′ =
    present (K.annotationValueIRI iri′)
  ... | absent =
    absent
  structuralAnnotationValue table (rawAnnotationValueAnonymous name) with
    annotationBlankNodeLookup table name
  ... | present name′ =
    present (K.annotationValueAnonymous name′)
  ... | absent =
    absent
  structuralAnnotationValue table (rawAnnotationValueLiteral literal) with
    structuralLiteral table literal
  ... | present literal′ =
    present (K.annotationValueLiteral literal′)
  ... | absent =
    absent

  appendAnnotationOptional :
    ∀ {ℓ} {A : Type ℓ} →
    Optional A →
    List A →
    List A
  appendAnnotationOptional absent values =
    values
  appendAnnotationOptional (present value) values =
    value ∷ values

  mutual
    structuralAnnotation :
      (table : SymbolTable) →
      RawAnnotation →
      Optional (K.Annotation (symbolTableSignature table))
    structuralAnnotation table (rawAnnotation annotations property value) with
      annotationPropertyLookup table property |
      structuralAnnotationValue table value
    ... | present property′ | present value′ =
      present
        (K.annotation
          (structuralAnnotations table annotations)
          property′
          value′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent

    structuralAnnotations :
      (table : SymbolTable) →
      List RawAnnotation →
      List (K.Annotation (symbolTableSignature table))
    structuralAnnotations table [] =
      []
    structuralAnnotations table (annotation ∷ annotations) =
      appendAnnotationOptional
        (structuralAnnotation table annotation)
        (structuralAnnotations table annotations)

  mutual
    structuralDataRangeList :
      (table : SymbolTable) →
      List RawDataRange →
      Optional (List (K.DataRange (symbolTableSignature table)))
    structuralDataRangeList table [] =
      present []
    structuralDataRangeList table (range ∷ ranges) with
      structuralDataRange table range |
      structuralDataRangeList table ranges
    ... | present range′ | present ranges′ =
      present (range′ ∷ ranges′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent

    structuralNonEmptyDataRangeList :
      (table : SymbolTable) →
      List RawDataRange →
      Optional (K.NonEmpty (K.DataRange (symbolTableSignature table)))
    structuralNonEmptyDataRangeList table [] =
      absent
    structuralNonEmptyDataRangeList table (range ∷ ranges) with
      structuralDataRange table range |
      structuralDataRangeList table ranges
    ... | present range′ | present ranges′ =
      present (K.nonEmpty range′ ranges′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent

    structuralDataRange :
      (table : SymbolTable) →
      RawDataRange →
      Optional (K.DataRange (symbolTableSignature table))
    structuralDataRange table (rawDatatype iri) with datatypeLookup table iri
    ... | present name =
      present (K.datatype name (K.trivialDatatypeSupported name))
    ... | absent =
      absent
    structuralDataRange table (rawDatatypeRestriction iri restrictions) with
      datatypeLookup table iri |
      structuralFacetRestrictions table restrictions
    ... | present name | present restrictions′ =
      present
        (K.datatypeRestriction
          name
          (K.trivialDatatypeSupported name)
          restrictions′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent
    structuralDataRange table rawDataTop =
      present K.dataTop
    structuralDataRange table rawDataBottom =
      present K.dataBottom
    structuralDataRange table (rawDataComplementOf range) with
      structuralDataRange table range
    ... | present range′ =
      present (K.dataComplementOf range′)
    ... | absent =
      absent
    structuralDataRange table (rawDataIntersectionOf ranges) with
      structuralNonEmptyDataRangeList table ranges
    ... | present ranges′ =
      present (K.dataIntersectionOf ranges′)
    ... | absent =
      absent
    structuralDataRange table (rawDataUnionOf ranges) with
      structuralNonEmptyDataRangeList table ranges
    ... | present ranges′ =
      present (K.dataUnionOf ranges′)
    ... | absent =
      absent
    structuralDataRange table (rawDataOneOf literals) with
      structuralNonEmptyLiteralList table literals
    ... | present literals′ =
      present (K.dataOneOf literals′)
    ... | absent =
      absent

  structuralOptionalDataRange :
    (table : SymbolTable) →
    Optional RawDataRange →
    Optional (Optional (K.DataRange (symbolTableSignature table)))
  structuralOptionalDataRange table absent =
    present absent
  structuralOptionalDataRange table (present range) with structuralDataRange table range
  ... | present range′ =
    present (present range′)
  ... | absent =
    absent

  structuralIndividual :
    (table : SymbolTable) →
    RawIndividual →
    Optional (K.Individual (symbolTableSignature table))
  structuralIndividual table (rawNamedIndividual iri) with
    individualLookup table iri
  ... | present name =
    present (K.namedIndividual name)
  ... | absent =
    absent
  structuralIndividual table (rawAnonymousIndividual name) =
    absent

  structuralIndividualList :
    (table : SymbolTable) →
    List RawIndividual →
    Optional (List (K.Individual (symbolTableSignature table)))
  structuralIndividualList table [] =
    present []
  structuralIndividualList table (individual ∷ individuals) with
    structuralIndividual table individual |
    structuralIndividualList table individuals
  ... | present individual′ | present individuals′ =
    present (individual′ ∷ individuals′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent

  structuralNonEmptyIndividualList :
    (table : SymbolTable) →
    List RawIndividual →
    Optional (K.NonEmpty (K.Individual (symbolTableSignature table)))
  structuralNonEmptyIndividualList table [] =
    absent
  structuralNonEmptyIndividualList table (individual ∷ individuals) with
    structuralIndividual table individual |
    structuralIndividualList table individuals
  ... | present individual′ | present individuals′ =
    present (K.nonEmpty individual′ individuals′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent

  structuralAtLeastTwoIndividualList :
    (table : SymbolTable) →
    List RawIndividual →
    Optional (K.AtLeastTwo (K.Individual (symbolTableSignature table)))
  structuralAtLeastTwoIndividualList table [] =
    absent
  structuralAtLeastTwoIndividualList table (individual ∷ []) =
    absent
  structuralAtLeastTwoIndividualList table (first ∷ second ∷ rest) with
    structuralIndividual table first |
    structuralIndividual table second |
    structuralIndividualList table rest
  ... | present first′ | present second′ | present rest′ =
    present (K.atLeastTwo first′ second′ rest′)
  ... | absent | _ | _ =
    absent
  ... | _ | absent | _ =
    absent
  ... | _ | _ | absent =
    absent

  mutual
    structuralClassExpressionList :
      (table : SymbolTable) →
      K.RegularityContext (symbolTableSignature table) →
      List RawClassExpression →
      Optional (List (K.ClassExpression (symbolTableSignature table)))
    structuralClassExpressionList table context [] =
      present []
    structuralClassExpressionList table context (class ∷ classes) with
      structuralClassExpression table context class |
      structuralClassExpressionList table context classes
    ... | present class′ | present classes′ =
      present (class′ ∷ classes′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent

    structuralNonEmptyClassExpressionList :
      (table : SymbolTable) →
      K.RegularityContext (symbolTableSignature table) →
      List RawClassExpression →
      Optional (K.NonEmpty (K.ClassExpression (symbolTableSignature table)))
    structuralNonEmptyClassExpressionList table context [] =
      absent
    structuralNonEmptyClassExpressionList table context (class ∷ classes) with
      structuralClassExpression table context class |
      structuralClassExpressionList table context classes
    ... | present class′ | present classes′ =
      present (K.nonEmpty class′ classes′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent

    structuralAtLeastTwoClassExpressionList :
      (table : SymbolTable) →
      K.RegularityContext (symbolTableSignature table) →
      List RawClassExpression →
      Optional (K.AtLeastTwo (K.ClassExpression (symbolTableSignature table)))
    structuralAtLeastTwoClassExpressionList table context [] =
      absent
    structuralAtLeastTwoClassExpressionList table context (class ∷ []) =
      absent
    structuralAtLeastTwoClassExpressionList
      table
      context
      (first ∷ second ∷ rest) with
      structuralClassExpression table context first |
      structuralClassExpression table context second |
      structuralClassExpressionList table context rest
    ... | present first′ | present second′ | present rest′ =
      present (K.atLeastTwo first′ second′ rest′)
    ... | absent | _ | _ =
      absent
    ... | _ | absent | _ =
      absent
    ... | _ | _ | absent =
      absent

    structuralOptionalClassExpression :
      (table : SymbolTable) →
      K.RegularityContext (symbolTableSignature table) →
      Optional RawClassExpression →
      Optional (Optional (K.ClassExpression (symbolTableSignature table)))
    structuralOptionalClassExpression table context absent =
      present absent
    structuralOptionalClassExpression table context (present class) with
      structuralClassExpression table context class
    ... | present class′ =
      present (present class′)
    ... | absent =
      absent

    structuralClassExpression :
      (table : SymbolTable) →
      K.RegularityContext (symbolTableSignature table) →
      RawClassExpression →
      Optional (K.ClassExpression (symbolTableSignature table))
    structuralClassExpression table context (rawNamedClass iri)
      with classLookup table iri
    ... | present name =
      present (K.namedClass name)
    ... | absent =
      absent
    structuralClassExpression table context rawOwlThing =
      present K.owlThing
    structuralClassExpression table context rawOwlNothing =
      present K.owlNothing
    structuralClassExpression table context (rawObjectIntersectionOf classes) with
      structuralNonEmptyClassExpressionList table context classes
    ... | present classes′ =
      present (K.objectIntersectionOf classes′)
    ... | absent =
      absent
    structuralClassExpression table context (rawObjectUnionOf classes) with
      structuralNonEmptyClassExpressionList table context classes
    ... | present classes′ =
      present (K.objectUnionOf classes′)
    ... | absent =
      absent
    structuralClassExpression table context (rawObjectOneOf individuals) with
      structuralNonEmptyIndividualList table individuals
    ... | present individuals′ =
      present (K.objectOneOf individuals′)
    ... | absent =
      absent
    structuralClassExpression table context (rawObjectComplementOf class) with
      structuralClassExpression table context class
    ... | present class′ =
      present (K.objectComplementOf class′)
    ... | absent =
      absent
    structuralClassExpression
      table
      context
      (rawObjectSomeValuesFrom property class) with
      structuralObjectPropertyExpression table property |
      structuralClassExpression table context class
    ... | present property′ | present class′ =
      present (K.objectSomeValuesFrom property′ class′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent
    structuralClassExpression
      table
      context
      (rawObjectAllValuesFrom property class) with
      structuralObjectPropertyExpression table property |
      structuralClassExpression table context class
    ... | present property′ | present class′ =
      present (K.objectAllValuesFrom property′ class′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent
    structuralClassExpression
      table
      context
      (rawObjectHasValue property individual) with
      structuralObjectPropertyExpression table property |
      structuralIndividual table individual
    ... | present property′ | present individual′ =
      present (K.objectHasValue property′ individual′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent
    structuralClassExpression table context (rawObjectHasSelf property) with
      structuralSimpleObjectPropertyName table context property
    ... | present property′ =
      present (K.objectHasSelf property′)
    ... | absent =
      absent
    structuralClassExpression
      table
      context
      (rawObjectMinCardinality n property class) with
      structuralSimpleObjectPropertyName table context property |
      structuralOptionalClassExpression table context class
    ... | present property′ | present class′ =
      present (K.objectMinCardinality n property′ class′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent
    structuralClassExpression
      table
      context
      (rawObjectMaxCardinality n property class) with
      structuralSimpleObjectPropertyName table context property |
      structuralOptionalClassExpression table context class
    ... | present property′ | present class′ =
      present (K.objectMaxCardinality n property′ class′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent
    structuralClassExpression
      table
      context
      (rawObjectExactCardinality n property class) with
      structuralSimpleObjectPropertyName table context property |
      structuralOptionalClassExpression table context class
    ... | present property′ | present class′ =
      present (K.objectExactCardinality n property′ class′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent
    structuralClassExpression table context (rawDataSomeValuesFrom property range) =
      structuralDataSomeValuesFrom table property range
    structuralClassExpression table context (rawDataAllValuesFrom property range) =
      structuralDataAllValuesFrom table property range
    structuralClassExpression table context (rawDataHasValue property literal) =
      structuralDataHasValue table property literal
    structuralClassExpression table context (rawDataMinCardinality n property range) =
      structuralDataMinCardinality table n property range
    structuralClassExpression table context (rawDataMaxCardinality n property range) =
      structuralDataMaxCardinality table n property range
    structuralClassExpression table context (rawDataExactCardinality n property range) =
      structuralDataExactCardinality table n property range

    structuralDataSomeValuesFrom :
      (table : SymbolTable) →
      RawDataPropertyExpression →
      RawDataRange →
      Optional (K.ClassExpression (symbolTableSignature table))
    structuralDataSomeValuesFrom table property range with
      structuralDataPropertyExpression table property |
      structuralDataRange table range
    ... | present property′ | present range′ =
      present (K.dataSomeValuesFrom property′ range′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent

    structuralDataAllValuesFrom :
      (table : SymbolTable) →
      RawDataPropertyExpression →
      RawDataRange →
      Optional (K.ClassExpression (symbolTableSignature table))
    structuralDataAllValuesFrom table property range with
      structuralDataPropertyExpression table property |
      structuralDataRange table range
    ... | present property′ | present range′ =
      present (K.dataAllValuesFrom property′ range′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent

    structuralDataHasValue :
      (table : SymbolTable) →
      RawDataPropertyExpression →
      RawLiteral →
      Optional (K.ClassExpression (symbolTableSignature table))
    structuralDataHasValue table property literal with
      structuralDataPropertyExpression table property |
      structuralLiteral table literal
    ... | present property′ | present literal′ =
      present (K.dataHasValue property′ literal′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent

    structuralDataMinCardinality :
      (table : SymbolTable) →
      ℕ →
      RawDataPropertyExpression →
      Optional RawDataRange →
      Optional (K.ClassExpression (symbolTableSignature table))
    structuralDataMinCardinality table n property range with
      structuralDataPropertyExpression table property |
      structuralOptionalDataRange table range
    ... | present property′ | present range′ =
      present (K.dataMinCardinality n property′ range′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent

    structuralDataMaxCardinality :
      (table : SymbolTable) →
      ℕ →
      RawDataPropertyExpression →
      Optional RawDataRange →
      Optional (K.ClassExpression (symbolTableSignature table))
    structuralDataMaxCardinality table n property range with
      structuralDataPropertyExpression table property |
      structuralOptionalDataRange table range
    ... | present property′ | present range′ =
      present (K.dataMaxCardinality n property′ range′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent

    structuralDataExactCardinality :
      (table : SymbolTable) →
      ℕ →
      RawDataPropertyExpression →
      Optional RawDataRange →
      Optional (K.ClassExpression (symbolTableSignature table))
    structuralDataExactCardinality table n property range with
      structuralDataPropertyExpression table property |
      structuralOptionalDataRange table range
    ... | present property′ | present range′ =
      present (K.dataExactCardinality n property′ range′)
    ... | absent | _ =
      absent
    ... | _ | absent =
      absent

  structuralAxiom :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    RawAxiom →
    Optional (K.Axiom (symbolTableSignature table))
  structuralAxiom table context (rawDeclaration entity) =
    entityDeclarationAxiom table entity
  structuralAxiom table context (rawSubClassOf sub sup) with
    structuralClassExpression table context sub |
    structuralClassExpression table context sup
  ... | present sub′ | present sup′ =
    present (K.subClassOf sub′ sup′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom table context (rawEquivalentClasses classes) with
    structuralAtLeastTwoClassExpressionList table context classes
  ... | present classes′ =
    present (K.equivalentClasses classes′)
  ... | absent =
    absent
  structuralAxiom table context (rawDisjointClasses classes) with
    structuralAtLeastTwoClassExpressionList table context classes
  ... | present classes′ =
    present (K.disjointClasses classes′)
  ... | absent =
    absent
  structuralAxiom table context (rawDisjointUnion class classes) with
    classLookup table class |
    structuralAtLeastTwoClassExpressionList table context classes
  ... | present class′ | present classes′ =
    present (K.disjointUnion class′ classes′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom
    table
    context
    (rawSubObjectPropertyOf (rawSubObjectPropertyChain properties) sup) =
    absent
  structuralAxiom
    table
    context
    (rawSubObjectPropertyOf (rawSubObjectProperty sub) sup) with
    structuralObjectPropertyExpression table sub |
    structuralObjectPropertyExpression table sup
  ... | present sub′ | present sup′ =
    present (K.subObjectPropertyOf (K.subObjectProperty sub′) sup′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom table context (rawEquivalentObjectProperties properties) with
    structuralAtLeastTwoObjectPropertyExpressionList table properties
  ... | present properties′ =
    present (K.equivalentObjectProperties properties′)
  ... | absent =
    absent
  structuralAxiom table context (rawDisjointObjectProperties properties) with
    structuralAtLeastTwoSimpleObjectPropertyNameList table context properties
  ... | present properties′ =
    present (K.disjointObjectProperties properties′)
  ... | absent =
    absent
  structuralAxiom table context (rawInverseObjectProperties left right) with
    structuralObjectPropertyExpression table left |
    structuralObjectPropertyExpression table right
  ... | present left′ | present right′ =
    present (K.inverseObjectProperties left′ right′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom table context (rawObjectPropertyDomain property class) with
    structuralObjectPropertyExpression table property |
    structuralClassExpression table context class
  ... | present property′ | present class′ =
    present (K.objectPropertyDomain property′ class′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom table context (rawObjectPropertyRange property class) with
    structuralObjectPropertyExpression table property |
    structuralClassExpression table context class
  ... | present property′ | present class′ =
    present (K.objectPropertyRange property′ class′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom table context (rawFunctionalObjectProperty property) with
    structuralSimpleObjectPropertyName table context property
  ... | present property′ =
    present (K.functionalObjectProperty property′)
  ... | absent =
    absent
  structuralAxiom table context (rawInverseFunctionalObjectProperty property) with
    structuralSimpleObjectPropertyName table context property
  ... | present property′ =
    present (K.inverseFunctionalObjectProperty property′)
  ... | absent =
    absent
  structuralAxiom table context (rawReflexiveObjectProperty property) with
    structuralObjectPropertyExpression table property
  ... | present property′ =
    present (K.reflexiveObjectProperty property′)
  ... | absent =
    absent
  structuralAxiom table context (rawIrreflexiveObjectProperty property) with
    structuralSimpleObjectPropertyName table context property
  ... | present property′ =
    present (K.irreflexiveObjectProperty property′)
  ... | absent =
    absent
  structuralAxiom table context (rawSymmetricObjectProperty property) with
    structuralObjectPropertyExpression table property
  ... | present property′ =
    present (K.symmetricObjectProperty property′)
  ... | absent =
    absent
  structuralAxiom table context (rawAsymmetricObjectProperty property) with
    structuralSimpleObjectPropertyName table context property
  ... | present property′ =
    present (K.asymmetricObjectProperty property′)
  ... | absent =
    absent
  structuralAxiom table context (rawTransitiveObjectProperty property) with
    structuralObjectPropertyExpression table property
  ... | present property′ =
    present (K.transitiveObjectProperty property′)
  ... | absent =
    absent
  structuralAxiom table context (rawSubDataPropertyOf sub sup) with
    structuralDataPropertyExpression table sub |
    structuralDataPropertyExpression table sup
  ... | present sub′ | present sup′ =
    present (K.subDataPropertyOf sub′ sup′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom table context (rawEquivalentDataProperties properties) with
    structuralAtLeastTwoDataPropertyExpressionList table properties
  ... | present properties′ =
    present (K.equivalentDataProperties properties′)
  ... | absent =
    absent
  structuralAxiom table context (rawDisjointDataProperties properties) with
    structuralAtLeastTwoDataPropertyExpressionList table properties
  ... | present properties′ =
    present (K.disjointDataProperties properties′)
  ... | absent =
    absent
  structuralAxiom table context (rawDataPropertyDomain property class) with
    structuralDataPropertyExpression table property |
    structuralClassExpression table context class
  ... | present property′ | present class′ =
    present (K.dataPropertyDomain property′ class′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom table context (rawDataPropertyRange property range) with
    structuralDataPropertyExpression table property |
    structuralDataRange table range
  ... | present property′ | present range′ =
    present (K.dataPropertyRange property′ range′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom table context (rawFunctionalDataProperty property) with
    structuralDataPropertyExpression table property
  ... | present property′ =
    present (K.functionalDataProperty property′)
  ... | absent =
    absent
  structuralAxiom table context (rawDatatypeDefinition datatype range) with
    datatypeLookup table datatype |
    structuralDataRange table range
  ... | present datatype′ | present range′ =
    present
      (K.datatypeDefinition
        datatype′
        (K.trivialDatatypeSupported datatype′)
        range′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom
    table
    context
    (rawHasKey class objectProperties dataProperties) with
    structuralClassExpression table context class |
    structuralSimpleObjectPropertyNameList table context objectProperties |
    structuralDataPropertyExpressionList table dataProperties
  ... | present class′ | present objectProperties′ | present dataProperties′ =
    present
      (K.hasKey
        class′
        (K.propertyKey objectProperties′ dataProperties′))
  ... | absent | _ | _ =
    absent
  ... | _ | absent | _ =
    absent
  ... | _ | _ | absent =
    absent
  structuralAxiom table context (rawSameIndividual individuals) with
    structuralAtLeastTwoIndividualList table individuals
  ... | present individuals′ =
    present (K.sameIndividual individuals′)
  ... | absent =
    absent
  structuralAxiom table context (rawDifferentIndividuals individuals) with
    structuralAtLeastTwoIndividualList table individuals
  ... | present individuals′ =
    present (K.differentIndividuals individuals′)
  ... | absent =
    absent
  structuralAxiom table context (rawClassAssertion class individual) with
    structuralClassExpression table context class |
    structuralIndividual table individual
  ... | present class′ | present individual′ =
    present (K.classAssertion class′ individual′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom
    table
    context
    (rawObjectPropertyAssertion property subject object) with
    structuralObjectPropertyExpression table property |
    structuralIndividual table subject |
    structuralIndividual table object
  ... | present property′ | present subject′ | present object′ =
    present (K.objectPropertyAssertion property′ subject′ object′)
  ... | absent | _ | _ =
    absent
  ... | _ | absent | _ =
    absent
  ... | _ | _ | absent =
    absent
  structuralAxiom
    table
    context
    (rawNegativeObjectPropertyAssertion property subject object) with
    structuralObjectPropertyExpression table property |
    structuralIndividual table subject |
    structuralIndividual table object
  ... | present property′ | present subject′ | present object′ =
    present (K.negativeObjectPropertyAssertion property′ subject′ object′)
  ... | absent | _ | _ =
    absent
  ... | _ | absent | _ =
    absent
  ... | _ | _ | absent =
    absent
  structuralAxiom
    table
    context
    (rawDataPropertyAssertion property subject literal) with
    structuralDataPropertyExpression table property |
    structuralIndividual table subject |
    structuralLiteral table literal
  ... | present property′ | present subject′ | present literal′ =
    present (K.dataPropertyAssertion property′ subject′ literal′)
  ... | absent | _ | _ =
    absent
  ... | _ | absent | _ =
    absent
  ... | _ | _ | absent =
    absent
  structuralAxiom
    table
    context
    (rawNegativeDataPropertyAssertion property subject literal) with
    structuralDataPropertyExpression table property |
    structuralIndividual table subject |
    structuralLiteral table literal
  ... | present property′ | present subject′ | present literal′ =
    present (K.negativeDataPropertyAssertion property′ subject′ literal′)
  ... | absent | _ | _ =
    absent
  ... | _ | absent | _ =
    absent
  ... | _ | _ | absent =
    absent
  structuralAxiom table context (rawAnnotationAssertion property subject value) with
    annotationPropertyLookup table property |
    structuralAnnotationSubject table subject |
    structuralAnnotationValue table value
  ... | present property′ | present subject′ | present value′ =
    present (K.annotationAssertion property′ subject′ value′)
  ... | absent | _ | _ =
    absent
  ... | _ | absent | _ =
    absent
  ... | _ | _ | absent =
    absent
  structuralAxiom table context (rawSubAnnotationPropertyOf sub sup) with
    annotationPropertyLookup table sub |
    annotationPropertyLookup table sup
  ... | present sub′ | present sup′ =
    present (K.subAnnotationPropertyOf sub′ sup′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom table context (rawAnnotationPropertyDomain property iri) with
    annotationPropertyLookup table property |
    annotationIRILookup table iri
  ... | present property′ | present iri′ =
    present (K.annotationPropertyDomain property′ iri′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom table context (rawAnnotationPropertyRange property iri) with
    annotationPropertyLookup table property |
    annotationIRILookup table iri
  ... | present property′ | present iri′ =
    present (K.annotationPropertyRange property′ iri′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent
  structuralAxiom table context (rawUnsupportedAxiom reason) =
    absent

  appendStructuralOptional :
    ∀ {ℓ} {A : Type ℓ} →
    Optional A →
    List A →
    List A
  appendStructuralOptional absent values =
    values
  appendStructuralOptional (present value) values =
    value ∷ values

  structuralAxioms :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    List (RawAnnotated RawAxiom) →
    List (K.Axiom (symbolTableSignature table))
  structuralAxioms table context [] =
    []
  structuralAxioms table context (axiom ∷ axioms) =
    appendStructuralOptional
      (structuralAxiom table context (body axiom))
      (structuralAxioms table context axioms)

  structuralAnnotatedAxiom :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    RawAnnotated RawAxiom →
    Optional (K.Annotated
      (symbolTableSignature table)
      (K.Axiom (symbolTableSignature table)))
  structuralAnnotatedAxiom table context axiom with
    structuralAxiom table context (body axiom)
  ... | present body′ =
    present
      (K.annotated
        (structuralAnnotations table (annotations axiom))
        body′)
  ... | absent =
    absent

  structuralAnnotatedAxioms :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    List (RawAnnotated RawAxiom) →
    List (K.Annotated
      (symbolTableSignature table)
      (K.Axiom (symbolTableSignature table)))
  structuralAnnotatedAxioms table context [] =
    []
  structuralAnnotatedAxioms table context (axiom ∷ axioms) =
    appendStructuralOptional
      (structuralAnnotatedAxiom table context axiom)
      (structuralAnnotatedAxioms table context axioms)

  record ChainFreeAnnotatedAxiom (Sig : K.Signature) : Type₀ where
    constructor chainFreeAnnotatedAxiom
    field
      checkedAnnotatedAxiom :
        K.Annotated Sig (K.Axiom Sig)
      checkedAxiomChainFree :
        K.AxiomPropertyChainFree (K.itemBody checkedAnnotatedAxiom)

  open ChainFreeAnnotatedAxiom

  record ChainFreeAnnotatedAxiomList (Sig : K.Signature) : Type₀ where
    constructor chainFreeAnnotatedAxiomList
    field
      checkedAnnotatedAxioms :
        List (K.Annotated Sig (K.Axiom Sig))
      checkedAxiomsChainFree :
        K.AxiomsPropertyChainFree
          (K.annotatedBodies checkedAnnotatedAxioms)

  open ChainFreeAnnotatedAxiomList

  appendChainFreeAnnotatedAxiom :
    {Sig : K.Signature} →
    Optional (ChainFreeAnnotatedAxiom Sig) →
    ChainFreeAnnotatedAxiomList Sig →
    ChainFreeAnnotatedAxiomList Sig
  appendChainFreeAnnotatedAxiom absent bundle =
    bundle
  appendChainFreeAnnotatedAxiom (present axiom) bundle =
    chainFreeAnnotatedAxiomList
      (checkedAnnotatedAxiom axiom ∷ checkedAnnotatedAxioms bundle)
      (checkedAxiomChainFree axiom , checkedAxiomsChainFree bundle)

  structuralChainFreeAnnotatedAxiom :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    RawAnnotated RawAxiom →
    Optional (ChainFreeAnnotatedAxiom (symbolTableSignature table))
  structuralChainFreeAnnotatedAxiom table context axiom with
    structuralAnnotatedAxiom table context axiom
  ... | absent =
    absent
  ... | present checked with
    K.axiomPropertyChainFree? (K.itemBody checked)
  ...   | present chainFree =
    present (chainFreeAnnotatedAxiom checked chainFree)
  ...   | absent =
    absent

  structuralChainFreeAnnotatedAxioms :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    List (RawAnnotated RawAxiom) →
    ChainFreeAnnotatedAxiomList (symbolTableSignature table)
  structuralChainFreeAnnotatedAxioms table context [] =
    chainFreeAnnotatedAxiomList [] tt
  structuralChainFreeAnnotatedAxioms table context (axiom ∷ axioms) =
    appendChainFreeAnnotatedAxiom
      (structuralChainFreeAnnotatedAxiom table context axiom)
      (structuralChainFreeAnnotatedAxioms table context axioms)

  structuralDatatypeSupport :
    (table : SymbolTable) →
    (axioms : List (K.Axiom (symbolTableSignature table))) →
    K.OntologyDatatypeSupport (symbolTableSignature table) axioms
  structuralDatatypeSupport table axioms =
    K.completeOntologyDatatypeSupport axioms

  structuralRegularity :
    (table : SymbolTable) →
    K.RegularityContext (symbolTableSignature table) →
    (axioms : List (K.Axiom (symbolTableSignature table))) →
    K.AxiomsPropertyChainFree axioms →
    K.OntologyRegularity (symbolTableSignature table) axioms
  structuralRegularity table context axioms chainFree =
    K.ontologyRegularity context chainFree

structuralOntologyFromTable :
  (table : SymbolTable) →
  K.RegularityContext (symbolTableSignature table) →
  RawOntology →
  K.Ontology (symbolTableSignature table)
structuralOntologyFromTable table context raw =
  K.ontology
    (structuralAnnotations table (annotations raw))
    annotatedAxiomList
    axiomList
    refl
    (structuralDatatypeSupport table axiomList)
    (structuralRegularity table context axiomList axiomListChainFree)
  where
  annotatedAxiomBundle :
    ChainFreeAnnotatedAxiomList (symbolTableSignature table)
  annotatedAxiomBundle =
    structuralChainFreeAnnotatedAxioms table context (axioms raw)

  annotatedAxiomList :
    List (K.Annotated
      (symbolTableSignature table)
      (K.Axiom (symbolTableSignature table)))
  annotatedAxiomList =
    checkedAnnotatedAxioms annotatedAxiomBundle

  axiomList : List (K.Axiom (symbolTableSignature table))
  axiomList =
    K.annotatedBodies annotatedAxiomList

  axiomListChainFree : K.AxiomsPropertyChainFree axiomList
  axiomListChainFree =
    checkedAxiomsChainFree annotatedAxiomBundle

checkedImportFromCleanStructural :
  ImportPolicy →
  (raw : RawOntology) →
  CleanDiagnostics (structuralElaborationDiagnostics raw) →
  CheckedImport
checkedImportFromCleanStructural policy raw clean =
  checkedImport
    policy
    (symbolTableSignature table)
    ontology′
    (K.completeSourceOntologySemanticSupport (K.axioms ontology′))
    (completeDeclarationEvidence (sourceTableTraceFromRaw raw))
    (completePropertyRoleEvidence (sourceTableTraceFromRaw raw))
    (trivialPolicyEvidence policy)
    (noRawImportClosure raw (structuralRawImportsClosed raw clean))
  where
  table : SymbolTable
  table =
    symbolTableFromRaw raw

  context : K.RegularityContext (symbolTableSignature table)
  context =
    structuralRegularityContext table (axioms raw)

  ontology′ : K.Ontology (symbolTableSignature table)
  ontology′ =
    structuralOntologyFromTable table context raw

structuralElaborationEvidence? :
  ImportPolicy →
  RawOntology →
  Optional CheckedImport
structuralElaborationEvidence? policy raw =
  evidenceFromCleanDiagnostics
    (structuralElaborationDiagnostics raw)
    (checkedImportFromCleanStructural policy raw)

structuralCleanEvidence :
  (policy : ImportPolicy) →
  (raw : RawOntology) →
  CleanDiagnostics (structuralElaborationDiagnostics raw) →
  Present (structuralElaborationEvidence? policy raw)
structuralCleanEvidence policy raw clean =
  cleanEvidenceFromCleanDiagnostics
    (structuralElaborationDiagnostics raw)
    (checkedImportFromCleanStructural policy raw)
    clean

structuralElaborationSound :
  (policy : ImportPolicy) →
  (raw : RawOntology) →
  (proof :
    Present
      (structuralElaborationEvidence?
        policy
        raw)) →
  ElaboratesToCheckedImport raw (presentValue proof)
structuralElaborationSound policy raw proof =
  elaboratesToCheckedImport
    refl
    ( cong
        (λ checked → requestedImports (sourceImportClosure checked))
        (presentValueFromEvidenceFromCleanDiagnostics
          (structuralElaborationDiagnostics raw)
          (checkedImportFromCleanStructural policy raw)
          proof)
    ∙ refl)

elaborateStructuralKernel :
  ImportPolicy →
  RawOntology →
  ElaborationResult
elaborateStructuralKernel policy raw =
  let diagnostics = structuralElaborationDiagnostics raw in
  record
    { input =
        raw
    ; diagnostics =
        diagnostics
    ; clean? =
        diagnosticsClean? diagnostics
    ; evidence? =
        structuralElaborationEvidence? policy raw
    ; cleanEvidence =
        structuralCleanEvidence policy raw
    ; sound =
        structuralElaborationSound policy raw
    }

elaborateStructuralKernelStrict : RawOntology → ElaborationResult
elaborateStructuralKernelStrict =
  elaborateStructuralKernel strictPolicy