rf "Lnat.ch". rf "Llist.ch". def min_max: Lnat * Lnat -> Lnat * Lnat = (m, n) => fn ( n , {| Lzero: () => (fn: _ => (m, n)) | Lsucc: f => (fn: Lzero => (n, m) | Lsucc n' => fn (lid n', lid f) ) |} m ). def max_min = pn => {(m, n) => (n, m)} min_max pn. def new_min = pn => p0 min_max pn. def new_max = pn => p1 min_max pn. def new_zip: Llist(A) * Llist(B) -> Llist(A * B) = (l1, l2) => fn (l2 , {| Lnil : () => (fn: _ => Lnil) | Lcons: p => (fn: Lnil => Lnil | Lcons (b, (lid: l2')) => { (a, f) => Lcons ( (a, b) , (lid: fn (l2', f)) ) } (p0 p, lid p1 p) ) |} l1 ). def take_drop: Lnat * list(A) -> list(A) * list(A) = (n, l) => fn (l , {| Lzero: () => (fn: l' => ([], l')) | Lsucc: f => (fn: nil => ([], []) | cons (a, l') => { (t, d) => (cons (a, t), d) } fn (l', lid f) ) |} n ). def new_take = p => p0 take_drop p. def new_drop = p => p1 take_drop p. def new_eq: Lnat * Lnat -> bool = (m, n) => fn (n, {| Lzero: () => (fn: Lzero => true | Lsucc _ => false ) | Lsucc: f => (fn: Lzero => false | Lsucc (lid: n') => fn (n', lid f) ) |} m ). def new_neq = pn => not new_eq pn. def bwhile{ initial: A -> C , iterate: C -> C , final : C -> B , cond : C -> bool }: A * Lnat -> SF(B) = (a, n) => SF{final} fn (initial a , {| Lzero: () => (fn: _ => ff) | Lsucc: f => (fn: c => { true => fn ( iterate c , lid f ) | false => ss c } cond c ) |} n ). def diff: Lnat * Lnat -> Lnat * Lnat = (m, n) => max_min (n, Lsub (m, n)). def gcd: Lnat * Lnat -> SF(Lnat) = pn => bwhile{max_min, diff, p0, new_neq} (pn, new_max pn). (***** EXERCISES --------- 1. Write new_takewhile{pred: A -> bool}: Llist(A) -> Llist(A) new_dropwhile{pred: A -> bool}: Llist(A) -> Llist(A) (hint: write take_drop_while for lazy lists, much as take_drop is written). 2. Write eq_Llist{eq_A: A * A -> bool}: Llist(A) * Llist(A) -> bool 3. Write the list indexing functions get: Lnat * list(A) -> list(A) set: Lnat * list(A) * A -> list(A) *****)