Mercurial > urweb

annotate lib/ur/list.ur @ 845:6725d73c3c31

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mark current as effectful; add List functions
author Adam Chlipala <adamc@hcoop.net>
date Tue, 09 Jun 2009 11:12:34 -0400
parents 74a1e3bdf430
children 0d30e6338c65
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@845 13 fun foldl [a] [b] f =
adamc@845 14 let
adamc@845 15 fun foldl' acc ls =
adamc@845 16 case ls of
adamc@845 17 [] => acc
adamc@845 18 | x :: ls => foldl' (f x acc) ls
adamc@845 19 in
adamc@845 20 foldl'
adamc@845 21 end
adamc@845 22
adamc@826 23 val rev = fn [a] =>
adamc@826 24 let
adamc@826 25 fun rev' acc (ls : list a) =
adamc@826 26 case ls of
adamc@826 27 [] => acc
adamc@826 28 | x :: ls => rev' (x :: acc) ls
adamc@826 29 in
adamc@826 30 rev' []
adamc@826 31 end
adamc@794 32
adamc@826 33 val revAppend = fn [a] =>
adamc@826 34 let
adamc@826 35 fun ra (ls : list a) acc =
adamc@826 36 case ls of
adamc@826 37 [] => acc
adamc@826 38 | x :: ls => ra ls (x :: acc)
adamc@826 39 in
adamc@826 40 ra
adamc@826 41 end
adamc@821 42
adamc@826 43 fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
adamc@821 44
adamc@826 45 fun mp [a] [b] f =
adamc@794 46 let
adamc@794 47 fun mp' acc ls =
adamc@794 48 case ls of
adamc@794 49 [] => rev acc
adamc@794 50 | x :: ls => mp' (f x :: acc) ls
adamc@794 51 in
adamc@794 52 mp' []
adamc@794 53 end
adamc@796 54
adamc@826 55 fun mapPartial [a] [b] f =
adamc@821 56 let
adamc@821 57 fun mp' acc ls =
adamc@821 58 case ls of
adamc@821 59 [] => rev acc
adamc@821 60 | x :: ls => mp' (case f x of
adamc@821 61 None => acc
adamc@821 62 | Some y => y :: acc) ls
adamc@821 63 in
adamc@821 64 mp' []
adamc@821 65 end
adamc@821 66
adamc@826 67 fun mapX [a] [ctx ::: {Unit}] f =
adamc@796 68 let
adamc@796 69 fun mapX' ls =
adamc@796 70 case ls of
adamc@796 71 [] => <xml/>
adamc@796 72 | x :: ls => <xml>{f x}{mapX' ls}</xml>
adamc@796 73 in
adamc@796 74 mapX'
adamc@796 75 end
adamc@800 76
adamc@826 77 fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
adamc@800 78 let
adamc@800 79 fun mapM' acc ls =
adamc@800 80 case ls of
adamc@818 81 [] => return (rev acc)
adamc@818 82 | x :: ls => x' <- f x; mapM' (x' :: acc) ls
adamc@800 83 in
adamc@818 84 mapM' []
adamc@800 85 end
adamc@821 86
adamc@830 87 fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f =
adamc@830 88 let
adamc@830 89 fun mapXM' ls =
adamc@830 90 case ls of
adamc@830 91 [] => return <xml/>
adamc@830 92 | x :: ls =>
adamc@830 93 this <- f x;
adamc@830 94 rest <- mapXM' ls;
adamc@830 95 return <xml>{this}{rest}</xml>
adamc@830 96 in
adamc@830 97 mapXM'
adamc@830 98 end
adamc@830 99
adamc@826 100 fun filter [a] f =
adamc@821 101 let
adamc@821 102 fun fil acc ls =
adamc@821 103 case ls of
adamc@821 104 [] => rev acc
adamc@821 105 | x :: ls => fil (if f x then x :: acc else acc) ls
adamc@821 106 in
adamc@821 107 fil []
adamc@821 108 end
adamc@822 109
adamc@826 110 fun exists [a] f =
adamc@822 111 let
adamc@822 112 fun ex ls =
adamc@822 113 case ls of
adamc@822 114 [] => False
adamc@822 115 | x :: ls =>
adamc@822 116 if f x then
adamc@822 117 True
adamc@822 118 else
adamc@822 119 ex ls
adamc@822 120 in
adamc@822 121 ex
adamc@822 122 end
adamc@822 123
adamc@826 124 fun foldlMap [a] [b] [c] f =
adamc@822 125 let
adamc@822 126 fun fold ls' st ls =
adamc@822 127 case ls of
adamc@822 128 [] => (rev ls', st)
adamc@822 129 | x :: ls =>
adamc@822 130 case f x st of
adamc@822 131 (y, st) => fold (y :: ls') st ls
adamc@822 132 in
adamc@822 133 fold []
adamc@822 134 end
adamc@839 135
adamc@839 136 fun search [a] [b] f =
adamc@839 137 let
adamc@839 138 fun search' ls =
adamc@839 139 case ls of
adamc@839 140 [] => None
adamc@839 141 | x :: ls =>
adamc@839 142 case f x of
adamc@839 143 None => search' ls
adamc@839 144 | v => v
adamc@839 145 in
adamc@839 146 search'
adamc@839 147 end
adamc@839 148
adamc@840 149 fun foldlM [m] (_ : monad m) [a] [b] f =
adamc@840 150 let
adamc@840 151 fun foldlM' acc ls =
adamc@840 152 case ls of
adamc@840 153 [] => return acc
adamc@840 154 | x :: ls =>
adamc@840 155 acc <- f x acc;
adamc@840 156 foldlM' acc ls
adamc@840 157 in
adamc@840 158 foldlM'
adamc@840 159 end
adamc@843 160
adamc@843 161 fun all [m] f =
adamc@843 162 let
adamc@843 163 fun all' ls =
adamc@843 164 case ls of
adamc@843 165 [] => True
adamc@843 166 | x :: ls => f x && all' ls
adamc@843 167 in
adamc@843 168 all'
adamc@843 169 end
adamc@844 170
adamc@844 171 fun app [m] (_ : monad m) [a] f =
adamc@844 172 let
adamc@844 173 fun app' ls =
adamc@844 174 case ls of
adamc@844 175 [] => return ()
adamc@844 176 | x :: ls =>
adamc@844 177 f x;
adamc@844 178 app' ls
adamc@844 179 in
adamc@844 180 app'
adamc@844 181 end
adamc@845 182
adamc@845 183 fun assoc [a] [b] (_ : eq a) (x : a) =
adamc@845 184 let
adamc@845 185 fun assoc' (ls : list (a * b)) =
adamc@845 186 case ls of
adamc@845 187 [] => None
adamc@845 188 | (y, z) :: ls =>
adamc@845 189 if x = y then
adamc@845 190 Some z
adamc@845 191 else
adamc@845 192 assoc' ls
adamc@845 193 in
adamc@845 194 assoc'
adamc@845 195 end
adamc@845 196
adamc@845 197 fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
adamc@845 198 case assoc x ls of
adamc@845 199 None => (x, y) :: ls
adamc@845 200 | Some _ => ls