------------------------------------------------------------------------
-- "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₂ ⟩T e₂⟶e₃