module DCESH1 (Node : Set) where
open import GeneralLemmas
open import Heap
open import MachineCode Node
open import Relation
open import Tagged

ClosPtr = Ptr
mutual
  Closure = Code × Env
  data Val : Set where
    nat   :          Val
    clos  : ClosPtr   Val
  Env = List Val

ClosHeap = Heap Closure
ContPtr   = Ptr
Stack     = List Val × Maybe ContPtr
ContHeap  = Heap (Closure × Stack)

Thread    = Code × Env × Stack
Machine   = Maybe Thread × ClosHeap × ContHeap

data Msg : Set where
  APPLY   : ClosPtr   Val  ContPtr  Msg
  RETURN  : ContPtr   Val  Msg

data  _⟶<_>_ : Machine  Tagged Msg  Machine  Set where
  VAR             :  {n c e s v r clh conth}  lookup n e  just v 
    (just (VAR n SEQ c , e , s , r) , clh , conth) ⟶< silent > (just (c , e , v  s , r), clh , conth)
  CLOSURE         :  {c' c e s r clh conth}  let (clh' , clptr) = clh  (c' , e) in
    (just (CLOSURE c' SEQ c , e , s , r), clh , conth) ⟶< silent > (just (c , e , clos clptr  s , r) , clh' , conth)
  APPLY-send      :  {c e v clptr s r clh conth}  let (conth' , contptr) = conth  ((c , e) , s , r) in
    (just (APPLY SEQ c , e , v  clos clptr  s , r), clh , conth) ⟶< send (APPLY clptr v contptr) > (nothing , clh , conth')
  APPLY-receive   :  {clh conth clptr v contptr c e}  clh ! clptr  just (c , e) 
    (nothing , clh , conth) ⟶< receive (APPLY clptr v contptr) > (just (c , v  e , [] , just contptr), clh , conth)
  RETURN-send     :  {e v contptr clh conth} 
    (just (RETURN , e , v  [] , just contptr) , clh , conth) ⟶< send (RETURN contptr v) > (nothing , clh , conth)
  RETURN-receive  :  {clh conth contptr v c e s r}  conth ! contptr  just ((c , e), s , r) 
    (nothing , clh , conth) ⟶< receive (RETURN contptr v) > (just (c , e , v  s , r), clh , conth)
  COND-0          :  {c c' e s r clh conth} 
    (just (COND c c' , e , nat 0  s , r) , clh , conth) ⟶< silent > (just (c , e , s , r) , clh , conth)
  COND-suc        :  {c c' e n s r clh conth} 
    (just (COND c c' , e , nat (suc n)  s , r) , clh , conth) ⟶< silent > (just (c' , e , s , r) , clh , conth)
  LIT             :  {l c e s r clh conth} 
    (just (LIT l SEQ c , e , s , r), clh , conth) ⟶< silent > (just (c , e , nat l  s , r), clh , conth)
  PRIMOP          :  {f c e l₁ l₂ s r clh conth} 
     (just (PRIMOP f SEQ c , e , nat l₁  nat l₂  s , r), clh , conth) ⟶< silent > (just (c , e , nat (f l₁ l₂)  s , r), clh , conth)