src/Pure/General/seq.ML
changeset 12851 e87496286934
parent 11721 0d60622b668f
child 14981 e73f8140af78
     1.1 --- a/src/Pure/General/seq.ML	Fri Jan 25 15:42:59 2002 +0100
     1.2 +++ b/src/Pure/General/seq.ML	Sat Jan 26 19:15:51 2002 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/General/seq.ML
     1.5      ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Author:   	Markus Wenzel, TU Munich
     1.8 +    Author:     Markus Wenzel, TU Munich
     1.9      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.10  
    1.11  Unbounded sequences implemented by closures.  RECOMPUTES if sequence
    1.12 @@ -43,6 +43,7 @@
    1.13    val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
    1.14    val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
    1.15    val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
    1.16 +  val DETERM: ('a -> 'b seq) -> 'a -> 'b seq
    1.17  end;
    1.18  
    1.19  structure Seq: SEQ =
    1.20 @@ -188,12 +189,11 @@
    1.21  
    1.22  
    1.23  
    1.24 -(** sequence functions **)      (*some code duplicated from Pure/tctical.ML*)
    1.25 +(** sequence functions **)      (*some code copied from Pure/tctical.ML*)
    1.26  
    1.27  fun succeed x = single x;
    1.28  fun fail _ = empty;
    1.29  
    1.30 -
    1.31  fun op THEN (f, g) x = flat (map g (f x));
    1.32  
    1.33  fun op ORELSE (f, g) x =
    1.34 @@ -204,11 +204,9 @@
    1.35  fun op APPEND (f, g) x =
    1.36    append (f x, make (fn () => pull (g x)));
    1.37  
    1.38 -
    1.39  fun EVERY fs = foldr THEN (fs, succeed);
    1.40  fun FIRST fs = foldr ORELSE (fs, fail);
    1.41  
    1.42 -
    1.43  fun TRY f = ORELSE (f, succeed);
    1.44  
    1.45  fun REPEAT f =
    1.46 @@ -226,10 +224,13 @@
    1.47  
    1.48  fun REPEAT1 f = THEN (f, REPEAT f);
    1.49  
    1.50 -
    1.51  fun INTERVAL f i j x =
    1.52    if i > j then single x
    1.53    else op THEN (f j, INTERVAL f i (j - 1)) x;
    1.54  
    1.55 +fun DETERM f x =
    1.56 +  (case pull (f x) of
    1.57 +    None => empty
    1.58 +  | Some (x', _) => cons (x', empty));
    1.59  
    1.60  end;