--- a/src/Pure/IsaMakefile Wed Feb 11 14:48:14 2009 +1100
+++ b/src/Pure/IsaMakefile Wed Feb 11 16:03:10 2009 +1100
@@ -85,7 +85,7 @@
pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML \
subgoal.ML tactic.ML tctical.ML term.ML term_ord.ML term_subst.ML \
theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML \
- ../Tools/quickcheck.ML
+ ../Tools/quickcheck.ML ../Tools/auto_solve.ML
@./mk
--- a/src/Pure/Isar/find_theorems.ML Wed Feb 11 14:48:14 2009 +1100
+++ b/src/Pure/Isar/find_theorems.ML Wed Feb 11 16:03:10 2009 +1100
@@ -370,10 +370,6 @@
val lim = the_default (! limit) opt_limit;
val thms = Library.drop (len - lim, matches);
- fun prt_fact (thmref, thm) = Pretty.block
- [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
- ProofContext.pretty_thm ctxt thm];
-
val end_msg = " in " ^
(List.nth (String.tokens Char.isSpace (end_timing start), 3))
^ " secs"
@@ -386,7 +382,7 @@
(if len <= lim then ""
else " (" ^ string_of_int lim ^ " displayed)")
^ end_msg ^ ":"), Pretty.str ""] @
- map prt_fact thms)
+ map Display.pretty_fact thms)
|> Pretty.chunks |> Pretty.writeln
end
--- a/src/Pure/ProofGeneral/ROOT.ML Wed Feb 11 14:48:14 2009 +1100
+++ b/src/Pure/ProofGeneral/ROOT.ML Wed Feb 11 16:03:10 2009 +1100
@@ -17,7 +17,8 @@
(use
|> setmp Proofterm.proofs 1
|> setmp quick_and_dirty true
- |> setmp auto_quickcheck true) "preferences.ML";
+ |> setmp auto_quickcheck true
+ |> setmp auto_solve false) "preferences.ML";
use "pgip_parser.ML";
--- a/src/Pure/ProofGeneral/preferences.ML Wed Feb 11 14:48:14 2009 +1100
+++ b/src/Pure/ProofGeneral/preferences.ML Wed Feb 11 16:03:10 2009 +1100
@@ -151,6 +151,12 @@
nat_pref Quickcheck.auto_time_limit
"auto-quickcheck-time-limit"
"Time limit for automatic quickcheck (in milliseconds).",
+ bool_pref AutoSolve.auto
+ "auto-solve"
+ "Try to solve newly declared lemmas with existing theorems.",
+ nat_pref AutoSolve.auto_time_limit
+ "auto-solve-time-limit"
+ "Time limit for seeking automatic solutions (in milliseconds).",
thm_deps_pref];
val proof_preferences =
--- a/src/Pure/Tools/ROOT.ML Wed Feb 11 14:48:14 2009 +1100
+++ b/src/Pure/Tools/ROOT.ML Wed Feb 11 16:03:10 2009 +1100
@@ -9,5 +9,6 @@
(*basic XML support*)
use "xml_syntax.ML";
-(*quickcheck needed here because of pg preferences*)
-use "../../Tools/quickcheck.ML"
+(*quickcheck/autosolve needed here because of pg preferences*)
+use "../../Tools/quickcheck.ML";
+use "../../Tools/auto_solve.ML";
--- a/src/Pure/display.ML Wed Feb 11 14:48:14 2009 +1100
+++ b/src/Pure/display.ML Wed Feb 11 16:03:10 2009 +1100
@@ -20,6 +20,7 @@
val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
val pretty_thm: thm -> Pretty.T
val string_of_thm: thm -> string
+ val pretty_fact: Facts.ref * thm -> Pretty.T
val pretty_thms: thm list -> Pretty.T
val pretty_thm_sg: theory -> thm -> Pretty.T
val pretty_thms_sg: theory -> thm list -> Pretty.T
@@ -92,6 +93,10 @@
val string_of_thm = Pretty.string_of o pretty_thm;
+fun pretty_fact (thmref, thm) = Pretty.block
+ [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
+ pretty_thm thm];
+
fun pretty_thms [th] = pretty_thm th
| pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/auto_solve.ML Wed Feb 11 16:03:10 2009 +1100
@@ -0,0 +1,93 @@
+(* Title: 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 implemenation is based in part on Berghofer and
+ Haftmann's Pure/codegen.ML. It relies critically on
+ the FindTheorems solves feature.
+*)
+
+signature AUTO_SOLVE =
+sig
+ val auto : bool ref;
+ val auto_time_limit : int ref;
+
+ val seek_solution : bool -> Proof.state -> Proof.state;
+end;
+
+structure AutoSolve : AUTO_SOLVE =
+struct
+ structure FT = FindTheorems;
+
+ val auto = ref false;
+ val auto_time_limit = ref 5000;
+
+ fun seek_solution int state = 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, FT.Solves)];
+ fun find g = (NONE, FT.find_theorems ctxt g true crits);
+ fun find_cterm g = (SOME g, FT.find_theorems ctxt
+ (SOME (Goal.init g)) true crits);
+
+ fun prt_result (goal, results) = let
+ val msg = case goal of
+ NONE => "The current goal"
+ | SOME g => Syntax.string_of_term ctxt (term_of g);
+ in
+ Pretty.big_list (msg ^ " could be solved directly with:")
+ (map Display.pretty_fact results)
+ 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 frs = filter_out (null o snd) rs;
+
+ in if null frs then NONE else SOME frs end;
+
+ fun go () = let
+ val res = TimeLimit.timeLimit
+ (Time.fromMilliseconds (!auto_time_limit))
+ (try seek_against_goal) ();
+ in
+ case Option.join res of
+ NONE => state
+ | SOME results => (Proof.goal_message
+ (fn () => Pretty.chunks [Pretty.str "",
+ Pretty.markup Markup.hilite
+ (Library.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;
+