src/Provers/astar.ML

moved from Contrib

(*  Title: 	astar
    ID:         $Id$
    Author: 	Norbert Voelker, FernUniversitaet Hagen
    Remarks:    Implementation of A*-like proof procedure by modification
		of the existing code for BEST_FIRST and best_tac so that the 
		current level of search is taken into account.
*)		
		
(*Insertion into priority queue of states, marked with level *)
fun insert_with_level (lnth: int*int*thm, []) = [lnth]
  | insert_with_level ((l,m,th), (l',n,th')::nths) = 
      if  n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
      else if  n=m andalso eq_thm(th,th')
              then (l',n,th')::nths
              else (l,m,th)::(l',n,th')::nths;

(*For creating output sequence*)
fun some_of_list []     = None
  | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));

infix THEN_ASTAR;
val trace_ASTAR = ref false; 

fun (Tactic tf0) THEN_ASTAR (satp, costf, tac) = 
  let val tf = tracify trace_ASTAR tac;   
      fun bfs (news,nprfs,level) =
      let fun cost thm = (level,costf level thm,thm)
      in (case  partition satp news  of
            ([],nonsats) 
		 => next (foldr insert_with_level (map cost nonsats, nprfs))
          | (sats,_)  => some_of_list sats)
      end and    
      next []  = None
        | next ((level,n,prf)::nprfs)  =
            (if !trace_ASTAR 
               then writeln("level = " ^ string_of_int level ^
			 "  cost = " ^ string_of_int n ^ 
                         "  queue length =" ^ string_of_int (length nprfs))  
               else ();
             bfs (Sequence.list_of_s (tf prf), nprfs,level+1))
      fun tf st = bfs (Sequence.list_of_s (tf0 st), [], 0)
  in traced_tac tf end;

(*Ordinary ASTAR, with no initial tactic*)
fun ASTAR (satp,costf) tac = all_tac THEN_ASTAR (satp,costf,tac);

(* ASTAR with weight weight_ASTAR as a classical prover *) 
val weight_ASTAR = ref 5; 

fun astar_tac cs = 
  SELECT_GOAL ( ASTAR (has_fewer_prems 1
	      , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
	      (step_tac cs 1));

fun slow_astar_tac cs = 
  SELECT_GOAL ( ASTAR (has_fewer_prems 1
	      , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
	      (slow_step_tac cs 1));