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)