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

module OWL2.Elab.Empty 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.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.empty" name

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

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

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

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

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

unsupportedImportDiagnostic : Diagnostic
unsupportedImportDiagnostic =
  diagnostic
    (elabCode "unsupported-import")
    severityError
    importsPath
    "The initial checked-kernel elaborator accepts only raw ontologies without imports."

unsupportedOntologyIRIDiagnostic : Diagnostic
unsupportedOntologyIRIDiagnostic =
  diagnostic
    (elabCode "unsupported-ontology-iri")
    severityError
    ontologyIRIPath
    "The initial checked-kernel elaborator does not erase ontology IRIs."

unsupportedVersionIRIDiagnostic : Diagnostic
unsupportedVersionIRIDiagnostic =
  diagnostic
    (elabCode "unsupported-version-iri")
    severityError
    versionIRIPath
    "The initial checked-kernel elaborator does not erase version IRIs."

unsupportedOntologyAnnotationDiagnostic : Diagnostic
unsupportedOntologyAnnotationDiagnostic =
  diagnostic
    (elabCode "unsupported-ontology-annotation")
    severityError
    annotationsPath
    "The initial checked-kernel elaborator does not erase ontology annotations."

unsupportedAxiomDiagnostic : Diagnostic
unsupportedAxiomDiagnostic =
  diagnostic
    (elabCode "unsupported-axiom")
    severityError
    axiomsPath
    "The initial checked-kernel elaborator accepts only raw ontologies without axioms."

emptySignature : K.Signature
emptySignature =
  K.signature          K.noPunning

emptyDatatypeSupport : K.OntologyDatatypeSupport emptySignature []
emptyDatatypeSupport =
  K.completeOntologyDatatypeSupport []

emptyRegularity : K.OntologyRegularity emptySignature []
emptyRegularity =
  K.ontologyRegularity K.trivialRegularityContext tt

importsDiagnostics : List RawIRI → Diagnostics
importsDiagnostics [] =
  noDiagnostics
importsDiagnostics (iri ∷ imports) =
  singleDiagnostic unsupportedImportDiagnostic

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

ontologyIRIDiagnostics : Optional RawIRI → Diagnostics
ontologyIRIDiagnostics absent =
  noDiagnostics
ontologyIRIDiagnostics (present iri) =
  singleDiagnostic unsupportedOntologyIRIDiagnostic

versionIRIDiagnostics : Optional RawIRI → Diagnostics
versionIRIDiagnostics absent =
  noDiagnostics
versionIRIDiagnostics (present iri) =
  singleDiagnostic unsupportedVersionIRIDiagnostic

emptyAnnotationsDiagnostics : List RawAnnotation → Diagnostics
emptyAnnotationsDiagnostics [] =
  noDiagnostics
emptyAnnotationsDiagnostics (annotation ∷ annotations) =
  singleDiagnostic unsupportedOntologyAnnotationDiagnostic

emptyAnnotationsDiagnosticsClosed :
  (rawAnnotations : List RawAnnotation) →
  CleanDiagnostics (emptyAnnotationsDiagnostics rawAnnotations) →
  rawAnnotations ≡ []
emptyAnnotationsDiagnosticsClosed [] clean =
  refl
emptyAnnotationsDiagnosticsClosed (annotation ∷ annotations) ()

axiomsDiagnostics : List (RawAnnotated RawAxiom) → Diagnostics
axiomsDiagnostics [] =
  noDiagnostics
axiomsDiagnostics (axiom ∷ axioms) =
  singleDiagnostic unsupportedAxiomDiagnostic

axiomsDiagnosticsClosed :
  (rawAxioms : List (RawAnnotated RawAxiom)) →
  CleanDiagnostics (axiomsDiagnostics rawAxioms) →
  rawAxioms ≡ []
axiomsDiagnosticsClosed [] clean =
  refl
axiomsDiagnosticsClosed (axiom ∷ axioms) ()

emptyElaborationDiagnostics : RawOntology → Diagnostics
emptyElaborationDiagnostics raw =
  importsDiagnostics (imports raw) ++
  ontologyIRIDiagnostics (ontologyIRI raw) ++
  versionIRIDiagnostics (versionIRI raw) ++
  emptyAnnotationsDiagnostics (annotations raw) ++
  axiomsDiagnostics (axioms raw)

emptyRawImportsClosed :
  (raw : RawOntology) →
  CleanDiagnostics (emptyElaborationDiagnostics raw) →
  imports raw ≡ []
emptyRawImportsClosed raw clean =
  importsDiagnosticsClosed
    (imports raw)
    (cleanAppendLeft
      (importsDiagnostics (imports raw))
      (ontologyIRIDiagnostics (ontologyIRI raw) ++
       versionIRIDiagnostics (versionIRI raw) ++
       emptyAnnotationsDiagnostics (annotations raw) ++
       axiomsDiagnostics (axioms raw))
      clean)

emptyRawAnnotationsClosed :
  (raw : RawOntology) →
  CleanDiagnostics (emptyElaborationDiagnostics raw) →
  annotations raw ≡ []
emptyRawAnnotationsClosed raw clean =
  emptyAnnotationsDiagnosticsClosed
    (annotations raw)
    (cleanAppendLeft
      (emptyAnnotationsDiagnostics (annotations raw))
      (axiomsDiagnostics (axioms raw))
      (cleanAppendRight
        (versionIRIDiagnostics (versionIRI raw))
        (emptyAnnotationsDiagnostics (annotations raw) ++
         axiomsDiagnostics (axioms raw))
        (cleanAppendRight
          (ontologyIRIDiagnostics (ontologyIRI raw))
          (versionIRIDiagnostics (versionIRI raw) ++
           emptyAnnotationsDiagnostics (annotations raw) ++
           axiomsDiagnostics (axioms raw))
          (cleanAppendRight
            (importsDiagnostics (imports raw))
            (ontologyIRIDiagnostics (ontologyIRI raw) ++
             versionIRIDiagnostics (versionIRI raw) ++
             emptyAnnotationsDiagnostics (annotations raw) ++
             axiomsDiagnostics (axioms raw))
            clean))))

emptyRawAxiomsClosed :
  (raw : RawOntology) →
  CleanDiagnostics (emptyElaborationDiagnostics raw) →
  axioms raw ≡ []
emptyRawAxiomsClosed raw clean =
  axiomsDiagnosticsClosed
    (axioms raw)
    (cleanAppendRight
      (emptyAnnotationsDiagnostics (annotations raw))
      (axiomsDiagnostics (axioms raw))
      (cleanAppendRight
        (versionIRIDiagnostics (versionIRI raw))
        (emptyAnnotationsDiagnostics (annotations raw) ++
         axiomsDiagnostics (axioms raw))
        (cleanAppendRight
          (ontologyIRIDiagnostics (ontologyIRI raw))
          (versionIRIDiagnostics (versionIRI raw) ++
           emptyAnnotationsDiagnostics (annotations raw) ++
           axiomsDiagnostics (axioms raw))
          (cleanAppendRight
            (importsDiagnostics (imports raw))
            (ontologyIRIDiagnostics (ontologyIRI raw) ++
             versionIRIDiagnostics (versionIRI raw) ++
             emptyAnnotationsDiagnostics (annotations raw) ++
             axiomsDiagnostics (axioms raw))
            clean))))

emptySourceTableSignature :
  (raw : RawOntology) →
  (clean : CleanDiagnostics (emptyElaborationDiagnostics raw)) →
  symbolTableSignature (symbolTableFromRaw raw) ≡ emptySignature
emptySourceTableSignature
  (rawOntology provenance ontologyIRI versionIRI
    (importIRI ∷ imports) rawAnnotations rawAxioms)
  ()
emptySourceTableSignature
  (rawOntology provenance (present ontologyIRI) versionIRI
    [] rawAnnotations rawAxioms)
  ()
emptySourceTableSignature
  (rawOntology provenance absent (present versionIRI)
    [] rawAnnotations rawAxioms)
  ()
emptySourceTableSignature
  (rawOntology provenance absent absent
    [] (annotation ∷ rawAnnotations) rawAxioms)
  ()
emptySourceTableSignature
  (rawOntology provenance absent absent [] [] (rawAxiom ∷ rawAxioms))
  ()
emptySourceTableSignature
  (rawOntology provenance absent absent [] [] [])
  clean =
  refl

emptySourceTableTrace :
  (raw : RawOntology) →
  (clean : CleanDiagnostics (emptyElaborationDiagnostics raw)) →
  CheckedSourceTableTrace emptySignature
emptySourceTableTrace raw clean =
  checkedSourceTableTrace
    (symbolTableFromRaw raw)
    (emptySourceTableSignature raw clean)
    (present
      (checkedSourceTableRawTrace
        raw
        refl
        (provenance raw)
        refl))

emptyCheckedImport :
  ImportPolicy →
  (raw : RawOntology) →
  CleanDiagnostics (emptyElaborationDiagnostics raw) →
  CheckedImport
emptyCheckedImport policy raw clean =
  checkedImport
    policy
    emptySignature
    (K.emptyOntology emptyDatatypeSupport emptyRegularity)
    (K.completeSourceOntologySemanticSupport [])
    (completeDeclarationEvidence (emptySourceTableTrace raw clean))
    (completePropertyRoleEvidence (emptySourceTableTrace raw clean))
    (trivialPolicyEvidence policy)
    (noRawImportClosure raw (emptyRawImportsClosed raw clean))

emptyElaborationEvidence? :
  ImportPolicy →
  RawOntology →
  Optional CheckedImport
emptyElaborationEvidence? policy raw =
  evidenceFromCleanDiagnostics
    (emptyElaborationDiagnostics raw)
    (λ clean →
      emptyCheckedImport policy raw clean)

emptyElaborationCleanEvidence :
  (policy : ImportPolicy) →
  (raw : RawOntology) →
  CleanDiagnostics (emptyElaborationDiagnostics raw) →
  Present (emptyElaborationEvidence? policy raw)
emptyElaborationCleanEvidence policy raw clean =
  cleanEvidenceFromCleanDiagnostics
    (emptyElaborationDiagnostics raw)
    (λ clean →
      emptyCheckedImport policy raw clean)
    clean

emptyElaborationSound :
  (policy : ImportPolicy) →
  (raw : RawOntology) →
  (proof :
    Present
      (emptyElaborationEvidence?
        policy
        raw)) →
  ElaboratesToCheckedImport raw (presentValue proof)
emptyElaborationSound policy raw proof =
  elaboratesToCheckedImport
    refl
    ( cong
        (λ checked → requestedImports (sourceImportClosure checked))
        (presentValueFromEvidenceFromCleanDiagnostics
          (emptyElaborationDiagnostics raw)
          (λ clean →
            emptyCheckedImport policy raw clean)
          proof)
    ∙ refl)

elaborateEmptyKernel :
  ImportPolicy →
  RawOntology →
  ElaborationResult
elaborateEmptyKernel policy raw =
  let diagnostics = emptyElaborationDiagnostics raw in
  record
    { input =
        raw
    ; diagnostics =
        diagnostics
    ; clean? =
        diagnosticsClean? diagnostics
    ; evidence? =
        emptyElaborationEvidence? policy raw
    ; cleanEvidence =
        emptyElaborationCleanEvidence policy raw
    ; sound =
        emptyElaborationSound policy raw
    }

elaborateEmptyKernelStrict : RawOntology → ElaborationResult
elaborateEmptyKernelStrict =
  elaborateEmptyKernel strictPolicy