Mercurial > urweb

annotate lib/ur/list.ur @ 1092:6f4b05fc4361

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