module CESH(Node : Set) where

open import GeneralLemmas

open import Heap
open import MachineCode Node
open import Relation

ClosPtr = Ptr
mutual
  Closure = Code × Env
  data Value : Set where
    nat   :          Value
    clos  : ClosPtr   Value
  Env = List Value
data StackElem : Set where
  val   : Value     StackElem
  cont  : Closure   StackElem

Stack = List StackElem
ClosHeap = Heap Closure
Config = Code × Env × Stack × ClosHeap

data _⟶CESH_ : Rel Config Config where
  CLOSURE   :  {c' c e s h}  let (h' , clptr) = h  (c' , e) in
    (CLOSURE c' SEQ c , e , s , h) ⟶CESH (c , e , val (clos clptr)  s , h')
  APPLY     :  {c e v clptr c' e' s h}  h ! clptr  just (c' , e') 
    (APPLY SEQ c , e , val v  val (clos clptr)  s , h) ⟶CESH (c' , v  e' , cont (c , e)  s , h)
  VAR       :  {n c e s h v}  lookup n e  just v 
    (VAR n SEQ c , e , s , h) ⟶CESH (c , e , val v  s , h)
  RETURN    :  {e v c e' s h} 
    (RETURN , e , val v  cont (c , e')  s , h) ⟶CESH (c , e' , val v  s , h)
  LIT       :  {l c e s h} 
    (LIT l SEQ c , e , s , h) ⟶CESH (c , e , val (nat l)  s , h)
  PRIMOP    :  {f c e l₁ l₂ s h} 
    (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s , h) ⟶CESH (c , e , val (nat (f l₁ l₂))  s , h)
  COND-0    :  {c c' e s h} 
    (COND c c' , e , val (nat 0)  s , h) ⟶CESH (c , e , s , h)
  COND-suc  :  {c c' e n s h} 
    (COND c c' , e , val (nat (suc n))  s , h) ⟶CESH (c' , e , s , h)
  REMOTE   :  {c' i c e s h} 
    (REMOTE c' i SEQ c , e , s , h) ⟶CESH (c' , [] , cont (c , e)  s , h)