adamc@794: datatype t = datatype Basis.list adamc@794: adamc@826: val show = fn [a] (_ : show a) => adamc@826: let adamc@826: fun show' (ls : list a) = adamc@826: case ls of adamc@826: [] => "[]" adamc@826: | x :: ls => show x ^ " :: " ^ show' ls adamc@826: in adamc@826: mkShow show' adamc@826: end adamc@794: adamc@826: val rev = fn [a] => adamc@826: let adamc@826: fun rev' acc (ls : list a) = adamc@826: case ls of adamc@826: [] => acc adamc@826: | x :: ls => rev' (x :: acc) ls adamc@826: in adamc@826: rev' [] adamc@826: end adamc@794: adamc@826: val revAppend = fn [a] => adamc@826: let adamc@826: fun ra (ls : list a) acc = adamc@826: case ls of adamc@826: [] => acc adamc@826: | x :: ls => ra ls (x :: acc) adamc@826: in adamc@826: ra adamc@826: end adamc@821: adamc@826: fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2 adamc@821: adamc@826: fun mp [a] [b] f = adamc@794: let adamc@794: fun mp' acc ls = adamc@794: case ls of adamc@794: [] => rev acc adamc@794: | x :: ls => mp' (f x :: acc) ls adamc@794: in adamc@794: mp' [] adamc@794: end adamc@796: adamc@826: fun mapPartial [a] [b] f = adamc@821: let adamc@821: fun mp' acc ls = adamc@821: case ls of adamc@821: [] => rev acc adamc@821: | x :: ls => mp' (case f x of adamc@821: None => acc adamc@821: | Some y => y :: acc) ls adamc@821: in adamc@821: mp' [] adamc@821: end adamc@821: adamc@826: fun mapX [a] [ctx ::: {Unit}] f = adamc@796: let adamc@796: fun mapX' ls = adamc@796: case ls of adamc@796: [] => adamc@796: | x :: ls => {f x}{mapX' ls} adamc@796: in adamc@796: mapX' adamc@796: end adamc@800: adamc@826: fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f = adamc@800: let adamc@800: fun mapM' acc ls = adamc@800: case ls of adamc@818: [] => return (rev acc) adamc@818: | x :: ls => x' <- f x; mapM' (x' :: acc) ls adamc@800: in adamc@818: mapM' [] adamc@800: end adamc@821: adamc@830: fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f = adamc@830: let adamc@830: fun mapXM' ls = adamc@830: case ls of adamc@830: [] => return adamc@830: | x :: ls => adamc@830: this <- f x; adamc@830: rest <- mapXM' ls; adamc@830: return {this}{rest} adamc@830: in adamc@830: mapXM' adamc@830: end adamc@830: adamc@826: fun filter [a] f = adamc@821: let adamc@821: fun fil acc ls = adamc@821: case ls of adamc@821: [] => rev acc adamc@821: | x :: ls => fil (if f x then x :: acc else acc) ls adamc@821: in adamc@821: fil [] adamc@821: end adamc@822: adamc@826: fun exists [a] f = adamc@822: let adamc@822: fun ex ls = adamc@822: case ls of adamc@822: [] => False adamc@822: | x :: ls => adamc@822: if f x then adamc@822: True adamc@822: else adamc@822: ex ls adamc@822: in adamc@822: ex adamc@822: end adamc@822: adamc@826: fun foldlMap [a] [b] [c] f = adamc@822: let adamc@822: fun fold ls' st ls = adamc@822: case ls of adamc@822: [] => (rev ls', st) adamc@822: | x :: ls => adamc@822: case f x st of adamc@822: (y, st) => fold (y :: ls') st ls adamc@822: in adamc@822: fold [] adamc@822: end adamc@839: adamc@839: fun assoc [a] [b] (_ : eq a) (x : a) = adamc@839: let adamc@839: fun assoc' ls = adamc@839: case ls of adamc@839: [] => None adamc@839: | (y, z) :: ls => adamc@839: if x = y then adamc@839: Some z adamc@839: else adamc@839: assoc' ls adamc@839: in adamc@839: assoc' adamc@839: end adamc@839: adamc@839: fun search [a] [b] f = adamc@839: let adamc@839: fun search' ls = adamc@839: case ls of adamc@839: [] => None adamc@839: | x :: ls => adamc@839: case f x of adamc@839: None => search' ls adamc@839: | v => v adamc@839: in adamc@839: search' adamc@839: end adamc@839: adamc@840: fun foldlM [m] (_ : monad m) [a] [b] f = adamc@840: let adamc@840: fun foldlM' acc ls = adamc@840: case ls of adamc@840: [] => return acc adamc@840: | x :: ls => adamc@840: acc <- f x acc; adamc@840: foldlM' acc ls adamc@840: in adamc@840: foldlM' adamc@840: end adamc@843: adamc@843: fun all [m] f = adamc@843: let adamc@843: fun all' ls = adamc@843: case ls of adamc@843: [] => True adamc@843: | x :: ls => f x && all' ls adamc@843: in adamc@843: all' adamc@843: end