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