author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 23178  07ba6b58b3d2 
child 25955  94a515ed8a39 
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 

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 

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))*) 
19475  73 
fun cons x xq = make (fn () => SOME (x, xq)); 
5014  74 

19475  75 
fun single x = cons x empty; 
5014  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 = 

21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21270
diff
changeset

83 
(case Basics.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*) 

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

93 
(case pull xq of 

15531  94 
NONE => ([], xq) 
21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21270
diff
changeset

95 
 SOME (x, xq') => apfst (Basics.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*) 

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

106 

17347  107 
(*sequence append: put the elements of xq in front of those of yq*) 
19865  108 
fun append xq yq = 
17347  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 
19865  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; 

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

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

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

5014  163 

19912  164 
fun singleton f x = f [x] > map (fn [y] => y  _ => raise Empty); 
165 

166 

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

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

173 
(case pull xq of 

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

5014  177 

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

179 
fun it_right f (xq, yq) = 

180 
let 

181 
fun its s = 

182 
make (fn () => 

183 
(case pull s of 

15531  184 
NONE => pull yq 
185 
 SOME (a, s') => pull (f (a, its s')))) 

5014  186 
in its xq end; 
187 

188 

189 

21270  190 
(** sequence functions **) (*cf. Pure/tctical.ML*) 
5014  191 

192 
fun succeed x = single x; 

193 
fun fail _ = empty; 

194 

21270  195 
fun op THEN (f, g) x = maps g (f x); 
5014  196 

5864  197 
fun op ORELSE (f, g) x = 
5014  198 
(case pull (f x) of 
15531  199 
NONE => g x 
5014  200 
 some => make (fn () => some)); 
201 

5864  202 
fun op APPEND (f, g) x = 
19865  203 
append (f x) (make (fn () => pull (g x))); 
5014  204 

23178  205 
fun EVERY fs = fold_rev (curry op THEN) fs succeed; 
206 
fun FIRST fs = fold_rev (curry op ORELSE) fs fail; 

5014  207 

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

209 

210 
fun REPEAT f = 

211 
let 

212 
fun rep qs x = 

213 
(case pull (f x) of 

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

216 
and repq [] = NONE 

5014  217 
 repq (q :: qs) = 
218 
(case pull q of 

15531  219 
NONE => repq qs 
220 
 SOME (x, q) => rep (q :: qs) x); 

5014  221 
in fn x => make (fn () => rep [] x) end; 
222 

5558  223 
fun REPEAT1 f = THEN (f, REPEAT f); 
224 

8535  225 
fun INTERVAL f i j x = 
226 
if i > j then single x 

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

228 

12851  229 
fun DETERM f x = 
230 
(case pull (f x) of 

15531  231 
NONE => empty 
19475  232 
 SOME (x', _) => cons x' empty); 
8535  233 

5014  234 
end; 