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@1279
|
104 fun mapi [a] [b] f =
|
adamc@1279
|
105 let
|
adamc@1279
|
106 fun mp' n acc ls =
|
adamc@1279
|
107 case ls of
|
adamc@1279
|
108 [] => rev acc
|
adamc@1279
|
109 | x :: ls => mp' (n + 1) (f n x :: acc) ls
|
adamc@1279
|
110 in
|
adamc@1279
|
111 mp' 0 []
|
adamc@1279
|
112 end
|
adamc@1279
|
113
|
adamc@826
|
114 fun mapPartial [a] [b] f =
|
adamc@821
|
115 let
|
adamc@821
|
116 fun mp' acc ls =
|
adamc@821
|
117 case ls of
|
adamc@821
|
118 [] => rev acc
|
adamc@821
|
119 | x :: ls => mp' (case f x of
|
adamc@821
|
120 None => acc
|
adamc@821
|
121 | Some y => y :: acc) ls
|
adamc@821
|
122 in
|
adamc@821
|
123 mp' []
|
adamc@821
|
124 end
|
adamc@821
|
125
|
adamc@826
|
126 fun mapX [a] [ctx ::: {Unit}] f =
|
adamc@796
|
127 let
|
adamc@796
|
128 fun mapX' ls =
|
adamc@796
|
129 case ls of
|
adamc@796
|
130 [] => <xml/>
|
adamc@796
|
131 | x :: ls => <xml>{f x}{mapX' ls}</xml>
|
adamc@796
|
132 in
|
adamc@796
|
133 mapX'
|
adamc@796
|
134 end
|
adamc@800
|
135
|
adamc@826
|
136 fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
|
adamc@800
|
137 let
|
adamc@800
|
138 fun mapM' acc ls =
|
adamc@800
|
139 case ls of
|
adamc@818
|
140 [] => return (rev acc)
|
adamc@818
|
141 | x :: ls => x' <- f x; mapM' (x' :: acc) ls
|
adamc@800
|
142 in
|
adamc@818
|
143 mapM' []
|
adamc@800
|
144 end
|
adamc@821
|
145
|
adamc@1107
|
146 fun mapPartialM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
|
adamc@1107
|
147 let
|
adamc@1107
|
148 fun mapPartialM' acc ls =
|
adamc@1107
|
149 case ls of
|
adamc@1107
|
150 [] => return (rev acc)
|
adamc@1107
|
151 | x :: ls =>
|
adamc@1107
|
152 v <- f x;
|
adamc@1107
|
153 mapPartialM' (case v of
|
adamc@1107
|
154 None => acc
|
adamc@1107
|
155 | Some x' => x' :: acc) ls
|
adamc@1107
|
156 in
|
adamc@1107
|
157 mapPartialM' []
|
adamc@1107
|
158 end
|
adamc@1107
|
159
|
adamc@830
|
160 fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f =
|
adamc@830
|
161 let
|
adamc@830
|
162 fun mapXM' ls =
|
adamc@830
|
163 case ls of
|
adamc@830
|
164 [] => return <xml/>
|
adamc@830
|
165 | x :: ls =>
|
adamc@830
|
166 this <- f x;
|
adamc@830
|
167 rest <- mapXM' ls;
|
adamc@830
|
168 return <xml>{this}{rest}</xml>
|
adamc@830
|
169 in
|
adamc@830
|
170 mapXM'
|
adamc@830
|
171 end
|
adamc@830
|
172
|
adamc@826
|
173 fun filter [a] f =
|
adamc@821
|
174 let
|
adamc@821
|
175 fun fil acc ls =
|
adamc@821
|
176 case ls of
|
adamc@821
|
177 [] => rev acc
|
adamc@821
|
178 | x :: ls => fil (if f x then x :: acc else acc) ls
|
adamc@821
|
179 in
|
adamc@821
|
180 fil []
|
adamc@821
|
181 end
|
adamc@822
|
182
|
adamc@826
|
183 fun exists [a] f =
|
adamc@822
|
184 let
|
adamc@822
|
185 fun ex ls =
|
adamc@822
|
186 case ls of
|
adamc@822
|
187 [] => False
|
adamc@822
|
188 | x :: ls =>
|
adamc@822
|
189 if f x then
|
adamc@822
|
190 True
|
adamc@822
|
191 else
|
adamc@822
|
192 ex ls
|
adamc@822
|
193 in
|
adamc@822
|
194 ex
|
adamc@822
|
195 end
|
adamc@822
|
196
|
adamc@826
|
197 fun foldlMap [a] [b] [c] f =
|
adamc@822
|
198 let
|
adamc@822
|
199 fun fold ls' st ls =
|
adamc@822
|
200 case ls of
|
adamc@822
|
201 [] => (rev ls', st)
|
adamc@822
|
202 | x :: ls =>
|
adamc@822
|
203 case f x st of
|
adamc@822
|
204 (y, st) => fold (y :: ls') st ls
|
adamc@822
|
205 in
|
adamc@822
|
206 fold []
|
adamc@822
|
207 end
|
adamc@839
|
208
|
adamc@839
|
209 fun search [a] [b] f =
|
adamc@839
|
210 let
|
adamc@839
|
211 fun search' ls =
|
adamc@839
|
212 case ls of
|
adamc@839
|
213 [] => None
|
adamc@839
|
214 | x :: ls =>
|
adamc@839
|
215 case f x of
|
adamc@839
|
216 None => search' ls
|
adamc@839
|
217 | v => v
|
adamc@839
|
218 in
|
adamc@839
|
219 search'
|
adamc@839
|
220 end
|
adamc@839
|
221
|
adamc@840
|
222 fun foldlM [m] (_ : monad m) [a] [b] f =
|
adamc@840
|
223 let
|
adamc@840
|
224 fun foldlM' acc ls =
|
adamc@840
|
225 case ls of
|
adamc@840
|
226 [] => return acc
|
adamc@840
|
227 | x :: ls =>
|
adamc@840
|
228 acc <- f x acc;
|
adamc@840
|
229 foldlM' acc ls
|
adamc@840
|
230 in
|
adamc@840
|
231 foldlM'
|
adamc@840
|
232 end
|
adamc@843
|
233
|
adamc@843
|
234 fun all [m] f =
|
adamc@843
|
235 let
|
adamc@843
|
236 fun all' ls =
|
adamc@843
|
237 case ls of
|
adamc@843
|
238 [] => True
|
adamc@843
|
239 | x :: ls => f x && all' ls
|
adamc@843
|
240 in
|
adamc@843
|
241 all'
|
adamc@843
|
242 end
|
adamc@844
|
243
|
adamc@844
|
244 fun app [m] (_ : monad m) [a] f =
|
adamc@844
|
245 let
|
adamc@844
|
246 fun app' ls =
|
adamc@844
|
247 case ls of
|
adamc@844
|
248 [] => return ()
|
adamc@844
|
249 | x :: ls =>
|
adamc@844
|
250 f x;
|
adamc@844
|
251 app' ls
|
adamc@844
|
252 in
|
adamc@844
|
253 app'
|
adamc@844
|
254 end
|
adamc@845
|
255
|
adamc@908
|
256 fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
|
adam@1394
|
257 [tables ~ exps] (q : sql_query [] [] tables exps)
|
adamc@908
|
258 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> t) =
|
adamc@995
|
259 ls <- query q
|
adamc@995
|
260 (fn fs acc => return (f fs :: acc))
|
adamc@995
|
261 [];
|
adamc@995
|
262 return (rev ls)
|
adamc@908
|
263
|
adamc@1107
|
264 fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
|
adam@1394
|
265 [tables ~ exps] (q : sql_query [] [] tables exps)
|
adamc@1107
|
266 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t) =
|
adamc@1107
|
267 ls <- query q
|
adamc@1107
|
268 (fn fs acc => v <- f fs; return (v :: acc))
|
adamc@1107
|
269 [];
|
adamc@1107
|
270 return (rev ls)
|
adamc@1107
|
271
|
adamc@1107
|
272 fun mapQueryPartialM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
|
adam@1394
|
273 [tables ~ exps] (q : sql_query [] [] tables exps)
|
adamc@1107
|
274 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t)) =
|
adamc@1107
|
275 ls <- query q
|
adamc@1107
|
276 (fn fs acc => v <- f fs;
|
adamc@1107
|
277 return (case v of
|
adamc@1107
|
278 None => acc
|
adamc@1107
|
279 | Some v => v :: acc))
|
adamc@1107
|
280 [];
|
adamc@1107
|
281 return (rev ls)
|
adamc@1107
|
282
|
adam@1321
|
283 fun sort [a] (gt : a -> a -> bool) (ls : t a) : t a =
|
adam@1321
|
284 let
|
adam@1321
|
285 fun split ls acc1 acc2 =
|
adam@1321
|
286 case ls of
|
adam@1321
|
287 [] => (rev acc1, rev acc2)
|
adam@1321
|
288 | x :: [] => (rev (x :: acc1), rev acc2)
|
adam@1321
|
289 | x1 :: x2 :: ls' => split ls' (x1 :: acc1) (x2 :: acc2)
|
adam@1321
|
290
|
adam@1321
|
291 fun merge ls1 ls2 acc =
|
adam@1321
|
292 case (ls1, ls2) of
|
adam@1321
|
293 ([], _) => revAppend acc ls2
|
adam@1321
|
294 | (_, []) => revAppend acc ls1
|
adam@1321
|
295 | (x1 :: ls1', x2 :: ls2') => if gt x1 x2 then merge ls1 ls2' (x2 :: acc) else merge ls1' ls2 (x1 :: acc)
|
adam@1321
|
296
|
adam@1321
|
297 fun sort' ls =
|
adam@1321
|
298 case ls of
|
adam@1321
|
299 [] => ls
|
adam@1321
|
300 | _ :: [] => ls
|
adam@1321
|
301 | _ =>
|
adam@1321
|
302 let
|
adam@1321
|
303 val (ls1, ls2) = split ls [] []
|
adam@1321
|
304 in
|
adam@1321
|
305 merge (sort' ls1) (sort' ls2) []
|
adam@1321
|
306 end
|
adam@1321
|
307 in
|
adam@1321
|
308 sort' ls
|
adam@1321
|
309 end
|
adam@1321
|
310
|
adam@1322
|
311 val nth [a] =
|
adam@1322
|
312 let
|
adam@1322
|
313 fun nth (ls : list a) (n : int) : option a =
|
adam@1322
|
314 case ls of
|
adam@1322
|
315 [] => None
|
adam@1322
|
316 | x :: ls' =>
|
adam@1322
|
317 if n <= 0 then
|
adam@1322
|
318 Some x
|
adam@1322
|
319 else
|
adam@1322
|
320 nth ls' (n-1)
|
adam@1322
|
321 in
|
adam@1322
|
322 nth
|
adam@1322
|
323 end
|
adam@1322
|
324
|
adam@1345
|
325 fun replaceNth [a] (ls : list a) (n : int) (v : a) : list a =
|
adam@1345
|
326 let
|
adam@1345
|
327 fun repNth (ls : list a) (n : int) (acc : list a) =
|
adam@1345
|
328 case ls of
|
adam@1345
|
329 [] => rev acc
|
adam@1345
|
330 | x :: ls' => if n <= 0 then
|
adam@1345
|
331 revAppend acc (v :: ls')
|
adam@1345
|
332 else
|
adam@1345
|
333 repNth ls' (n-1) (x :: acc)
|
adam@1345
|
334 in
|
adam@1345
|
335 repNth ls n []
|
adam@1345
|
336 end
|
adam@1345
|
337
|
adamc@845
|
338 fun assoc [a] [b] (_ : eq a) (x : a) =
|
adamc@845
|
339 let
|
adamc@845
|
340 fun assoc' (ls : list (a * b)) =
|
adamc@845
|
341 case ls of
|
adamc@845
|
342 [] => None
|
adamc@845
|
343 | (y, z) :: ls =>
|
adamc@845
|
344 if x = y then
|
adamc@845
|
345 Some z
|
adamc@845
|
346 else
|
adamc@845
|
347 assoc' ls
|
adamc@845
|
348 in
|
adamc@845
|
349 assoc'
|
adamc@845
|
350 end
|
adamc@845
|
351
|
adamc@845
|
352 fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
|
adamc@845
|
353 case assoc x ls of
|
adamc@845
|
354 None => (x, y) :: ls
|
adamc@845
|
355 | Some _ => ls
|
greenrd@1481
|
356
|
greenrd@1481
|
357 fun recToList [a ::: Type] [r ::: {Unit}] (fl : folder r)
|
greenrd@1481
|
358 = @foldUR [a] [fn _ => list a] (fn [nm ::_] [rest ::_] [[nm] ~ rest] x xs =>
|
greenrd@1481
|
359 x :: xs) [] fl
|