6118
|
1 |
(* Title: Pure/General/seq.ML
|
5014
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
12851
|
4 |
Author: Markus Wenzel, TU Munich
|
5014
|
5 |
|
|
6 |
Unbounded sequences implemented by closures. RECOMPUTES if sequence
|
|
7 |
is re-inspected. Memoing, using polymorphic refs, was found to be
|
|
8 |
slower! (More GCs)
|
|
9 |
*)
|
|
10 |
|
|
11 |
signature SEQ =
|
|
12 |
sig
|
|
13 |
type 'a seq
|
|
14 |
val make: (unit -> ('a * 'a seq) option) -> 'a seq
|
|
15 |
val pull: 'a seq -> ('a * 'a seq) option
|
|
16 |
val empty: 'a seq
|
|
17 |
val cons: 'a * 'a seq -> 'a seq
|
|
18 |
val single: 'a -> 'a seq
|
11721
|
19 |
val try: ('a -> 'b) -> 'a -> 'b seq
|
5014
|
20 |
val hd: 'a seq -> 'a
|
|
21 |
val tl: 'a seq -> 'a seq
|
|
22 |
val chop: int * 'a seq -> 'a list * 'a seq
|
|
23 |
val list_of: 'a seq -> 'a list
|
|
24 |
val of_list: 'a list -> 'a seq
|
|
25 |
val map: ('a -> 'b) -> 'a seq -> 'b seq
|
|
26 |
val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
|
|
27 |
val append: 'a seq * 'a seq -> 'a seq
|
|
28 |
val filter: ('a -> bool) -> 'a seq -> 'a seq
|
|
29 |
val flat: 'a seq seq -> 'a seq
|
|
30 |
val interleave: 'a seq * 'a seq -> 'a seq
|
|
31 |
val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
|
|
32 |
val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
|
6927
|
33 |
val commute: 'a seq list -> 'a list seq
|
5014
|
34 |
val succeed: 'a -> 'a seq
|
|
35 |
val fail: 'a -> 'b seq
|
|
36 |
val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
|
|
37 |
val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
|
|
38 |
val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
|
|
39 |
val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
|
|
40 |
val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
|
|
41 |
val TRY: ('a -> 'a seq) -> 'a -> 'a seq
|
|
42 |
val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
|
5558
|
43 |
val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
|
8535
|
44 |
val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
|
12851
|
45 |
val DETERM: ('a -> 'b seq) -> 'a -> 'b seq
|
5014
|
46 |
end;
|
|
47 |
|
|
48 |
structure Seq: SEQ =
|
|
49 |
struct
|
|
50 |
|
|
51 |
|
|
52 |
(** lazy sequences **)
|
|
53 |
|
|
54 |
datatype 'a seq = Seq of unit -> ('a * 'a seq) option;
|
|
55 |
|
|
56 |
(*the abstraction for making a sequence*)
|
|
57 |
val make = Seq;
|
|
58 |
|
15531
|
59 |
(*return next sequence element as NONE or SOME (x, xq)*)
|
5014
|
60 |
fun pull (Seq f) = f ();
|
|
61 |
|
|
62 |
|
|
63 |
(*the empty sequence*)
|
15531
|
64 |
val empty = Seq (fn () => NONE);
|
5014
|
65 |
|
|
66 |
(*prefix an element to the sequence -- use cons (x, xq) only if
|
|
67 |
evaluation of xq need not be delayed, otherwise use
|
15531
|
68 |
make (fn () => SOME (x, xq))*)
|
|
69 |
fun cons x_xq = make (fn () => SOME x_xq);
|
5014
|
70 |
|
|
71 |
fun single x = cons (x, empty);
|
|
72 |
|
|
73 |
(*head and tail -- beware of calling the sequence function twice!!*)
|
15570
|
74 |
fun hd xq = #1 (valOf (pull xq))
|
|
75 |
and tl xq = #2 (valOf (pull xq));
|
5014
|
76 |
|
11721
|
77 |
(*partial function as procedure*)
|
|
78 |
fun try f x =
|
|
79 |
(case Library.try f x of
|
15531
|
80 |
SOME y => single y
|
|
81 |
| NONE => empty);
|
11721
|
82 |
|
5014
|
83 |
|
|
84 |
(*the list of the first n elements, paired with rest of sequence;
|
|
85 |
if length of list is less than n, then sequence had less than n elements*)
|
|
86 |
fun chop (n, xq) =
|
|
87 |
if n <= 0 then ([], xq)
|
|
88 |
else
|
|
89 |
(case pull xq of
|
15531
|
90 |
NONE => ([], xq)
|
|
91 |
| SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
|
5014
|
92 |
|
|
93 |
(*conversion from sequence to list*)
|
|
94 |
fun list_of xq =
|
|
95 |
(case pull xq of
|
15531
|
96 |
NONE => []
|
|
97 |
| SOME (x, xq') => x :: list_of xq');
|
5014
|
98 |
|
|
99 |
(*conversion from list to sequence*)
|
15570
|
100 |
fun of_list xs = Library.foldr cons (xs, empty);
|
5014
|
101 |
|
|
102 |
|
|
103 |
(*map the function f over the sequence, making a new sequence*)
|
|
104 |
fun map f xq =
|
|
105 |
make (fn () =>
|
|
106 |
(case pull xq of
|
15531
|
107 |
NONE => NONE
|
|
108 |
| SOME (x, xq') => SOME (f x, map f xq')));
|
5014
|
109 |
|
|
110 |
(*map over a sequence xq, append the sequence yq*)
|
|
111 |
fun mapp f xq yq =
|
|
112 |
let
|
|
113 |
fun copy s =
|
|
114 |
make (fn () =>
|
|
115 |
(case pull s of
|
15531
|
116 |
NONE => pull yq
|
|
117 |
| SOME (x, s') => SOME (f x, copy s')))
|
5014
|
118 |
in copy xq end;
|
|
119 |
|
|
120 |
(*sequence append: put the elements of xq in front of those of yq*)
|
|
121 |
fun append (xq, yq) =
|
|
122 |
let
|
|
123 |
fun copy s =
|
|
124 |
make (fn () =>
|
|
125 |
(case pull s of
|
15531
|
126 |
NONE => pull yq
|
|
127 |
| SOME (x, s') => SOME (x, copy s')))
|
5014
|
128 |
in copy xq end;
|
|
129 |
|
|
130 |
(*filter sequence by predicate*)
|
|
131 |
fun filter pred xq =
|
|
132 |
let
|
|
133 |
fun copy s =
|
|
134 |
make (fn () =>
|
|
135 |
(case pull s of
|
15531
|
136 |
NONE => NONE
|
|
137 |
| SOME (x, s') => if pred x then SOME (x, copy s') else pull (copy s')));
|
5014
|
138 |
in copy xq end;
|
|
139 |
|
|
140 |
(*flatten a sequence of sequences to a single sequence*)
|
|
141 |
fun flat xqq =
|
|
142 |
make (fn () =>
|
|
143 |
(case pull xqq of
|
15531
|
144 |
NONE => NONE
|
|
145 |
| SOME (xq, xqq') => pull (append (xq, flat xqq'))));
|
5014
|
146 |
|
|
147 |
(*interleave elements of xq with those of yq -- fairer than append*)
|
|
148 |
fun interleave (xq, yq) =
|
|
149 |
make (fn () =>
|
|
150 |
(case pull xq of
|
15531
|
151 |
NONE => pull yq
|
|
152 |
| SOME (x, xq') => SOME (x, interleave (yq, xq'))));
|
5014
|
153 |
|
|
154 |
|
|
155 |
(*functional to print a sequence, up to "count" elements;
|
|
156 |
the function prelem should print the element number and also the element*)
|
|
157 |
fun print prelem count seq =
|
|
158 |
let
|
|
159 |
fun pr (k, xq) =
|
|
160 |
if k > count then ()
|
|
161 |
else
|
|
162 |
(case pull xq of
|
15531
|
163 |
NONE => ()
|
|
164 |
| SOME (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
|
5014
|
165 |
in pr (1, seq) end;
|
|
166 |
|
|
167 |
(*accumulating a function over a sequence; this is lazy*)
|
|
168 |
fun it_right f (xq, yq) =
|
|
169 |
let
|
|
170 |
fun its s =
|
|
171 |
make (fn () =>
|
|
172 |
(case pull s of
|
15531
|
173 |
NONE => pull yq
|
|
174 |
| SOME (a, s') => pull (f (a, its s'))))
|
5014
|
175 |
in its xq end;
|
|
176 |
|
6927
|
177 |
(*turn a list of sequences into a sequence of lists*)
|
|
178 |
fun commute [] = single []
|
|
179 |
| commute (xq :: xqs) =
|
|
180 |
make (fn () =>
|
|
181 |
(case pull xq of
|
15531
|
182 |
NONE => NONE
|
|
183 |
| SOME (x, xq') =>
|
6927
|
184 |
(case pull (commute xqs) of
|
15531
|
185 |
NONE => NONE
|
|
186 |
| SOME (xs, xsq) =>
|
|
187 |
SOME (x :: xs, append (map (Library.cons x) xsq, commute (xq' :: xqs))))));
|
6927
|
188 |
|
5014
|
189 |
|
|
190 |
|
12851
|
191 |
(** sequence functions **) (*some code copied from Pure/tctical.ML*)
|
5014
|
192 |
|
|
193 |
fun succeed x = single x;
|
|
194 |
fun fail _ = empty;
|
|
195 |
|
5864
|
196 |
fun op THEN (f, g) x = flat (map g (f x));
|
5014
|
197 |
|
5864
|
198 |
fun op ORELSE (f, g) x =
|
5014
|
199 |
(case pull (f x) of
|
15531
|
200 |
NONE => g x
|
5014
|
201 |
| some => make (fn () => some));
|
|
202 |
|
5864
|
203 |
fun op APPEND (f, g) x =
|
5014
|
204 |
append (f x, make (fn () => pull (g x)));
|
|
205 |
|
15570
|
206 |
fun EVERY fs = Library.foldr THEN (fs, succeed);
|
|
207 |
fun FIRST fs = Library.foldr ORELSE (fs, fail);
|
5014
|
208 |
|
|
209 |
fun TRY f = ORELSE (f, succeed);
|
|
210 |
|
|
211 |
fun REPEAT f =
|
|
212 |
let
|
|
213 |
fun rep qs x =
|
|
214 |
(case pull (f x) of
|
15531
|
215 |
NONE => SOME (x, make (fn () => repq qs))
|
|
216 |
| SOME (x', q) => rep (q :: qs) x')
|
|
217 |
and repq [] = NONE
|
5014
|
218 |
| repq (q :: qs) =
|
|
219 |
(case pull q of
|
15531
|
220 |
NONE => repq qs
|
|
221 |
| SOME (x, q) => rep (q :: qs) x);
|
5014
|
222 |
in fn x => make (fn () => rep [] x) end;
|
|
223 |
|
5558
|
224 |
fun REPEAT1 f = THEN (f, REPEAT f);
|
|
225 |
|
8535
|
226 |
fun INTERVAL f i j x =
|
|
227 |
if i > j then single x
|
|
228 |
else op THEN (f j, INTERVAL f i (j - 1)) x;
|
|
229 |
|
12851
|
230 |
fun DETERM f x =
|
|
231 |
(case pull (f x) of
|
15531
|
232 |
NONE => empty
|
|
233 |
| SOME (x', _) => cons (x', empty));
|
8535
|
234 |
|
5014
|
235 |
end;
|