module CES(Node : Set) where

open import GeneralLemmas

open import MachineCode Node
open import Relation

mutual
  Closure = Code × Env
  data Value : Set where
    nat   :          Value
    clos  : Closure   Value
  Env = List Value

data StackElem : Set where
  val   : Value     StackElem
  cont  : Closure   StackElem

Stack = List StackElem

Config = Code × Env × Stack

data _⟶CES_ : Rel Config Config where
  VAR       :  {n c e s v}  lookup n e  just v   (VAR n SEQ c , e , s) ⟶CES (c ,    e , val v  s)
  CLOSURE   :  {c' c e s}        (CLOSURE c' SEQ c , e , s) ⟶CES (c ,  e , val (clos (c' , e))  s)
  APPLY     :  {c e v c' e' s}   (APPLY SEQ c , e , val v  val (clos (c' , e'))  s) ⟶CES (c' , v  e' , cont (c , e)  s)
  RETURN    :  {e v c e' s}      (RETURN , e , val v  cont (c , e')  s) ⟶CES (c , e' , val v  s)
  LIT       :  {n c e s}         (LIT n SEQ c , e , s) ⟶CES (c , e , val (nat n)  s)
  PRIMOP    :  {f c e n₁ n₂ s}   (PRIMOP f SEQ c , e , val (nat n₁)  val (nat n₂)  s)  ⟶CES (c , e , val (nat (f n₁ n₂))  s)
  COND-0    :  {c c' e s}        (COND c c' , e , val (nat 0)  s) ⟶CES (c , e , s)
  COND-suc  :  {c c' e n s}      (COND c c' , e , val (nat (suc n))  s) ⟶CES (c' , e , s)
  REMOTE    :  {c' i c e s}      (REMOTE c' i SEQ c , e , s) ⟶CES (c' , [] , cont (c , e)  s)