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