--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Sat Sep 11 10:20:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Sat Sep 11 10:21:52 2010 +0200
@@ -270,7 +270,7 @@
val tvars = gen_TVars (length args)
val tvars_srts = ListPair.zip (tvars, args)
in
- ArityClause {name = name,
+ ArityClause {name = name,
conclLit = TConsLit (`make_type_class cls,
`make_fixed_type_const tcons,
tvars ~~ tvars),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sat Sep 11 10:20:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sat Sep 11 10:21:52 2010 +0200
@@ -28,7 +28,7 @@
timeout: Time.time,
expect: string}
type problem =
- {ctxt: Proof.context,
+ {state: Proof.state,
goal: thm,
subgoal: int,
axioms: (term * ((string * locality) * fol_formula) option) list}
@@ -52,8 +52,8 @@
val messages: int option -> unit
val get_prover_fun : theory -> string -> prover
val run_sledgehammer :
- params -> int -> relevance_override -> (string -> minimize_command)
- -> Proof.state -> unit
+ params -> bool -> int -> relevance_override -> (string -> minimize_command)
+ -> Proof.state -> bool * Proof.state
val setup : theory -> theory
end;
@@ -97,7 +97,7 @@
expect: string}
type problem =
- {ctxt: Proof.context,
+ {state: Proof.state,
goal: thm,
subgoal: int,
axioms: (term * ((string * locality) * fol_formula) option) list}
@@ -230,18 +230,18 @@
(* generic TPTP-based provers *)
-fun prover_fun atp_name
+fun prover_fun auto atp_name
{exec, required_execs, arguments, has_incomplete_mode, proof_delims,
known_failures, default_max_relevant, explicit_forall,
use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
- minimize_command ({ctxt, goal, subgoal, axioms} : problem) =
+ minimize_command ({state, goal, subgoal, axioms} : problem) =
let
+ val ctxt = Proof.context_of state
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
val max_relevant = the_default default_max_relevant max_relevant
val axioms = take max_relevant axioms
- (* path to unique problem file *)
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
else Config.get ctxt dest_dir
val the_problem_prefix = Config.get ctxt problem_prefix
@@ -285,7 +285,7 @@
| [] =>
if File.exists command then
let
- fun do_run complete timeout =
+ fun run complete timeout =
let
val command = command_line complete timeout probfile
val ((output, msecs), res_code) =
@@ -309,17 +309,17 @@
val conjecture_shape =
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
|> map single
+ val run_twice = has_incomplete_mode andalso not auto
val timer = Timer.startRealTimer ()
val result =
- do_run false (if has_incomplete_mode then
- Time.fromMilliseconds
+ run false (if run_twice then
+ Time.fromMilliseconds
(2 * Time.toMilliseconds timeout div 3)
- else
- timeout)
- |> has_incomplete_mode
+ else
+ timeout)
+ |> run_twice
? (fn (_, msecs0, _, SOME _) =>
- do_run true
- (Time.- (timeout, Timer.checkRealTimer timer))
+ run true (Time.- (timeout, Timer.checkRealTimer timer))
|> (fn (output, msecs, proof, outcome) =>
(output, msecs0 + msecs, proof, outcome))
| result => result)
@@ -367,14 +367,15 @@
conjecture_shape = conjecture_shape}
end
-fun get_prover_fun thy name = prover_fun name (get_prover thy name)
+fun get_prover_fun thy name = prover_fun false name (get_prover thy name)
-fun run_prover ctxt (params as {blocking, verbose, max_relevant, timeout,
- expect, ...})
- i n relevance_override minimize_command
- (problem as {goal, axioms, ...})
+fun run_prover (params as {blocking, verbose, max_relevant, timeout, expect,
+ ...})
+ auto i n relevance_override minimize_command
+ (problem as {state, goal, axioms, ...})
(prover as {default_max_relevant, ...}, atp_name) =
let
+ val ctxt = Proof.context_of state
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, timeout)
val max_relevant = the_default default_max_relevant max_relevant
@@ -390,72 +391,94 @@
""
else
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
- fun run () =
+ fun go () =
let
val (outcome_code, message) =
- prover_fun atp_name prover params (minimize_command atp_name) problem
+ prover_fun auto atp_name prover params (minimize_command atp_name)
+ problem
|> (fn {outcome, message, ...} =>
(if is_some outcome then "none" else "some", message))
handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
| exn => ("unknown", "Internal error:\n" ^
ML_Compiler.exn_message exn ^ "\n")
- in
- if expect = "" orelse outcome_code = expect then
- ()
- else if blocking then
- error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
- else
- warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
- message
+ val _ =
+ if expect = "" orelse outcome_code = expect then
+ ()
+ else if blocking then
+ error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
+ else
+ warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
+ in (outcome_code = "some", message) end
+ in
+ if auto then
+ let val (success, message) = TimeLimit.timeLimit timeout go () in
+ (success, state |> success ? Proof.goal_message (fn () =>
+ Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite
+ (Pretty.str ("Sledgehammer found a proof! " ^ message))]))
end
- in
- if blocking then priority (desc ^ "\n" ^ TimeLimit.timeLimit timeout run ())
- else Async_Manager.launch das_Tool birth_time death_time desc run
+ else if blocking then
+ let val (success, message) = TimeLimit.timeLimit timeout go () in
+ priority (desc ^ "\n" ^ message); (success, state)
+ end
+ else
+ (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
+ (false, state))
end
+val auto_max_relevant_divisor = 2
+
fun run_sledgehammer (params as {blocking, verbose, atps, full_types,
relevance_thresholds, max_relevant, ...})
- i relevance_override minimize_command state =
- if null atps then error "No ATP is set."
- else case subgoal_count state of
- 0 => priority "No subgoal!"
- | n =>
- let
- val thy = Proof.theory_of state
- val timer = Timer.startRealTimer ()
- val _ = () |> not blocking ? kill_atps
- val _ = priority "Sledgehammering..."
- val provers = map (`(get_prover thy)) atps
- fun run () =
- let
- val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
- val (_, hyp_ts, concl_t) = strip_subgoal goal i
- val max_max_relevant =
- case max_relevant of
- SOME n => n
- | NONE => fold (Integer.max o #default_max_relevant o fst)
- provers 0
- val axioms =
- relevant_facts ctxt full_types relevance_thresholds
- max_max_relevant relevance_override chained_ths
- hyp_ts concl_t
- val problem =
- {ctxt = ctxt, goal = goal, subgoal = i,
- axioms = map (prepare_axiom ctxt) axioms}
- val num_axioms = length axioms
- val _ =
- (if blocking then Par_List.map else map)
- (run_prover ctxt params i n relevance_override
- minimize_command problem) provers
- in
- if verbose andalso blocking then
- priority ("Total time: " ^
- signed_string_of_int (Time.toMilliseconds
- (Timer.checkRealTimer timer)) ^ " ms.")
- else
- ()
- end
- in if blocking then run () else Future.fork run |> K () end
+ auto i relevance_override minimize_command state =
+ if null atps then
+ error "No ATP is set."
+ else case subgoal_count state of
+ 0 => (priority "No subgoal!"; (false, state))
+ | n =>
+ let
+ val thy = Proof.theory_of state
+ val timer = Timer.startRealTimer ()
+ val _ = () |> not blocking ? kill_atps
+ val _ = if auto then () else priority "Sledgehammering..."
+ val provers = map (`(get_prover thy)) atps
+ fun go () =
+ let
+ val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
+ val (_, hyp_ts, concl_t) = strip_subgoal goal i
+ val max_max_relevant =
+ case max_relevant of
+ SOME n => n
+ | NONE =>
+ 0 |> fold (Integer.max o #default_max_relevant o fst) provers
+ |> auto ? (fn n => n div auto_max_relevant_divisor)
+ val axioms =
+ relevant_facts ctxt full_types relevance_thresholds
+ max_max_relevant relevance_override chained_ths
+ hyp_ts concl_t
+ val problem =
+ {state = state, goal = goal, subgoal = i,
+ axioms = map (prepare_axiom ctxt) axioms}
+ val run_prover =
+ run_prover params auto i n relevance_override minimize_command
+ problem
+ val num_axioms = length axioms
+ in
+ if auto then
+ fold (fn prover => fn (true, state) => (true, state)
+ | (false, _) => run_prover prover)
+ provers (false, state)
+ else
+ (if blocking then Par_List.map else map) run_prover provers
+ |> tap (fn _ =>
+ if verbose then
+ priority ("Total time: " ^
+ signed_string_of_int (Time.toMilliseconds
+ (Timer.checkRealTimer timer)) ^ " ms.")
+ else
+ ())
+ |> exists fst |> rpair state
+ end
+ in if blocking then go () else Future.fork (tap go) |> K (false, state) end
val setup =
dest_dir_setup
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Sep 11 10:20:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Sep 11 10:21:52 2010 +0200
@@ -8,10 +8,12 @@
sig
type params = Sledgehammer.params
- val atps: string Unsynchronized.ref
- val timeout: int Unsynchronized.ref
- val full_types: bool Unsynchronized.ref
+ val auto : bool Unsynchronized.ref
+ val atps : string Unsynchronized.ref
+ val timeout : int Unsynchronized.ref
+ val full_types : bool Unsynchronized.ref
val default_params : theory -> (string * string) list -> params
+ val setup : theory -> theory
end;
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
@@ -22,11 +24,19 @@
open Sledgehammer
open Sledgehammer_Minimize
+val auto = Unsynchronized.ref false
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_tracing
+ (Preferences.bool_pref auto "auto-sledgehammer"
+ "Whether to run Sledgehammer automatically.")
+
(** Sledgehammer commands **)
-fun add_to_relevance_override ns : relevance_override =
+val no_relevance_override = {add = [], del = [], only = false}
+fun add_relevance_override ns : relevance_override =
{add = ns, del = [], only = false}
-fun del_from_relevance_override ns : relevance_override =
+fun del_relevance_override ns : relevance_override =
{add = [], del = ns, only = false}
fun only_relevance_override ns : relevance_override =
{add = ns, del = [], only = true}
@@ -132,7 +142,7 @@
val infinity_time_in_secs = 60 * 60 * 24 * 365
val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
-fun extract_params default_params override_params =
+fun extract_params auto default_params override_params =
let
val override_params = map unalias_raw_param override_params
val raw_params = rev override_params @ rev default_params
@@ -145,9 +155,9 @@
val lookup_bool = the o general_lookup_bool false (SOME false)
val lookup_bool_option = general_lookup_bool true NONE
fun lookup_time name =
- the_timeout (case lookup name of
- NONE => NONE
- | SOME s => parse_time_option name s)
+ case lookup name of
+ SOME s => parse_time_option name s
+ | NONE => NONE
fun lookup_int name =
case lookup name of
NONE => 0
@@ -167,11 +177,11 @@
case lookup name of
SOME "smart" => NONE
| _ => SOME (lookup_int name)
- val blocking = lookup_bool "blocking"
- val debug = lookup_bool "debug"
- val verbose = debug orelse lookup_bool "verbose"
+ val blocking = auto orelse lookup_bool "blocking"
+ val debug = not auto andalso lookup_bool "debug"
+ val verbose = debug orelse (not auto andalso lookup_bool "verbose")
val overlord = lookup_bool "overlord"
- val atps = lookup_string "atps" |> space_explode " "
+ val atps = lookup_string "atps" |> space_explode " " |> auto ? single o hd
val full_types = lookup_bool "full_types"
val explicit_apply = lookup_bool "explicit_apply"
val relevance_thresholds =
@@ -180,7 +190,7 @@
val max_relevant = lookup_int_option "max_relevant"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
- val timeout = lookup_time "timeout"
+ val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
val expect = lookup_string "expect"
in
{blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
@@ -190,8 +200,8 @@
timeout = timeout, expect = expect}
end
-fun get_params thy = extract_params (default_raw_params thy)
-fun default_params thy = get_params thy o map (apsnd single)
+fun get_params auto thy = extract_params auto (default_raw_params thy)
+fun default_params thy = get_params false thy o map (apsnd single)
(* Sledgehammer the given subgoal *)
@@ -225,11 +235,13 @@
in
if subcommand = runN then
let val i = the_default 1 opt_i in
- run_sledgehammer (get_params thy override_params) i relevance_override
- (minimize_command override_params i) state
+ run_sledgehammer (get_params false thy override_params) false i
+ relevance_override (minimize_command override_params i)
+ state
+ |> K ()
end
else if subcommand = minimizeN then
- run_minimize (get_params thy override_params) (the_default 1 opt_i)
+ run_minimize (get_params false thy override_params) (the_default 1 opt_i)
(#add relevance_override) state
else if subcommand = messagesN then
messages opt_i
@@ -254,7 +266,7 @@
fun sledgehammer_params_trans params =
Toplevel.theory
(fold set_default_raw_param params
- #> tap (fn thy =>
+ #> tap (fn thy =>
writeln ("Default parameters for Sledgehammer:\n" ^
(case rev (default_raw_params thy) of
[] => "none"
@@ -270,14 +282,13 @@
val parse_fact_refs =
Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
val parse_relevance_chunk =
- (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
- || (Args.del |-- Args.colon |-- parse_fact_refs
- >> del_from_relevance_override)
+ (Args.add |-- Args.colon |-- parse_fact_refs >> add_relevance_override)
+ || (Args.del |-- Args.colon |-- parse_fact_refs >> del_relevance_override)
|| (parse_fact_refs >> only_relevance_override)
val parse_relevance_override =
Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
>> merge_relevance_overrides))
- (add_to_relevance_override [])
+ no_relevance_override
val parse_sledgehammer_command =
(Scan.optional Parse.short_ident runN -- parse_params
-- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans
@@ -293,4 +304,16 @@
"set and display the default parameters for Sledgehammer" Keyword.thy_decl
parse_sledgehammer_params_command
+fun auto_sledgehammer state =
+ if not (!auto) then
+ (false, state)
+ else
+ let val thy = Proof.theory_of state in
+ run_sledgehammer (get_params true thy []) true 1 no_relevance_override
+ (minimize_command [] 1) state
+ end
+
+val setup =
+ Auto_Counterexample.register_tool ("sledgehammer", auto_sledgehammer)
+
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Sep 11 10:20:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Sep 11 10:21:52 2010 +0200
@@ -60,7 +60,7 @@
val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
val {context = ctxt, goal, ...} = Proof.goal state
val problem =
- {ctxt = ctxt, goal = goal, subgoal = subgoal,
+ {state = state, goal = goal, subgoal = subgoal,
axioms = map (prepare_axiom ctxt) axioms}
val result as {outcome, used_thm_names, ...} = prover params (K "") problem
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Sep 11 10:20:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Sep 11 10:21:52 2010 +0200
@@ -25,7 +25,7 @@
val strip_subgoal : thm -> int -> (string * typ) list * term list * term
val reserved_isar_keyword_table : unit -> unit Symtab.table
end;
-
+
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
struct