Charity

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