type term =
| Tvar of int
| Tint of int
| Tfun of term
| Tapp of term * term
type value =
| Vint of int
| Vclo of term * value list
type env = value list
type instr =
| Ivar of int
| Iint of int
| Iclo of instr list
| Iapp
| Iret
type mcode = instr list
type mvalue =
| Mint of int
| Mclo of mcode * mvalue list
type menv = mvalue list
type slot =
| Sval of mvalue
| Sret of mcode * menv
type mstack = slot list
let rec compile k = function
| Tvar i -> (Ivar i)::k
| Tint n -> (Iint n)::k
| Tfun t1 -> (Iclo (compile [Iret] t1))::k
| Tapp (t1,t2) -> compile (compile (Iapp::k) t2) t1
let rec run e s = function
| [] -> let (Sval v)::_ = s in v
| i::k -> match i with
| Ivar n -> run e (Sval(List.nth e n)::s) k
| Iint n -> run e (Sval(Mint(n))::s) k
| Iclo c -> run e (Sval(Mclo(c,e))::s) k
| Iapp -> let Sval(v)::Sval(Mclo(k2,e2))::s2 = s in
run (v::e2) (Sret(k,e)::s2) k2
| Iret -> let (Sval(v)::Sret(k2,e2)::s2) = s in
run e2 (Sval(v)::s2) k2
let exec t =
let k = compile [] t in
let Mint n = run [] [] k in
n