generic DETERM;
authorwenzelm
Sat Jan 26 19:15:51 2002 +0100 (2002-01-26)
changeset 12851e87496286934
parent 12850 d3c16021e999
child 12852 c6a8e310aec5
generic DETERM;
src/Pure/General/seq.ML
src/Pure/tctical.ML
     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;
     2.1 --- a/src/Pure/tctical.ML	Fri Jan 25 15:42:59 2002 +0100
     2.2 +++ b/src/Pure/tctical.ML	Sat Jan 26 19:15:51 2002 +0100
     2.3 @@ -133,11 +133,7 @@
     2.4  
     2.5  
     2.6  (*Make a tactic deterministic by chopping the tail of the proof sequence*)
     2.7 -fun DETERM tac st =  
     2.8 -      case Seq.pull (tac st) of
     2.9 -              None => Seq.empty
    2.10 -            | Some(x,_) => Seq.cons(x, Seq.empty);
    2.11 -
    2.12 +fun DETERM tac = Seq.DETERM tac;
    2.13  
    2.14  (*Conditional tactical: testfun controls which tactic to use next.
    2.15    Beware: due to eager evaluation, both thentac and elsetac are evaluated.*)