blob: 0776ff3094f1c26e1e0cf98e00b0bc5e884f89c3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
datatype t = datatype Basis.list
val show = fn [a] (_ : show a) =>
let
fun show' (ls : list a) =
case ls of
[] => "[]"
| x :: ls => show x ^ " :: " ^ show' ls
in
mkShow show'
end
val rev = fn [a] =>
let
fun rev' acc (ls : list a) =
case ls of
[] => acc
| x :: ls => rev' (x :: acc) ls
in
rev' []
end
val revAppend = fn [a] =>
let
fun ra (ls : list a) acc =
case ls of
[] => acc
| x :: ls => ra ls (x :: acc)
in
ra
end
fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
fun mp [a] [b] f =
let
fun mp' acc ls =
case ls of
[] => rev acc
| x :: ls => mp' (f x :: acc) ls
in
mp' []
end
fun mapPartial [a] [b] f =
let
fun mp' acc ls =
case ls of
[] => rev acc
| x :: ls => mp' (case f x of
None => acc
| Some y => y :: acc) ls
in
mp' []
end
fun mapX [a] [ctx ::: {Unit}] f =
let
fun mapX' ls =
case ls of
[] => <xml/>
| x :: ls => <xml>{f x}{mapX' ls}</xml>
in
mapX'
end
fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
let
fun mapM' acc ls =
case ls of
[] => return (rev acc)
| x :: ls => x' <- f x; mapM' (x' :: acc) ls
in
mapM' []
end
fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f =
let
fun mapXM' ls =
case ls of
[] => return <xml/>
| x :: ls =>
this <- f x;
rest <- mapXM' ls;
return <xml>{this}{rest}</xml>
in
mapXM'
end
fun filter [a] f =
let
fun fil acc ls =
case ls of
[] => rev acc
| x :: ls => fil (if f x then x :: acc else acc) ls
in
fil []
end
fun exists [a] f =
let
fun ex ls =
case ls of
[] => False
| x :: ls =>
if f x then
True
else
ex ls
in
ex
end
fun foldlMap [a] [b] [c] f =
let
fun fold ls' st ls =
case ls of
[] => (rev ls', st)
| x :: ls =>
case f x st of
(y, st) => fold (y :: ls') st ls
in
fold []
end
|
