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

module OWL2.Import.OBOGraph.Checked 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.Structural
open import OWL2.Foundation.Maybe
open import OWL2.Import.OBOGraph.Raw
open import OWL2.OBOGraph.Syntax
open import OWL2.Raw
open import OWL2.Semantics.Complete
import OWL2.Kernel.Semantics as KS

obographCheckedDiagnosticsFromRawDiagnostics :
  ImportPolicy →
  GraphDocument →
  Diagnostics →
  Diagnostics
obographCheckedDiagnosticsFromRawDiagnostics policy doc [] =
  structuralElaborationDiagnostics (rawOntologyFromOBOGraph doc)
obographCheckedDiagnosticsFromRawDiagnostics policy doc (d ∷ diagnostics) =
  d ∷ diagnostics

obographCheckedDiagnostics :
  ImportPolicy →
  GraphDocument →
  Diagnostics
obographCheckedDiagnostics policy doc =
  obographCheckedDiagnosticsFromRawDiagnostics
    policy
    doc
    (obographRawDiagnostics policy doc)

record ImportsOBOGraphToChecked
  (doc : GraphDocument)
  (checked : CheckedImport)
  : Type₀ where
  constructor importsOBOGraphToChecked
  field
    checkedRawOntology :
      RawOntology
    checkedRawSound :
      ImportsOBOGraphToRaw doc checkedRawOntology
    checkedElaborationSound :
      ElaboratesToCheckedImport checkedRawOntology checked

open ImportsOBOGraphToChecked public

OBOGraphCheckedImportResult : Type₀
OBOGraphCheckedImportResult =
  CheckResult
    GraphDocument
    (λ _ → CheckedImport)
    ImportsOBOGraphToChecked

obographCheckedEvidenceFromRawDiagnostics :
  ImportPolicy →
  GraphDocument →
  Diagnostics →
  Optional CheckedImport
obographCheckedEvidenceFromRawDiagnostics policy doc [] =
  structuralElaborationEvidence? policy (rawOntologyFromOBOGraph doc)
obographCheckedEvidenceFromRawDiagnostics policy doc (d ∷ diagnostics) =
  absent

obographCheckedEvidence? :
  ImportPolicy →
  GraphDocument →
  Optional CheckedImport
obographCheckedEvidence? policy doc =
  obographCheckedEvidenceFromRawDiagnostics
    policy
    doc
    (obographRawDiagnostics policy doc)

obographCheckedCleanEvidenceFromRawDiagnostics :
  (policy : ImportPolicy) →
  (doc : GraphDocument) →
  (rawDiagnostics : Diagnostics) →
  CleanDiagnostics
    (obographCheckedDiagnosticsFromRawDiagnostics policy doc rawDiagnostics) →
  Present
    (obographCheckedEvidenceFromRawDiagnostics policy doc rawDiagnostics)
obographCheckedCleanEvidenceFromRawDiagnostics policy doc [] clean =
  structuralCleanEvidence policy (rawOntologyFromOBOGraph doc) clean
obographCheckedCleanEvidenceFromRawDiagnostics policy doc (d ∷ diagnostics) ()

obographCheckedCleanEvidence :
  (policy : ImportPolicy) →
  (doc : GraphDocument) →
  CleanDiagnostics (obographCheckedDiagnostics policy doc) →
  Present (obographCheckedEvidence? policy doc)
obographCheckedCleanEvidence policy doc =
  obographCheckedCleanEvidenceFromRawDiagnostics
    policy
    doc
    (obographRawDiagnostics policy doc)

obographCheckedSoundFromRawDiagnostics :
  (policy : ImportPolicy) →
  (doc : GraphDocument) →
  (rawDiagnostics : Diagnostics) →
  (proof :
    Present
      (obographCheckedEvidenceFromRawDiagnostics
        policy
        doc
        rawDiagnostics)) →
  ImportsOBOGraphToChecked doc (presentValue proof)
obographCheckedSoundFromRawDiagnostics policy doc [] proof =
  importsOBOGraphToChecked
    (rawOntologyFromOBOGraph doc)
    (importsOBOGraphToRaw refl)
    (structuralElaborationSound policy (rawOntologyFromOBOGraph doc) proof)
obographCheckedSoundFromRawDiagnostics policy doc (d ∷ diagnostics) ()

obographCheckedSound :
  (policy : ImportPolicy) →
  (doc : GraphDocument) →
  (proof : Present (obographCheckedEvidence? policy doc)) →
  ImportsOBOGraphToChecked doc (presentValue proof)
obographCheckedSound policy doc =
  obographCheckedSoundFromRawDiagnostics
    policy
    doc
    (obographRawDiagnostics policy doc)

importOBOGraphChecked :
  ImportPolicy →
  GraphDocument →
  OBOGraphCheckedImportResult
importOBOGraphChecked policy doc =
  let diagnostics = obographCheckedDiagnostics policy doc in
  record
    { input =
        doc
    ; diagnostics =
        diagnostics
    ; clean? =
        diagnosticsClean? diagnostics
    ; evidence? =
        obographCheckedEvidence? policy doc
    ; cleanEvidence =
        obographCheckedCleanEvidence policy doc
    ; sound =
        obographCheckedSound policy doc
    }

importOBOGraphCheckedStrict :
  GraphDocument →
  OBOGraphCheckedImportResult
importOBOGraphCheckedStrict =
  importOBOGraphChecked strictPolicy

importOBOGraphCheckedCompatibility :
  GraphDocument →
  OBOGraphCheckedImportResult
importOBOGraphCheckedCompatibility =
  importOBOGraphChecked compatibilityPolicy

obographCheckedImportSucceeded :
  (result : OBOGraphCheckedImportResult) →
  EvidenceAvailable result →
  CheckedImport
obographCheckedImportSucceeded result evidence =
  evidenceValue result evidence

checkedImportSucceeded :
  (result : OBOGraphCheckedImportResult) →
  EvidenceAvailable result →
  CheckedImport
checkedImportSucceeded =
  obographCheckedImportSucceeded

obographCheckedImportFromClean :
  (result : OBOGraphCheckedImportResult) →
  Clean result →
  CheckedImport
obographCheckedImportFromClean result clean =
  evidenceFromClean result clean

obographCheckedSourceEvidenceFromClean :
  (result : OBOGraphCheckedImportResult) →
  (clean : Clean result) →
  CheckedSourceEvidence (obographCheckedImportFromClean result clean)
obographCheckedSourceEvidenceFromClean result clean =
  checkedSourceEvidenceOf (obographCheckedImportFromClean result clean)

obographCheckedSoundFromClean :
  (result : OBOGraphCheckedImportResult) →
  (clean : Clean result) →
  ImportsOBOGraphToChecked
    (input result)
    (obographCheckedImportFromClean result clean)
obographCheckedSoundFromClean result clean =
  soundFromClean result clean

ModelOfCompleteOBOGraphImport :
  (result : OBOGraphCheckedImportResult) →
  (clean : Clean result) →
  KS.Interpretation (signature (obographCheckedImportFromClean result clean)) →
  Type₀
ModelOfCompleteOBOGraphImport result clean interpretation =
  ModelOfCompleteCheckedImport
    (obographCheckedImportFromClean result clean)
    (obographCheckedSourceEvidenceFromClean result clean)
    interpretation

record CompleteOBOGraphImportModel
  (result : OBOGraphCheckedImportResult)
  (clean : Clean result)
  : Type₁ where
  constructor completeOBOGraphImportModel
  field
    completeOBOGraphInterpretation :
      KS.Interpretation
        (signature (obographCheckedImportFromClean result clean))
    completeOBOGraphSatisfies :
      ModelOfCompleteOBOGraphImport
        result
        clean
        completeOBOGraphInterpretation

open CompleteOBOGraphImportModel public