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

module Project.Cesk where

open import Data.Product renaming (_,_ to ⦅_,_⦆)
open import Project.Definitions using (Aexp; Exp; Env; State; Letk; Kont; Value; Type; atomic; kont; letk; lookup; call/cc; case; mkState; halt; `ℕ; _,_; _k⇒_; _⇒_; _∋_; _·_; _∘_; _[_∶_]; ∅)
open import Project.Util using (_$_)
open import Project.Do using (StepResult; part; done; do-kont; do-apply)

open Aexp
open Value
open State

astep : ∀ {Γ A} → Aexp Γ A → Env Γ → Value A
astep zero _  = zero
astep (suc c) e = suc $ astep c e
astep (` id) e = lookup e id
astep (ƛ body) e = clo body e

inject : (A : Type) → Exp ∅ A → State A
inject A C = mkState A ∅ C ∅ halt

step : ∀ {Tω : Type} → State Tω → StepResult Tω
step (mkState Tc Γ (case c cz cs) E K) with ⦅ astep c E , astep cs E ⦆
... | ⦅ zero , _ ⦆ = part $ mkState Tc Γ cz E K
... | ⦅ suc n , clo {Γc} cc cloE ⦆ =
        part $ mkState Tc (Γc , `ℕ) cc (cloE [ `ℕ ∶ n ]) K
step (mkState Tc Γ (C₁ · C₂) E K) =
  let C₁′ = astep C₁ E in
  let C₂′ = astep C₂ E in
  do-apply C₁′ C₂′ K
step (mkState Tc Γ (atomic x) E K) with K
... | halt = done $ astep x E
... | kont l = part $ do-kont l $ astep x E
step (mkState Tc Γ (call/cc C) E K) =
  part $ mkState ({!   !} k⇒ {!   !}) Γ {!  !} {!   !} {!   !}

-- 3 + (call/cc k . k 2 + k 4)
-- (k . k 2 + k 4) (\x . 3 + x)
-- ((\x . 3 + x) 2 + (\x . 3 + x) 4)