Mercurial > urweb

annotate lib/ur/list.ur @ 987:6dd122f10c0c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Better location calculation for record unification error messages; infer kind arguments to module-projected variables
author Adam Chlipala <adamc@hcoop.net>
date Mon, 05 Oct 2009 16:36:38 -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