Mercurial > urweb

annotate lib/ur/list.ur @ 1249:7c6fc92f6c31

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Complain about DValRec; optimizations for unit-valued ECase and forgetting of path conditions across ESeq
author Adam Chlipala <adamc@hcoop.net>
date Thu, 29 Apr 2010 11:47:24 -0400
parents 61c3139eab12
children 4c367c8f5b2d
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@1107 136 fun mapPartialM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
adamc@1107 137 let
adamc@1107 138 fun mapPartialM' acc ls =
adamc@1107 139 case ls of
adamc@1107 140 [] => return (rev acc)
adamc@1107 141 | x :: ls =>
adamc@1107 142 v <- f x;
adamc@1107 143 mapPartialM' (case v of
adamc@1107 144 None => acc
adamc@1107 145 | Some x' => x' :: acc) ls
adamc@1107 146 in
adamc@1107 147 mapPartialM' []
adamc@1107 148 end
adamc@1107 149
adamc@830 150 fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f =
adamc@830 151 let
adamc@830 152 fun mapXM' ls =
adamc@830 153 case ls of
adamc@830 154 [] => return <xml/>
adamc@830 155 | x :: ls =>
adamc@830 156 this <- f x;
adamc@830 157 rest <- mapXM' ls;
adamc@830 158 return <xml>{this}{rest}</xml>
adamc@830 159 in
adamc@830 160 mapXM'
adamc@830 161 end
adamc@830 162
adamc@826 163 fun filter [a] f =
adamc@821 164 let
adamc@821 165 fun fil acc ls =
adamc@821 166 case ls of
adamc@821 167 [] => rev acc
adamc@821 168 | x :: ls => fil (if f x then x :: acc else acc) ls
adamc@821 169 in
adamc@821 170 fil []
adamc@821 171 end
adamc@822 172
adamc@826 173 fun exists [a] f =
adamc@822 174 let
adamc@822 175 fun ex ls =
adamc@822 176 case ls of
adamc@822 177 [] => False
adamc@822 178 | x :: ls =>
adamc@822 179 if f x then
adamc@822 180 True
adamc@822 181 else
adamc@822 182 ex ls
adamc@822 183 in
adamc@822 184 ex
adamc@822 185 end
adamc@822 186
adamc@826 187 fun foldlMap [a] [b] [c] f =
adamc@822 188 let
adamc@822 189 fun fold ls' st ls =
adamc@822 190 case ls of
adamc@822 191 [] => (rev ls', st)
adamc@822 192 | x :: ls =>
adamc@822 193 case f x st of
adamc@822 194 (y, st) => fold (y :: ls') st ls
adamc@822 195 in
adamc@822 196 fold []
adamc@822 197 end
adamc@839 198
adamc@839 199 fun search [a] [b] f =
adamc@839 200 let
adamc@839 201 fun search' ls =
adamc@839 202 case ls of
adamc@839 203 [] => None
adamc@839 204 | x :: ls =>
adamc@839 205 case f x of
adamc@839 206 None => search' ls
adamc@839 207 | v => v
adamc@839 208 in
adamc@839 209 search'
adamc@839 210 end
adamc@839 211
adamc@840 212 fun foldlM [m] (_ : monad m) [a] [b] f =
adamc@840 213 let
adamc@840 214 fun foldlM' acc ls =
adamc@840 215 case ls of
adamc@840 216 [] => return acc
adamc@840 217 | x :: ls =>
adamc@840 218 acc <- f x acc;
adamc@840 219 foldlM' acc ls
adamc@840 220 in
adamc@840 221 foldlM'
adamc@840 222 end
adamc@843 223
adamc@843 224 fun all [m] f =
adamc@843 225 let
adamc@843 226 fun all' ls =
adamc@843 227 case ls of
adamc@843 228 [] => True
adamc@843 229 | x :: ls => f x && all' ls
adamc@843 230 in
adamc@843 231 all'
adamc@843 232 end
adamc@844 233
adamc@844 234 fun app [m] (_ : monad m) [a] f =
adamc@844 235 let
adamc@844 236 fun app' ls =
adamc@844 237 case ls of
adamc@844 238 [] => return ()
adamc@844 239 | x :: ls =>
adamc@844 240 f x;
adamc@844 241 app' ls
adamc@844 242 in
adamc@844 243 app'
adamc@844 244 end
adamc@845 245
adamc@908 246 fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adamc@1191 247 [tables ~ exps] (q : sql_query [] tables exps)
adamc@908 248 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> t) =
adamc@995 249 ls <- query q
adamc@995 250 (fn fs acc => return (f fs :: acc))
adamc@995 251 [];
adamc@995 252 return (rev ls)
adamc@908 253
adamc@1107 254 fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adamc@1191 255 [tables ~ exps] (q : sql_query [] tables exps)
adamc@1107 256 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t) =
adamc@1107 257 ls <- query q
adamc@1107 258 (fn fs acc => v <- f fs; return (v :: acc))
adamc@1107 259 [];
adamc@1107 260 return (rev ls)
adamc@1107 261
adamc@1107 262 fun mapQueryPartialM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adamc@1191 263 [tables ~ exps] (q : sql_query [] tables exps)
adamc@1107 264 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t)) =
adamc@1107 265 ls <- query q
adamc@1107 266 (fn fs acc => v <- f fs;
adamc@1107 267 return (case v of
adamc@1107 268 None => acc
adamc@1107 269 | Some v => v :: acc))
adamc@1107 270 [];
adamc@1107 271 return (rev ls)
adamc@1107 272
adamc@845 273 fun assoc [a] [b] (_ : eq a) (x : a) =
adamc@845 274 let
adamc@845 275 fun assoc' (ls : list (a * b)) =
adamc@845 276 case ls of
adamc@845 277 [] => None
adamc@845 278 | (y, z) :: ls =>
adamc@845 279 if x = y then
adamc@845 280 Some z
adamc@845 281 else
adamc@845 282 assoc' ls
adamc@845 283 in
adamc@845 284 assoc'
adamc@845 285 end
adamc@845 286
adamc@845 287 fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
adamc@845 288 case assoc x ls of
adamc@845 289 None => (x, y) :: ls
adamc@845 290 | Some _ => ls