annotate lib/ur/list.ur @ 811:50b4825115f0

Fix initialization of cselect from source
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 16:59:24 -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