Mercurial > urweb

annotate lib/ur/list.ur @ 853:19fdeef40ada

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Factor out common request functionality, in preparation for supporting different protocols
author Adam Chlipala <adamc@hcoop.net>
date Tue, 23 Jun 2009 14:05:12 -0400
parents 1c2f335297b7
children ed06e25c70ef
rev   line source
adamc@794 1 datatype t = datatype Basis.list
adamc@794 2
adamc@826 3 val show = fn [a] (_ : show a) =>
adamc@826 4 let
adamc@826 5 fun show' (ls : list a) =
adamc@826 6 case ls of
adamc@826 7 [] => "[]"
adamc@826 8 | x :: ls => show x ^ " :: " ^ show' ls
adamc@826 9 in
adamc@826 10 mkShow show'
adamc@826 11 end
adamc@794 12
adamc@846 13 val eq = fn [a] (_ : eq a) =>
adamc@846 14 let
adamc@846 15 fun eq' (ls1 : list a) ls2 =
adamc@846 16 case (ls1, ls2) of
adamc@846 17 ([], []) => True
adamc@846 18 | (x1 :: ls1, x2 :: ls2) => x1 = x2 && eq' ls1 ls2
adamc@846 19 | _ => False
adamc@846 20 in
adamc@846 21 mkEq eq'
adamc@846 22 end
adamc@846 23
adamc@845 24 fun foldl [a] [b] f =
adamc@845 25 let
adamc@845 26 fun foldl' acc ls =
adamc@845 27 case ls of
adamc@845 28 [] => acc
adamc@845 29 | x :: ls => foldl' (f x acc) ls
adamc@845 30 in
adamc@845 31 foldl'
adamc@845 32 end
adamc@845 33
adamc@850 34 fun foldlAbort [a] [b] f =
adamc@846 35 let
adamc@850 36 fun foldlAbort' acc ls =
adamc@846 37 case ls of
adamc@846 38 [] => Some acc
adamc@846 39 | x :: ls =>
adamc@846 40 case f x acc of
adamc@846 41 None => None
adamc@850 42 | Some acc' => foldlAbort' acc' ls
adamc@846 43 in
adamc@850 44 foldlAbort'
adamc@846 45 end
adamc@846 46
adamc@826 47 val rev = fn [a] =>
adamc@826 48 let
adamc@826 49 fun rev' acc (ls : list a) =
adamc@826 50 case ls of
adamc@826 51 [] => acc
adamc@826 52 | x :: ls => rev' (x :: acc) ls
adamc@826 53 in
adamc@826 54 rev' []
adamc@826 55 end
adamc@794 56
adamc@850 57 fun foldlMapAbort [a] [b] [c] f =
adamc@850 58 let
adamc@850 59 fun foldlMapAbort' ls' acc ls =
adamc@850 60 case ls of
adamc@850 61 [] => Some (rev ls', acc)
adamc@850 62 | x :: ls =>
adamc@850 63 case f x acc of
adamc@850 64 None => None
adamc@850 65 | Some (x', acc') => foldlMapAbort' (x' :: ls') acc' ls
adamc@850 66 in
adamc@850 67 foldlMapAbort' []
adamc@850 68 end
adamc@850 69
adamc@826 70 val revAppend = fn [a] =>
adamc@826 71 let
adamc@826 72 fun ra (ls : list a) acc =
adamc@826 73 case ls of
adamc@826 74 [] => acc
adamc@826 75 | x :: ls => ra ls (x :: acc)
adamc@826 76 in
adamc@826 77 ra
adamc@826 78 end
adamc@821 79
adamc@826 80 fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
adamc@821 81
adamc@826 82 fun mp [a] [b] f =
adamc@794 83 let
adamc@794 84 fun mp' acc ls =
adamc@794 85 case ls of
adamc@794 86 [] => rev acc
adamc@794 87 | x :: ls => mp' (f x :: acc) ls
adamc@794 88 in
adamc@794 89 mp' []
adamc@794 90 end
adamc@796 91
adamc@826 92 fun mapPartial [a] [b] f =
adamc@821 93 let
adamc@821 94 fun mp' acc ls =
adamc@821 95 case ls of
adamc@821 96 [] => rev acc
adamc@821 97 | x :: ls => mp' (case f x of
adamc@821 98 None => acc
adamc@821 99 | Some y => y :: acc) ls
adamc@821 100 in
adamc@821 101 mp' []
adamc@821 102 end
adamc@821 103
adamc@826 104 fun mapX [a] [ctx ::: {Unit}] f =
adamc@796 105 let
adamc@796 106 fun mapX' ls =
adamc@796 107 case ls of
adamc@796 108 [] => <xml/>
adamc@796 109 | x :: ls => <xml>{f x}{mapX' ls}</xml>
adamc@796 110 in
adamc@796 111 mapX'
adamc@796 112 end
adamc@800 113
adamc@826 114 fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
adamc@800 115 let
adamc@800 116 fun mapM' acc ls =
adamc@800 117 case ls of
adamc@818 118 [] => return (rev acc)
adamc@818 119 | x :: ls => x' <- f x; mapM' (x' :: acc) ls
adamc@800 120 in
adamc@818 121 mapM' []
adamc@800 122 end
adamc@821 123
adamc@830 124 fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f =
adamc@830 125 let
adamc@830 126 fun mapXM' ls =
adamc@830 127 case ls of
adamc@830 128 [] => return <xml/>
adamc@830 129 | x :: ls =>
adamc@830 130 this <- f x;
adamc@830 131 rest <- mapXM' ls;
adamc@830 132 return <xml>{this}{rest}</xml>
adamc@830 133 in
adamc@830 134 mapXM'
adamc@830 135 end
adamc@830 136
adamc@826 137 fun filter [a] f =
adamc@821 138 let
adamc@821 139 fun fil acc ls =
adamc@821 140 case ls of
adamc@821 141 [] => rev acc
adamc@821 142 | x :: ls => fil (if f x then x :: acc else acc) ls
adamc@821 143 in
adamc@821 144 fil []
adamc@821 145 end
adamc@822 146
adamc@826 147 fun exists [a] f =
adamc@822 148 let
adamc@822 149 fun ex ls =
adamc@822 150 case ls of
adamc@822 151 [] => False
adamc@822 152 | x :: ls =>
adamc@822 153 if f x then
adamc@822 154 True
adamc@822 155 else
adamc@822 156 ex ls
adamc@822 157 in
adamc@822 158 ex
adamc@822 159 end
adamc@822 160
adamc@826 161 fun foldlMap [a] [b] [c] f =
adamc@822 162 let
adamc@822 163 fun fold ls' st ls =
adamc@822 164 case ls of
adamc@822 165 [] => (rev ls', st)
adamc@822 166 | x :: ls =>
adamc@822 167 case f x st of
adamc@822 168 (y, st) => fold (y :: ls') st ls
adamc@822 169 in
adamc@822 170 fold []
adamc@822 171 end
adamc@839 172
adamc@839 173 fun search [a] [b] f =
adamc@839 174 let
adamc@839 175 fun search' ls =
adamc@839 176 case ls of
adamc@839 177 [] => None
adamc@839 178 | x :: ls =>
adamc@839 179 case f x of
adamc@839 180 None => search' ls
adamc@839 181 | v => v
adamc@839 182 in
adamc@839 183 search'
adamc@839 184 end
adamc@839 185
adamc@840 186 fun foldlM [m] (_ : monad m) [a] [b] f =
adamc@840 187 let
adamc@840 188 fun foldlM' acc ls =
adamc@840 189 case ls of
adamc@840 190 [] => return acc
adamc@840 191 | x :: ls =>
adamc@840 192 acc <- f x acc;
adamc@840 193 foldlM' acc ls
adamc@840 194 in
adamc@840 195 foldlM'
adamc@840 196 end
adamc@843 197
adamc@843 198 fun all [m] f =
adamc@843 199 let
adamc@843 200 fun all' ls =
adamc@843 201 case ls of
adamc@843 202 [] => True
adamc@843 203 | x :: ls => f x && all' ls
adamc@843 204 in
adamc@843 205 all'
adamc@843 206 end
adamc@844 207
adamc@844 208 fun app [m] (_ : monad m) [a] f =
adamc@844 209 let
adamc@844 210 fun app' ls =
adamc@844 211 case ls of
adamc@844 212 [] => return ()
adamc@844 213 | x :: ls =>
adamc@844 214 f x;
adamc@844 215 app' ls
adamc@844 216 in
adamc@844 217 app'
adamc@844 218 end
adamc@845 219
adamc@845 220 fun assoc [a] [b] (_ : eq a) (x : a) =
adamc@845 221 let
adamc@845 222 fun assoc' (ls : list (a * b)) =
adamc@845 223 case ls of
adamc@845 224 [] => None
adamc@845 225 | (y, z) :: ls =>
adamc@845 226 if x = y then
adamc@845 227 Some z
adamc@845 228 else
adamc@845 229 assoc' ls
adamc@845 230 in
adamc@845 231 assoc'
adamc@845 232 end
adamc@845 233
adamc@845 234 fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
adamc@845 235 case assoc x ls of
adamc@845 236 None => (x, y) :: ls
adamc@845 237 | Some _ => ls