```------------------------------------------------------------------------
-- Values
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Atom

module Values (atoms : χ-atoms) where

open import Equality.Propositional
open import Prelude hiding (const)

open import Chi atoms
open import Deterministic atoms

open χ-atoms atoms

-- Values.

mutual

infixr 5 _∷_

data Value : Exp → Set where
lambda : ∀ x e → Value (lambda x e)
const  : ∀ c {es} → Values es → Value (const c es)

data Values : List Exp → Set where
[]  : Values []
_∷_ : ∀ {e es} → Value e → Values es → Values (e ∷ es)

-- Constructor applications.

data Consts : Set where
const : Const → List Consts → Consts

mutual

data Constructor-application : Exp → Set where
const : ∀ c {es} →
Constructor-applications es →
Constructor-application (const c es)

data Constructor-applications : List Exp → Set where
[]  : Constructor-applications []
_∷_ : ∀ {e es} →
Constructor-application e → Constructor-applications es →
Constructor-applications (e ∷ es)

-- Constructor applications are values.

mutual

const→value : ∀ {e} → Constructor-application e → Value e
const→value (const c cs) = const c (consts→values cs)

consts→values : ∀ {es} → Constructor-applications es → Values es
consts→values []       = []
consts→values (c ∷ cs) = const→value c ∷ consts→values cs

-- The second argument of _⇓_ is always a Value.

mutual

⇓-Value : ∀ {e v} → e ⇓ v → Value v
⇓-Value (apply _ _ p)  = ⇓-Value p
⇓-Value (case _ _ _ p) = ⇓-Value p
⇓-Value (rec p)        = ⇓-Value p
⇓-Value lambda         = lambda _ _
⇓-Value (const ps)     = const _ (⇓⋆-Values ps)

⇓⋆-Values : ∀ {es vs} → es ⇓⋆ vs → Values vs
⇓⋆-Values []       = []
⇓⋆-Values (p ∷ ps) = ⇓-Value p ∷ ⇓⋆-Values ps

mutual

values-compute-to-themselves : ∀ {v} → Value v → v ⇓ v
values-compute-to-themselves (lambda _ _) = lambda
values-compute-to-themselves (const _ ps) =
const (values-compute-to-themselves⋆ ps)

values-compute-to-themselves⋆ : ∀ {vs} → Values vs → vs ⇓⋆ vs
values-compute-to-themselves⋆ []       = []
values-compute-to-themselves⋆ (p ∷ ps) =
values-compute-to-themselves p ∷ values-compute-to-themselves⋆ ps

values-only-compute-to-themselves :
∀ {v₁ v₂} → Value v₁ → v₁ ⇓ v₂ → v₁ ≡ v₂
values-only-compute-to-themselves p q =
⇓-deterministic (values-compute-to-themselves p) q

values-only-compute-to-themselves⋆ :
∀ {vs₁ vs₂} → Values vs₁ → vs₁ ⇓⋆ vs₂ → vs₁ ≡ vs₂
values-only-compute-to-themselves⋆ ps qs =
⇓⋆-deterministic (values-compute-to-themselves⋆ ps) qs
```