```------------------------------------------------------------------------
-- "Reasoning" combinators
------------------------------------------------------------------------

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

open import Atom

module Reasoning (atoms : χ-atoms) where

open import Equality.Propositional

open import Chi    atoms
open import Values atoms

infix  -1 finally-⇓ _■⟨_⟩ _■⟨_⟩⋆
infixr -2 step-≡⇓ step-⇓ _⟶⟨⟩_ modus-ponens-⇓

step-≡⇓ : ∀ e₁ {e₂ e₃} → e₂ ⇓ e₃ → e₁ ≡ e₂ → e₁ ⇓ e₃
step-≡⇓ _ e₂⇓e₃ refl = e₂⇓e₃

syntax step-≡⇓ e₁ e₂⇓e₃ e₁≡e₂ = e₁ ≡⟨ e₁≡e₂ ⟩⟶ e₂⇓e₃

_⟶⟨⟩_ : ∀ e₁ {e₂} → e₁ ⇓ e₂ → e₁ ⇓ e₂
_ ⟶⟨⟩ e₁⇓e₂ = e₁⇓e₂

mutual

_■⟨_⟩ : ∀ e → Value e → e ⇓ e
_ ■⟨ lambda x e ⟩ = lambda
_ ■⟨ const c vs ⟩ = const (_ ■⟨ vs ⟩⋆)

_■⟨_⟩⋆ : ∀ es → Values es → es ⇓⋆ es
_ ■⟨ []     ⟩⋆ = []
_ ■⟨ v ∷ vs ⟩⋆ = (_ ■⟨ v ⟩) ∷ (_ ■⟨ vs ⟩⋆)

finally-⇓ : (e₁ e₂ : Exp) → e₁ ⇓ e₂ → e₁ ⇓ e₂
finally-⇓ _ _ e₁⇓e₂ = e₁⇓e₂

syntax finally-⇓ e₁ e₂ e₁⇓e₂ = e₁ ⇓⟨ e₁⇓e₂ ⟩■ e₂

modus-ponens-⇓ : ∀ e {e′ v} → e′ ⇓ v → (e′ ⇓ v → e ⇓ v) → e ⇓ v
modus-ponens-⇓ _ x f = f x

syntax modus-ponens-⇓ e x f = e ⟶⟨ f ⟩ x

mutual

trans-⇓ : ∀ {e₁ e₂ e₃} → e₁ ⇓ e₂ → e₂ ⇓ e₃ → e₁ ⇓ e₃
trans-⇓ (apply p q r)  s          = apply p q (trans-⇓ r s)
trans-⇓ (case p q r s) t          = case p q r (trans-⇓ s t)
trans-⇓ (rec p)        q          = rec (trans-⇓ p q)
trans-⇓ lambda         lambda     = lambda
trans-⇓ (const ps)     (const qs) = const (trans-⇓⋆ ps qs)

trans-⇓⋆ : ∀ {es₁ es₂ es₃} → es₁ ⇓⋆ es₂ → es₂ ⇓⋆ es₃ → es₁ ⇓⋆ es₃
trans-⇓⋆ []       []       = []
trans-⇓⋆ (p ∷ ps) (q ∷ qs) = trans-⇓ p q ∷ trans-⇓⋆ ps qs

step-⇓ : ∀ e₁ {e₂ e₃} → e₂ ⇓ e₃ → e₁ ⇓ e₂ → e₁ ⇓ e₃
step-⇓ _ e₂⇓e₃ e₁⇓e₂ = trans-⇓ e₁⇓e₂ e₂⇓e₃

syntax step-⇓ e₁ e₂⇓e₃ e₁⇓e₂ = e₁ ⇓⟨ e₁⇓e₂ ⟩ e₂⇓e₃
```