Mercurial > urweb

annotate lib/ur/list.ur @ 1058:86b831978b8d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Recursive hnormSgn for projections of signatures from modules
author Adam Chlipala <adamc@hcoop.net>
date Sat, 05 Dec 2009 14:34:44 -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