summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Pure/General/seq.ML

changeset 5014 | 32e6cab5e7d4 |

child 5558 | 64a8495201d1 |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/seq.ML Wed Jun 10 11:52:59 1998 +0200 @@ -0,0 +1,204 @@ +(* Title: Pure/seq.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + +Unbounded sequences implemented by closures. RECOMPUTES if sequence +is re-inspected. Memoing, using polymorphic refs, was found to be +slower! (More GCs) +*) + +signature SEQ = +sig + type 'a seq + val make: (unit -> ('a * 'a seq) option) -> 'a seq + val pull: 'a seq -> ('a * 'a seq) option + val empty: 'a seq + val cons: 'a * 'a seq -> 'a seq + val single: 'a -> 'a seq + val hd: 'a seq -> 'a + val tl: 'a seq -> 'a seq + val chop: int * 'a seq -> 'a list * 'a seq + val list_of: 'a seq -> 'a list + val of_list: 'a list -> 'a seq + val map: ('a -> 'b) -> 'a seq -> 'b seq + val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq + val append: 'a seq * 'a seq -> 'a seq + val filter: ('a -> bool) -> 'a seq -> 'a seq + val flat: 'a seq seq -> 'a seq + val interleave: 'a seq * 'a seq -> 'a seq + val print: (int -> 'a -> unit) -> int -> 'a seq -> unit + val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq + val succeed: 'a -> 'a seq + val fail: 'a -> 'b seq + val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq + val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq + val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq + val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq + val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq + val TRY: ('a -> 'a seq) -> 'a -> 'a seq + val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq +end; + +structure Seq: SEQ = +struct + + +(** lazy sequences **) + +datatype 'a seq = Seq of unit -> ('a * 'a seq) option; + +(*the abstraction for making a sequence*) +val make = Seq; + +(*return next sequence element as None or Some (x, xq)*) +fun pull (Seq f) = f (); + + +(*the empty sequence*) +val empty = Seq (fn () => None); + +(*prefix an element to the sequence -- use cons (x, xq) only if + evaluation of xq need not be delayed, otherwise use + make (fn () => Some (x, xq))*) +fun cons x_xq = make (fn () => Some x_xq); + +fun single x = cons (x, empty); + +(*head and tail -- beware of calling the sequence function twice!!*) +fun hd xq = #1 (the (pull xq)) +and tl xq = #2 (the (pull xq)); + + +(*the list of the first n elements, paired with rest of sequence; + if length of list is less than n, then sequence had less than n elements*) +fun chop (n, xq) = + if n <= 0 then ([], xq) + else + (case pull xq of + None => ([], xq) + | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq'))); + +(*conversion from sequence to list*) +fun list_of xq = + (case pull xq of + None => [] + | Some (x, xq') => x :: list_of xq'); + +(*conversion from list to sequence*) +fun of_list xs = foldr cons (xs, empty); + + +(*map the function f over the sequence, making a new sequence*) +fun map f xq = + make (fn () => + (case pull xq of + None => None + | Some (x, xq') => Some (f x, map f xq'))); + +(*map over a sequence xq, append the sequence yq*) +fun mapp f xq yq = + let + fun copy s = + make (fn () => + (case pull s of + None => pull yq + | Some (x, s') => Some (f x, copy s'))) + in copy xq end; + +(*sequence append: put the elements of xq in front of those of yq*) +fun append (xq, yq) = + let + fun copy s = + make (fn () => + (case pull s of + None => pull yq + | Some (x, s') => Some (x, copy s'))) + in copy xq end; + +(*filter sequence by predicate*) +fun filter pred xq = + let + fun copy s = + make (fn () => + (case pull s of + None => None + | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s'))); + in copy xq end; + +(*flatten a sequence of sequences to a single sequence*) +fun flat xqq = + make (fn () => + (case pull xqq of + None => None + | Some (xq, xqq') => pull (append (xq, flat xqq')))); + +(*interleave elements of xq with those of yq -- fairer than append*) +fun interleave (xq, yq) = + make (fn () => + (case pull xq of + None => pull yq + | Some (x, xq') => Some (x, interleave (yq, xq')))); + + +(*functional to print a sequence, up to "count" elements; + the function prelem should print the element number and also the element*) +fun print prelem count seq = + let + fun pr (k, xq) = + if k > count then () + else + (case pull xq of + None => () + | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq'))) + in pr (1, seq) end; + +(*accumulating a function over a sequence; this is lazy*) +fun it_right f (xq, yq) = + let + fun its s = + make (fn () => + (case pull s of + None => pull yq + | Some (a, s') => pull (f (a, its s')))) + in its xq end; + + + +(** sequence functions **) (*some code duplicated from Pure/tctical.ML*) + +fun succeed x = single x; +fun fail _ = empty; + + +fun THEN (f, g) x = flat (map g (f x)); + +fun ORELSE (f, g) x = + (case pull (f x) of + None => g x + | some => make (fn () => some)); + +fun APPEND (f, g) x = + append (f x, make (fn () => pull (g x))); + + +fun EVERY fs = foldr THEN (fs, succeed); +fun FIRST fs = foldr ORELSE (fs, fail); + + +fun TRY f = ORELSE (f, succeed); + +fun REPEAT f = + let + fun rep qs x = + (case pull (f x) of + None => Some (x, make (fn () => repq qs)) + | Some (x', q) => rep (q :: qs) x') + and repq [] = None + | repq (q :: qs) = + (case pull q of + None => repq qs + | Some (x, q) => rep (q :: qs) x); + in fn x => make (fn () => rep [] x) end; + + +end;