# HG changeset patch # User wenzelm # Date 1255598583 -7200 # Node ID 51d450f278ce3db532a00da1bd08356098b1263b # Parent 1b5a401c78cb597268ddc1a317b06c3d17e27c0d tuned signature; tuned; diff -r 1b5a401c78cb -r 51d450f278ce src/Pure/search.ML --- a/src/Pure/search.ML Thu Oct 15 11:12:09 2009 +0200 +++ b/src/Pure/search.ML Thu Oct 15 11:23:03 2009 +0200 @@ -7,48 +7,32 @@ infix 1 THEN_MAYBE THEN_MAYBE'; signature SEARCH = - sig - val DEEPEN : int*int -> (int->int->tactic) -> int -> int -> tactic - - val THEN_MAYBE : tactic * tactic -> tactic - val THEN_MAYBE' : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic) - - val trace_DEPTH_FIRST : bool Unsynchronized.ref - val DEPTH_FIRST : (thm -> bool) -> tactic -> tactic - val DEPTH_SOLVE : tactic -> tactic - val DEPTH_SOLVE_1 : tactic -> tactic - val ITER_DEEPEN : (thm->bool) -> (int->tactic) -> tactic - val THEN_ITER_DEEPEN : tactic -> (thm->bool) -> (int->tactic) -> tactic - val iter_deepen_limit : int Unsynchronized.ref - - val has_fewer_prems : int -> thm -> bool - val IF_UNSOLVED : tactic -> tactic - val SOLVE : tactic -> tactic +sig + val trace_DEPTH_FIRST: bool Unsynchronized.ref + val DEPTH_FIRST: (thm -> bool) -> tactic -> tactic + val has_fewer_prems: int -> thm -> bool + val IF_UNSOLVED: tactic -> tactic + val SOLVE: tactic -> tactic val DETERM_UNTIL_SOLVED: tactic -> tactic - val trace_BEST_FIRST : bool Unsynchronized.ref - val BEST_FIRST : (thm -> bool) * (thm -> int) -> tactic -> tactic - val THEN_BEST_FIRST : tactic -> (thm->bool) * (thm->int) -> tactic - -> tactic - val trace_ASTAR : bool Unsynchronized.ref - val ASTAR : (thm -> bool) * (int->thm->int) -> tactic -> tactic - val THEN_ASTAR : tactic -> (thm->bool) * (int->thm->int) -> tactic - -> tactic - val BREADTH_FIRST : (thm -> bool) -> tactic -> tactic - val QUIET_BREADTH_FIRST : (thm -> bool) -> tactic -> tactic - end; + val THEN_MAYBE: tactic * tactic -> tactic + val THEN_MAYBE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic + val DEPTH_SOLVE: tactic -> tactic + val DEPTH_SOLVE_1: tactic -> tactic + val iter_deepen_limit: int Unsynchronized.ref + val THEN_ITER_DEEPEN: tactic -> (thm -> bool) -> (int -> tactic) -> tactic + val ITER_DEEPEN: (thm -> bool) -> (int -> tactic) -> tactic + val DEEPEN: int * int -> (int -> int -> tactic) -> int -> int -> tactic + val trace_BEST_FIRST: bool Unsynchronized.ref + val THEN_BEST_FIRST: tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic + val BEST_FIRST: (thm -> bool) * (thm -> int) -> tactic -> tactic + val BREADTH_FIRST: (thm -> bool) -> tactic -> tactic + val QUIET_BREADTH_FIRST: (thm -> bool) -> tactic -> tactic + val trace_ASTAR: bool Unsynchronized.ref + val THEN_ASTAR: tactic -> (thm -> bool) * (int -> thm -> int) -> tactic -> tactic + val ASTAR: (thm -> bool) * (int -> thm -> int) -> tactic -> tactic +end; - -(** Instantiation of heaps for best-first search **) - -(*total ordering on theorems, allowing duplicates to be found*) -structure ThmHeap = Heap -( - type elem = int * thm; - val ord = prod_ord int_ord (TermOrd.term_ord o pairself Thm.prop_of); -); - - -structure Search : SEARCH = +structure Search: SEARCH = struct (**** Depth-first search ****) @@ -87,7 +71,7 @@ (*Execute tac1, but only execute tac2 if there are at least as many subgoals as before. This ensures that tac2 is only applied to an outcome of tac1.*) fun (tac1 THEN_MAYBE tac2) st = - (tac1 THEN COND (has_fewer_prems (nprems_of st)) all_tac tac2) st; + (tac1 THEN COND (has_fewer_prems (nprems_of st)) all_tac tac2) st; fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x; @@ -200,8 +184,16 @@ tacf m i ORELSE dpn (m+inc))) in dpn m end; + (*** Best-first search ***) +(*total ordering on theorems, allowing duplicates to be found*) +structure Thm_Heap = Heap +( + type elem = int * thm; + val ord = prod_ord int_ord (TermOrd.term_ord o pairself Thm.prop_of); +); + val trace_BEST_FIRST = Unsynchronized.ref false; (*For creating output sequence*) @@ -209,11 +201,11 @@ | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l)); (*Check for and delete duplicate proof states*) -fun deleteAllMin prf heap = - if ThmHeap.is_empty heap then heap - else if Thm.eq_thm (prf, #2 (ThmHeap.min heap)) - then deleteAllMin prf (ThmHeap.delete_min heap) - else heap; +fun delete_all_min prf heap = + if Thm_Heap.is_empty heap then heap + else if Thm.eq_thm (prf, #2 (Thm_Heap.min heap)) + then delete_all_min prf (Thm_Heap.delete_min heap) + else heap; (*Best-first search for a state that satisfies satp (incl initial state) Function sizef estimates size of problem remaining (smaller means better). @@ -223,19 +215,19 @@ fun pairsize th = (sizef th, th); fun bfs (news,nprf_heap) = (case List.partition satp news of - ([],nonsats) => next(fold_rev ThmHeap.insert (map pairsize nonsats) nprf_heap) + ([],nonsats) => next(fold_rev Thm_Heap.insert (map pairsize nonsats) nprf_heap) | (sats,_) => some_of_list sats) and next nprf_heap = - if ThmHeap.is_empty nprf_heap then NONE + if Thm_Heap.is_empty nprf_heap then NONE else - let val (n,prf) = ThmHeap.min nprf_heap + let val (n,prf) = Thm_Heap.min nprf_heap in if !trace_BEST_FIRST then tracing("state size = " ^ string_of_int n) else (); bfs (Seq.list_of (tac prf), - deleteAllMin prf (ThmHeap.delete_min nprf_heap)) + delete_all_min prf (Thm_Heap.delete_min nprf_heap)) end - fun btac st = bfs (Seq.list_of (tac0 st), ThmHeap.empty) + fun btac st = bfs (Seq.list_of (tac0 st), Thm_Heap.empty) in traced_tac btac end; (*Ordinary best-first search, with no initial tactic*)