--- 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;
--- a/src/Pure/tctical.ML Fri Jan 25 15:42:59 2002 +0100
+++ b/src/Pure/tctical.ML Sat Jan 26 19:15:51 2002 +0100
@@ -133,11 +133,7 @@
(*Make a tactic deterministic by chopping the tail of the proof sequence*)
-fun DETERM tac st =
- case Seq.pull (tac st) of
- None => Seq.empty
- | Some(x,_) => Seq.cons(x, Seq.empty);
-
+fun DETERM tac = Seq.DETERM tac;
(*Conditional tactical: testfun controls which tactic to use next.
Beware: due to eager evaluation, both thentac and elsetac are evaluated.*)