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

module OWL2.Portable.Check.Core where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics

legacyCheckDiagnostics : Diagnostics
legacyCheckDiagnostics =
  noDiagnostics

successfulResultWithDiagnostics :
  ∀ {ℓᵢ ℓᵉ ℓᵐ}
    {Input : Type ℓᵢ}
    {Evidence : Input → Type ℓᵉ}
    {Meaning : (input : Input) → Evidence input → Type ℓᵐ} →
  Diagnostics →
  (input : Input) →
  (evidence : Evidence input) →
  Meaning input evidence →
  CheckResult Input Evidence Meaning
successfulResultWithDiagnostics {Meaning = Meaning} diagnostics input evidence meaning =
  checkResult
    input
    diagnostics
    (diagnosticsClean? diagnostics)
    (evidenceWhenNoDiagnostics evidence diagnostics)
    (cleanEvidenceWhenNoDiagnostics evidence diagnostics)
    (λ proof →
      subst
        (Meaning input)
        (sym
          (presentValueFromEvidenceWhenNoDiagnostics
            evidence
            diagnostics
            proof))
        meaning)

successfulResult :
  ∀ {ℓᵢ ℓᵉ ℓᵐ}
    {Input : Type ℓᵢ}
    {Evidence : Input → Type ℓᵉ}
    {Meaning : (input : Input) → Evidence input → Type ℓᵐ} →
  (input : Input) →
  (evidence : Evidence input) →
  Meaning input evidence →
  CheckResult Input Evidence Meaning
successfulResult =
  successfulResultWithDiagnostics legacyCheckDiagnostics