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.