Require Import Deep.

Notation "'a" := (`1`0) (at level 0) : var_scope.
Notation "'a1" := (`2`0) (at level 0) : var_scope.
Notation "'a2" := (`1`1`0) (at level 0) : var_scope.
Notation "'accu" := (`1`2`0) (at level 0) : var_scope.
Notation "'append" := (`2`1`0) (at level 0) : var_scope.
Notation "'assoc" := (`2`2`0) (at level 0) : var_scope.
Notation "'b" := (`1`1`1`0) (at level 0) : var_scope.
Notation "'chop" := (`1`1`2`0) (at level 0) : var_scope.
Notation "'cmp" := (`1`2`1`0) (at level 0) : var_scope.
Notation "'combine" := (`1`2`2`0) (at level 0) : var_scope.
Notation "'exists2_" := (`2`1`1`0) (at level 0) : var_scope.
Notation "'exists_" := (`2`1`2`0) (at level 0) : var_scope.
Notation "'f" := (`2`2`1`0) (at level 0) : var_scope.
Notation "'find" := (`2`2`2`0) (at level 0) : var_scope.
Notation "'flatten" := (`1`1`1`1`0) (at level 0) : var_scope.
Notation "'fold_left" := (`1`1`1`2`0) (at level 0) : var_scope.
Notation "'fold_left2" := (`1`1`2`1`0) (at level 0) : var_scope.
Notation "'fold_right" := (`1`1`2`2`0) (at level 0) : var_scope.
Notation "'fold_right2" := (`1`2`1`1`0) (at level 0) : var_scope.
Notation "'for_all" := (`1`2`1`2`0) (at level 0) : var_scope.
Notation "'for_all2" := (`1`2`2`1`0) (at level 0) : var_scope.
Notation "'h1" := (`1`2`2`2`0) (at level 0) : var_scope.
Notation "'h2" := (`2`1`1`1`0) (at level 0) : var_scope.
Notation "'k" := (`2`1`1`2`0) (at level 0) : var_scope.
Notation "'l" := (`2`1`2`1`0) (at level 0) : var_scope.
Notation "'l1" := (`2`1`2`2`0) (at level 0) : var_scope.
Notation "'l2" := (`2`2`1`1`0) (at level 0) : var_scope.
Notation "'len" := (`2`2`1`2`0) (at level 0) : var_scope.
Notation "'length_aux" := (`2`2`2`1`0) (at level 0) : var_scope.
Notation "'map" := (`2`2`2`2`0) (at level 0) : var_scope.
Notation "'map2" := (`1`1`1`1`1`0) (at level 0) : var_scope.
Notation "'mem" := (`1`1`1`1`2`0) (at level 0) : var_scope.
Notation "'mem_assoc" := (`1`1`1`2`1`0) (at level 0) : var_scope.
Notation "'merge" := (`1`1`1`2`2`0) (at level 0) : var_scope.
Notation "'my_find" := (`1`1`2`1`1`0) (at level 0) : var_scope.

Notation "'no" := (`1`1`2`2`1`0) (at level 0) : var_scope.
Notation "'nth_aux" := (`1`1`2`2`2`0) (at level 0) : var_scope.
Notation "'p" := (`1`2`1`1`1`0) (at level 0) : var_scope.
Notation "'pair" := (`1`2`1`1`2`0) (at level 0) : var_scope.
Notation "'part" := (`1`2`1`2`1`0) (at level 0) : var_scope.
Notation "'r" := (`1`2`1`2`2`0) (at level 0) : var_scope.
Notation "'remove_assoc" := (`1`2`2`1`1`0) (at level 0) : var_scope.
Notation "'rev_append" := (`1`2`2`1`2`0) (at level 0) : var_scope.
Notation "'rmap2_f" := (`1`2`2`2`1`0) (at level 0) : var_scope.
Notation "'rmap_f" := (`1`2`2`2`2`0) (at level 0) : var_scope.
Notation "'rx" := (`2`1`1`1`1`0) (at level 0) : var_scope.
Notation "'ry" := (`2`1`1`1`2`0) (at level 0) : var_scope.
Notation "'split" := (`2`1`1`2`1`0) (at level 0) : var_scope.
Notation "'t" := (`2`1`1`2`2`0) (at level 0) : var_scope.
Notation "'t1" := (`2`1`2`1`1`0) (at level 0) : var_scope.
Notation "'t2" := (`2`1`2`1`2`0) (at level 0) : var_scope.
Notation "'x" := (`2`1`2`2`1`0) (at level 0) : var_scope.
Notation "'y" := (`2`1`2`2`2`0) (at level 0) : var_scope.
Notation "'yes" := (`2`2`1`1`1`0) (at level 0) : var_scope.
Notation "'n" := (`1`1`2`1`2`0) (at level 0) : var_scope.
Definition length_aux : val := 'let_rec_fun 'length_aux '= 'fun 'len '->
'function 
  '| '[] '-> 'len
  '| ('a'::'l) '-> 'length_aux ' (prim_add ' 'len ' (_Int 1)) ' 'l.

Definition length : val := ('fun 'l '-> length_aux ' (_Int 0) ' 'l)%val.

Definition hd : val := ('function 
  '| '[] '-> 'fail
  '| ('a'::'l) '-> 'a)%val.

Definition tl : val := ('function 
  '| '[] '-> 'fail
  '| ('a'::'l) '-> 'l)%val.

Definition nth : val := ('fun 'l '->
'fun 'n '->
'if prim_lt ' 'n ' (_Int 0) 'then 'fail
'else 'let_rec_fun 'nth_aux '=
'fun 'l '->
'fun 'n '->
('match 'l 'with
 '| '[] '-> 'fail '| ('a'::'l) '->
'if prim_equ ' 'n ' (_Int 0) 'then 'a
'else 'nth_aux ' 'l ' (prim_sub ' 'n ' (_Int 1))) 'in
'nth_aux ' 'l ' 'n)%val.

Definition append : val := 'let_rec_fun 'append '= 'fun 'l1 '->
'fun 'l2 '->
('match 'l1 'with  '| '[] '-> 'l2 '| ('a'::'l) '-> 'a'::('append ' 'l ' 'l2)).

Definition rev_append : val := 'let_rec_fun 'rev_append '= 'fun 'l1 '->
'fun 'l2 '->
('match 'l1 'with
 '| '[] '-> 'l2 '| ('a'::'l) '-> 'rev_append ' 'l ' ('a'::'l2)).

Definition rev : val := ('fun 'l '-> rev_append ' 'l ' '[])%val.

Definition flatten : val := 'let_rec_function 'flatten '= 'function 
  '| '[] '-> '[]
  '| ('l'::'r) '-> append ' 'l ' ('flatten ' 'r).

Definition concat : val := (flatten)%val.

Definition map : val := 'let_rec_fun 'map '= 'fun 'f '->
'function 
  '| '[] '-> '[]
  '| ('a'::'l) '-> 'let 'r '= 'f ' 'a 'in 'r'::('map ' 'f ' 'l).

Definition rev_map : val := ('fun 'f '->
'fun 'l '->
'let_rec_fun 'rmap_f '=
'fun 'accu '->
'function 
  '| '[] '-> 'accu
  '| ('a'::'l) '-> 'rmap_f ' (('f ' 'a)'::'accu) ' 'l 'in
'rmap_f ' '[] ' 'l)%val.

Definition fold_left : val := 'let_rec_fun 'fold_left '= 'fun 'f '->
'fun 'accu '->
'fun 'l '->
('match 'l 'with
 '| '[] '-> 'accu '| ('a'::'l) '-> 'fold_left ' 'f ' ('f ' 'accu ' 'a) ' 'l).

Definition fold_right : val := 'let_rec_fun 'fold_right '= 'fun 'f '->
'fun 'l '->
'fun 'accu '->
('match 'l 'with
 '| '[] '-> 'accu '| ('a'::'l) '-> 'f ' 'a ' ('fold_right ' 'f ' 'l ' 'accu)).

Definition map2 : val := 'let_rec_fun 'map2 '= 'fun 'f '->
'fun 'l1 '->
'fun 'l2 '->
('match #('l1, 'l2) 'with
 '| (#('[],'[])) '-> '[] '| (#('a1'::'l1,'a2'::'l2)) '->
'let 'r '= 'f ' 'a1 ' 'a2 'in 'r'::('map2 ' 'f ' 'l1 ' 'l2) '| (#('_,'_)) '-> 'fail).

Definition rev_map2 : val := ('fun 'f '->
'fun 'l1 '->
'fun 'l2 '->
'let_rec_fun 'rmap2_f '=
'fun 'accu '->
'fun 'l1 '->
'fun 'l2 '->
('match #('l1, 'l2) 'with
 '| (#('[],'[])) '-> 'accu '| (#('a1'::'l1,'a2'::'l2)) '->
'rmap2_f ' (('f ' 'a1 ' 'a2)'::'accu) ' 'l1 ' 'l2 '| (#('_,'_)) '-> 'fail) 'in
'rmap2_f ' '[] ' 'l1 ' 'l2)%val.

Definition fold_left2 : val := 'let_rec_fun 'fold_left2 '= 'fun 'f '->
'fun 'accu '->
'fun 'l1 '->
'fun 'l2 '->
('match #('l1, 'l2) 'with
 '| (#('[],'[])) '-> 'accu '| (#('a1'::'l1,'a2'::'l2)) '->
'fold_left2 ' 'f ' ('f ' 'accu ' 'a1 ' 'a2) ' 'l1 ' 'l2 '| (#('_,'_)) '-> 'fail).

Definition fold_right2 : val := 'let_rec_fun 'fold_right2 '= 'fun 'f '->
'fun 'l1 '->
'fun 'l2 '->
'fun 'accu '->
('match #('l1, 'l2) 'with
 '| (#('[],'[])) '-> 'accu '| (#('a1'::'l1,'a2'::'l2)) '->
'f ' 'a1 ' 'a2 ' ('fold_right2 ' 'f ' 'l1 ' 'l2 ' 'accu) '| (#('_,'_)) '-> 'fail).

Definition for_all : val := 'let_rec_fun 'for_all '= 'fun 'p '->
'function 
  '| '[] '-> true
  '| ('a'::'l) '-> prim_and ' ('p ' 'a) ' ('for_all ' 'p ' 'l).

Definition exists_ : val := 'let_rec_fun 'exists_ '= 'fun 'p '->
'function 
  '| '[] '-> false
  '| ('a'::'l) '-> prim_or ' ('p ' 'a) ' ('exists_ ' 'p ' 'l).

Definition for_all2 : val := 'let_rec_fun 'for_all2 '= 'fun 'p '->
'fun 'l1 '->
'fun 'l2 '->
('match #('l1, 'l2) 'with
 '| (#('[],'[])) '-> true '| (#('a1'::'l1,'a2'::'l2)) '->
prim_and ' ('p ' 'a1 ' 'a2) ' ('for_all2 ' 'p ' 'l1 ' 'l2) '| (#('_,'_)) '-> 'fail).

Definition exists2_ : val := 'let_rec_fun 'exists2_ '= 'fun 'p '->
'fun 'l1 '->
'fun 'l2 '->
('match #('l1, 'l2) 'with
 '| (#('[],'[])) '-> false '| (#('a1'::'l1,'a2'::'l2)) '->
prim_or ' ('p ' 'a1 ' 'a2) ' ('exists2_ ' 'p ' 'l1 ' 'l2) '| (#('_,'_)) '-> 'fail).

Definition mem : val := 'let_rec_fun 'mem '= 'fun 'x '->
'function 
  '| '[] '-> false
  '| ('a'::'l) '->
prim_or ' (prim_equ ' (compare ' 'a ' 'x) ' (_Int 0)) ' ('mem ' 'x ' 'l).

Definition assoc : val := 'let_rec_fun 'assoc '= 'fun 'x '->
'function 
  '| '[] '-> 'raise ' ('Not_found#)
  '| ((#('a,'b))'::'l) '->
'if prim_equ ' (compare ' 'a ' 'x) ' (_Int 0) 'then 'b 'else 'assoc ' 'x ' 'l.

Definition mem_assoc : val := 'let_rec_fun 'mem_assoc '= 'fun 'x '->
'function 
  '| '[] '-> false
  '| ((#('a,'b))'::'l) '->
prim_or ' (prim_equ ' (compare ' 'a ' 'x) ' (_Int 0)) ' ('mem_assoc ' 'x ' 'l).

Definition remove_assoc : val := 'let_rec_fun 'remove_assoc '= 'fun 'x '->
'function 
  '| '[] '-> '[]
  '| ((#('a,'b) 'as 'pair)'::'l) '->
'if prim_equ ' (compare ' 'a ' 'x) ' (_Int 0) 'then 'l
'else 'pair'::('remove_assoc ' 'x ' 'l).

Definition find : val := 'let_rec_fun 'find '= 'fun 'p '->
'function 
  '| '[] '-> 'raise ' ('Not_found#)
  '| ('x'::'l) '-> 'if 'p ' 'x 'then 'x 'else 'find ' 'p ' 'l.

Definition find_all : val := ('fun 'p '->
'let_rec_fun 'my_find '=
'fun 'accu '->
'function 
  '| '[] '-> rev ' 'accu
  '| ('x'::'l) '->
'if 'p ' 'x 'then 'my_find ' ('x'::'accu) ' 'l 'else 'my_find ' 'accu ' 'l 'in
find ' '[])%val.

Definition filter : val := (find_all)%val.

Definition partition : val := ('fun 'p '->
'fun 'l '->
'let_rec_fun 'part '=
'fun 'yes '->
'fun 'no '->
'function 
  '| '[] '-> #(rev ' 'yes, rev ' 'no)
  '| ('x'::'l) '->
'if 'p ' 'x 'then 'part ' ('x'::'yes) ' 'no ' 'l
'else 'part ' 'yes ' ('x'::'no) ' 'l 'in
'part ' '[] ' '[] ' 'l)%val.

Definition split : val := 'let_rec_function 'split '= 'function 
  '| '[] '-> #('[], '[])
  '| ((#('x,'y))'::'l) '->
'let (#('rx,'ry)) '= 'split ' 'l 'in #('x'::'rx, 'y'::'ry).

Definition combine : val := 'let_rec_fun 'combine '= 'fun 'l1 '->
'fun 'l2 '->
('match #('l1, 'l2) 'with
 '| (#('[],'[])) '-> '[] '| (#('a1'::'l1,'a2'::'l2)) '-> #('a1, 'a2)'::('combine ' 'l1 ' 'l2) '| (#('_,'_)) '-> 'fail).

Definition merge : val := 'let_rec_fun 'merge '= 'fun 'cmp '->
'fun 'l1 '->
'fun 'l2 '->
('match #('l1, 'l2) 'with
 '| (#('[],'l2)) '-> 'l2 '| (#('l1,'[])) '-> 'l1 '| (#('h1'::'t1,'h2'::'t2)) '->
'if prim_leq ' ('cmp ' 'h1 ' 'h2) ' (_Int 0)
'then 'h1'::('merge ' 'cmp ' 't1 ' 'l2)
'else 'h2'::('merge ' 'cmp ' 'l1 ' 't2)).

Definition chop : val := 'let_rec_fun 'chop '= 'fun 'k '->
'fun 'l '->
'if prim_equ ' 'k ' (_Int 0) 'then 'l
'else ('match 'l 'with
 '| ('x'::'t) '-> 'chop ' (prim_sub ' 'k ' (_Int 1)) ' 't '| '_ '-> 'fail).