# HG changeset patch # User blanchet # Date 1288255109 -7200 # Node ID dfa0d94991e47fa8ce1a1e3345a3c70b31328d47 # Parent b283680d8044a78c65e5badf1169f6996330e2c6# Parent 2de5dd0cd3a2c55169a03191bc71a4ba36b6582a merged diff -r b283680d8044 -r dfa0d94991e4 src/HOL/HOL.thy --- 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 *} diff -r b283680d8044 -r dfa0d94991e4 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- 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 diff -r b283680d8044 -r dfa0d94991e4 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 diff -r b283680d8044 -r dfa0d94991e4 src/HOL/Tools/Nitpick/nitpick.ML --- 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) @ diff -r b283680d8044 -r dfa0d94991e4 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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 diff -r b283680d8044 -r dfa0d94991e4 src/HOL/Tools/try.ML --- 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; diff -r b283680d8044 -r dfa0d94991e4 src/Tools/quickcheck.ML --- 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"]);