Ur/Web: lib/ur/list.ur annotate

Change List.mapM' to avoid leaving functions around

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 21 May 2009 11:45:04 -0400
parents	e92cfac1608f
children	395a5d450cc0

rev	line source
adamc@794	1 datatype t = datatype Basis.list
adamc@794	2
adamc@794	3 val show (a ::: Type) (_ : show a) =
adamc@794	4 let
adamc@794	5 fun show' (ls : list a) =
adamc@794	6 case ls of
adamc@794	7 [] => "[]"
adamc@794	8 \| x :: ls => show x ^ " :: " ^ show' ls
adamc@794	9 in
adamc@794	10 mkShow show'
adamc@794	11 end
adamc@794	12
adamc@794	13 val rev (a ::: Type) =
adamc@794	14 let
adamc@794	15 fun rev' acc (ls : list a) =
adamc@794	16 case ls of
adamc@794	17 [] => acc
adamc@794	18 \| x :: ls => rev' (x :: acc) ls
adamc@794	19 in
adamc@794	20 rev' []
adamc@794	21 end
adamc@794	22
adamc@794	23 fun mp (a ::: Type) (b ::: Type) f =
adamc@794	24 let
adamc@794	25 fun mp' acc ls =
adamc@794	26 case ls of
adamc@794	27 [] => rev acc
adamc@794	28 \| x :: ls => mp' (f x :: acc) ls
adamc@794	29 in
adamc@794	30 mp' []
adamc@794	31 end
adamc@796	32
adamc@796	33 fun mapX (a ::: Type) (ctx ::: {Unit}) f =
adamc@796	34 let
adamc@796	35 fun mapX' ls =
adamc@796	36 case ls of
adamc@796	37 [] => <xml/>
adamc@796	38 \| x :: ls => <xml>{f x}{mapX' ls}</xml>
adamc@796	39 in
adamc@796	40 mapX'
adamc@796	41 end
adamc@800	42
adamc@800	43 fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f =
adamc@800	44 let
adamc@800	45 fun mapM' acc ls =
adamc@800	46 case ls of
adamc@818	47 [] => return (rev acc)
adamc@818	48 \| x :: ls => x' <- f x; mapM' (x' :: acc) ls
adamc@800	49 in
adamc@818	50 mapM' []
adamc@800	51 end

Mercurial > urweb