Require Import Deep. Notation "'c" := (`1`0) (at level 0) : var_scope. Notation "'compile" := (`2`0) (at level 0) : var_scope. Notation "'e" := (`1`1`0) (at level 0) : var_scope. Notation "'e2" := (`1`2`0) (at level 0) : var_scope. Notation "'i" := (`2`1`0) (at level 0) : var_scope. Notation "'k" := (`2`2`0) (at level 0) : var_scope. Notation "'k2" := (`1`1`1`0) (at level 0) : var_scope. Notation "'n" := (`1`1`2`0) (at level 0) : var_scope. Notation "'run" := (`1`2`1`0) (at level 0) : var_scope. Notation "'s" := (`1`2`2`0) (at level 0) : var_scope. Notation "'s2" := (`2`1`1`0) (at level 0) : var_scope. Notation "'t" := (`2`1`2`0) (at level 0) : var_scope. Notation "'t1" := (`2`2`1`0) (at level 0) : var_scope. Notation "'t2" := (`2`2`2`0) (at level 0) : var_scope. Notation "'v" := (`1`1`1`1`0) (at level 0) : var_scope. Inductive Term : Set := | Tvar : int -> Term | Tint : int -> Term | Tfun : Term -> Term | Tapp : Term -> Term -> Term. Definition tvar : con := `1`0. Definition tint : con := `2`0. Definition tfun : con := `1`1`0. Definition tapp : con := `1`2`0. Fixpoint _Term (X:Term) {struct X} : val := match X with | Tvar x0 => val_con tvar ((_Int x0)::nil) | Tint x0 => val_con tint ((_Int x0)::nil) | Tfun x0 => val_con tfun ((_Term x0)::nil) | Tapp x0 x1 => val_con tapp ((_Term x0)::(_Term x1)::nil) end. Inductive Value : Set := | Vint : int -> Value | Vclo : Term -> list Value -> Value. Definition vint : con := `2`1`0. Definition vclo : con := `2`2`0. Fixpoint _Value (X:Value) {struct X} : val := match X with | Vint x0 => val_con vint ((_Int x0)::nil) | Vclo x0 x1 => val_con vclo ((_Term x0)::(_List _Value x1)::nil) end. Definition Env := list Value. Definition _Env := _List _Value. Inductive Instr : Set := | Ivar : int -> Instr | Iint : int -> Instr | Iclo : list Instr -> Instr | Iapp : Instr | Iret : Instr. Definition ivar : con := `1`1`1`0. Definition iint : con := `1`1`2`0. Definition iclo : con := `1`2`1`0. Definition iapp : con := `1`2`2`0. Definition iret : con := `2`1`1`0. Fixpoint _Instr (X:Instr) {struct X} : val := match X with | Ivar x0 => val_con ivar ((_Int x0)::nil) | Iint x0 => val_con iint ((_Int x0)::nil) | Iclo x0 => val_con iclo ((_List _Instr x0)::nil) | Iapp => val_con iapp (nil) | Iret => val_con iret (nil) end. Definition Mcode := list Instr. Definition _Mcode := _List _Instr. Inductive Mvalue : Set := | Mint : int -> Mvalue | Mclo : Mcode -> list Mvalue -> Mvalue. Definition mint : con := `2`1`2`0. Definition mclo : con := `2`2`1`0. Fixpoint _Mvalue (X:Mvalue) {struct X} : val := match X with | Mint x0 => val_con mint ((_Int x0)::nil) | Mclo x0 x1 => val_con mclo ((_Mcode x0)::(_List _Mvalue x1)::nil) end. Definition Menv := list Mvalue. Definition _Menv := _List _Mvalue. Inductive Slot : Set := | Sval : Mvalue -> Slot | Sret : Mcode -> Menv -> Slot. Definition sval : con := `2`2`2`0. Definition sret : con := `1`1`1`1`0. Fixpoint _Slot (X:Slot) {struct X} : val := match X with | Sval x0 => val_con sval ((_Mvalue x0)::nil) | Sret x0 x1 => val_con sret ((_Mcode x0)::(_Menv x1)::nil) end. Definition Mstack := list Slot. Definition _Mstack := _List _Slot. Definition compile : val := 'let_rec_fun 'compile '= 'fun '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. Definition run : val := 'let_rec_fun 'run '= 'fun 'e '-> 'fun '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). Definition exec : val := ('fun 't '-> 'let 'k '= compile ' '[] ' 't 'in 'let (mint#('n)) '= run ' '[] ' '[] ' 'k 'in 'n)%val.