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.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;
```