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
|
adam@1539
|
136 fun mapXi [a] [ctx ::: {Unit}] f =
|
adam@1539
|
137 let
|
adam@1539
|
138 fun mapX' i ls =
|
adam@1539
|
139 case ls of
|
adam@1539
|
140 [] => <xml/>
|
adam@1539
|
141 | x :: ls => <xml>{f i x}{mapX' (i + 1) ls}</xml>
|
adam@1539
|
142 in
|
adam@1539
|
143 mapX' 0
|
adam@1539
|
144 end
|
adam@1539
|
145
|
adamc@826
|
146 fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
|
adamc@800
|
147 let
|
adamc@800
|
148 fun mapM' acc ls =
|
adamc@800
|
149 case ls of
|
adamc@818
|
150 [] => return (rev acc)
|
adamc@818
|
151 | x :: ls => x' <- f x; mapM' (x' :: acc) ls
|
adamc@800
|
152 in
|
adamc@818
|
153 mapM' []
|
adamc@800
|
154 end
|
adamc@821
|
155
|
adamc@1107
|
156 fun mapPartialM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
|
adamc@1107
|
157 let
|
adamc@1107
|
158 fun mapPartialM' acc ls =
|
adamc@1107
|
159 case ls of
|
adamc@1107
|
160 [] => return (rev acc)
|
adamc@1107
|
161 | x :: ls =>
|
adamc@1107
|
162 v <- f x;
|
adamc@1107
|
163 mapPartialM' (case v of
|
adamc@1107
|
164 None => acc
|
adamc@1107
|
165 | Some x' => x' :: acc) ls
|
adamc@1107
|
166 in
|
adamc@1107
|
167 mapPartialM' []
|
adamc@1107
|
168 end
|
adamc@1107
|
169
|
adamc@830
|
170 fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f =
|
adamc@830
|
171 let
|
adamc@830
|
172 fun mapXM' ls =
|
adamc@830
|
173 case ls of
|
adamc@830
|
174 [] => return <xml/>
|
adamc@830
|
175 | x :: ls =>
|
adamc@830
|
176 this <- f x;
|
adamc@830
|
177 rest <- mapXM' ls;
|
adamc@830
|
178 return <xml>{this}{rest}</xml>
|
adamc@830
|
179 in
|
adamc@830
|
180 mapXM'
|
adamc@830
|
181 end
|
adamc@830
|
182
|
adamc@826
|
183 fun filter [a] f =
|
adamc@821
|
184 let
|
adamc@821
|
185 fun fil acc ls =
|
adamc@821
|
186 case ls of
|
adamc@821
|
187 [] => rev acc
|
adamc@821
|
188 | x :: ls => fil (if f x then x :: acc else acc) ls
|
adamc@821
|
189 in
|
adamc@821
|
190 fil []
|
adamc@821
|
191 end
|
adamc@822
|
192
|
adamc@826
|
193 fun exists [a] f =
|
adamc@822
|
194 let
|
adamc@822
|
195 fun ex ls =
|
adamc@822
|
196 case ls of
|
adamc@822
|
197 [] => False
|
adamc@822
|
198 | x :: ls =>
|
adamc@822
|
199 if f x then
|
adamc@822
|
200 True
|
adamc@822
|
201 else
|
adamc@822
|
202 ex ls
|
adamc@822
|
203 in
|
adamc@822
|
204 ex
|
adamc@822
|
205 end
|
adamc@822
|
206
|
adamc@826
|
207 fun foldlMap [a] [b] [c] f =
|
adamc@822
|
208 let
|
adamc@822
|
209 fun fold ls' st ls =
|
adamc@822
|
210 case ls of
|
adamc@822
|
211 [] => (rev ls', st)
|
adamc@822
|
212 | x :: ls =>
|
adamc@822
|
213 case f x st of
|
adamc@822
|
214 (y, st) => fold (y :: ls') st ls
|
adamc@822
|
215 in
|
adamc@822
|
216 fold []
|
adamc@822
|
217 end
|
adamc@839
|
218
|
adam@1519
|
219 fun find [a] f =
|
adam@1519
|
220 let
|
adam@1519
|
221 fun find' ls =
|
adam@1519
|
222 case ls of
|
adam@1519
|
223 [] => None
|
adam@1519
|
224 | x :: ls =>
|
adam@1519
|
225 if f x then
|
adam@1519
|
226 Some x
|
adam@1519
|
227 else
|
adam@1519
|
228 find' ls
|
adam@1519
|
229 in
|
adam@1519
|
230 find'
|
adam@1519
|
231 end
|
adam@1519
|
232
|
adamc@839
|
233 fun search [a] [b] f =
|
adamc@839
|
234 let
|
adamc@839
|
235 fun search' ls =
|
adamc@839
|
236 case ls of
|
adamc@839
|
237 [] => None
|
adamc@839
|
238 | x :: ls =>
|
adamc@839
|
239 case f x of
|
adamc@839
|
240 None => search' ls
|
adamc@839
|
241 | v => v
|
adamc@839
|
242 in
|
adamc@839
|
243 search'
|
adamc@839
|
244 end
|
adamc@839
|
245
|
adamc@840
|
246 fun foldlM [m] (_ : monad m) [a] [b] f =
|
adamc@840
|
247 let
|
adamc@840
|
248 fun foldlM' acc ls =
|
adamc@840
|
249 case ls of
|
adamc@840
|
250 [] => return acc
|
adamc@840
|
251 | x :: ls =>
|
adamc@840
|
252 acc <- f x acc;
|
adamc@840
|
253 foldlM' acc ls
|
adamc@840
|
254 in
|
adamc@840
|
255 foldlM'
|
adamc@840
|
256 end
|
adamc@843
|
257
|
adam@1547
|
258 fun foldlMi [m] (_ : monad m) [a] [b] f =
|
adam@1547
|
259 let
|
adam@1547
|
260 fun foldlMi' i acc ls =
|
adam@1547
|
261 case ls of
|
adam@1547
|
262 [] => return acc
|
adam@1547
|
263 | x :: ls =>
|
adam@1547
|
264 acc <- f i x acc;
|
adam@1547
|
265 foldlMi' (i + 1) acc ls
|
adam@1547
|
266 in
|
adam@1547
|
267 foldlMi' 0
|
adam@1547
|
268 end
|
adam@1547
|
269
|
adam@1634
|
270 fun filterM [m] (_ : monad m) [a] (p : a -> m bool) =
|
adam@1634
|
271 let
|
adam@1634
|
272 fun filterM' (acc : list a) (xs : list a) : m (list a) =
|
adam@1634
|
273 case xs of
|
adam@1634
|
274 [] => return (rev acc)
|
adam@1634
|
275 | x :: xs =>
|
adam@1634
|
276 c <- p x;
|
adam@1634
|
277 filterM' (if c then x :: acc else acc) xs
|
adam@1634
|
278 in
|
adam@1634
|
279 filterM' []
|
adam@1634
|
280 end
|
adam@1634
|
281
|
adamc@843
|
282 fun all [m] f =
|
adamc@843
|
283 let
|
adamc@843
|
284 fun all' ls =
|
adamc@843
|
285 case ls of
|
adamc@843
|
286 [] => True
|
adamc@843
|
287 | x :: ls => f x && all' ls
|
adamc@843
|
288 in
|
adamc@843
|
289 all'
|
adamc@843
|
290 end
|
adamc@844
|
291
|
adamc@844
|
292 fun app [m] (_ : monad m) [a] f =
|
adamc@844
|
293 let
|
adamc@844
|
294 fun app' ls =
|
adamc@844
|
295 case ls of
|
adamc@844
|
296 [] => return ()
|
adamc@844
|
297 | x :: ls =>
|
adamc@844
|
298 f x;
|
adamc@844
|
299 app' ls
|
adamc@844
|
300 in
|
adamc@844
|
301 app'
|
adamc@844
|
302 end
|
adamc@845
|
303
|
adamc@908
|
304 fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
|
adam@1394
|
305 [tables ~ exps] (q : sql_query [] [] tables exps)
|
adamc@908
|
306 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> t) =
|
adamc@995
|
307 ls <- query q
|
adamc@995
|
308 (fn fs acc => return (f fs :: acc))
|
adamc@995
|
309 [];
|
adamc@995
|
310 return (rev ls)
|
adamc@908
|
311
|
adamc@1107
|
312 fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
|
adam@1394
|
313 [tables ~ exps] (q : sql_query [] [] tables exps)
|
adamc@1107
|
314 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t) =
|
adamc@1107
|
315 ls <- query q
|
adamc@1107
|
316 (fn fs acc => v <- f fs; return (v :: acc))
|
adamc@1107
|
317 [];
|
adamc@1107
|
318 return (rev ls)
|
adamc@1107
|
319
|
adamc@1107
|
320 fun mapQueryPartialM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
|
adam@1394
|
321 [tables ~ exps] (q : sql_query [] [] tables exps)
|
adamc@1107
|
322 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t)) =
|
adamc@1107
|
323 ls <- query q
|
adamc@1107
|
324 (fn fs acc => v <- f fs;
|
adamc@1107
|
325 return (case v of
|
adamc@1107
|
326 None => acc
|
adamc@1107
|
327 | Some v => v :: acc))
|
adamc@1107
|
328 [];
|
adamc@1107
|
329 return (rev ls)
|
adamc@1107
|
330
|
adam@1321
|
331 fun sort [a] (gt : a -> a -> bool) (ls : t a) : t a =
|
adam@1321
|
332 let
|
adam@1321
|
333 fun split ls acc1 acc2 =
|
adam@1321
|
334 case ls of
|
adam@1321
|
335 [] => (rev acc1, rev acc2)
|
adam@1321
|
336 | x :: [] => (rev (x :: acc1), rev acc2)
|
adam@1321
|
337 | x1 :: x2 :: ls' => split ls' (x1 :: acc1) (x2 :: acc2)
|
adam@1321
|
338
|
adam@1321
|
339 fun merge ls1 ls2 acc =
|
adam@1321
|
340 case (ls1, ls2) of
|
adam@1321
|
341 ([], _) => revAppend acc ls2
|
adam@1321
|
342 | (_, []) => revAppend acc ls1
|
adam@1321
|
343 | (x1 :: ls1', x2 :: ls2') => if gt x1 x2 then merge ls1 ls2' (x2 :: acc) else merge ls1' ls2 (x1 :: acc)
|
adam@1321
|
344
|
adam@1321
|
345 fun sort' ls =
|
adam@1321
|
346 case ls of
|
adam@1321
|
347 [] => ls
|
adam@1321
|
348 | _ :: [] => ls
|
adam@1321
|
349 | _ =>
|
adam@1321
|
350 let
|
adam@1321
|
351 val (ls1, ls2) = split ls [] []
|
adam@1321
|
352 in
|
adam@1321
|
353 merge (sort' ls1) (sort' ls2) []
|
adam@1321
|
354 end
|
adam@1321
|
355 in
|
adam@1321
|
356 sort' ls
|
adam@1321
|
357 end
|
adam@1321
|
358
|
adam@1322
|
359 val nth [a] =
|
adam@1322
|
360 let
|
adam@1322
|
361 fun nth (ls : list a) (n : int) : option a =
|
adam@1322
|
362 case ls of
|
adam@1322
|
363 [] => None
|
adam@1322
|
364 | x :: ls' =>
|
adam@1322
|
365 if n <= 0 then
|
adam@1322
|
366 Some x
|
adam@1322
|
367 else
|
adam@1322
|
368 nth ls' (n-1)
|
adam@1322
|
369 in
|
adam@1322
|
370 nth
|
adam@1322
|
371 end
|
adam@1322
|
372
|
adam@1345
|
373 fun replaceNth [a] (ls : list a) (n : int) (v : a) : list a =
|
adam@1345
|
374 let
|
adam@1345
|
375 fun repNth (ls : list a) (n : int) (acc : list a) =
|
adam@1345
|
376 case ls of
|
adam@1345
|
377 [] => rev acc
|
adam@1345
|
378 | x :: ls' => if n <= 0 then
|
adam@1345
|
379 revAppend acc (v :: ls')
|
adam@1345
|
380 else
|
adam@1345
|
381 repNth ls' (n-1) (x :: acc)
|
adam@1345
|
382 in
|
adam@1345
|
383 repNth ls n []
|
adam@1345
|
384 end
|
adam@1345
|
385
|
adamc@845
|
386 fun assoc [a] [b] (_ : eq a) (x : a) =
|
adamc@845
|
387 let
|
adamc@845
|
388 fun assoc' (ls : list (a * b)) =
|
adamc@845
|
389 case ls of
|
adamc@845
|
390 [] => None
|
adamc@845
|
391 | (y, z) :: ls =>
|
adamc@845
|
392 if x = y then
|
adamc@845
|
393 Some z
|
adamc@845
|
394 else
|
adamc@845
|
395 assoc' ls
|
adamc@845
|
396 in
|
adamc@845
|
397 assoc'
|
adamc@845
|
398 end
|
adamc@845
|
399
|
adamc@845
|
400 fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
|
adamc@845
|
401 case assoc x ls of
|
adamc@845
|
402 None => (x, y) :: ls
|
adamc@845
|
403 | Some _ => ls
|
greenrd@1481
|
404
|
greenrd@1481
|
405 fun recToList [a ::: Type] [r ::: {Unit}] (fl : folder r)
|
greenrd@1481
|
406 = @foldUR [a] [fn _ => list a] (fn [nm ::_] [rest ::_] [[nm] ~ rest] x xs =>
|
greenrd@1481
|
407 x :: xs) [] fl
|
adam@1634
|
408
|
adam@1634
|
409 fun take [a] (n : int) (xs : list a) : list a =
|
adam@1634
|
410 if n <= 0 then
|
adam@1634
|
411 []
|
adam@1634
|
412 else
|
adam@1634
|
413 case xs of
|
adam@1634
|
414 [] => []
|
adam@1634
|
415 | x :: xs => x :: take (n-1) xs
|
adam@1634
|
416
|
adam@1634
|
417 fun drop [a] (n : int) (xs : list a) : list a =
|
adam@1634
|
418 if n <= 0 then
|
adam@1634
|
419 xs
|
adam@1634
|
420 else
|
adam@1634
|
421 case xs of
|
adam@1634
|
422 [] => []
|
adam@1634
|
423 | x :: xs => drop (n-1) xs
|
adam@1634
|
424
|
adam@1634
|
425 fun splitAt [a] (n : int) (xs : list a) : list a * list a =
|
adam@1634
|
426 (take n xs, drop n xs)
|
adam@1768
|
427
|
adam@1768
|
428 fun mapXiM [m ::: Type -> Type] (_ : monad m) [a] [ctx ::: {Unit}] (f : int -> a -> m (xml ctx [] [])) : t a -> m (xml ctx [] []) =
|
adam@1768
|
429 let
|
adam@1768
|
430 fun mapXiM' i ls =
|
adam@1768
|
431 case ls of
|
adam@1768
|
432 [] => return <xml/>
|
adam@1768
|
433 | x :: ls =>
|
adam@1768
|
434 this <- f i x;
|
adam@1768
|
435 rest <- mapXiM' (i+1) ls;
|
adam@1768
|
436 return <xml>{this}{rest}</xml>
|
adam@1768
|
437 in
|
adam@1768
|
438 mapXiM' 0
|
adam@1768
|
439 end
|