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