annotate lib/ur/list.ur @ 821:395a5d450cc0

Chars and more string operations
author Adam Chlipala <adamc@hcoop.net>
date Tue, 26 May 2009 12:25:06 -0400
parents 066493f7f008
children d4e811beb8eb
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@821 23 val revAppend (a ::: Type) =
adamc@821 24 let
adamc@821 25 fun ra (ls : list a) acc =
adamc@821 26 case ls of
adamc@821 27 [] => acc
adamc@821 28 | x :: ls => ra ls (x :: acc)
adamc@821 29 in
adamc@821 30 ra
adamc@821 31 end
adamc@821 32
adamc@821 33 fun append (a ::: Type) (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
adamc@821 34
adamc@794 35 fun mp (a ::: Type) (b ::: Type) f =
adamc@794 36 let
adamc@794 37 fun mp' acc ls =
adamc@794 38 case ls of
adamc@794 39 [] => rev acc
adamc@794 40 | x :: ls => mp' (f x :: acc) ls
adamc@794 41 in
adamc@794 42 mp' []
adamc@794 43 end
adamc@796 44
adamc@821 45 fun mapPartial (a ::: Type) (b ::: Type) f =
adamc@821 46 let
adamc@821 47 fun mp' acc ls =
adamc@821 48 case ls of
adamc@821 49 [] => rev acc
adamc@821 50 | x :: ls => mp' (case f x of
adamc@821 51 None => acc
adamc@821 52 | Some y => y :: acc) ls
adamc@821 53 in
adamc@821 54 mp' []
adamc@821 55 end
adamc@821 56
adamc@796 57 fun mapX (a ::: Type) (ctx ::: {Unit}) f =
adamc@796 58 let
adamc@796 59 fun mapX' ls =
adamc@796 60 case ls of
adamc@796 61 [] => <xml/>
adamc@796 62 | x :: ls => <xml>{f x}{mapX' ls}</xml>
adamc@796 63 in
adamc@796 64 mapX'
adamc@796 65 end
adamc@800 66
adamc@800 67 fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f =
adamc@800 68 let
adamc@800 69 fun mapM' acc ls =
adamc@800 70 case ls of
adamc@818 71 [] => return (rev acc)
adamc@818 72 | x :: ls => x' <- f x; mapM' (x' :: acc) ls
adamc@800 73 in
adamc@818 74 mapM' []
adamc@800 75 end
adamc@821 76
adamc@821 77 fun filter (a ::: Type) f =
adamc@821 78 let
adamc@821 79 fun fil acc ls =
adamc@821 80 case ls of
adamc@821 81 [] => rev acc
adamc@821 82 | x :: ls => fil (if f x then x :: acc else acc) ls
adamc@821 83 in
adamc@821 84 fil []
adamc@821 85 end