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

module OWL2.Elab.Declarations where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
open import OWL2.Elab.CheckedImport
open import OWL2.Elab.Policy
open import OWL2.Elab.Punning
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.declarations" 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" ∷ [])

  annotationsPath : SourcePath
  annotationsPath =
    sourcePath (fieldSegment "annotations" ∷ [])

  axiomAnnotationsPath : SourcePath
  axiomAnnotationsPath =
    sourcePath (fieldSegment "axioms" ∷ opaqueSegment "annotations" ∷ [])

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

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

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

unsupportedDeclarationAxiomDiagnostic : Diagnostic
unsupportedDeclarationAxiomDiagnostic =
  diagnostic
    (elabCode "unsupported-axiom")
    severityError
    axiomsPath
    "Only declaration axioms are accepted by this elaborator stage."

unsupportedDeclarationOntologyAnnotationDiagnostic : Diagnostic
unsupportedDeclarationOntologyAnnotationDiagnostic =
  diagnostic
    (elabCode "unsupported-ontology-annotation")
    severityError
    annotationsPath
    "The declaration elaborator does not erase ontology annotations."

unsupportedDeclarationAxiomAnnotationDiagnostic : Diagnostic
unsupportedDeclarationAxiomAnnotationDiagnostic =
  diagnostic
    (elabCode "unsupported-axiom-annotation")
    severityError
    axiomAnnotationsPath
    "The declaration elaborator does not erase axiom annotations."

unknownEntityKindDiagnostic : Diagnostic
unknownEntityKindDiagnostic =
  diagnostic
    (elabCode "unknown-entity-kind")
    severityError
    axiomsPath
    "A raw declaration has unknown entity kind."

declarationAxiomDiagnostics : RawAxiom → Diagnostics
declarationAxiomDiagnostics (rawDeclaration entity) with kind entity
... | rawUnknownEntityKind =
  singleDiagnostic unknownEntityKindDiagnostic
... | rawClass =
  noDiagnostics
... | rawObjectProperty =
  noDiagnostics
... | rawDataProperty =
  noDiagnostics
... | rawDatatype =
  noDiagnostics
... | rawIndividual =
  noDiagnostics
... | rawAnnotationProperty =
  noDiagnostics
declarationAxiomDiagnostics (rawSubClassOf sub sup) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawEquivalentClasses classes) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawDisjointClasses classes) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawDisjointUnion class classes) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawSubObjectPropertyOf sub sup) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawEquivalentObjectProperties properties) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawDisjointObjectProperties properties) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawInverseObjectProperties left right) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawObjectPropertyDomain property class) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawObjectPropertyRange property class) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawFunctionalObjectProperty property) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawInverseFunctionalObjectProperty property) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawReflexiveObjectProperty property) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawIrreflexiveObjectProperty property) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawSymmetricObjectProperty property) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawAsymmetricObjectProperty property) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawTransitiveObjectProperty property) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawSubDataPropertyOf sub sup) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawEquivalentDataProperties properties) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawDisjointDataProperties properties) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawDataPropertyDomain property class) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawDataPropertyRange property range) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawFunctionalDataProperty property) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawDatatypeDefinition datatype range) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawHasKey class objectProperties dataProperties) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawSameIndividual individuals) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawDifferentIndividuals individuals) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawClassAssertion class individual) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawObjectPropertyAssertion property subject object) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics
  (rawNegativeObjectPropertyAssertion property subject object) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawDataPropertyAssertion property subject literal) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics
  (rawNegativeDataPropertyAssertion property subject literal) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawAnnotationAssertion property subject value) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawSubAnnotationPropertyOf sub sup) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawAnnotationPropertyDomain property iri) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawAnnotationPropertyRange property iri) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic
declarationAxiomDiagnostics (rawUnsupportedAxiom reason) =
  singleDiagnostic unsupportedDeclarationAxiomDiagnostic

annotatedDeclarationDiagnostics : RawAnnotated RawAxiom → Diagnostics
annotatedDeclarationDiagnostics axiom =
  declarationAnnotationDiagnostics (annotations axiom) ++
  declarationAxiomDiagnostics (body axiom)
  where
  declarationAnnotationDiagnostics : List RawAnnotation → Diagnostics
  declarationAnnotationDiagnostics [] =
    noDiagnostics
  declarationAnnotationDiagnostics (annotation ∷ annotations) =
    singleDiagnostic unsupportedDeclarationAxiomAnnotationDiagnostic

declarationsDiagnostics : List (RawAnnotated RawAxiom) → Diagnostics
declarationsDiagnostics [] =
  noDiagnostics
declarationsDiagnostics (axiom ∷ axioms) =
  annotatedDeclarationDiagnostics axiom ++ declarationsDiagnostics axioms

declarationOntologyAnnotationDiagnostics : List RawAnnotation → Diagnostics
declarationOntologyAnnotationDiagnostics [] =
  noDiagnostics
declarationOntologyAnnotationDiagnostics (annotation ∷ annotations) =
  singleDiagnostic unsupportedDeclarationOntologyAnnotationDiagnostic

declarationImportsDiagnostics : List RawIRI → Diagnostics
declarationImportsDiagnostics [] =
  noDiagnostics
declarationImportsDiagnostics (iri ∷ imports) =
  singleDiagnostic unsupportedDeclarationImportDiagnostic

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

declarationOntologyIRIDiagnostics : Optional RawIRI → Diagnostics
declarationOntologyIRIDiagnostics absent =
  noDiagnostics
declarationOntologyIRIDiagnostics (present iri) =
  singleDiagnostic unsupportedDeclarationOntologyIRIDiagnostic

declarationVersionIRIDiagnostics : Optional RawIRI → Diagnostics
declarationVersionIRIDiagnostics absent =
  noDiagnostics
declarationVersionIRIDiagnostics (present iri) =
  singleDiagnostic unsupportedDeclarationVersionIRIDiagnostic

declarationElaborationDiagnostics : RawOntology → Diagnostics
declarationElaborationDiagnostics raw =
  declarationImportsDiagnostics (imports raw) ++
  declarationOntologyIRIDiagnostics (ontologyIRI raw) ++
  declarationVersionIRIDiagnostics (versionIRI raw) ++
  declarationOntologyAnnotationDiagnostics (annotations raw) ++
  rawPunningDiagnosticsFromSymbolTable (symbolTableFromRaw raw) ++
  declarationsDiagnostics (axioms raw)

declarationRawImportsClosed :
  (raw : RawOntology) →
  CleanDiagnostics (declarationElaborationDiagnostics raw) →
  imports raw ≡ []
declarationRawImportsClosed raw clean =
  declarationImportsDiagnosticsClosed
    (imports raw)
    (cleanAppendLeft
      (declarationImportsDiagnostics (imports raw))
      (declarationOntologyIRIDiagnostics (ontologyIRI raw) ++
       declarationVersionIRIDiagnostics (versionIRI raw) ++
       declarationOntologyAnnotationDiagnostics (annotations raw) ++
       rawPunningDiagnosticsFromSymbolTable (symbolTableFromRaw raw) ++
       declarationsDiagnostics (axioms raw))
      clean)

entityDeclarationAxiom :
  (table : SymbolTable) →
  RawEntity →
  Optional (K.Axiom (symbolTableSignature table))
entityDeclarationAxiom table entity with kind entity
... | rawClass with classLookup table (iri entity)
... | present name =
  present (K.declaration (K.classEntity name))
... | absent =
  absent
entityDeclarationAxiom table entity | rawObjectProperty with
  objectPropertyLookup table (iri entity)
... | present name =
  present (K.declaration (K.objectPropertyEntity name))
... | absent =
  absent
entityDeclarationAxiom table entity | rawDataProperty with
  dataPropertyLookup table (iri entity)
... | present name =
  present (K.declaration (K.dataPropertyEntity name))
... | absent =
  absent
entityDeclarationAxiom table entity | rawDatatype with datatypeLookup table (iri entity)
... | present name =
  present (K.declaration (K.datatypeEntity name))
... | absent =
  absent
entityDeclarationAxiom table entity | rawIndividual with
  individualLookup table (iri entity)
... | present name =
  present (K.declaration (K.individualEntity name))
... | absent =
  absent
entityDeclarationAxiom table entity | rawAnnotationProperty with
  annotationPropertyLookup table (iri entity)
... | present name =
  present (K.declaration (K.annotationPropertyEntity name))
... | absent =
  absent
entityDeclarationAxiom table entity | rawUnknownEntityKind =
  absent

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

record DeclarationAxiomList (Sig : K.Signature) : Type₀ where
  constructor declarationAxiomList
  field
    checkedAxioms :
      List (K.Axiom Sig)
    checkedAxiomsChainFree :
      K.AxiomsPropertyChainFree checkedAxioms

open DeclarationAxiomList public

appendDeclarationAxiom :
  {Sig : K.Signature} →
  Optional (K.Axiom Sig) →
  DeclarationAxiomList Sig →
  DeclarationAxiomList Sig
appendDeclarationAxiom absent bundle =
  bundle
appendDeclarationAxiom (present axiom) bundle with
  K.axiomPropertyChainFree? axiom
... | present chainFree =
  declarationAxiomList
    (axiom ∷ checkedAxioms bundle)
    (chainFree , checkedAxiomsChainFree bundle)
... | absent =
  bundle

declarationAxioms :
  (table : SymbolTable) →
  List (RawAnnotated RawAxiom) →
  DeclarationAxiomList (symbolTableSignature table)
declarationAxioms table [] =
  declarationAxiomList [] tt
declarationAxioms table (axiom ∷ axioms) with annotatedEntity axiom
... | present entity =
  appendDeclarationAxiom
    (entityDeclarationAxiom table entity)
    (declarationAxioms table axioms)
... | absent =
  declarationAxioms table axioms

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

regularity :
  (table : SymbolTable) →
  (axioms : List (K.Axiom (symbolTableSignature table))) →
  K.AxiomsPropertyChainFree axioms →
  K.OntologyRegularity (symbolTableSignature table) axioms
regularity table axioms chainFree =
  K.ontologyRegularity K.trivialRegularityContext chainFree

checkedImportFromDeclarations :
  ImportPolicy →
  (raw : RawOntology) →
  imports raw ≡ [] →
  CheckedImport
checkedImportFromDeclarations policy raw rawImportsClosed =
  checkedImport
    policy
    (symbolTableSignature table)
    (K.plainOntology
      axiomList
      (datatypeSupport table axiomList)
      (regularity table axiomList axiomListChainFree))
    (K.completeSourceOntologySemanticSupport axiomList)
    (completeDeclarationEvidence (sourceTableTraceFromRaw raw))
    (completePropertyRoleEvidence (sourceTableTraceFromRaw raw))
    (trivialPolicyEvidence policy)
    (noRawImportClosure raw rawImportsClosed)
  where
  table : SymbolTable
  table =
    symbolTableFromRaw raw

  axiomBundle : DeclarationAxiomList (symbolTableSignature table)
  axiomBundle =
    declarationAxioms table (axioms raw)

  axiomList : List (K.Axiom (symbolTableSignature table))
  axiomList =
    checkedAxioms axiomBundle

  axiomListChainFree : K.AxiomsPropertyChainFree axiomList
  axiomListChainFree =
    checkedAxiomsChainFree axiomBundle

declarationElaborationEvidence? :
  ImportPolicy →
  RawOntology →
  Optional CheckedImport
declarationElaborationEvidence? policy raw =
  evidenceFromCleanDiagnostics
    (declarationElaborationDiagnostics raw)
    (λ clean →
      checkedImportFromDeclarations
        policy
        raw
        (declarationRawImportsClosed raw clean))

declarationCleanEvidence :
  (policy : ImportPolicy) →
  (raw : RawOntology) →
  CleanDiagnostics (declarationElaborationDiagnostics raw) →
  Present (declarationElaborationEvidence? policy raw)
declarationCleanEvidence policy raw clean =
  cleanEvidenceFromCleanDiagnostics
    (declarationElaborationDiagnostics raw)
    (λ clean →
      checkedImportFromDeclarations
        policy
        raw
        (declarationRawImportsClosed raw clean))
    clean

declarationElaborationSound :
  (policy : ImportPolicy) →
  (raw : RawOntology) →
  (proof :
    Present
      (declarationElaborationEvidence?
        policy
        raw)) →
  ElaboratesToCheckedImport raw (presentValue proof)
declarationElaborationSound policy raw proof =
  elaboratesToCheckedImport
    refl
    ( cong
        (λ checked → requestedImports (sourceImportClosure checked))
        (presentValueFromEvidenceFromCleanDiagnostics
          (declarationElaborationDiagnostics raw)
          (λ clean →
            checkedImportFromDeclarations
              policy
              raw
              (declarationRawImportsClosed raw clean))
          proof)
    ∙ refl)

elaborateDeclarationsKernel :
  ImportPolicy →
  RawOntology →
  ElaborationResult
elaborateDeclarationsKernel policy raw =
  let diagnostics = declarationElaborationDiagnostics raw in
  record
    { input =
        raw
    ; diagnostics =
        diagnostics
    ; clean? =
        diagnosticsClean? diagnostics
    ; evidence? =
        declarationElaborationEvidence? policy raw
    ; cleanEvidence =
        declarationCleanEvidence policy raw
    ; sound =
        declarationElaborationSound policy raw
    }

elaborateDeclarationsKernelStrict : RawOntology → ElaborationResult
elaborateDeclarationsKernelStrict =
  elaborateDeclarationsKernel strictPolicy