diff -r d3c16021e999 -r e87496286934 src/Pure/General/seq.ML --- a/src/Pure/General/seq.ML Fri Jan 25 15:42:59 2002 +0100 +++ b/src/Pure/General/seq.ML Sat Jan 26 19:15:51 2002 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/General/seq.ML ID: \$Id\$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Markus Wenzel, TU Munich + Author: Markus Wenzel, TU Munich License: GPL (GNU GENERAL PUBLIC LICENSE) Unbounded sequences implemented by closures. RECOMPUTES if sequence @@ -43,6 +43,7 @@ val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq + val DETERM: ('a -> 'b seq) -> 'a -> 'b seq end; structure Seq: SEQ = @@ -188,12 +189,11 @@ -(** sequence functions **) (*some code duplicated from Pure/tctical.ML*) +(** sequence functions **) (*some code copied from Pure/tctical.ML*) fun succeed x = single x; fun fail _ = empty; - fun op THEN (f, g) x = flat (map g (f x)); fun op ORELSE (f, g) x = @@ -204,11 +204,9 @@ fun op 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 = @@ -226,10 +224,13 @@ fun REPEAT1 f = THEN (f, REPEAT f); - fun INTERVAL f i j x = if i > j then single x else op THEN (f j, INTERVAL f i (j - 1)) x; +fun DETERM f x = + (case pull (f x) of + None => empty + | Some (x', _) => cons (x', empty)); end;