src/Pure/search.ML
changeset 3538 ed9de44032e0
parent 2869 acee08856cc9
child 4270 957c887b89b5
     1.1 --- a/src/Pure/search.ML	Tue Jul 22 11:12:55 1997 +0200
     1.2 +++ b/src/Pure/search.ML	Tue Jul 22 11:14:18 1997 +0200
     1.3 @@ -66,19 +66,17 @@
     1.4  
     1.5  (*Execute tac1, but only execute tac2 if there are at least as many subgoals
     1.6    as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
     1.7 -fun tac1 THEN_MAYBE tac2 = STATE
     1.8 -    (fn st => tac1  THEN  
     1.9 -	 COND (has_fewer_prems (nprems_of st)) all_tac tac2);
    1.10 +fun (tac1 THEN_MAYBE tac2) st = 
    1.11 +    (tac1  THEN  COND (has_fewer_prems (nprems_of st)) all_tac tac2)  st;
    1.12  
    1.13  fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
    1.14  
    1.15  (*Tactical to reduce the number of premises by 1.
    1.16    If no subgoals then it must fail! *)
    1.17 -fun DEPTH_SOLVE_1 tac = STATE
    1.18 - (fn st => 
    1.19 +fun DEPTH_SOLVE_1 tac st = st |>
    1.20      (case nprems_of st of
    1.21  	0 => no_tac
    1.22 -      | n => DEPTH_FIRST (has_fewer_prems n) tac));
    1.23 +      | n => DEPTH_FIRST (has_fewer_prems n) tac);
    1.24  
    1.25  (*Uses depth-first search to solve ALL subgoals*)
    1.26  val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1);
    1.27 @@ -166,12 +164,11 @@
    1.28  (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
    1.29    using increment "inc" up to limit "lim". *)
    1.30  fun DEEPEN (inc,lim) tacf m i = 
    1.31 -  let fun dpn m = STATE(fn state => 
    1.32 -			if has_fewer_prems i state then no_tac
    1.33 -			else if m>lim then 
    1.34 -			     (writeln "Giving up..."; no_tac)
    1.35 -			else (writeln ("Depth = " ^ string_of_int m);
    1.36 -			      tacf m i  ORELSE  dpn (m+inc)))
    1.37 +  let fun dpn m st = st |> (if has_fewer_prems i st then no_tac
    1.38 +			    else if m>lim then 
    1.39 +				(writeln "Giving up..."; no_tac)
    1.40 +				 else (writeln ("Depth = " ^ string_of_int m);
    1.41 +				       tacf m i  ORELSE  dpn (m+inc)))
    1.42    in  dpn m  end;
    1.43  
    1.44  (*** Best-first search ***)