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

module Spartan6.Validation.CheckResult where

open import Spartan6.Prelude

import Spartan6.Validation.Diagnostic as Diagnostic

open import Cubical.Data.Bool.Properties using (false≢true)
import Cubical.Data.Empty as Empty

-- Representation-independent eliminators and constructor facts for the
-- existing diagnostic result type.  Domain-specific canonicality predicates
-- stay in their owning validation modules.

foldResult : ∀ {A B : Type₀}
  → (Diagnostic.Diagnostics → B)
  → (A → B)
  → Diagnostic.CheckResult A
  → B
foldResult on-rejected on-accepted (Diagnostic.accepted value) =
  on-accepted value
foldResult on-rejected on-accepted (Diagnostic.rejected diagnostics) =
  on-rejected diagnostics

accepted? : ∀ {A : Type₀} → Diagnostic.CheckResult A → Bool
accepted? (Diagnostic.accepted value) = true
accepted? (Diagnostic.rejected diagnostics) = false

extractAccepted : ∀ {A : Type₀}
  → (result : Diagnostic.CheckResult A)
  → accepted? result ≡ true → A
extractAccepted (Diagnostic.accepted value) proof = value
extractAccepted (Diagnostic.rejected diagnostics) proof =
  Empty.rec (false≢true proof)

rejected≢accepted : ∀ {A : Type₀} {diagnostics value}
  → Diagnostic.rejected {A = A} diagnostics
    ≡ Diagnostic.accepted value
  → Empty.⊥
rejected≢accepted path = false≢true (cong accepted? path)

accepted≢rejected : ∀ {A : Type₀} {value diagnostics}
  → Diagnostic.accepted value
    ≡ Diagnostic.rejected {A = A} diagnostics
  → Empty.⊥
accepted≢rejected path = rejected≢accepted (sym path)

accepted-injective : ∀ {A : Type₀} {left right : A}
  → Diagnostic.accepted left ≡ Diagnostic.accepted right
  → left ≡ right
accepted-injective {left = left} path =
  cong
    (foldResult (λ diagnostics → left) (λ value → value))
    path

rejected-injective : ∀ {A : Type₀} {left right}
  → Diagnostic.rejected {A = A} left
    ≡ Diagnostic.rejected right
  → left ≡ right
rejected-injective {left = left} path =
  cong
    (foldResult (λ diagnostics → diagnostics) (λ value → left))
    path

andThen : ∀ {A B : Type₀}
  → Diagnostic.CheckResult A
  → (A → Diagnostic.CheckResult B)
  → Diagnostic.CheckResult B
andThen (Diagnostic.accepted value) next = next value
andThen (Diagnostic.rejected diagnostics) next =
  Diagnostic.rejected diagnostics

traverseResults : ∀ {A B : Type₀}
  → (A → Diagnostic.CheckResult B)
  → List A
  → Diagnostic.CheckResult (List B)
traverseResults check []ᴸ = Diagnostic.accepted []ᴸ
traverseResults check (value ∷ᴸ values) with check value
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted checked with traverseResults check values
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted checked-values =
  Diagnostic.accepted (checked ∷ᴸ checked-values)

sequenceResults : ∀ {A : Type₀}
  → List (Diagnostic.CheckResult A)
  → Diagnostic.CheckResult (List A)
sequenceResults = traverseResults (λ result → result)

mapResult-identity : ∀ {A : Type₀} (result : Diagnostic.CheckResult A)
  → Diagnostic.mapResult (λ value → value) result ≡ result
mapResult-identity (Diagnostic.accepted value) = refl
mapResult-identity (Diagnostic.rejected diagnostics) = refl

mapResult-compose : ∀ {A B C : Type₀}
  (first : A → B)
  (second : B → C)
  (result : Diagnostic.CheckResult A)
  → Diagnostic.mapResult second (Diagnostic.mapResult first result)
    ≡ Diagnostic.mapResult (λ value → second (first value)) result
mapResult-compose first second (Diagnostic.accepted value) = refl
mapResult-compose first second (Diagnostic.rejected diagnostics) = refl

andThen-accepted : ∀ {A B : Type₀}
  (value : A) (next : A → Diagnostic.CheckResult B)
  → andThen (Diagnostic.accepted value) next ≡ next value
andThen-accepted value next = refl

andThen-rejected : ∀ {A B : Type₀}
  (diagnostics : Diagnostic.Diagnostics)
  (next : A → Diagnostic.CheckResult B)
  → andThen (Diagnostic.rejected diagnostics) next
    ≡ Diagnostic.rejected diagnostics
andThen-rejected diagnostics next = refl

traverseResults-empty : ∀ {A B : Type₀}
  (check : A → Diagnostic.CheckResult B)
  → traverseResults check []ᴸ ≡ Diagnostic.accepted []ᴸ
traverseResults-empty check = refl