open import GeneralLemmas using (Dec; _≡_)
module DCESH
  (Node : Set)
  (_≟_ : (n n' : Node)  Dec (n  n'))
  where
open import GeneralLemmas

open import Heap
open import Lambda
open Term Node
open import MachineCode Node as MachineCode
open import Relation
open import Tagged

RPtr = Ptr × Node
ClosPtr  = RPtr
mutual
  Closure = Code × Env
  data Value : Set where
    nat   :          Value
    clos  : ClosPtr   Value
  Env = List Value

ClosHeap = Heap Closure

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

ContPtr  = RPtr
Stack     = List StackElem × Maybe ContPtr
ContHeap  = Heap (Closure × Stack)

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

data Msg : Set where
  REMOTE  : Code      Node    ContPtr  Msg
  RETURN  : ContPtr   Value   Msg
  APPLY   : ClosPtr   Value   ContPtr  Msg

_⊢_▸_ : {A : Set}  Node   Heap A  A  Heap A × RPtr
i  h  x = let (h' , ptr) = h  x in h' , (ptr , i)

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

open import Network Node _≟_ _⊢_⟶Machine<_>_ public

initial-network-sync : Code  Node  SyncNetwork
initial-network-sync c i = update  i'  (nothing ,  , ))
  i (just (c , [] , [] , nothing),  , )

initial-network-async :  Code  Node  AsyncNetwork
initial-network-async c i = initial-network-sync c i , []