30980

1 
(* Title: Tools/auto_solve.ML


2 
Author: Timothy Bourke and Gerwin Klein, NICTA


3 


4 
Check whether a newly stated theorem can be solved directly by an


5 
existing theorem. Duplicate lemmas can be detected in this way.


6 


7 
The implementation is based in part on Berghofer and Haftmann's


8 
quickcheck.ML. It relies critically on the FindTheorems solves


9 
feature.


10 
*)


11 


12 
signature AUTO_SOLVE =


13 
sig


14 
val auto : bool ref


15 
val auto_time_limit : int ref


16 
val limit : int ref


17 
end;


18 


19 
structure AutoSolve : AUTO_SOLVE =


20 
struct


21 


22 
(* preferences *)


23 


24 
val auto = ref false;


25 
val auto_time_limit = ref 2500;


26 
val limit = ref 5;


27 


28 
val _ =


29 
ProofGeneralPgip.add_preference Preferences.category_tracing


30 
(setmp auto true (fn () =>


31 
Preferences.bool_pref auto


32 
"autosolve"


33 
"Try to solve newly declared lemmas with existing theorems.") ());


34 


35 
val _ =


36 
ProofGeneralPgip.add_preference Preferences.category_tracing


37 
(Preferences.nat_pref auto_time_limit


38 
"autosolvetimelimit"


39 
"Time limit for seeking automatic solutions (in milliseconds).");


40 


41 


42 
(* hook *)


43 


44 
val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>


45 
let


46 
val ctxt = Proof.context_of state;


47 


48 
val crits = [(true, FindTheorems.Solves)];


49 
fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);


50 


51 
fun prt_result (goal, results) =


52 
let


53 
val msg =


54 
(case goal of


55 
NONE => "The current goal"


56 
 SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));


57 
in


58 
Pretty.big_list


59 
(msg ^ " could be solved directly with:")


60 
(map (FindTheorems.pretty_thm ctxt) results)


61 
end;


62 


63 
fun seek_against_goal () =


64 
(case try Proof.get_goal state of


65 
NONE => NONE


66 
 SOME (_, (_, goal)) =>


67 
let


68 
val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);


69 
val rs =


70 
if length subgoals = 1


71 
then [(NONE, find goal)]


72 
else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;


73 
val results = filter_out (null o snd) rs;


74 
in if null results then NONE else SOME results end);


75 


76 
fun go () =


77 
let


78 
val res =


79 
TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))


80 
(try seek_against_goal) ();


81 
in


82 
(case res of


83 
SOME (SOME results) =>


84 
state > Proof.goal_message


85 
(fn () => Pretty.chunks


86 
[Pretty.str "",


87 
Pretty.markup Markup.hilite


88 
(separate (Pretty.brk 0) (map prt_result results))])


89 
 _ => state)


90 
end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);


91 
in


92 
if int andalso ! auto andalso not (! Toplevel.quiet)


93 
then go ()


94 
else state


95 
end));


96 


97 
end;


98 


99 
val auto_solve = AutoSolve.auto;


100 
val auto_solve_time_limit = AutoSolve.auto_time_limit;


101 
