adamc@794: datatype t = datatype Basis.list
adamc@794:
adamc@794: val show (a ::: Type) (_ : show a) =
adamc@794: let
adamc@794: fun show' (ls : list a) =
adamc@794: case ls of
adamc@794: [] => "[]"
adamc@794: | x :: ls => show x ^ " :: " ^ show' ls
adamc@794: in
adamc@794: mkShow show'
adamc@794: end
adamc@794:
adamc@794: val rev (a ::: Type) =
adamc@794: let
adamc@794: fun rev' acc (ls : list a) =
adamc@794: case ls of
adamc@794: [] => acc
adamc@794: | x :: ls => rev' (x :: acc) ls
adamc@794: in
adamc@794: rev' []
adamc@794: end
adamc@794:
adamc@794: fun mp (a ::: Type) (b ::: Type) 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@796: fun mapX (a ::: Type) (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@800: fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f =
adamc@800: let
adamc@800: fun mapM' acc ls =
adamc@800: case ls of
adamc@800: [] => acc
adamc@800: | x :: ls => mapM' (x' <- f x; ls' <- acc; return (x' :: ls')) ls
adamc@800: in
adamc@800: mapM' (return [])
adamc@800: end