Mercurial > urweb

annotate lib/ur/list.ur @ 925:552c989c1601

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Change string URLification to avoid using the empty string, which confuses Apache no2slash()
author Adam Chlipala <adamc@hcoop.net>
date Sat, 12 Sep 2009 09:31:50 -0400
parents b873feb3eb52
children 166ea3944b91
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@916 47 val length = fn [a] =>
adamc@916 48 let
adamc@916 49 fun length' acc (ls : list a) =
adamc@916 50 case ls of
adamc@916 51 [] => acc
adamc@916 52 | _ :: ls => length' (acc + 1) ls
adamc@916 53 in
adamc@916 54 length' 0
adamc@916 55 end
adamc@916 56
adamc@826 57 val rev = fn [a] =>
adamc@826 58 let
adamc@826 59 fun rev' acc (ls : list a) =
adamc@826 60 case ls of
adamc@826 61 [] => acc
adamc@826 62 | x :: ls => rev' (x :: acc) ls
adamc@826 63 in
adamc@826 64 rev' []
adamc@826 65 end
adamc@794 66
adamc@850 67 fun foldlMapAbort [a] [b] [c] f =
adamc@850 68 let
adamc@850 69 fun foldlMapAbort' ls' acc ls =
adamc@850 70 case ls of
adamc@850 71 [] => Some (rev ls', acc)
adamc@850 72 | x :: ls =>
adamc@850 73 case f x acc of
adamc@850 74 None => None
adamc@850 75 | Some (x', acc') => foldlMapAbort' (x' :: ls') acc' ls
adamc@850 76 in
adamc@850 77 foldlMapAbort' []
adamc@850 78 end
adamc@850 79
adamc@826 80 val revAppend = fn [a] =>
adamc@826 81 let
adamc@826 82 fun ra (ls : list a) acc =
adamc@826 83 case ls of
adamc@826 84 [] => acc
adamc@826 85 | x :: ls => ra ls (x :: acc)
adamc@826 86 in
adamc@826 87 ra
adamc@826 88 end
adamc@821 89
adamc@826 90 fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
adamc@821 91
adamc@826 92 fun mp [a] [b] f =
adamc@794 93 let
adamc@794 94 fun mp' acc ls =
adamc@794 95 case ls of
adamc@794 96 [] => rev acc
adamc@794 97 | x :: ls => mp' (f x :: acc) ls
adamc@794 98 in
adamc@794 99 mp' []
adamc@794 100 end
adamc@796 101
adamc@826 102 fun mapPartial [a] [b] f =
adamc@821 103 let
adamc@821 104 fun mp' acc ls =
adamc@821 105 case ls of
adamc@821 106 [] => rev acc
adamc@821 107 | x :: ls => mp' (case f x of
adamc@821 108 None => acc
adamc@821 109 | Some y => y :: acc) ls
adamc@821 110 in
adamc@821 111 mp' []
adamc@821 112 end
adamc@821 113
adamc@826 114 fun mapX [a] [ctx ::: {Unit}] f =
adamc@796 115 let
adamc@796 116 fun mapX' ls =
adamc@796 117 case ls of
adamc@796 118 [] => <xml/>
adamc@796 119 | x :: ls => <xml>{f x}{mapX' ls}</xml>
adamc@796 120 in
adamc@796 121 mapX'
adamc@796 122 end
adamc@800 123
adamc@826 124 fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
adamc@800 125 let
adamc@800 126 fun mapM' acc ls =
adamc@800 127 case ls of
adamc@818 128 [] => return (rev acc)
adamc@818 129 | x :: ls => x' <- f x; mapM' (x' :: acc) ls
adamc@800 130 in
adamc@818 131 mapM' []
adamc@800 132 end
adamc@821 133
adamc@830 134 fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f =
adamc@830 135 let
adamc@830 136 fun mapXM' ls =
adamc@830 137 case ls of
adamc@830 138 [] => return <xml/>
adamc@830 139 | x :: ls =>
adamc@830 140 this <- f x;
adamc@830 141 rest <- mapXM' ls;
adamc@830 142 return <xml>{this}{rest}</xml>
adamc@830 143 in
adamc@830 144 mapXM'
adamc@830 145 end
adamc@830 146
adamc@826 147 fun filter [a] f =
adamc@821 148 let
adamc@821 149 fun fil acc ls =
adamc@821 150 case ls of
adamc@821 151 [] => rev acc
adamc@821 152 | x :: ls => fil (if f x then x :: acc else acc) ls
adamc@821 153 in
adamc@821 154 fil []
adamc@821 155 end
adamc@822 156
adamc@826 157 fun exists [a] f =
adamc@822 158 let
adamc@822 159 fun ex ls =
adamc@822 160 case ls of
adamc@822 161 [] => False
adamc@822 162 | x :: ls =>
adamc@822 163 if f x then
adamc@822 164 True
adamc@822 165 else
adamc@822 166 ex ls
adamc@822 167 in
adamc@822 168 ex
adamc@822 169 end
adamc@822 170
adamc@826 171 fun foldlMap [a] [b] [c] f =
adamc@822 172 let
adamc@822 173 fun fold ls' st ls =
adamc@822 174 case ls of
adamc@822 175 [] => (rev ls', st)
adamc@822 176 | x :: ls =>
adamc@822 177 case f x st of
adamc@822 178 (y, st) => fold (y :: ls') st ls
adamc@822 179 in
adamc@822 180 fold []
adamc@822 181 end
adamc@839 182
adamc@839 183 fun search [a] [b] f =
adamc@839 184 let
adamc@839 185 fun search' ls =
adamc@839 186 case ls of
adamc@839 187 [] => None
adamc@839 188 | x :: ls =>
adamc@839 189 case f x of
adamc@839 190 None => search' ls
adamc@839 191 | v => v
adamc@839 192 in
adamc@839 193 search'
adamc@839 194 end
adamc@839 195
adamc@840 196 fun foldlM [m] (_ : monad m) [a] [b] f =
adamc@840 197 let
adamc@840 198 fun foldlM' acc ls =
adamc@840 199 case ls of
adamc@840 200 [] => return acc
adamc@840 201 | x :: ls =>
adamc@840 202 acc <- f x acc;
adamc@840 203 foldlM' acc ls
adamc@840 204 in
adamc@840 205 foldlM'
adamc@840 206 end
adamc@843 207
adamc@843 208 fun all [m] f =
adamc@843 209 let
adamc@843 210 fun all' ls =
adamc@843 211 case ls of
adamc@843 212 [] => True
adamc@843 213 | x :: ls => f x && all' ls
adamc@843 214 in
adamc@843 215 all'
adamc@843 216 end
adamc@844 217
adamc@844 218 fun app [m] (_ : monad m) [a] f =
adamc@844 219 let
adamc@844 220 fun app' ls =
adamc@844 221 case ls of
adamc@844 222 [] => return ()
adamc@844 223 | x :: ls =>
adamc@844 224 f x;
adamc@844 225 app' ls
adamc@844 226 in
adamc@844 227 app'
adamc@844 228 end
adamc@845 229
adamc@908 230 fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adamc@908 231 [tables ~ exps] (q : sql_query tables exps)
adamc@908 232 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> t) =
adamc@908 233 query q
adamc@908 234 (fn fs acc => return (f fs :: acc))
adamc@908 235 []
adamc@908 236
adamc@845 237 fun assoc [a] [b] (_ : eq a) (x : a) =
adamc@845 238 let
adamc@845 239 fun assoc' (ls : list (a * b)) =
adamc@845 240 case ls of
adamc@845 241 [] => None
adamc@845 242 | (y, z) :: ls =>
adamc@845 243 if x = y then
adamc@845 244 Some z
adamc@845 245 else
adamc@845 246 assoc' ls
adamc@845 247 in
adamc@845 248 assoc'
adamc@845 249 end
adamc@845 250
adamc@845 251 fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
adamc@845 252 case assoc x ls of
adamc@845 253 None => (x, y) :: ls
adamc@845 254 | Some _ => ls