author | wenzelm |
Mon, 06 Oct 1997 18:22:22 +0200 | |
changeset 3776 | 38f8ec304b95 |
parent 1501 | bb7f99a0a6f0 |
permissions | -rw-r--r-- |
1460 | 1 |
(* Title: sequence |
0 | 2 |
ID: $Id$ |
1460 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1988 University of Cambridge |
720
e6cf828a0c67
Pure/sequence: added comment explaining that memoing sequences were found
lcp
parents:
669
diff
changeset
|
5 |
|
e6cf828a0c67
Pure/sequence: added comment explaining that memoing sequences were found
lcp
parents:
669
diff
changeset
|
6 |
Unbounded sequences implemented by closures. |
0 | 7 |
|
720
e6cf828a0c67
Pure/sequence: added comment explaining that memoing sequences were found
lcp
parents:
669
diff
changeset
|
8 |
RECOMPUTES if sequence is re-inspected. |
0 | 9 |
|
720
e6cf828a0c67
Pure/sequence: added comment explaining that memoing sequences were found
lcp
parents:
669
diff
changeset
|
10 |
Memoing, using polymorphic refs, was found to be slower! (More GCs) |
0 | 11 |
*) |
12 |
||
13 |
||
14 |
signature SEQUENCE = |
|
15 |
sig |
|
16 |
type 'a seq |
|
1460 | 17 |
val append : 'a seq * 'a seq -> 'a seq |
18 |
val chop : int * 'a seq -> 'a list * 'a seq |
|
19 |
val cons : 'a * 'a seq -> 'a seq |
|
20 |
val filters : ('a -> bool) -> 'a seq -> 'a seq |
|
21 |
val flats : 'a seq seq -> 'a seq |
|
22 |
val hd : 'a seq -> 'a |
|
669 | 23 |
val interleave: 'a seq * 'a seq -> 'a seq |
1460 | 24 |
val its_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq |
25 |
val list_of_s : 'a seq -> 'a list |
|
26 |
val mapp : ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq |
|
27 |
val maps : ('a -> 'b) -> 'a seq -> 'b seq |
|
28 |
val null : 'a seq |
|
29 |
val prints : (int -> 'a -> unit) -> int -> 'a seq -> unit |
|
30 |
val pull : 'a seq -> ('a * 'a seq) option |
|
31 |
val s_of_list : 'a list -> 'a seq |
|
32 |
val seqof : (unit -> ('a * 'a seq) option) -> 'a seq |
|
33 |
val single : 'a -> 'a seq |
|
34 |
val tl : 'a seq -> 'a seq |
|
0 | 35 |
end; |
36 |
||
37 |
||
1501 | 38 |
structure Sequence : SEQUENCE = |
0 | 39 |
struct |
40 |
||
41 |
datatype 'a seq = Seq of unit -> ('a * 'a seq)option; |
|
42 |
||
43 |
(*Return next sequence element as None or Some(x,str) *) |
|
44 |
fun pull(Seq f) = f(); |
|
45 |
||
669 | 46 |
(*Head and tail. Beware of calling the sequence function twice!!*) |
47 |
fun hd s = #1 (the (pull s)) |
|
48 |
and tl s = #2 (the (pull s)); |
|
49 |
||
0 | 50 |
(*the abstraction for making a sequence*) |
51 |
val seqof = Seq; |
|
52 |
||
53 |
(*prefix an element to the sequence |
|
54 |
use cons(x,s) only if evaluation of s need not be delayed, |
|
55 |
otherwise use seqof(fn()=> Some(x,s)) *) |
|
56 |
fun cons all = Seq(fn()=>Some all); |
|
57 |
||
58 |
(*the empty sequence*) |
|
59 |
val null = Seq(fn()=>None); |
|
60 |
||
61 |
fun single(x) = cons (x, null); |
|
62 |
||
63 |
(*The list of the first n elements, paired with rest of sequence. |
|
64 |
If length of list is less than n, then sequence had less than n elements.*) |
|
65 |
fun chop (n:int, s: 'a seq): 'a list * 'a seq = |
|
66 |
if n<=0 then ([],s) |
|
67 |
else case pull(s) of |
|
68 |
None => ([],s) |
|
69 |
| Some(x,s') => let val (xs,s'') = chop (n-1,s') |
|
1460 | 70 |
in (x::xs, s'') end; |
0 | 71 |
|
72 |
(*conversion from sequence to list*) |
|
73 |
fun list_of_s (s: 'a seq) : 'a list = case pull(s) of |
|
74 |
None => [] |
|
75 |
| Some(x,s') => x :: list_of_s s'; |
|
76 |
||
77 |
||
78 |
(*conversion from list to sequence*) |
|
79 |
fun s_of_list [] = null |
|
80 |
| s_of_list (x::l) = cons (x, s_of_list l); |
|
81 |
||
82 |
||
83 |
(*functional to print a sequence, up to "count" elements |
|
84 |
the function prelem should print the element number and also the element*) |
|
85 |
fun prints (prelem: int -> 'a -> unit) count (s: 'a seq) : unit = |
|
86 |
let fun pr (k,s) = |
|
1460 | 87 |
if k>count then () |
88 |
else case pull(s) of |
|
89 |
None => () |
|
90 |
| Some(x,s') => (prelem k x; prs"\n"; pr (k+1, s')) |
|
0 | 91 |
in pr(1,s) end; |
92 |
||
93 |
(*Map the function f over the sequence, making a new sequence*) |
|
94 |
fun maps f xq = seqof (fn()=> case pull(xq) of |
|
95 |
None => None |
|
96 |
| Some(x,yq) => Some(f x, maps f yq)); |
|
97 |
||
98 |
(*Sequence append: put the elements of xq in front of those of yq*) |
|
99 |
fun append (xq,yq) = |
|
100 |
let fun copy xq = seqof (fn()=> |
|
1460 | 101 |
case pull xq of |
102 |
None => pull yq |
|
103 |
| Some(x,xq') => Some (x, copy xq')) |
|
0 | 104 |
in copy xq end; |
105 |
||
106 |
(*Interleave elements of xq with those of yq -- fairer than append*) |
|
107 |
fun interleave (xq,yq) = seqof (fn()=> |
|
108 |
case pull(xq) of |
|
109 |
None => pull yq |
|
1460 | 110 |
| Some(x,xq') => Some (x, interleave(yq, xq'))); |
0 | 111 |
|
112 |
(*map over a sequence xq, append the sequence yq*) |
|
113 |
fun mapp f xq yq = |
|
114 |
let fun copy s = seqof (fn()=> |
|
115 |
case pull(s) of |
|
1460 | 116 |
None => pull(yq) |
0 | 117 |
| Some(x,xq') => Some(f x, copy xq')) |
118 |
in copy xq end; |
|
119 |
||
120 |
(*Flatten a sequence of sequences to a single sequence. *) |
|
121 |
fun flats ss = seqof (fn()=> case pull(ss) of |
|
122 |
None => None |
|
123 |
| Some(s,ss') => pull(append(s, flats ss'))); |
|
124 |
||
125 |
(*accumulating a function over a sequence; this is lazy*) |
|
126 |
fun its_right (f: 'a * 'b seq -> 'b seq) (s: 'a seq, bstr: 'b seq) : 'b seq = |
|
127 |
let fun its s = seqof (fn()=> |
|
128 |
case pull(s) of |
|
1460 | 129 |
None => pull bstr |
130 |
| Some(a,s') => pull(f(a, its s'))) |
|
0 | 131 |
in its s end; |
132 |
||
133 |
fun filters pred xq = |
|
134 |
let fun copy s = seqof (fn()=> |
|
135 |
case pull(s) of |
|
1460 | 136 |
None => None |
0 | 137 |
| Some(x,xq') => if pred x then Some(x, copy xq') |
1460 | 138 |
else pull (copy xq') ) |
0 | 139 |
in copy xq end |
140 |
||
141 |
end; |