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

module OWL2.Check.Result where

open import Agda.Primitive using (_⊔_)
open import OWL2.Prelude
open import OWL2.Foundation.Maybe
open import OWL2.Diagnostics.Algebra

record CheckResult
  {ℓᵢ ℓᵉ ℓᵐ : Level}
  (Input : Type ℓᵢ)
  (Evidence : Input → Type ℓᵉ)
  (Meaning : (input : Input) → Evidence input → Type ℓᵐ)
  : Type (ℓᵢ ⊔ ℓᵉ ⊔ ℓᵐ) where
  constructor checkResult
  field
    input :
      Input
    diagnostics :
      Diagnostics
    clean? :
      Bool
    evidence? :
      Optional (Evidence input)
    cleanEvidence :
      CleanDiagnostics diagnostics → Present evidence?
    sound :
      (proof : Present evidence?) →
      Meaning input (presentValue proof)

open CheckResult public

evidenceWhenNoDiagnostics :
  ∀ {ℓ} {Evidence : Type ℓ} →
  Evidence →
  Diagnostics →
  Optional Evidence
evidenceWhenNoDiagnostics evidence [] =
  present evidence
evidenceWhenNoDiagnostics evidence (d ∷ diagnostics) =
  absent

cleanEvidenceWhenNoDiagnostics :
  ∀ {ℓ} {Evidence : Type ℓ} →
  (evidence : Evidence) →
  (diagnostics : Diagnostics) →
  CleanDiagnostics diagnostics →
  Present (evidenceWhenNoDiagnostics evidence diagnostics)
cleanEvidenceWhenNoDiagnostics evidence [] clean =
  presentWitness evidence
cleanEvidenceWhenNoDiagnostics evidence (d ∷ diagnostics) ()

cleanDiagnosticsFromEvidenceWhenNoDiagnostics :
  ∀ {ℓ} {Evidence : Type ℓ} →
  (evidence : Evidence) →
  (diagnostics : Diagnostics) →
  Present (evidenceWhenNoDiagnostics evidence diagnostics) →
  CleanDiagnostics diagnostics
cleanDiagnosticsFromEvidenceWhenNoDiagnostics evidence [] proof =
  tt
cleanDiagnosticsFromEvidenceWhenNoDiagnostics evidence (d ∷ diagnostics) ()

presentValueFromEvidenceWhenNoDiagnostics :
  ∀ {ℓ} {Evidence : Type ℓ} →
  (evidence : Evidence) →
  (diagnostics : Diagnostics) →
  (proof : Present (evidenceWhenNoDiagnostics evidence diagnostics)) →
  presentValue proof ≡ evidence
presentValueFromEvidenceWhenNoDiagnostics evidence [] (presentWitness value) =
  refl
presentValueFromEvidenceWhenNoDiagnostics evidence (d ∷ diagnostics) ()

evidenceFromCleanDiagnostics :
  ∀ {ℓ} {Evidence : Type ℓ} →
  (diagnostics : Diagnostics) →
  (CleanDiagnostics diagnostics → Evidence) →
  Optional Evidence
evidenceFromCleanDiagnostics [] build =
  present (build tt)
evidenceFromCleanDiagnostics (d ∷ diagnostics) build =
  absent

cleanEvidenceFromCleanDiagnostics :
  ∀ {ℓ} {Evidence : Type ℓ} →
  (diagnostics : Diagnostics) →
  (build : CleanDiagnostics diagnostics → Evidence) →
  (clean : CleanDiagnostics diagnostics) →
  Present (evidenceFromCleanDiagnostics diagnostics build)
cleanEvidenceFromCleanDiagnostics [] build tt =
  presentWitness (build tt)
cleanEvidenceFromCleanDiagnostics (d ∷ diagnostics) build ()

cleanDiagnosticsFromEvidenceFromCleanDiagnostics :
  ∀ {ℓ} {Evidence : Type ℓ} →
  (diagnostics : Diagnostics) →
  (build : CleanDiagnostics diagnostics → Evidence) →
  Present (evidenceFromCleanDiagnostics diagnostics build) →
  CleanDiagnostics diagnostics
cleanDiagnosticsFromEvidenceFromCleanDiagnostics [] build proof =
  tt
cleanDiagnosticsFromEvidenceFromCleanDiagnostics (d ∷ diagnostics) build ()

presentValueFromEvidenceFromCleanDiagnostics :
  ∀ {ℓ} {Evidence : Type ℓ} →
  (diagnostics : Diagnostics) →
  (build : CleanDiagnostics diagnostics → Evidence) →
  (proof : Present (evidenceFromCleanDiagnostics diagnostics build)) →
  presentValue proof ≡
  build (cleanDiagnosticsFromEvidenceFromCleanDiagnostics diagnostics build proof)
presentValueFromEvidenceFromCleanDiagnostics [] build (presentWitness value) =
  refl
presentValueFromEvidenceFromCleanDiagnostics (d ∷ diagnostics) build ()

Clean :
  ∀ {ℓᵢ ℓᵉ ℓᵐ}
    {Input : Type ℓᵢ}
    {Evidence : Input → Type ℓᵉ}
    {Meaning : (input : Input) → Evidence input → Type ℓᵐ} →
  CheckResult Input Evidence Meaning → Type₀
Clean result =
  CleanDiagnostics (diagnostics result)

EvidenceAvailable :
  ∀ {ℓᵢ ℓᵉ ℓᵐ}
    {Input : Type ℓᵢ}
    {Evidence : Input → Type ℓᵉ}
    {Meaning : (input : Input) → Evidence input → Type ℓᵐ} →
  (result : CheckResult Input Evidence Meaning) → Type ℓᵉ
EvidenceAvailable result =
  Present (evidence? result)

EvidenceUnavailable :
  ∀ {ℓᵢ ℓᵉ ℓᵐ}
    {Input : Type ℓᵢ}
    {Evidence : Input → Type ℓᵉ}
    {Meaning : (input : Input) → Evidence input → Type ℓᵐ} →
  (result : CheckResult Input Evidence Meaning) → Type ℓᵉ
EvidenceUnavailable result =
  evidence? result ≡ absent

evidenceUnavailable :
  ∀ {ℓᵢ ℓᵉ ℓᵐ}
    {Input : Type ℓᵢ}
    {Evidence : Input → Type ℓᵉ}
    {Meaning : (input : Input) → Evidence input → Type ℓᵐ}
    (result : CheckResult Input Evidence Meaning) →
  evidence? result ≡ absent →
  EvidenceUnavailable result
evidenceUnavailable result proof =
  proof

evidenceValue :
  ∀ {ℓᵢ ℓᵉ ℓᵐ}
    {Input : Type ℓᵢ}
    {Evidence : Input → Type ℓᵉ}
    {Meaning : (input : Input) → Evidence input → Type ℓᵐ}
    (result : CheckResult Input Evidence Meaning) →
  EvidenceAvailable result → Evidence (input result)
evidenceValue result proof =
  presentValue proof

evidenceFromClean :
  ∀ {ℓᵢ ℓᵉ ℓᵐ}
    {Input : Type ℓᵢ}
    {Evidence : Input → Type ℓᵉ}
    {Meaning : (input : Input) → Evidence input → Type ℓᵐ}
    (result : CheckResult Input Evidence Meaning) →
  Clean result → Evidence (input result)
evidenceFromClean result clean =
  presentValue (cleanEvidence result clean)

soundFromClean :
  ∀ {ℓᵢ ℓᵉ ℓᵐ}
    {Input : Type ℓᵢ}
    {Evidence : Input → Type ℓᵉ}
    {Meaning : (input : Input) → Evidence input → Type ℓᵐ}
    (result : CheckResult Input Evidence Meaning)
    (clean : Clean result) →
  Meaning (input result) (evidenceFromClean result clean)
soundFromClean result clean =
  sound result (cleanEvidence result clean)