Require Import Deep.

Notation "'b" := (`1`0) (at level 0) : var_scope.
Notation "'eval" := (`2`0) (at level 0) : var_scope.
Notation "'subst" := (`1`1`0) (at level 0) : var_scope.
Notation "'t" := (`1`2`0) (at level 0) : var_scope.
Notation "'t1" := (`2`1`0) (at level 0) : var_scope.
Notation "'t2" := (`2`2`0) (at level 0) : var_scope.
Notation "'v" := (`1`1`1`0) (at level 0) : var_scope.
Notation "'x" := (`1`1`2`0) (at level 0) : var_scope.
Notation "'y" := (`1`2`1`0) (at level 0) : var_scope.

Inductive Term : Set :=
  | Tvar : int -> Term
  | Tint : int -> Term
  | Tfun : int -> 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 x1 => val_con tfun ((_Int x0)::(_Term x1)::nil)
  | Tapp x0 x1 => val_con tapp ((_Term x0)::(_Term x1)::nil)
end.

Definition subst : val := 'let_rec_fun 'subst '= 'fun 'x '->
'fun 'v '->
'fun 't '->
('match 't 'with
 '| (tvar#('y)) '-> 'if prim_equ ' 'x ' 'y 'then 'v 'else 't '| (tint#('_)) '-> 't '| (tfun#('y,'b)) '->
tfun#('y, 'if prim_equ ' 'x ' 'y 'then 'b 'else 'subst ' 'x ' 'v ' 'b) '| (tapp#('t1,'t2)) '-> tapp#('subst ' 'x ' 'v ' 't1, 'subst ' 'x ' 'v ' 't2)).

Definition eval : val := 'let_rec_fun 'eval '= 'fun 't '->
('match 't 'with
 '| (tvar#('y)) '-> 'fail '| (tapp#('t1,'t2)) '->
'let (tfun#('y,'b)) '= 'eval ' 't1 'in
'eval ' (subst ' 'y ' ('eval ' 't2) ' 'b) '| '_ '-> 't).