module CES(Node : Set) where open import GeneralLemmas open import MachineCode Node open import Relation mutual Closure = Code × Env data Value : Set where nat : ℕ → Value clos : Closure → Value Env = List Value data StackElem : Set where val : Value → StackElem cont : Closure → StackElem Stack = List StackElem Config = Code × Env × Stack data _⟶CES_ : Rel Config Config where VAR : ∀ {n c e s v} → lookup n e ≡ just v → (VAR n SEQ c , e , s) ⟶CES (c , e , val v ∷ s) CLOSURE : ∀ {c' c e s} → (CLOSURE c' SEQ c , e , s) ⟶CES (c , e , val (clos (c' , e)) ∷ s) APPLY : ∀ {c e v c' e' s} → (APPLY SEQ c , e , val v ∷ val (clos (c' , e')) ∷ s) ⟶CES (c' , v ∷ e' , cont (c , e) ∷ s) RETURN : ∀ {e v c e' s} → (RETURN , e , val v ∷ cont (c , e') ∷ s) ⟶CES (c , e' , val v ∷ s) LIT : ∀ {n c e s} → (LIT n SEQ c , e , s) ⟶CES (c , e , val (nat n) ∷ s) PRIMOP : ∀ {f c e n₁ n₂ s} → (PRIMOP f SEQ c , e , val (nat n₁) ∷ val (nat n₂) ∷ s) ⟶CES (c , e , val (nat (f n₁ n₂)) ∷ s) COND-0 : ∀ {c c' e s} → (COND c c' , e , val (nat 0) ∷ s) ⟶CES (c , e , s) COND-suc : ∀ {c c' e n s} → (COND c c' , e , val (nat (suc n)) ∷ s) ⟶CES (c' , e , s) REMOTE : ∀ {c' i c e s} → (REMOTE c' i SEQ c , e , s) ⟶CES (c' , [] , cont (c , e) ∷ s)