diff -r 2e608fa6c404 -r 530e7a33b3dd src/Pure/search.ML --- a/src/Pure/search.ML Tue Jun 20 11:53:35 2000 +0200 +++ b/src/Pure/search.ML Tue Jun 20 11:54:07 2000 +0200 @@ -37,6 +37,23 @@ val QUIET_BREADTH_FIRST : (thm -> bool) -> tactic -> tactic end; + +(** Instantiation of leftist heaps for best-first search **) + +(*Termless makes the ordering total, allowing duplicates to be found*) +structure MeasureThm : ORDERED = +struct + type T = int * thm + fun eq ((m,th):T, (m',th')) = (m=m' andalso eq_thm(th,th')) + fun lt ((m,th):T, (m',th')) = + (m some_of_list l)); +(*Check for and delete duplicate proof states*) +fun deleteAllMin prf heap = + if MeasureThmHeap.isEmpty heap then heap + else if eq_thm (prf, #2 (MeasureThmHeap.findMin heap)) + then deleteAllMin prf (MeasureThmHeap.deleteMin 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). @@ -203,19 +218,22 @@ fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = let val tac = tracify trace_BEST_FIRST tac1 fun pairsize th = (sizef th, th); - fun bfs (news,nprfs) = + fun bfs (news,nprf_heap) = (case partition satp news of - ([],nonsats) => next(foldr insert - (map pairsize nonsats, nprfs)) + ([],nonsats) => next(foldr MeasureThmHeap.insert + (map pairsize nonsats, nprf_heap)) | (sats,_) => some_of_list sats) - and next [] = None - | next ((n,prf)::nprfs) = - (if !trace_BEST_FIRST - then writeln("state size = " ^ string_of_int n ^ - " queue length =" ^ string_of_int (length nprfs)) + and next nprf_heap = + if MeasureThmHeap.isEmpty nprf_heap then None + else + let val (n,prf) = MeasureThmHeap.findMin nprf_heap + in if !trace_BEST_FIRST + then writeln("state size = " ^ string_of_int n) else (); - bfs (Seq.list_of (tac prf), nprfs)) - fun btac st = bfs (Seq.list_of (tac0 st), []) + bfs (Seq.list_of (tac prf), + deleteAllMin prf (MeasureThmHeap.deleteMin nprf_heap)) + end + fun btac st = bfs (Seq.list_of (tac0 st), MeasureThmHeap.empty) in traced_tac btac end; (*Ordinary best-first search, with no initial tactic*)