src/Pure/search.ML
changeset 5693 998af7667fa3
parent 4270 957c887b89b5
child 5754 98744e38ded1
     1.1 --- a/src/Pure/search.ML	Tue Oct 20 16:33:13 1998 +0200
     1.2 +++ b/src/Pure/search.ML	Tue Oct 20 16:33:47 1998 +0200
     1.3 @@ -32,6 +32,7 @@
     1.4    val THEN_ASTAR	: tactic -> (thm->bool) * (int->thm->int) -> tactic
     1.5  			  -> tactic
     1.6    val BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
     1.7 +  val QUIET_BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
     1.8    end;
     1.9  
    1.10  structure Search : SEARCH = 
    1.11 @@ -214,17 +215,20 @@
    1.12  
    1.13  (*Breadth-first search to satisfy satpred (including initial state) 
    1.14    SLOW -- SHOULD NOT USE APPEND!*)
    1.15 -fun BREADTH_FIRST satpred tac = 
    1.16 +fun gen_BREADTH_FIRST message satpred (tac:tactic) = 
    1.17    let val tacf = Seq.list_of o tac;
    1.18        fun bfs prfs =
    1.19  	 (case  partition satpred prfs  of
    1.20  	      ([],[]) => []
    1.21  	    | ([],nonsats) => 
    1.22 -		  (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
    1.23 +		  (message("breadth=" ^ string_of_int(length nonsats) ^ "\n");
    1.24  		   bfs (List.concat (map tacf nonsats)))
    1.25  	    | (sats,_)  => sats)
    1.26    in (fn st => Seq.of_list (bfs [st])) end;
    1.27  
    1.28 +val BREADTH_FIRST = gen_BREADTH_FIRST prs;
    1.29 +val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ());
    1.30 +
    1.31  
    1.32  (*  Author: 	Norbert Voelker, FernUniversitaet Hagen
    1.33      Remarks:    Implementation of A*-like proof procedure by modification