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)