wenzelm@6118: (* Title: Pure/General/seq.ML wenzelm@5014: ID: $Id$ wenzelm@5014: Author: Lawrence C Paulson, Cambridge University Computer Laboratory wenzelm@12851: Author: Markus Wenzel, TU Munich wenzelm@5014: wenzelm@5014: Unbounded sequences implemented by closures. RECOMPUTES if sequence wenzelm@5014: is re-inspected. Memoing, using polymorphic refs, was found to be wenzelm@5014: slower! (More GCs) wenzelm@5014: *) wenzelm@5014: wenzelm@5014: signature SEQ = wenzelm@5014: sig wenzelm@5014: type 'a seq wenzelm@5014: val make: (unit -> ('a * 'a seq) option) -> 'a seq wenzelm@5014: val pull: 'a seq -> ('a * 'a seq) option wenzelm@5014: val empty: 'a seq wenzelm@19475: val cons: 'a -> 'a seq -> 'a seq wenzelm@5014: val single: 'a -> 'a seq wenzelm@11721: val try: ('a -> 'b) -> 'a -> 'b seq wenzelm@5014: val hd: 'a seq -> 'a wenzelm@5014: val tl: 'a seq -> 'a seq wenzelm@19865: val chop: int -> 'a seq -> 'a list * 'a seq wenzelm@5014: val list_of: 'a seq -> 'a list wenzelm@5014: val of_list: 'a list -> 'a seq wenzelm@19865: val append: 'a seq -> 'a seq -> 'a seq wenzelm@5014: val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq wenzelm@17347: val interleave: 'a seq * 'a seq -> 'a seq wenzelm@5014: val filter: ('a -> bool) -> 'a seq -> 'a seq wenzelm@5014: val flat: 'a seq seq -> 'a seq wenzelm@17347: val map: ('a -> 'b) -> 'a seq -> 'b seq wenzelm@17347: val maps: ('a -> 'b seq) -> 'a seq -> 'b seq wenzelm@19484: val map_filter: ('a -> 'b option) -> 'a seq -> 'b seq wenzelm@17347: val lift: ('a -> 'b -> 'c) -> 'a seq -> 'b -> 'c seq wenzelm@17347: val lifts: ('a -> 'b -> 'c seq) -> 'a seq -> 'b -> 'c seq wenzelm@19912: val singleton: ('a list -> 'b list seq) -> 'a -> 'b seq wenzelm@5014: val print: (int -> 'a -> unit) -> int -> 'a seq -> unit wenzelm@5014: val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq wenzelm@5014: val succeed: 'a -> 'a seq wenzelm@5014: val fail: 'a -> 'b seq wenzelm@5014: val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq wenzelm@5014: val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq wenzelm@5014: val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq wenzelm@5014: val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq wenzelm@5014: val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq wenzelm@5014: val TRY: ('a -> 'a seq) -> 'a -> 'a seq wenzelm@5014: val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq wenzelm@5558: val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq wenzelm@8535: val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq wenzelm@12851: val DETERM: ('a -> 'b seq) -> 'a -> 'b seq wenzelm@5014: end; wenzelm@5014: wenzelm@5014: structure Seq: SEQ = wenzelm@5014: struct wenzelm@5014: wenzelm@5014: wenzelm@5014: (** lazy sequences **) wenzelm@5014: wenzelm@5014: datatype 'a seq = Seq of unit -> ('a * 'a seq) option; wenzelm@5014: wenzelm@5014: (*the abstraction for making a sequence*) wenzelm@5014: val make = Seq; wenzelm@5014: skalberg@15531: (*return next sequence element as NONE or SOME (x, xq)*) wenzelm@5014: fun pull (Seq f) = f (); wenzelm@5014: wenzelm@5014: wenzelm@5014: (*the empty sequence*) skalberg@15531: val empty = Seq (fn () => NONE); wenzelm@5014: wenzelm@5014: (*prefix an element to the sequence -- use cons (x, xq) only if wenzelm@5014: evaluation of xq need not be delayed, otherwise use skalberg@15531: make (fn () => SOME (x, xq))*) wenzelm@19475: fun cons x xq = make (fn () => SOME (x, xq)); wenzelm@5014: wenzelm@19475: fun single x = cons x empty; wenzelm@5014: wenzelm@5014: (*head and tail -- beware of calling the sequence function twice!!*) wenzelm@16002: fun hd xq = #1 (the (pull xq)) wenzelm@16002: and tl xq = #2 (the (pull xq)); wenzelm@5014: wenzelm@11721: (*partial function as procedure*) wenzelm@11721: fun try f x = wenzelm@21395: (case Basics.try f x of skalberg@15531: SOME y => single y skalberg@15531: | NONE => empty); wenzelm@11721: wenzelm@5014: wenzelm@5014: (*the list of the first n elements, paired with rest of sequence; wenzelm@5014: if length of list is less than n, then sequence had less than n elements*) wenzelm@19865: fun chop n xq = wenzelm@5014: if n <= 0 then ([], xq) wenzelm@5014: else wenzelm@5014: (case pull xq of skalberg@15531: NONE => ([], xq) wenzelm@21395: | SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1) xq')); wenzelm@5014: wenzelm@5014: (*conversion from sequence to list*) wenzelm@5014: fun list_of xq = wenzelm@5014: (case pull xq of skalberg@15531: NONE => [] skalberg@15531: | SOME (x, xq') => x :: list_of xq'); wenzelm@5014: wenzelm@5014: (*conversion from list to sequence*) wenzelm@19475: fun of_list xs = fold_rev cons xs empty; wenzelm@5014: wenzelm@5014: wenzelm@17347: (*sequence append: put the elements of xq in front of those of yq*) wenzelm@19865: fun append xq yq = wenzelm@17347: let wenzelm@17347: fun copy s = wenzelm@17347: make (fn () => wenzelm@17347: (case pull s of wenzelm@17347: NONE => pull yq wenzelm@17347: | SOME (x, s') => SOME (x, copy s'))) wenzelm@17347: in copy xq end; wenzelm@5014: wenzelm@5014: (*map over a sequence xq, append the sequence yq*) wenzelm@5014: fun mapp f xq yq = wenzelm@5014: let wenzelm@5014: fun copy s = wenzelm@5014: make (fn () => wenzelm@5014: (case pull s of skalberg@15531: NONE => pull yq skalberg@15531: | SOME (x, s') => SOME (f x, copy s'))) wenzelm@5014: in copy xq end; wenzelm@5014: wenzelm@17347: (*interleave elements of xq with those of yq -- fairer than append*) wenzelm@17347: fun interleave (xq, yq) = wenzelm@17347: make (fn () => wenzelm@17347: (case pull xq of wenzelm@17347: NONE => pull yq wenzelm@17347: | SOME (x, xq') => SOME (x, interleave (yq, xq')))); wenzelm@5014: wenzelm@5014: (*filter sequence by predicate*) wenzelm@5014: fun filter pred xq = wenzelm@5014: let wenzelm@5014: fun copy s = wenzelm@5014: make (fn () => wenzelm@5014: (case pull s of skalberg@15531: NONE => NONE skalberg@15531: | SOME (x, s') => if pred x then SOME (x, copy s') else pull (copy s'))); wenzelm@5014: in copy xq end; wenzelm@5014: wenzelm@5014: (*flatten a sequence of sequences to a single sequence*) wenzelm@5014: fun flat xqq = wenzelm@5014: make (fn () => wenzelm@5014: (case pull xqq of skalberg@15531: NONE => NONE wenzelm@19865: | SOME (xq, xqq') => pull (append xq (flat xqq')))); wenzelm@5014: wenzelm@17347: (*map the function f over the sequence, making a new sequence*) wenzelm@17347: fun map f xq = wenzelm@5014: make (fn () => wenzelm@5014: (case pull xq of wenzelm@17347: NONE => NONE wenzelm@17347: | SOME (x, xq') => SOME (f x, map f xq'))); wenzelm@17347: wenzelm@17347: fun maps f = flat o map f; wenzelm@19484: fun map_filter f = maps (fn x => (case f x of NONE => empty | SOME y => single y)); wenzelm@17347: wenzelm@17347: fun lift f xq y = map (fn x => f x y) xq; wenzelm@17347: fun lifts f xq y = maps (fn x => f x y) xq; wenzelm@5014: wenzelm@19912: fun singleton f x = f [x] |> map (fn [y] => y | _ => raise Empty); wenzelm@19912: wenzelm@19912: wenzelm@16534: (*print a sequence, up to "count" elements*) wenzelm@16534: fun print print_elem count = wenzelm@5014: let wenzelm@16534: fun prnt k xq = wenzelm@5014: if k > count then () wenzelm@5014: else wenzelm@5014: (case pull xq of skalberg@15531: NONE => () wenzelm@16534: | SOME (x, xq') => (print_elem k x; writeln ""; prnt (k + 1) xq')); wenzelm@16534: in prnt 1 end; wenzelm@5014: wenzelm@5014: (*accumulating a function over a sequence; this is lazy*) wenzelm@5014: fun it_right f (xq, yq) = wenzelm@5014: let wenzelm@5014: fun its s = wenzelm@5014: make (fn () => wenzelm@5014: (case pull s of skalberg@15531: NONE => pull yq skalberg@15531: | SOME (a, s') => pull (f (a, its s')))) wenzelm@5014: in its xq end; wenzelm@5014: wenzelm@5014: wenzelm@5014: wenzelm@21270: (** sequence functions **) (*cf. Pure/tctical.ML*) wenzelm@5014: wenzelm@5014: fun succeed x = single x; wenzelm@5014: fun fail _ = empty; wenzelm@5014: wenzelm@21270: fun op THEN (f, g) x = maps g (f x); wenzelm@5014: wenzelm@5864: fun op ORELSE (f, g) x = wenzelm@5014: (case pull (f x) of skalberg@15531: NONE => g x wenzelm@5014: | some => make (fn () => some)); wenzelm@5014: wenzelm@5864: fun op APPEND (f, g) x = wenzelm@19865: append (f x) (make (fn () => pull (g x))); wenzelm@5014: skalberg@15574: fun EVERY fs = foldr THEN succeed fs; skalberg@15574: fun FIRST fs = foldr ORELSE fail fs; wenzelm@5014: wenzelm@5014: fun TRY f = ORELSE (f, succeed); wenzelm@5014: wenzelm@5014: fun REPEAT f = wenzelm@5014: let wenzelm@5014: fun rep qs x = wenzelm@5014: (case pull (f x) of skalberg@15531: NONE => SOME (x, make (fn () => repq qs)) skalberg@15531: | SOME (x', q) => rep (q :: qs) x') skalberg@15531: and repq [] = NONE wenzelm@5014: | repq (q :: qs) = wenzelm@5014: (case pull q of skalberg@15531: NONE => repq qs skalberg@15531: | SOME (x, q) => rep (q :: qs) x); wenzelm@5014: in fn x => make (fn () => rep [] x) end; wenzelm@5014: wenzelm@5558: fun REPEAT1 f = THEN (f, REPEAT f); wenzelm@5558: wenzelm@8535: fun INTERVAL f i j x = wenzelm@8535: if i > j then single x wenzelm@8535: else op THEN (f j, INTERVAL f i (j - 1)) x; wenzelm@8535: wenzelm@12851: fun DETERM f x = wenzelm@12851: (case pull (f x) of skalberg@15531: NONE => empty wenzelm@19475: | SOME (x', _) => cons x' empty); wenzelm@8535: wenzelm@5014: end;