Mercurial > urweb

annotate lib/ur/list.ur @ 1280:3d06e0f7a6f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial version of equalKnown working for secret
author Adam Chlipala <adam@chlipala.net>
date Tue, 27 Jul 2010 11:42:30 -0400
parents 4c367c8f5b2d
children 4172863d049d
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@1279 104 fun mapi [a] [b] f =
adamc@1279 105 let
adamc@1279 106 fun mp' n acc ls =
adamc@1279 107 case ls of
adamc@1279 108 [] => rev acc
adamc@1279 109 | x :: ls => mp' (n + 1) (f n x :: acc) ls
adamc@1279 110 in
adamc@1279 111 mp' 0 []
adamc@1279 112 end
adamc@1279 113
adamc@826 114 fun mapPartial [a] [b] f =
adamc@821 115 let
adamc@821 116 fun mp' acc ls =
adamc@821 117 case ls of
adamc@821 118 [] => rev acc
adamc@821 119 | x :: ls => mp' (case f x of
adamc@821 120 None => acc
adamc@821 121 | Some y => y :: acc) ls
adamc@821 122 in
adamc@821 123 mp' []
adamc@821 124 end
adamc@821 125
adamc@826 126 fun mapX [a] [ctx ::: {Unit}] f =
adamc@796 127 let
adamc@796 128 fun mapX' ls =
adamc@796 129 case ls of
adamc@796 130 [] => <xml/>
adamc@796 131 | x :: ls => <xml>{f x}{mapX' ls}</xml>
adamc@796 132 in
adamc@796 133 mapX'
adamc@796 134 end
adamc@800 135
adamc@826 136 fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
adamc@800 137 let
adamc@800 138 fun mapM' acc ls =
adamc@800 139 case ls of
adamc@818 140 [] => return (rev acc)
adamc@818 141 | x :: ls => x' <- f x; mapM' (x' :: acc) ls
adamc@800 142 in
adamc@818 143 mapM' []
adamc@800 144 end
adamc@821 145
adamc@1107 146 fun mapPartialM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
adamc@1107 147 let
adamc@1107 148 fun mapPartialM' acc ls =
adamc@1107 149 case ls of
adamc@1107 150 [] => return (rev acc)
adamc@1107 151 | x :: ls =>
adamc@1107 152 v <- f x;
adamc@1107 153 mapPartialM' (case v of
adamc@1107 154 None => acc
adamc@1107 155 | Some x' => x' :: acc) ls
adamc@1107 156 in
adamc@1107 157 mapPartialM' []
adamc@1107 158 end
adamc@1107 159
adamc@830 160 fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f =
adamc@830 161 let
adamc@830 162 fun mapXM' ls =
adamc@830 163 case ls of
adamc@830 164 [] => return <xml/>
adamc@830 165 | x :: ls =>
adamc@830 166 this <- f x;
adamc@830 167 rest <- mapXM' ls;
adamc@830 168 return <xml>{this}{rest}</xml>
adamc@830 169 in
adamc@830 170 mapXM'
adamc@830 171 end
adamc@830 172
adamc@826 173 fun filter [a] f =
adamc@821 174 let
adamc@821 175 fun fil acc ls =
adamc@821 176 case ls of
adamc@821 177 [] => rev acc
adamc@821 178 | x :: ls => fil (if f x then x :: acc else acc) ls
adamc@821 179 in
adamc@821 180 fil []
adamc@821 181 end
adamc@822 182
adamc@826 183 fun exists [a] f =
adamc@822 184 let
adamc@822 185 fun ex ls =
adamc@822 186 case ls of
adamc@822 187 [] => False
adamc@822 188 | x :: ls =>
adamc@822 189 if f x then
adamc@822 190 True
adamc@822 191 else
adamc@822 192 ex ls
adamc@822 193 in
adamc@822 194 ex
adamc@822 195 end
adamc@822 196
adamc@826 197 fun foldlMap [a] [b] [c] f =
adamc@822 198 let
adamc@822 199 fun fold ls' st ls =
adamc@822 200 case ls of
adamc@822 201 [] => (rev ls', st)
adamc@822 202 | x :: ls =>
adamc@822 203 case f x st of
adamc@822 204 (y, st) => fold (y :: ls') st ls
adamc@822 205 in
adamc@822 206 fold []
adamc@822 207 end
adamc@839 208
adamc@839 209 fun search [a] [b] f =
adamc@839 210 let
adamc@839 211 fun search' ls =
adamc@839 212 case ls of
adamc@839 213 [] => None
adamc@839 214 | x :: ls =>
adamc@839 215 case f x of
adamc@839 216 None => search' ls
adamc@839 217 | v => v
adamc@839 218 in
adamc@839 219 search'
adamc@839 220 end
adamc@839 221
adamc@840 222 fun foldlM [m] (_ : monad m) [a] [b] f =
adamc@840 223 let
adamc@840 224 fun foldlM' acc ls =
adamc@840 225 case ls of
adamc@840 226 [] => return acc
adamc@840 227 | x :: ls =>
adamc@840 228 acc <- f x acc;
adamc@840 229 foldlM' acc ls
adamc@840 230 in
adamc@840 231 foldlM'
adamc@840 232 end
adamc@843 233
adamc@843 234 fun all [m] f =
adamc@843 235 let
adamc@843 236 fun all' ls =
adamc@843 237 case ls of
adamc@843 238 [] => True
adamc@843 239 | x :: ls => f x && all' ls
adamc@843 240 in
adamc@843 241 all'
adamc@843 242 end
adamc@844 243
adamc@844 244 fun app [m] (_ : monad m) [a] f =
adamc@844 245 let
adamc@844 246 fun app' ls =
adamc@844 247 case ls of
adamc@844 248 [] => return ()
adamc@844 249 | x :: ls =>
adamc@844 250 f x;
adamc@844 251 app' ls
adamc@844 252 in
adamc@844 253 app'
adamc@844 254 end
adamc@845 255
adamc@908 256 fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adamc@1191 257 [tables ~ exps] (q : sql_query [] tables exps)
adamc@908 258 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> t) =
adamc@995 259 ls <- query q
adamc@995 260 (fn fs acc => return (f fs :: acc))
adamc@995 261 [];
adamc@995 262 return (rev ls)
adamc@908 263
adamc@1107 264 fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adamc@1191 265 [tables ~ exps] (q : sql_query [] tables exps)
adamc@1107 266 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t) =
adamc@1107 267 ls <- query q
adamc@1107 268 (fn fs acc => v <- f fs; return (v :: acc))
adamc@1107 269 [];
adamc@1107 270 return (rev ls)
adamc@1107 271
adamc@1107 272 fun mapQueryPartialM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adamc@1191 273 [tables ~ exps] (q : sql_query [] tables exps)
adamc@1107 274 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t)) =
adamc@1107 275 ls <- query q
adamc@1107 276 (fn fs acc => v <- f fs;
adamc@1107 277 return (case v of
adamc@1107 278 None => acc
adamc@1107 279 | Some v => v :: acc))
adamc@1107 280 [];
adamc@1107 281 return (rev ls)
adamc@1107 282
adamc@845 283 fun assoc [a] [b] (_ : eq a) (x : a) =
adamc@845 284 let
adamc@845 285 fun assoc' (ls : list (a * b)) =
adamc@845 286 case ls of
adamc@845 287 [] => None
adamc@845 288 | (y, z) :: ls =>
adamc@845 289 if x = y then
adamc@845 290 Some z
adamc@845 291 else
adamc@845 292 assoc' ls
adamc@845 293 in
adamc@845 294 assoc'
adamc@845 295 end
adamc@845 296
adamc@845 297 fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
adamc@845 298 case assoc x ls of
adamc@845 299 None => (x, y) :: ls
adamc@845 300 | Some _ => ls