--- a/src/Tools/auto_solve.ML Tue Mar 31 21:31:23 2009 +0200
+++ b/src/Tools/auto_solve.ML Tue Mar 31 22:23:33 2009 +0200
@@ -1,11 +1,11 @@
-(* Title: Pure/Tools/auto_solve.ML
+(* 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.
+existing theorem. Duplicate lemmas can be detected in this way.
-The implemenation is based in part on Berghofer and Haftmann's
-Pure/codegen.ML. It relies critically on the FindTheorems solves
+The implementation is based in part on Berghofer and Haftmann's
+quickcheck.ML. It relies critically on the FindTheorems solves
feature.
*)
@@ -29,24 +29,15 @@
let
val ctxt = Proof.context_of state;
- fun conj_to_list [] = []
- | conj_to_list (t::ts) =
- (Conjunction.dest_conjunction t
- |> (fn (t1, t2) => conj_to_list (t1::t2::ts)))
- handle TERM _ => t::conj_to_list ts;
-
val crits = [(true, FindTheorems.Solves)];
- fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (! limit)) false crits));
- fun find_cterm g =
- (SOME g, snd (FindTheorems.find_theorems ctxt
- (SOME (Goal.init g)) (SOME (! limit)) false crits));
+ 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 g => Syntax.string_of_term ctxt (Thm.term_of g));
+ | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
in
Pretty.big_list
(msg ^ " could be solved directly with:")
@@ -54,22 +45,17 @@
end;
fun seek_against_goal () =
- let
- val goal = try Proof.get_goal state
- |> Option.map (#2 o #2);
-
- val goals = goal
- |> Option.map (fn g => cprem_of g 1)
- |> the_list
- |> conj_to_list;
-
- val rs =
- if length goals = 1
- then [find goal]
- else map find_cterm goals;
- val results = filter_out (null o snd) rs;
-
- in if null results then NONE else SOME results end;
+ (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
@@ -84,7 +70,7 @@
[Pretty.str "",
Pretty.markup Markup.hilite
(separate (Pretty.brk 0) (map prt_result results))])
- | NONE => state)
+ | _ => state)
end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
in
if int andalso ! auto andalso not (! Toplevel.quiet)