Mercurial > urweb

annotate lib/ur/list.ur @ 846:0d30e6338c65

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