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)))