author | wenzelm |
Tue, 13 Sep 2005 22:19:31 +0200 | |
changeset 17347 | fb3d42ef61ed |
parent 16534 | 95460b6eb712 |
child 19475 | 8aa2b380614a |
permissions | -rw-r--r-- |
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 |
|
17347 | 25 |
val append: 'a seq * 'a seq -> 'a seq |
5014 | 26 |
val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq |
17347 | 27 |
val interleave: 'a seq * 'a seq -> 'a seq |
5014 | 28 |
val filter: ('a -> bool) -> 'a seq -> 'a seq |
29 |
val flat: 'a seq seq -> 'a seq |
|
17347 | 30 |
val map: ('a -> 'b) -> 'a seq -> 'b seq |
31 |
val maps: ('a -> 'b seq) -> 'a seq -> 'b seq |
|
32 |
val lift: ('a -> 'b -> 'c) -> 'a seq -> 'b -> 'c seq |
|
33 |
val lifts: ('a -> 'b -> 'c seq) -> 'a seq -> 'b -> 'c seq |
|
5014 | 34 |
val print: (int -> 'a -> unit) -> int -> 'a seq -> unit |
35 |
val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq |
|
6927 | 36 |
val commute: 'a seq list -> 'a list seq |
17347 | 37 |
val map_list: ('a -> 'b seq) -> 'a list -> 'b list seq |
5014 | 38 |
val succeed: 'a -> 'a seq |
39 |
val fail: 'a -> 'b seq |
|
40 |
val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq |
|
41 |
val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq |
|
42 |
val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq |
|
43 |
val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq |
|
44 |
val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq |
|
45 |
val TRY: ('a -> 'a seq) -> 'a -> 'a seq |
|
46 |
val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq |
|
5558 | 47 |
val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq |
8535 | 48 |
val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq |
12851 | 49 |
val DETERM: ('a -> 'b seq) -> 'a -> 'b seq |
5014 | 50 |
end; |
51 |
||
52 |
structure Seq: SEQ = |
|
53 |
struct |
|
54 |
||
55 |
||
56 |
(** lazy sequences **) |
|
57 |
||
58 |
datatype 'a seq = Seq of unit -> ('a * 'a seq) option; |
|
59 |
||
60 |
(*the abstraction for making a sequence*) |
|
61 |
val make = Seq; |
|
62 |
||
15531 | 63 |
(*return next sequence element as NONE or SOME (x, xq)*) |
5014 | 64 |
fun pull (Seq f) = f (); |
65 |
||
66 |
||
67 |
(*the empty sequence*) |
|
15531 | 68 |
val empty = Seq (fn () => NONE); |
5014 | 69 |
|
70 |
(*prefix an element to the sequence -- use cons (x, xq) only if |
|
71 |
evaluation of xq need not be delayed, otherwise use |
|
15531 | 72 |
make (fn () => SOME (x, xq))*) |
73 |
fun cons x_xq = make (fn () => SOME x_xq); |
|
5014 | 74 |
|
75 |
fun single x = cons (x, empty); |
|
76 |
||
77 |
(*head and tail -- beware of calling the sequence function twice!!*) |
|
16002 | 78 |
fun hd xq = #1 (the (pull xq)) |
79 |
and tl xq = #2 (the (pull xq)); |
|
5014 | 80 |
|
11721 | 81 |
(*partial function as procedure*) |
82 |
fun try f x = |
|
83 |
(case Library.try f x of |
|
15531 | 84 |
SOME y => single y |
85 |
| NONE => empty); |
|
11721 | 86 |
|
5014 | 87 |
|
88 |
(*the list of the first n elements, paired with rest of sequence; |
|
89 |
if length of list is less than n, then sequence had less than n elements*) |
|
90 |
fun chop (n, xq) = |
|
91 |
if n <= 0 then ([], xq) |
|
92 |
else |
|
93 |
(case pull xq of |
|
15531 | 94 |
NONE => ([], xq) |
95 |
| SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq'))); |
|
5014 | 96 |
|
97 |
(*conversion from sequence to list*) |
|
98 |
fun list_of xq = |
|
99 |
(case pull xq of |
|
15531 | 100 |
NONE => [] |
101 |
| SOME (x, xq') => x :: list_of xq'); |
|
5014 | 102 |
|
103 |
(*conversion from list to sequence*) |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
104 |
fun of_list xs = foldr cons empty xs; |
5014 | 105 |
|
106 |
||
17347 | 107 |
(*sequence append: put the elements of xq in front of those of yq*) |
108 |
fun append (xq, yq) = |
|
109 |
let |
|
110 |
fun copy s = |
|
111 |
make (fn () => |
|
112 |
(case pull s of |
|
113 |
NONE => pull yq |
|
114 |
| SOME (x, s') => SOME (x, copy s'))) |
|
115 |
in copy xq end; |
|
5014 | 116 |
|
117 |
(*map over a sequence xq, append the sequence yq*) |
|
118 |
fun mapp f xq yq = |
|
119 |
let |
|
120 |
fun copy s = |
|
121 |
make (fn () => |
|
122 |
(case pull s of |
|
15531 | 123 |
NONE => pull yq |
124 |
| SOME (x, s') => SOME (f x, copy s'))) |
|
5014 | 125 |
in copy xq end; |
126 |
||
17347 | 127 |
(*interleave elements of xq with those of yq -- fairer than append*) |
128 |
fun interleave (xq, yq) = |
|
129 |
make (fn () => |
|
130 |
(case pull xq of |
|
131 |
NONE => pull yq |
|
132 |
| SOME (x, xq') => SOME (x, interleave (yq, xq')))); |
|
5014 | 133 |
|
134 |
(*filter sequence by predicate*) |
|
135 |
fun filter pred xq = |
|
136 |
let |
|
137 |
fun copy s = |
|
138 |
make (fn () => |
|
139 |
(case pull s of |
|
15531 | 140 |
NONE => NONE |
141 |
| SOME (x, s') => if pred x then SOME (x, copy s') else pull (copy s'))); |
|
5014 | 142 |
in copy xq end; |
143 |
||
144 |
(*flatten a sequence of sequences to a single sequence*) |
|
145 |
fun flat xqq = |
|
146 |
make (fn () => |
|
147 |
(case pull xqq of |
|
15531 | 148 |
NONE => NONE |
149 |
| SOME (xq, xqq') => pull (append (xq, flat xqq')))); |
|
5014 | 150 |
|
17347 | 151 |
(*map the function f over the sequence, making a new sequence*) |
152 |
fun map f xq = |
|
5014 | 153 |
make (fn () => |
154 |
(case pull xq of |
|
17347 | 155 |
NONE => NONE |
156 |
| SOME (x, xq') => SOME (f x, map f xq'))); |
|
157 |
||
158 |
fun maps f = flat o map f; |
|
159 |
||
160 |
fun lift f xq y = map (fn x => f x y) xq; |
|
161 |
fun lifts f xq y = maps (fn x => f x y) xq; |
|
5014 | 162 |
|
16534 | 163 |
(*print a sequence, up to "count" elements*) |
164 |
fun print print_elem count = |
|
5014 | 165 |
let |
16534 | 166 |
fun prnt k xq = |
5014 | 167 |
if k > count then () |
168 |
else |
|
169 |
(case pull xq of |
|
15531 | 170 |
NONE => () |
16534 | 171 |
| SOME (x, xq') => (print_elem k x; writeln ""; prnt (k + 1) xq')); |
172 |
in prnt 1 end; |
|
5014 | 173 |
|
174 |
(*accumulating a function over a sequence; this is lazy*) |
|
175 |
fun it_right f (xq, yq) = |
|
176 |
let |
|
177 |
fun its s = |
|
178 |
make (fn () => |
|
179 |
(case pull s of |
|
15531 | 180 |
NONE => pull yq |
181 |
| SOME (a, s') => pull (f (a, its s')))) |
|
5014 | 182 |
in its xq end; |
183 |
||
6927 | 184 |
(*turn a list of sequences into a sequence of lists*) |
185 |
fun commute [] = single [] |
|
186 |
| commute (xq :: xqs) = |
|
187 |
make (fn () => |
|
188 |
(case pull xq of |
|
15531 | 189 |
NONE => NONE |
190 |
| SOME (x, xq') => |
|
6927 | 191 |
(case pull (commute xqs) of |
15531 | 192 |
NONE => NONE |
193 |
| SOME (xs, xsq) => |
|
194 |
SOME (x :: xs, append (map (Library.cons x) xsq, commute (xq' :: xqs)))))); |
|
6927 | 195 |
|
17347 | 196 |
fun map_list f = commute o List.map f; |
197 |
||
5014 | 198 |
|
199 |
||
12851 | 200 |
(** sequence functions **) (*some code copied from Pure/tctical.ML*) |
5014 | 201 |
|
202 |
fun succeed x = single x; |
|
203 |
fun fail _ = empty; |
|
204 |
||
5864 | 205 |
fun op THEN (f, g) x = flat (map g (f x)); |
5014 | 206 |
|
5864 | 207 |
fun op ORELSE (f, g) x = |
5014 | 208 |
(case pull (f x) of |
15531 | 209 |
NONE => g x |
5014 | 210 |
| some => make (fn () => some)); |
211 |
||
5864 | 212 |
fun op APPEND (f, g) x = |
5014 | 213 |
append (f x, make (fn () => pull (g x))); |
214 |
||
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
215 |
fun EVERY fs = foldr THEN succeed fs; |
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
216 |
fun FIRST fs = foldr ORELSE fail fs; |
5014 | 217 |
|
218 |
fun TRY f = ORELSE (f, succeed); |
|
219 |
||
220 |
fun REPEAT f = |
|
221 |
let |
|
222 |
fun rep qs x = |
|
223 |
(case pull (f x) of |
|
15531 | 224 |
NONE => SOME (x, make (fn () => repq qs)) |
225 |
| SOME (x', q) => rep (q :: qs) x') |
|
226 |
and repq [] = NONE |
|
5014 | 227 |
| repq (q :: qs) = |
228 |
(case pull q of |
|
15531 | 229 |
NONE => repq qs |
230 |
| SOME (x, q) => rep (q :: qs) x); |
|
5014 | 231 |
in fn x => make (fn () => rep [] x) end; |
232 |
||
5558 | 233 |
fun REPEAT1 f = THEN (f, REPEAT f); |
234 |
||
8535 | 235 |
fun INTERVAL f i j x = |
236 |
if i > j then single x |
|
237 |
else op THEN (f j, INTERVAL f i (j - 1)) x; |
|
238 |
||
12851 | 239 |
fun DETERM f x = |
240 |
(case pull (f x) of |
|
15531 | 241 |
NONE => empty |
242 |
| SOME (x', _) => cons (x', empty)); |
|
8535 | 243 |
|
5014 | 244 |
end; |