--- a/src/HOL/HOL.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOL/HOL.thy Thu Oct 28 10:38:29 2010 +0200
@@ -1978,11 +1978,9 @@
*} "solve goal by normalization"
-(*
subsection {* Try *}
setup {* Try.setup *}
-*)
subsection {* Counterexample Search Units *}
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Oct 28 10:38:29 2010 +0200
@@ -95,8 +95,7 @@
else
()
-val default_max_relevant = 300
-val prover_name = ATP_Systems.eN (* arbitrary ATP *)
+val default_prover = ATP_Systems.eN (* arbitrary ATP *)
fun with_index (i, s) = s ^ "@" ^ string_of_int i
@@ -107,11 +106,16 @@
SOME proofs =>
let
val {context = ctxt, facts, goal} = Proof.goal pre
+ val thy = ProofContext.theory_of ctxt
+ val prover = AList.lookup (op =) args "prover"
+ |> the_default default_prover
+ val default_max_relevant =
+ Sledgehammer.default_max_relevant_for_prover thy prover
val irrelevant_consts =
- Sledgehammer.irrelevant_consts_for_prover prover_name
+ Sledgehammer.irrelevant_consts_for_prover prover
val relevance_fudge =
extract_relevance_fudge args
- (Sledgehammer.relevance_fudge_for_prover prover_name)
+ (Sledgehammer.relevance_fudge_for_prover prover)
val relevance_override = {add = [], del = [], only = false}
val {relevance_thresholds, full_types, max_relevant, ...} =
Sledgehammer_Isar.default_params ctxt args
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Oct 28 10:38:29 2010 +0200
@@ -336,8 +336,10 @@
| ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
end
-fun mk_not (Const (@{const_name Not}, _) $ b) = b
- | mk_not b = HOLogic.mk_not b
+fun s_not (@{const Not} $ t) = t
+ | s_not t = HOLogic.mk_not t
+fun simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
+ | simp_not_not t = t
(* Match untyped terms. *)
fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
@@ -351,16 +353,12 @@
| untyped_aconv _ _ = false
(* Finding the relative location of an untyped term within a list of terms *)
-fun literal_index lit =
+fun index_of_literal lit haystack =
let
- val lit = Envir.eta_contract lit
- fun get _ [] = raise Empty
- | get n (x :: xs) =
- if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then
- n
- else
- get (n+1) xs
- in get 1 end
+ val normalize = simp_not_not o Envir.eta_contract
+ val match_lit =
+ HOLogic.dest_Trueprop #> normalize #> untyped_aconv (lit |> normalize)
+ in case find_index match_lit haystack of ~1 => raise Empty | n => n + 1 end
(* Permute a rule's premises to move the i-th premise to the last position. *)
fun make_last i th =
@@ -391,16 +389,19 @@
i_th1
else
let
- val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems)
- (Metis_Term.Fn atm)
+ val i_atm =
+ singleton (hol_terms_from_fol ctxt mode old_skolems)
+ (Metis_Term.Fn atm)
val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
val prems_th1 = prems_of i_th1
val prems_th2 = prems_of i_th2
- val index_th1 = literal_index (mk_not i_atm) prems_th1
- handle Empty => raise Fail "Failed to find literal in th1"
+ val index_th1 =
+ index_of_literal (s_not i_atm) prems_th1
+ handle Empty => raise Fail "Failed to find literal in th1"
val _ = trace_msg ctxt (fn () => " index_th1: " ^ Int.toString index_th1)
- val index_th2 = literal_index i_atm prems_th2
- handle Empty => raise Fail "Failed to find literal in th2"
+ val index_th2 =
+ index_of_literal i_atm prems_th2
+ handle Empty => raise Fail "Failed to find literal in th2"
val _ = trace_msg ctxt (fn () => " index_th2: " ^ Int.toString index_th2)
in
resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Oct 28 10:38:29 2010 +0200
@@ -629,7 +629,7 @@
in
(pprint (Pretty.chunks
[Pretty.blk (0,
- (pstrs ("Nitpick found a" ^
+ (pstrs ((if auto then "Auto " else "") ^ "Nitpick found a" ^
(if not genuine then " potential "
else if genuine_means_genuine then " "
else " quasi genuine ") ^ das_wort_model) @
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Oct 28 10:38:29 2010 +0200
@@ -266,7 +266,7 @@
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
fun proof_banner auto =
- if auto then "Sledgehammer found a proof" else "Try this command"
+ if auto then "Auto Sledgehammer found a proof" else "Try this command"
(* generic TPTP-based ATPs *)
@@ -399,7 +399,7 @@
val (conjecture_shape, fact_names) =
repair_conjecture_shape_and_fact_names output conjecture_shape fact_names
val important_message =
- if random () <= important_message_keep_factor then
+ if not auto andalso random () <= important_message_keep_factor then
extract_important_message output
else
""
@@ -432,7 +432,7 @@
| failure_from_smt_failure SMT_Solver.Out_Of_Memory = OutOfResources
| failure_from_smt_failure _ = UnknownError
-fun run_smt_solver remote ({timeout, ...} : params) minimize_command
+fun run_smt_solver auto remote ({timeout, ...} : params) minimize_command
({state, subgoal, subgoal_count, facts, ...}
: prover_problem) =
let
@@ -443,7 +443,7 @@
val message =
case outcome of
NONE =>
- try_command_line (proof_banner false)
+ try_command_line (proof_banner auto)
(apply_on_subgoal subgoal subgoal_count ^
command_call smtN (map fst used_facts)) ^
minimize_line minimize_command (map fst used_facts)
@@ -458,8 +458,10 @@
end
fun get_prover thy auto name =
- if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix name)
- else run_atp auto name (get_atp thy name)
+ if is_smt_prover name then
+ run_smt_solver auto (String.isPrefix remote_prefix name)
+ else
+ run_atp auto name (get_atp thy name)
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
auto minimize_command
--- a/src/HOL/Tools/try.ML Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOL/Tools/try.ML Thu Oct 28 10:38:29 2010 +0200
@@ -2,33 +2,23 @@
Author: Jasmin Blanchette, TU Muenchen
Try a combination of proof methods.
-
-FIXME: reintroduce or remove commented code (see also HOL.thy)
*)
signature TRY =
sig
-(*
val auto : bool Unsynchronized.ref
-*)
val invoke_try : Time.time option -> Proof.state -> bool
-(*
val setup : theory -> theory
-*)
end;
structure Try : TRY =
struct
-(*
val auto = Unsynchronized.ref false
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
- (Unsynchronized.setmp auto true (fn () =>
- Preferences.bool_pref auto
- "auto-try" "Try standard proof methods.") ());
-*)
+ (Preferences.bool_pref auto "auto-try" "Try standard proof methods.")
val default_timeout = Time.fromSeconds 5
@@ -57,26 +47,37 @@
let val thy = ProofContext.theory_of ctxt in
Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
end
+ handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
-fun do_named_method (name, all_goals) timeout_opt st =
- do_generic timeout_opt
- (name ^ (if all_goals andalso
- nprems_of (#goal (Proof.goal st)) > 1 then
- "[1]"
- else
- "")) I (#goal o Proof.goal)
- (apply_named_method_on_first_goal name (Proof.context_of st)) st
+fun do_named_method (name, (all_goals, run_if_auto)) auto timeout_opt st =
+ if not auto orelse run_if_auto then
+ do_generic timeout_opt
+ (name ^ (if all_goals andalso
+ nprems_of (#goal (Proof.goal st)) > 1 then
+ "[1]"
+ else
+ "")) I (#goal o Proof.goal)
+ (apply_named_method_on_first_goal name (Proof.context_of st)) st
+ else
+ NONE
+(* name * (all_goals, run_if_auto) *)
val named_methods =
- [("simp", false), ("auto", true), ("fast", false), ("fastsimp", false),
- ("force", false), ("blast", false), ("metis", false), ("linarith", false),
- ("presburger", false)]
+ [("simp", (false, true)),
+ ("auto", (true, true)),
+ ("fast", (false, false)),
+ ("fastsimp", (false, false)),
+ ("force", (false, false)),
+ ("blast", (false, true)),
+ ("metis", (false, true)),
+ ("linarith", (false, true)),
+ ("presburger", (false, true))]
val do_methods = map do_named_method named_methods
fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
fun do_try auto timeout_opt st =
- case do_methods |> Par_List.map (fn f => f timeout_opt st)
+ case do_methods |> Par_List.map (fn f => f auto timeout_opt st)
|> map_filter I |> sort (int_ord o pairself snd) of
[] => (if auto then () else writeln "No proof found."; (false, st))
| xs as (s, _) :: _ =>
@@ -88,7 +89,7 @@
Markup.markup Markup.sendback
((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^
" " ^ s) ^
- ".\n(" ^ space_implode "; " (map time_string xs) ^ ")\n"
+ "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
in
(true, st |> (if auto then
Proof.goal_message
@@ -109,10 +110,8 @@
(Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
o Toplevel.proof_of)))
-(*
fun auto_try st = if not (!auto) then (false, st) else do_try true NONE st
val setup = Auto_Tools.register_tool (tryN, auto_try)
-*)
end;
--- a/src/Tools/quickcheck.ML Wed Oct 27 11:11:35 2010 -0700
+++ b/src/Tools/quickcheck.ML Thu Oct 28 10:38:29 2010 +0200
@@ -268,9 +268,11 @@
(* pretty printing *)
-fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample."
- | pretty_counterex ctxt (SOME cex) =
- Pretty.chunks (Pretty.str "Quickcheck found a counterexample:\n" ::
+fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck"
+
+fun pretty_counterex ctxt auto NONE = Pretty.str (tool_name auto ^ " found no counterexample.")
+ | pretty_counterex ctxt auto (SOME cex) =
+ Pretty.chunks (Pretty.str (tool_name auto ^ " found a counterexample:\n") ::
map (fn (s, t) =>
Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
@@ -299,8 +301,9 @@
(rev reports))
| pretty_reports ctxt NONE = Pretty.str ""
-fun pretty_counterex_and_reports ctxt (cex, timing_and_reports) =
- Pretty.chunks (pretty_counterex ctxt cex :: map (pretty_reports ctxt) (map snd timing_and_reports))
+fun pretty_counterex_and_reports ctxt auto (cex, timing_and_reports) =
+ Pretty.chunks (pretty_counterex ctxt auto cex ::
+ map (pretty_reports ctxt) (map snd timing_and_reports))
(* automatic testing *)
@@ -321,7 +324,7 @@
NONE => (false, state)
| SOME (NONE, report) => (false, state)
| SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
- Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state)
+ Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state)
end
val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck)
@@ -398,7 +401,7 @@
fun quickcheck_cmd args i state =
gen_quickcheck args i (Toplevel.proof_of state)
- |> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state);
+ |> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state) false;
val parse_arg = Parse.name -- (Scan.optional (Parse.$$$ "=" |--
((Parse.name >> single) || (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"))) ["true"]);