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

Mutual datatypes through Pathcheck

author	Adam Chlipala <adamc@hcoop.net>
date	Sat, 16 May 2009 15:55:15 -0400
parents	e92cfac1608f
children	066493f7f008

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@800	47 [] => acc
adamc@800	48 \| x :: ls => mapM' (x' <- f x; ls' <- acc; return (x' :: ls')) ls
adamc@800	49 in
adamc@800	50 mapM' (return [])
adamc@800	51 end

Mercurial > urweb