author | wenzelm |
Tue, 16 Oct 2012 13:06:40 +0200 | |
changeset 49859 | 52da6a736c32 |
parent 47060 | e2741ec9ae36 |
child 49863 | b5fb6e7f8d81 |
permissions | -rw-r--r-- |
6118 | 1 |
(* Title: Pure/General/seq.ML |
5014 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
12851 | 3 |
Author: Markus Wenzel, TU Munich |
5014 | 4 |
|
5 |
Unbounded sequences implemented by closures. RECOMPUTES if sequence |
|
6 |
is re-inspected. Memoing, using polymorphic refs, was found to be |
|
7 |
slower! (More GCs) |
|
8 |
*) |
|
9 |
||
10 |
signature SEQ = |
|
11 |
sig |
|
12 |
type 'a seq |
|
13 |
val make: (unit -> ('a * 'a seq) option) -> 'a seq |
|
14 |
val pull: 'a seq -> ('a * 'a seq) option |
|
15 |
val empty: 'a seq |
|
19475 | 16 |
val cons: 'a -> 'a seq -> 'a seq |
5014 | 17 |
val single: 'a -> 'a seq |
11721 | 18 |
val try: ('a -> 'b) -> 'a -> 'b seq |
5014 | 19 |
val hd: 'a seq -> 'a |
20 |
val tl: 'a seq -> 'a seq |
|
19865 | 21 |
val chop: int -> 'a seq -> 'a list * 'a seq |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29606
diff
changeset
|
22 |
val take: int -> 'a seq -> 'a seq |
5014 | 23 |
val list_of: 'a seq -> 'a list |
24 |
val of_list: 'a list -> 'a seq |
|
19865 | 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 |
|
19484 | 32 |
val map_filter: ('a -> 'b option) -> 'a seq -> 'b seq |
17347 | 33 |
val lift: ('a -> 'b -> 'c) -> 'a seq -> 'b -> 'c seq |
34 |
val lifts: ('a -> 'b -> 'c seq) -> 'a seq -> 'b -> 'c seq |
|
19912 | 35 |
val singleton: ('a list -> 'b list seq) -> 'a -> 'b seq |
5014 | 36 |
val print: (int -> 'a -> unit) -> int -> 'a seq -> unit |
37 |
val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq |
|
49859
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
38 |
datatype 'a result = Result of 'a | Error of unit -> string |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
39 |
val maps_results: ('a -> 'b result seq) -> 'a result seq -> 'b result seq |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
40 |
val maps_result: ('a -> 'b seq) -> 'a result seq -> 'b result seq |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
41 |
val map_result: ('a -> 'b) -> 'a result seq -> 'b result seq |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
42 |
val the_result: string -> 'a result seq -> 'a |
5014 | 43 |
val succeed: 'a -> 'a seq |
44 |
val fail: 'a -> 'b seq |
|
45 |
val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq |
|
46 |
val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq |
|
47 |
val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq |
|
48 |
val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq |
|
49 |
val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq |
|
50 |
val TRY: ('a -> 'a seq) -> 'a -> 'a seq |
|
51 |
val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq |
|
5558 | 52 |
val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq |
8535 | 53 |
val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq |
12851 | 54 |
val DETERM: ('a -> 'b seq) -> 'a -> 'b seq |
5014 | 55 |
end; |
56 |
||
57 |
structure Seq: SEQ = |
|
58 |
struct |
|
59 |
||
60 |
||
61 |
(** lazy sequences **) |
|
62 |
||
63 |
datatype 'a seq = Seq of unit -> ('a * 'a seq) option; |
|
64 |
||
65 |
(*the abstraction for making a sequence*) |
|
66 |
val make = Seq; |
|
67 |
||
15531 | 68 |
(*return next sequence element as NONE or SOME (x, xq)*) |
5014 | 69 |
fun pull (Seq f) = f (); |
70 |
||
71 |
||
72 |
(*the empty sequence*) |
|
15531 | 73 |
val empty = Seq (fn () => NONE); |
5014 | 74 |
|
75 |
(*prefix an element to the sequence -- use cons (x, xq) only if |
|
76 |
evaluation of xq need not be delayed, otherwise use |
|
15531 | 77 |
make (fn () => SOME (x, xq))*) |
19475 | 78 |
fun cons x xq = make (fn () => SOME (x, xq)); |
5014 | 79 |
|
19475 | 80 |
fun single x = cons x empty; |
5014 | 81 |
|
82 |
(*head and tail -- beware of calling the sequence function twice!!*) |
|
16002 | 83 |
fun hd xq = #1 (the (pull xq)) |
84 |
and tl xq = #2 (the (pull xq)); |
|
5014 | 85 |
|
11721 | 86 |
(*partial function as procedure*) |
87 |
fun try f x = |
|
21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21270
diff
changeset
|
88 |
(case Basics.try f x of |
15531 | 89 |
SOME y => single y |
90 |
| NONE => empty); |
|
11721 | 91 |
|
5014 | 92 |
|
93 |
(*the list of the first n elements, paired with rest of sequence; |
|
94 |
if length of list is less than n, then sequence had less than n elements*) |
|
19865 | 95 |
fun chop n xq = |
29897 | 96 |
if n <= (0 : int) then ([], xq) |
5014 | 97 |
else |
98 |
(case pull xq of |
|
15531 | 99 |
NONE => ([], xq) |
21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21270
diff
changeset
|
100 |
| SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1) xq')); |
5014 | 101 |
|
29897 | 102 |
(*truncate the sequence after n elements*) |
103 |
fun take n xq = |
|
104 |
if n <= (0 : int) then empty |
|
105 |
else make (fn () => |
|
106 |
(Option.map o apsnd) (take (n - 1)) (pull xq)); |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29606
diff
changeset
|
107 |
|
5014 | 108 |
(*conversion from sequence to list*) |
109 |
fun list_of xq = |
|
110 |
(case pull xq of |
|
15531 | 111 |
NONE => [] |
112 |
| SOME (x, xq') => x :: list_of xq'); |
|
5014 | 113 |
|
114 |
(*conversion from list to sequence*) |
|
19475 | 115 |
fun of_list xs = fold_rev cons xs empty; |
5014 | 116 |
|
117 |
||
49859
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
118 |
(*sequence append: put the elements of xq in front of those of yq*) |
19865 | 119 |
fun append xq yq = |
17347 | 120 |
let |
121 |
fun copy s = |
|
122 |
make (fn () => |
|
123 |
(case pull s of |
|
124 |
NONE => pull yq |
|
125 |
| SOME (x, s') => SOME (x, copy s'))) |
|
126 |
in copy xq end; |
|
5014 | 127 |
|
128 |
(*map over a sequence xq, append the sequence yq*) |
|
129 |
fun mapp f xq yq = |
|
130 |
let |
|
131 |
fun copy s = |
|
132 |
make (fn () => |
|
133 |
(case pull s of |
|
15531 | 134 |
NONE => pull yq |
135 |
| SOME (x, s') => SOME (f x, copy s'))) |
|
5014 | 136 |
in copy xq end; |
137 |
||
17347 | 138 |
(*interleave elements of xq with those of yq -- fairer than append*) |
139 |
fun interleave (xq, yq) = |
|
140 |
make (fn () => |
|
141 |
(case pull xq of |
|
142 |
NONE => pull yq |
|
143 |
| SOME (x, xq') => SOME (x, interleave (yq, xq')))); |
|
5014 | 144 |
|
145 |
(*filter sequence by predicate*) |
|
146 |
fun filter pred xq = |
|
147 |
let |
|
148 |
fun copy s = |
|
149 |
make (fn () => |
|
150 |
(case pull s of |
|
15531 | 151 |
NONE => NONE |
152 |
| SOME (x, s') => if pred x then SOME (x, copy s') else pull (copy s'))); |
|
5014 | 153 |
in copy xq end; |
154 |
||
155 |
(*flatten a sequence of sequences to a single sequence*) |
|
156 |
fun flat xqq = |
|
157 |
make (fn () => |
|
158 |
(case pull xqq of |
|
15531 | 159 |
NONE => NONE |
19865 | 160 |
| SOME (xq, xqq') => pull (append xq (flat xqq')))); |
5014 | 161 |
|
17347 | 162 |
(*map the function f over the sequence, making a new sequence*) |
163 |
fun map f xq = |
|
5014 | 164 |
make (fn () => |
165 |
(case pull xq of |
|
17347 | 166 |
NONE => NONE |
167 |
| SOME (x, xq') => SOME (f x, map f xq'))); |
|
168 |
||
49859
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
169 |
fun maps f xq = |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
170 |
make (fn () => |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
171 |
(case pull xq of |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
172 |
NONE => NONE |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
173 |
| SOME (x, xq') => pull (append (f x) (maps f xq')))); |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
174 |
|
19484 | 175 |
fun map_filter f = maps (fn x => (case f x of NONE => empty | SOME y => single y)); |
17347 | 176 |
|
177 |
fun lift f xq y = map (fn x => f x y) xq; |
|
178 |
fun lifts f xq y = maps (fn x => f x y) xq; |
|
5014 | 179 |
|
47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
32195
diff
changeset
|
180 |
fun singleton f x = f [x] |> map (fn [y] => y | _ => raise List.Empty); |
19912 | 181 |
|
16534 | 182 |
(*print a sequence, up to "count" elements*) |
183 |
fun print print_elem count = |
|
5014 | 184 |
let |
26887 | 185 |
fun prnt (k: int) xq = |
5014 | 186 |
if k > count then () |
187 |
else |
|
188 |
(case pull xq of |
|
15531 | 189 |
NONE => () |
16534 | 190 |
| SOME (x, xq') => (print_elem k x; writeln ""; prnt (k + 1) xq')); |
191 |
in prnt 1 end; |
|
5014 | 192 |
|
193 |
(*accumulating a function over a sequence; this is lazy*) |
|
194 |
fun it_right f (xq, yq) = |
|
195 |
let |
|
196 |
fun its s = |
|
197 |
make (fn () => |
|
198 |
(case pull s of |
|
15531 | 199 |
NONE => pull yq |
200 |
| SOME (a, s') => pull (f (a, its s')))) |
|
5014 | 201 |
in its xq end; |
202 |
||
203 |
||
49859
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
204 |
(* embedded errors *) |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
205 |
|
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
206 |
datatype 'a result = Result of 'a | Error of unit -> string; |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
207 |
|
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
208 |
fun maps_results f xq = |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
209 |
make (fn () => |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
210 |
(case pull xq of |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
211 |
NONE => NONE |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
212 |
| SOME (Result x, xq') => pull (append (f x) (maps_results f xq')) |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
213 |
| SOME (Error msg, xq') => SOME (Error msg, maps_results f xq'))); |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
214 |
|
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
215 |
fun maps_result f = maps_results (map Result o f); |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
216 |
fun map_result f = maps_result (single o f); |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
217 |
|
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
218 |
(*first result or first error within sequence*) |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
219 |
fun the_result default_msg seq = |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
220 |
let |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
221 |
fun result opt_msg xq = |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
222 |
(case (opt_msg, pull xq) of |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
223 |
(_, SOME (Result x, _)) => x |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
224 |
| (SOME _, SOME (Error _, xq')) => result opt_msg xq' |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
225 |
| (NONE, SOME (Error msg, xq')) => result (SOME msg) xq' |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
226 |
| (SOME msg, NONE) => error (msg ()) |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
227 |
| (NONE, NONE) => error (if default_msg = "" then "Empty result sequence" else default_msg)); |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
228 |
in result NONE seq end; |
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
229 |
|
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
47060
diff
changeset
|
230 |
|
5014 | 231 |
|
32169 | 232 |
(** sequence functions **) (*cf. Pure/tactical.ML*) |
5014 | 233 |
|
234 |
fun succeed x = single x; |
|
235 |
fun fail _ = empty; |
|
236 |
||
21270 | 237 |
fun op THEN (f, g) x = maps g (f x); |
5014 | 238 |
|
5864 | 239 |
fun op ORELSE (f, g) x = |
5014 | 240 |
(case pull (f x) of |
15531 | 241 |
NONE => g x |
5014 | 242 |
| some => make (fn () => some)); |
243 |
||
5864 | 244 |
fun op APPEND (f, g) x = |
19865 | 245 |
append (f x) (make (fn () => pull (g x))); |
5014 | 246 |
|
23178 | 247 |
fun EVERY fs = fold_rev (curry op THEN) fs succeed; |
248 |
fun FIRST fs = fold_rev (curry op ORELSE) fs fail; |
|
5014 | 249 |
|
250 |
fun TRY f = ORELSE (f, succeed); |
|
251 |
||
252 |
fun REPEAT f = |
|
253 |
let |
|
254 |
fun rep qs x = |
|
255 |
(case pull (f x) of |
|
15531 | 256 |
NONE => SOME (x, make (fn () => repq qs)) |
257 |
| SOME (x', q) => rep (q :: qs) x') |
|
258 |
and repq [] = NONE |
|
5014 | 259 |
| repq (q :: qs) = |
260 |
(case pull q of |
|
15531 | 261 |
NONE => repq qs |
262 |
| SOME (x, q) => rep (q :: qs) x); |
|
5014 | 263 |
in fn x => make (fn () => rep [] x) end; |
264 |
||
5558 | 265 |
fun REPEAT1 f = THEN (f, REPEAT f); |
266 |
||
26887 | 267 |
fun INTERVAL f (i: int) j x = |
8535 | 268 |
if i > j then single x |
269 |
else op THEN (f j, INTERVAL f i (j - 1)) x; |
|
270 |
||
12851 | 271 |
fun DETERM f x = |
272 |
(case pull (f x) of |
|
15531 | 273 |
NONE => empty |
19475 | 274 |
| SOME (x', _) => cons x' empty); |
8535 | 275 |
|
5014 | 276 |
end; |