module MachineCode(Node : Set) where open import GeneralLemmas open import Lambda Node mutual data Instr : Set where VAR : ℕ → Instr CLOSURE : Code → Instr APPLY : Instr LIT : ℕ → Instr PRIMOP : (ℕ → ℕ → ℕ) → Instr REMOTE : Code → Node → Instr data Code : Set where _SEQ_ : Instr → Code → Code COND : Code → Code → Code END : Code RETURN : Code compile' : Term → Code → Code compile' (ƛ t) c = CLOSURE (compile' t RETURN) SEQ c compile' (t $ t') c = compile' t (compile' t' (APPLY SEQ c)) compile' (var x) c = VAR x SEQ c compile' (lit n) c = LIT n SEQ c compile' (op f t t') c = compile' t' (compile' t (PRIMOP f SEQ c)) compile' (if0 b then t else f) c = compile' b (COND (compile' t c) (compile' f c)) compile' (t at i) c = REMOTE (compile' t RETURN) i SEQ c compile : Term → Code compile t = compile' t END codeExample = compile ((ƛ var 0) $ (ƛ (ƛ var 1)))