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

module OWL2.Elab.Result where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Elab.CheckedImport
open import OWL2.Raw

record ElaboratesToCheckedImport
  (raw : RawOntology)
  (checked : CheckedImport)
  : Type₀ where
  constructor elaboratesToCheckedImport
  field
    sourcePreserved :
      provenance raw ≡ provenance raw
    sourceImportsRecorded :
      requestedImports (sourceImportClosure checked) ≡ imports raw

open ElaboratesToCheckedImport public

ElaborationResult : Type₀
ElaborationResult =
  CheckResult
    RawOntology
    (λ _ → CheckedImport)
    ElaboratesToCheckedImport

elaborationSucceeded :
  (result : ElaborationResult) →
  EvidenceAvailable result → CheckedImport
elaborationSucceeded result evidence =
  evidenceValue result evidence