Mercurial > urweb

annotate lib/ur/list.ur @ 868:06497beb265b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Moved dml code into Settings
author Adam Chlipala <adamc@hcoop.net>
date Sun, 28 Jun 2009 16:22:17 -0400
parents 1c2f335297b7
children ed06e25c70ef
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@826 47 val rev = fn [a] =>
adamc@826 48 let
adamc@826 49 fun rev' acc (ls : list a) =
adamc@826 50 case ls of
adamc@826 51 [] => acc
adamc@826 52 | x :: ls => rev' (x :: acc) ls
adamc@826 53 in
adamc@826 54 rev' []
adamc@826 55 end
adamc@794 56
adamc@850 57 fun foldlMapAbort [a] [b] [c] f =
adamc@850 58 let
adamc@850 59 fun foldlMapAbort' ls' acc ls =
adamc@850 60 case ls of
adamc@850 61 [] => Some (rev ls', acc)
adamc@850 62 | x :: ls =>
adamc@850 63 case f x acc of
adamc@850 64 None => None
adamc@850 65 | Some (x', acc') => foldlMapAbort' (x' :: ls') acc' ls
adamc@850 66 in
adamc@850 67 foldlMapAbort' []
adamc@850 68 end
adamc@850 69
adamc@826 70 val revAppend = fn [a] =>
adamc@826 71 let
adamc@826 72 fun ra (ls : list a) acc =
adamc@826 73 case ls of
adamc@826 74 [] => acc
adamc@826 75 | x :: ls => ra ls (x :: acc)
adamc@826 76 in
adamc@826 77 ra
adamc@826 78 end
adamc@821 79
adamc@826 80 fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
adamc@821 81
adamc@826 82 fun mp [a] [b] f =
adamc@794 83 let
adamc@794 84 fun mp' acc ls =
adamc@794 85 case ls of
adamc@794 86 [] => rev acc
adamc@794 87 | x :: ls => mp' (f x :: acc) ls
adamc@794 88 in
adamc@794 89 mp' []
adamc@794 90 end
adamc@796 91
adamc@826 92 fun mapPartial [a] [b] f =
adamc@821 93 let
adamc@821 94 fun mp' acc ls =
adamc@821 95 case ls of
adamc@821 96 [] => rev acc
adamc@821 97 | x :: ls => mp' (case f x of
adamc@821 98 None => acc
adamc@821 99 | Some y => y :: acc) ls
adamc@821 100 in
adamc@821 101 mp' []
adamc@821 102 end
adamc@821 103
adamc@826 104 fun mapX [a] [ctx ::: {Unit}] f =
adamc@796 105 let
adamc@796 106 fun mapX' ls =
adamc@796 107 case ls of
adamc@796 108 [] => <xml/>
adamc@796 109 | x :: ls => <xml>{f x}{mapX' ls}</xml>
adamc@796 110 in
adamc@796 111 mapX'
adamc@796 112 end
adamc@800 113
adamc@826 114 fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
adamc@800 115 let
adamc@800 116 fun mapM' acc ls =
adamc@800 117 case ls of
adamc@818 118 [] => return (rev acc)
adamc@818 119 | x :: ls => x' <- f x; mapM' (x' :: acc) ls
adamc@800 120 in
adamc@818 121 mapM' []
adamc@800 122 end
adamc@821 123
adamc@830 124 fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f =
adamc@830 125 let
adamc@830 126 fun mapXM' ls =
adamc@830 127 case ls of
adamc@830 128 [] => return <xml/>
adamc@830 129 | x :: ls =>
adamc@830 130 this <- f x;
adamc@830 131 rest <- mapXM' ls;
adamc@830 132 return <xml>{this}{rest}</xml>
adamc@830 133 in
adamc@830 134 mapXM'
adamc@830 135 end
adamc@830 136
adamc@826 137 fun filter [a] f =
adamc@821 138 let
adamc@821 139 fun fil acc ls =
adamc@821 140 case ls of
adamc@821 141 [] => rev acc
adamc@821 142 | x :: ls => fil (if f x then x :: acc else acc) ls
adamc@821 143 in
adamc@821 144 fil []
adamc@821 145 end
adamc@822 146
adamc@826 147 fun exists [a] f =
adamc@822 148 let
adamc@822 149 fun ex ls =
adamc@822 150 case ls of
adamc@822 151 [] => False
adamc@822 152 | x :: ls =>
adamc@822 153 if f x then
adamc@822 154 True
adamc@822 155 else
adamc@822 156 ex ls
adamc@822 157 in
adamc@822 158 ex
adamc@822 159 end
adamc@822 160
adamc@826 161 fun foldlMap [a] [b] [c] f =
adamc@822 162 let
adamc@822 163 fun fold ls' st ls =
adamc@822 164 case ls of
adamc@822 165 [] => (rev ls', st)
adamc@822 166 | x :: ls =>
adamc@822 167 case f x st of
adamc@822 168 (y, st) => fold (y :: ls') st ls
adamc@822 169 in
adamc@822 170 fold []
adamc@822 171 end
adamc@839 172
adamc@839 173 fun search [a] [b] f =
adamc@839 174 let
adamc@839 175 fun search' ls =
adamc@839 176 case ls of
adamc@839 177 [] => None
adamc@839 178 | x :: ls =>
adamc@839 179 case f x of
adamc@839 180 None => search' ls
adamc@839 181 | v => v
adamc@839 182 in
adamc@839 183 search'
adamc@839 184 end
adamc@839 185
adamc@840 186 fun foldlM [m] (_ : monad m) [a] [b] f =
adamc@840 187 let
adamc@840 188 fun foldlM' acc ls =
adamc@840 189 case ls of
adamc@840 190 [] => return acc
adamc@840 191 | x :: ls =>
adamc@840 192 acc <- f x acc;
adamc@840 193 foldlM' acc ls
adamc@840 194 in
adamc@840 195 foldlM'
adamc@840 196 end
adamc@843 197
adamc@843 198 fun all [m] f =
adamc@843 199 let
adamc@843 200 fun all' ls =
adamc@843 201 case ls of
adamc@843 202 [] => True
adamc@843 203 | x :: ls => f x && all' ls
adamc@843 204 in
adamc@843 205 all'
adamc@843 206 end
adamc@844 207
adamc@844 208 fun app [m] (_ : monad m) [a] f =
adamc@844 209 let
adamc@844 210 fun app' ls =
adamc@844 211 case ls of
adamc@844 212 [] => return ()
adamc@844 213 | x :: ls =>
adamc@844 214 f x;
adamc@844 215 app' ls
adamc@844 216 in
adamc@844 217 app'
adamc@844 218 end
adamc@845 219
adamc@845 220 fun assoc [a] [b] (_ : eq a) (x : a) =
adamc@845 221 let
adamc@845 222 fun assoc' (ls : list (a * b)) =
adamc@845 223 case ls of
adamc@845 224 [] => None
adamc@845 225 | (y, z) :: ls =>
adamc@845 226 if x = y then
adamc@845 227 Some z
adamc@845 228 else
adamc@845 229 assoc' ls
adamc@845 230 in
adamc@845 231 assoc'
adamc@845 232 end
adamc@845 233
adamc@845 234 fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
adamc@845 235 case assoc x ls of
adamc@845 236 None => (x, y) :: ls
adamc@845 237 | Some _ => ls