-- {-# OPTIONS --allow-unsolved-metas #-}

module Project.Do where

open import Project.Definitions using (Letk; Kont; Exp; Value; State; Type; kont; halt; letk; clo; zero; suc; mkState; `_; `ℕ; _·_; _⇒_; _,_; _[_∶_])
open import Project.Util using (_$_)

data StepResult (A : Type) : Set where
  part : State A → StepResult A
  done : Value A → StepResult A

-- Apply the continuation to the value, resulting in a state.
do-kont : ∀ {Tv Tω} (L : Letk Tv Tω) → Value Tv → State Tω
do-kont {Tv} {Tω} (letk {Tc} Γ C E k) v =
  let Γ′ = Γ , Tv in
  let E′ = E [ Tv ∶ v ] in
  mkState Tc Γ′ C E′ k

applykont : ∀ {Tv Tω} → Letk Tv Tω → Value Tv → StepResult Tω
applykont {Tv} (letk {Tc} Γ C E K) v =
  part $ mkState Tc (Γ , Tv) C (E [ Tv ∶ v ]) K

chain-kont : ∀ {A B C} → Letk A B → Letk B C → Letk A C
chain-kont (letk Γ C E halt) b = letk Γ C E $ kont b
chain-kont (letk Γ C E (kont k)) b = letk Γ C E $ kont $ chain-kont k b

do-apply-kont : ∀ {A B Tω} → Value (A ⇒ B) → Value A → Letk B Tω → StepResult Tω
do-apply-kont (clo {Γ} {A} {B} body e) v k =
  let Γ′ = Γ , A in
  let E′ = e [ A ∶ v ] in
  part $ mkState B Γ′ body E′ (kont k)
do-apply-kont (kont halt) a k = part $ do-kont k a
do-apply-kont {A} {B} {Tω} (kont (kont x)) a k = 
  let k′ = chain-kont x k in
  part $ do-kont k′ a
-- do-apply-kont (kont halt) b (letk Γ C E K) = {! done b  !}
-- do-apply-kont (kont (kont x)) b (letk Γ C E K) = {!   !}

-- This needs to be a separate function in order to unify B with Tω
do-apply-halt : ∀ {A Tω} → Value (A ⇒ Tω) → Value A → StepResult Tω
do-apply-halt {A} {Tω} (clo {Γ} body e) v =
  let Γ′ = Γ , A in
  let E′ = e [ A ∶ v ] in
  part $ mkState Tω Γ′ body E′ halt
do-apply-halt (kont halt) a = done a
do-apply-halt (kont (kont k)) a = part $ do-kont k a