tuned ThmHeap;
authorwenzelm
Sun Jul 23 12:04:56 2000 +0200 (2000-07-23)
changeset 94110d5a171db2f0
parent 9410 612ee826a409
child 9412 55e8230f5665
tuned ThmHeap;
src/Pure/search.ML
     1.1 --- a/src/Pure/search.ML	Sun Jul 23 12:02:22 2000 +0200
     1.2 +++ b/src/Pure/search.ML	Sun Jul 23 12:04:56 2000 +0200
     1.3 @@ -38,20 +38,13 @@
     1.4    end;
     1.5  
     1.6  
     1.7 -(** Instantiation of leftist heaps for best-first search **)
     1.8 +(** Instantiation of heaps for best-first search **)
     1.9  
    1.10 -(*Termless makes the ordering total, allowing duplicates to be found*)
    1.11 -structure MeasureThm : ORDERED =
    1.12 -struct
    1.13 -  type T = int * thm
    1.14 -  fun eq ((m,th):T, (m',th')) = (m=m' andalso eq_thm(th,th'))
    1.15 -  fun lt ((m,th):T, (m',th')) = 
    1.16 -          (m<m' orelse 
    1.17 -	   m=m' andalso Term.termless (#prop(rep_thm th), #prop(rep_thm th')))
    1.18 -  fun leq (mth, mth') = not (lt (mth',mth))
    1.19 -end;
    1.20 -
    1.21 -structure MeasureThmHeap = LeftistHeap(MeasureThm);
    1.22 +(*total ordering on theorems, allowing duplicates to be found*)
    1.23 +structure ThmHeap =
    1.24 +  HeapFun (type elem = int * thm
    1.25 +    val ord = Library.prod_ord Library.int_ord
    1.26 +      (Term.term_ord o Library.pairself (#prop o Thm.rep_thm)));
    1.27  
    1.28  
    1.29  structure Search : SEARCH = 
    1.30 @@ -207,9 +200,9 @@
    1.31  
    1.32  (*Check for and delete duplicate proof states*)
    1.33  fun deleteAllMin prf heap = 
    1.34 -      if MeasureThmHeap.isEmpty heap then heap
    1.35 -      else if eq_thm (prf, #2 (MeasureThmHeap.findMin heap))
    1.36 -      then deleteAllMin prf (MeasureThmHeap.deleteMin heap)
    1.37 +      if ThmHeap.is_empty heap then heap
    1.38 +      else if eq_thm (prf, #2 (ThmHeap.min heap))
    1.39 +      then deleteAllMin prf (ThmHeap.delete_min heap)
    1.40        else heap;
    1.41  
    1.42  (*Best-first search for a state that satisfies satp (incl initial state)
    1.43 @@ -220,20 +213,20 @@
    1.44        fun pairsize th = (sizef th, th);
    1.45        fun bfs (news,nprf_heap) =
    1.46  	   (case  partition satp news  of
    1.47 -		([],nonsats) => next(foldr MeasureThmHeap.insert
    1.48 +		([],nonsats) => next(foldr ThmHeap.insert
    1.49  					(map pairsize nonsats, nprf_heap)) 
    1.50  	      | (sats,_)  => some_of_list sats)
    1.51        and next nprf_heap =
    1.52 -            if MeasureThmHeap.isEmpty nprf_heap then None
    1.53 +            if ThmHeap.is_empty nprf_heap then None
    1.54  	    else 
    1.55 -	    let val (n,prf) = MeasureThmHeap.findMin nprf_heap
    1.56 +	    let val (n,prf) = ThmHeap.min nprf_heap
    1.57  	    in if !trace_BEST_FIRST 
    1.58  	       then writeln("state size = " ^ string_of_int n)  
    1.59                 else ();
    1.60  	       bfs (Seq.list_of (tac prf), 
    1.61 -		    deleteAllMin prf (MeasureThmHeap.deleteMin nprf_heap))
    1.62 +		    deleteAllMin prf (ThmHeap.delete_min nprf_heap))
    1.63              end
    1.64 -      fun btac st = bfs (Seq.list_of (tac0 st),  MeasureThmHeap.empty)
    1.65 +      fun btac st = bfs (Seq.list_of (tac0 st), ThmHeap.empty)
    1.66    in traced_tac btac end;
    1.67  
    1.68  (*Ordinary best-first search, with no initial tactic*)