src/Provers/astar.ML
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 588 91d5ac5ebb17
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     1 (*  Title: 	astar
     2     ID:         $Id$
     3     Author: 	Norbert Voelker, FernUniversitaet Hagen
     4     Remarks:    Implementation of A*-like proof procedure by modification
     5 		of the existing code for BEST_FIRST and best_tac so that the 
     6 		current level of search is taken into account.
     7 *)		
     8 		
     9 (*Insertion into priority queue of states, marked with level *)
    10 fun insert_with_level (lnth: int*int*thm, []) = [lnth]
    11   | insert_with_level ((l,m,th), (l',n,th')::nths) = 
    12       if  n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
    13       else if  n=m andalso eq_thm(th,th')
    14               then (l',n,th')::nths
    15               else (l,m,th)::(l',n,th')::nths;
    16 
    17 (*For creating output sequence*)
    18 fun some_of_list []     = None
    19   | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));
    20 
    21 infix THEN_ASTAR;
    22 val trace_ASTAR = ref false; 
    23 
    24 fun tf0 THEN_ASTAR (satp, costf, tac) = 
    25   let val tf = tracify trace_ASTAR tac;   
    26       fun bfs (news,nprfs,level) =
    27       let fun cost thm = (level,costf level thm,thm)
    28       in (case  partition satp news  of
    29             ([],nonsats) 
    30 		 => next (foldr insert_with_level (map cost nonsats, nprfs))
    31           | (sats,_)  => some_of_list sats)
    32       end and    
    33       next []  = None
    34         | next ((level,n,prf)::nprfs)  =
    35             (if !trace_ASTAR 
    36                then writeln("level = " ^ string_of_int level ^
    37 			 "  cost = " ^ string_of_int n ^ 
    38                          "  queue length =" ^ string_of_int (length nprfs))  
    39                else ();
    40              bfs (Sequence.list_of_s (tf prf), nprfs,level+1))
    41       fun tf st = bfs (Sequence.list_of_s (tf0 st), [], 0)
    42   in traced_tac tf end;
    43 
    44 (*Ordinary ASTAR, with no initial tactic*)
    45 fun ASTAR (satp,costf) tac = all_tac THEN_ASTAR (satp,costf,tac);
    46 
    47 (* ASTAR with weight weight_ASTAR as a classical prover *) 
    48 val weight_ASTAR = ref 5; 
    49 
    50 fun astar_tac cs = 
    51   SELECT_GOAL ( ASTAR (has_fewer_prems 1
    52 	      , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
    53 	      (step_tac cs 1));
    54 
    55 fun slow_astar_tac cs = 
    56   SELECT_GOAL ( ASTAR (has_fewer_prems 1
    57 	      , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
    58 	      (slow_step_tac cs 1));
    59