list0_fold.dats

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

datatype list0 (a:t@ype) =
  | list0_nil (a) of ()
  | list0_cons (a) of (a, list0 a)

#define :: list0_cons

fun{a: t@ype}{b: t@ype}
list0_foldl(xs: list0 a, z: b, f: (a, b)-<cloref1> b): b =
  case+ xs of
  | x::xs => list0_foldl(xs, f(x, z), f)
  | list0_nil0 => z

fun{a: t@ype}{b: t@ype}
list0_foldr(xs: list0 a, z: b, f: (a, b)-<cloref1> b): b =
  case+ xs of
  | x::xs => f(x, list0_foldr(xs, z, f))
  | list0_nil => z

fun{a:t@ype}
list0_reverse(xs: list0 a): list0 a =
  list0_foldl(xs, list0_nil, lam(x, z) => x::z)

fun{a:t@ype}
list0_append(xs: list0 a, ys: list0 a) : list0 a =
  list0_foldr(xs, ys, lam(x, z) => x::z)