Mercurial > urweb

annotate lib/ur/list.ur @ 844:74a1e3bdf430

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