src/Pure/search.ML
changeset 2672 85d7e800d754
parent 2143 093bbe6d333b
child 2869 acee08856cc9
     1.1 --- a/src/Pure/search.ML	Fri Feb 21 15:30:41 1997 +0100
     1.2 +++ b/src/Pure/search.ML	Fri Feb 21 15:31:47 1997 +0100
     1.3 @@ -5,8 +5,13 @@
     1.4  Search tacticals
     1.5  *)
     1.6  
     1.7 +infix 1 THEN_MAYBE THEN_MAYBE';
     1.8 +
     1.9  signature SEARCH =
    1.10    sig
    1.11 +  val THEN_MAYBE	: tactic * tactic -> tactic
    1.12 +  val THEN_MAYBE'	: ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
    1.13 +
    1.14    val trace_DEPTH_FIRST	: bool ref
    1.15    val DEPTH_FIRST	: (thm -> bool) -> tactic -> tactic
    1.16    val DEPTH_SOLVE	: tactic -> tactic
    1.17 @@ -57,6 +62,14 @@
    1.18  (*Apply a tactic if subgoals remain, else do nothing.*)
    1.19  val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
    1.20  
    1.21 +(*Execute tac1, but only execute tac2 if there are at least as many subgoals
    1.22 +  as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
    1.23 +fun tac1 THEN_MAYBE tac2 = STATE
    1.24 +    (fn st => tac1  THEN  
    1.25 +	 COND (has_fewer_prems (nprems_of st)) all_tac tac2);
    1.26 +
    1.27 +fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
    1.28 +
    1.29  (*Tactical to reduce the number of premises by 1.
    1.30    If no subgoals then it must fail! *)
    1.31  fun DEPTH_SOLVE_1 tac = STATE
    1.32 @@ -198,7 +211,7 @@
    1.33  	      ([],[]) => []
    1.34  	    | ([],nonsats) => 
    1.35  		  (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
    1.36 -		   bfs (flat (map tacf nonsats)))
    1.37 +		   bfs (List.concat (map tacf nonsats)))
    1.38  	    | (sats,_)  => sats)
    1.39    in (fn st => Sequence.s_of_list (bfs [st])) end;
    1.40