module Project.Cesk where

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Product renaming (_,_ to ⦅_,_⦆)
open import Project.Definitions
open import Project.Util using (_$_)
open import Project.Do

open Aexp
open Value
open State

astep : ∀ {Tω Γ A} → Aexp Tω Γ A → Env Tω Γ → Value Tω A
astep (value v) _ = v
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 ∅ A → State A
inject {A} C = mkState A ∅ C ∅ halt

step : ∀ {Tω : Type} → State Tω → StepResult Tω
step (mkState Tc Γ (atomic x) E K) = apply-kont K $ astep x E
step (mkState Tc Γ (case C isZ isS) E K) with astep C E
... | zero = part $ mkState Tc Γ isZ E K
... | suc n = part $ mkState Tc Γ (isS · value n) E K
step (mkState Tc Γ (x₁ · x₂) E K) with astep x₁ E
... | clo body env = apply-proc-clo body env (astep x₂ E) K
step (mkState Tc Γ (x₁ ∘ x₂) E K) with astep x₁ E
... | cont k =
  let val = astep x₂ E in
  let K′ = kont $ letk Γ (atomic $ ` zero) E k in
  apply-kont K′ val
step {Tω} (mkState Tc Γ (call/cc {A} aexp) E K) with astep aexp E
... | clo {Γc} body env =
  let Γ′ = Γc , K[ A ⇒ ⊥ ] in
  let E′ = env [ K[ A ⇒ ⊥ ] ∶ cont K ] in
  part $ mkState Tω Γ′ body E′ halt
step (mkState Tc Γ (abort V⊥) E K) with astep V⊥ E
... | ()
step (mkState Tc Γ (`let {A} C₁ C₂) E K) =
  let K′ = letk Γ C₂ E K in
  part $ mkState A Γ C₁ E (kont K′)

data EvalResult : Set where
  complete : ∀ {A} → StepResult A → EvalResult
  exhausted : ∀ {A} → State A → EvalResult

eval′ : ∀ {A} → ℕ → State A → EvalResult
eval′ 0 s = exhausted s
eval′ (suc n) s with step s
... | part x = eval′ n x
... | done x = complete $ done x

eval : ∀ {A} → ℕ → Exp A ∅ A → EvalResult
eval n e = eval′ n (inject e)

exp : Exp `ℕ ∅ `ℕ
exp = 
  `let (call/cc (ƛ (`let (` zero ∘ suc (suc zero)) (abort (` zero)))))
  ((ƛ $ atomic $ suc $ ` zero) · ` zero)

expRes+ : eval 7 exp ≡ (complete $ done $ (suc (suc (suc zero))))
expRes+ = refl