author  wenzelm 
Mon, 12 Jun 2006 21:19:05 +0200  
changeset 19865  8e1cee9e03dc 
parent 19484  89484a62184a 
child 19912  4a3e35fd6e02 
permissions  rwrr 
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 reinspected. 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 

19475  17 
val cons: 'a > 'a seq > 'a seq 
5014  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 

19865  22 
val chop: int > 'a seq > 'a list * '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 

5014  35 
val print: (int > 'a > unit) > int > 'a seq > unit 
36 
val it_right : ('a * 'b seq > 'b seq) > 'a seq * 'b seq > 'b seq 

6927  37 
val commute: 'a seq list > 'a list seq 
17347  38 
val map_list: ('a > 'b seq) > 'a list > 'b list seq 
5014  39 
val succeed: 'a > 'a seq 
40 
val fail: 'a > 'b seq 

41 
val THEN: ('a > 'b seq) * ('b > 'c seq) > 'a > 'c seq 

42 
val ORELSE: ('a > 'b seq) * ('a > 'b seq) > 'a > 'b seq 

43 
val APPEND: ('a > 'b seq) * ('a > 'b seq) > 'a > 'b seq 

44 
val EVERY: ('a > 'a seq) list > 'a > 'a seq 

45 
val FIRST: ('a > 'b seq) list > 'a > 'b seq 

46 
val TRY: ('a > 'a seq) > 'a > 'a seq 

47 
val REPEAT: ('a > 'a seq) > 'a > 'a seq 

5558  48 
val REPEAT1: ('a > 'a seq) > 'a > 'a seq 
8535  49 
val INTERVAL: (int > 'a > 'a seq) > int > int > 'a > 'a seq 
12851  50 
val DETERM: ('a > 'b seq) > 'a > 'b seq 
5014  51 
end; 
52 

53 
structure Seq: SEQ = 

54 
struct 

55 

56 

57 
(** lazy sequences **) 

58 

59 
datatype 'a seq = Seq of unit > ('a * 'a seq) option; 

60 

61 
(*the abstraction for making a sequence*) 

62 
val make = Seq; 

63 

15531  64 
(*return next sequence element as NONE or SOME (x, xq)*) 
5014  65 
fun pull (Seq f) = f (); 
66 

67 

68 
(*the empty sequence*) 

15531  69 
val empty = Seq (fn () => NONE); 
5014  70 

71 
(*prefix an element to the sequence  use cons (x, xq) only if 

72 
evaluation of xq need not be delayed, otherwise use 

15531  73 
make (fn () => SOME (x, xq))*) 
19475  74 
fun cons x xq = make (fn () => SOME (x, xq)); 
5014  75 

19475  76 
fun single x = cons x empty; 
5014  77 

78 
(*head and tail  beware of calling the sequence function twice!!*) 

16002  79 
fun hd xq = #1 (the (pull xq)) 
80 
and tl xq = #2 (the (pull xq)); 

5014  81 

11721  82 
(*partial function as procedure*) 
83 
fun try f x = 

84 
(case Library.try f x of 

15531  85 
SOME y => single y 
86 
 NONE => empty); 

11721  87 

5014  88 

89 
(*the list of the first n elements, paired with rest of sequence; 

90 
if length of list is less than n, then sequence had less than n elements*) 

19865  91 
fun chop n xq = 
5014  92 
if n <= 0 then ([], xq) 
93 
else 

94 
(case pull xq of 

15531  95 
NONE => ([], xq) 
19865  96 
 SOME (x, xq') => apfst (Library.cons x) (chop (n  1) xq')); 
5014  97 

98 
(*conversion from sequence to list*) 

99 
fun list_of xq = 

100 
(case pull xq of 

15531  101 
NONE => [] 
102 
 SOME (x, xq') => x :: list_of xq'); 

5014  103 

104 
(*conversion from list to sequence*) 

19475  105 
fun of_list xs = fold_rev cons xs empty; 
5014  106 

107 

17347  108 
(*sequence append: put the elements of xq in front of those of yq*) 
19865  109 
fun append xq yq = 
17347  110 
let 
111 
fun copy s = 

112 
make (fn () => 

113 
(case pull s of 

114 
NONE => pull yq 

115 
 SOME (x, s') => SOME (x, copy s'))) 

116 
in copy xq end; 

5014  117 

118 
(*map over a sequence xq, append the sequence yq*) 

119 
fun mapp f xq yq = 

120 
let 

121 
fun copy s = 

122 
make (fn () => 

123 
(case pull s of 

15531  124 
NONE => pull yq 
125 
 SOME (x, s') => SOME (f x, copy s'))) 

5014  126 
in copy xq end; 
127 

17347  128 
(*interleave elements of xq with those of yq  fairer than append*) 
129 
fun interleave (xq, yq) = 

130 
make (fn () => 

131 
(case pull xq of 

132 
NONE => pull yq 

133 
 SOME (x, xq') => SOME (x, interleave (yq, xq')))); 

5014  134 

135 
(*filter sequence by predicate*) 

136 
fun filter pred xq = 

137 
let 

138 
fun copy s = 

139 
make (fn () => 

140 
(case pull s of 

15531  141 
NONE => NONE 
142 
 SOME (x, s') => if pred x then SOME (x, copy s') else pull (copy s'))); 

5014  143 
in copy xq end; 
144 

145 
(*flatten a sequence of sequences to a single sequence*) 

146 
fun flat xqq = 

147 
make (fn () => 

148 
(case pull xqq of 

15531  149 
NONE => NONE 
19865  150 
 SOME (xq, xqq') => pull (append xq (flat xqq')))); 
5014  151 

17347  152 
(*map the function f over the sequence, making a new sequence*) 
153 
fun map f xq = 

5014  154 
make (fn () => 
155 
(case pull xq of 

17347  156 
NONE => NONE 
157 
 SOME (x, xq') => SOME (f x, map f xq'))); 

158 

159 
fun maps f = flat o map f; 

19484  160 
fun map_filter f = maps (fn x => (case f x of NONE => empty  SOME y => single y)); 
17347  161 

162 
fun lift f xq y = map (fn x => f x y) xq; 

163 
fun lifts f xq y = maps (fn x => f x y) xq; 

5014  164 

16534  165 
(*print a sequence, up to "count" elements*) 
166 
fun print print_elem count = 

5014  167 
let 
16534  168 
fun prnt k xq = 
5014  169 
if k > count then () 
170 
else 

171 
(case pull xq of 

15531  172 
NONE => () 
16534  173 
 SOME (x, xq') => (print_elem k x; writeln ""; prnt (k + 1) xq')); 
174 
in prnt 1 end; 

5014  175 

176 
(*accumulating a function over a sequence; this is lazy*) 

177 
fun it_right f (xq, yq) = 

178 
let 

179 
fun its s = 

180 
make (fn () => 

181 
(case pull s of 

15531  182 
NONE => pull yq 
183 
 SOME (a, s') => pull (f (a, its s')))) 

5014  184 
in its xq end; 
185 

6927  186 
(*turn a list of sequences into a sequence of lists*) 
187 
fun commute [] = single [] 

188 
 commute (xq :: xqs) = 

189 
make (fn () => 

190 
(case pull xq of 

15531  191 
NONE => NONE 
192 
 SOME (x, xq') => 

6927  193 
(case pull (commute xqs) of 
15531  194 
NONE => NONE 
195 
 SOME (xs, xsq) => 

19865  196 
SOME (x :: xs, append (map (Library.cons x) xsq) (commute (xq' :: xqs)))))); 
6927  197 

17347  198 
fun map_list f = commute o List.map f; 
199 

5014  200 

201 

12851  202 
(** sequence functions **) (*some code copied from Pure/tctical.ML*) 
5014  203 

204 
fun succeed x = single x; 

205 
fun fail _ = empty; 

206 

5864  207 
fun op THEN (f, g) x = flat (map g (f x)); 
5014  208 

5864  209 
fun op ORELSE (f, g) x = 
5014  210 
(case pull (f x) of 
15531  211 
NONE => g x 
5014  212 
 some => make (fn () => some)); 
213 

5864  214 
fun op APPEND (f, g) x = 
19865  215 
append (f x) (make (fn () => pull (g x))); 
5014  216 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

217 
fun EVERY fs = foldr THEN succeed fs; 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

218 
fun FIRST fs = foldr ORELSE fail fs; 
5014  219 

220 
fun TRY f = ORELSE (f, succeed); 

221 

222 
fun REPEAT f = 

223 
let 

224 
fun rep qs x = 

225 
(case pull (f x) of 

15531  226 
NONE => SOME (x, make (fn () => repq qs)) 
227 
 SOME (x', q) => rep (q :: qs) x') 

228 
and repq [] = NONE 

5014  229 
 repq (q :: qs) = 
230 
(case pull q of 

15531  231 
NONE => repq qs 
232 
 SOME (x, q) => rep (q :: qs) x); 

5014  233 
in fn x => make (fn () => rep [] x) end; 
234 

5558  235 
fun REPEAT1 f = THEN (f, REPEAT f); 
236 

8535  237 
fun INTERVAL f i j x = 
238 
if i > j then single x 

239 
else op THEN (f j, INTERVAL f i (j  1)) x; 

240 

12851  241 
fun DETERM f x = 
242 
(case pull (f x) of 

15531  243 
NONE => empty 
19475  244 
 SOME (x', _) => cons x' empty); 
8535  245 

5014  246 
end; 