src/Tools/auto_solve.ML
 author wenzelm Tue, 31 Mar 2009 22:23:33 +0200 changeset 30825 14d24e1fe594 parent 30822 8aac4b974280 child 31007 7c871a9cf6f4 permissions -rw-r--r--
fixed header; misc simplification, use Conjunction.dest_conjunctions;
```
(*  Title:      Tools/auto_solve.ML
Author:     Timothy Bourke and Gerwin Klein, NICTA

Check whether a newly stated theorem can be solved directly by an
existing theorem.  Duplicate lemmas can be detected in this way.

The implementation is based in part on Berghofer and Haftmann's
quickcheck.ML.  It relies critically on the FindTheorems solves
feature.
*)

signature AUTO_SOLVE =
sig
val auto : bool ref
val auto_time_limit : int ref
val limit : int ref

val seek_solution : bool -> Proof.state -> Proof.state
end;

structure AutoSolve : AUTO_SOLVE =
struct

val auto = ref false;
val auto_time_limit = ref 2500;
val limit = ref 5;

fun seek_solution int state =
let
val ctxt = Proof.context_of state;

val crits = [(true, FindTheorems.Solves)];
fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);

fun prt_result (goal, results) =
let
val msg =
(case goal of
NONE => "The current goal"
| SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
in
Pretty.big_list
(msg ^ " could be solved directly with:")
(map (FindTheorems.pretty_thm ctxt) results)
end;

fun seek_against_goal () =
(case try Proof.get_goal state of
NONE => NONE
| SOME (_, (_, goal)) =>
let
val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
val rs =
if length subgoals = 1
then [(NONE, find goal)]
else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
val results = filter_out (null o snd) rs;
in if null results then NONE else SOME results end);

fun go () =
let
val res =
TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
(try seek_against_goal) ();
in
(case res of
SOME (SOME results) =>
state |> Proof.goal_message
(fn () => Pretty.chunks
[Pretty.str "",
Pretty.markup Markup.hilite
(separate (Pretty.brk 0) (map prt_result results))])
| _ => state)
end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
in
if int andalso ! auto andalso not (! Toplevel.quiet)
then go ()
else state
end;

end;

val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution);

val auto_solve = AutoSolve.auto;
val auto_solve_time_limit = AutoSolve.auto_time_limit;

```