{-# 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

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 x) b k = part $ do-kont 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) b = done b
do-apply-halt (kont (kont x)) b = part $ do-kont x b