--- a/src/HOL/IsaMakefile Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/IsaMakefile Thu Mar 25 17:56:31 2010 +0100
@@ -322,6 +322,7 @@
Tools/Sledgehammer/sledgehammer_hol_clause.ML \
Tools/Sledgehammer/sledgehammer_isar.ML \
Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
+ Tools/Sledgehammer/sledgehammer_util.ML \
Tools/string_code.ML \
Tools/string_syntax.ML \
Tools/transfer.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 25 17:56:31 2010 +0100
@@ -280,7 +280,8 @@
fun get_atp thy args =
let
- fun default_atp_name () = hd (ATP_Manager.get_atps ())
+ fun default_atp_name () =
+ hd (#atps (Sledgehammer_Isar.default_params thy []))
handle Empty => error "No ATP available."
fun get_prover name =
(case ATP_Manager.get_prover thy name of
@@ -302,22 +303,28 @@
fun run_sh prover hard_timeout timeout dir st =
let
val {context = ctxt, facts, goal} = Proof.goal st
+ val thy = ProofContext.theory_of ctxt
val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I)
val ctxt' =
ctxt
|> change_dir dir
|> Config.put ATP_Wrapper.measure_runtime true
- val problem = ATP_Manager.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
-
+ val params = Sledgehammer_Isar.default_params thy []
+ val problem =
+ {subgoal = 1, goal = (ctxt', (facts, goal)),
+ relevance_override = {add = [], del = [], only = false},
+ axiom_clauses = NONE, filtered_clauses = NONE}
val time_limit =
(case hard_timeout of
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
- val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Manager.prover_result,
- time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
+ val ({success, message, relevant_thm_names,
+ atp_run_time_in_msecs = time_atp, ...}: ATP_Manager.prover_result,
+ time_isa) = time_limit (Mirabelle.cpu_time
+ (prover params (Time.fromSeconds timeout))) problem
in
- if success then (message, SH_OK (time_isa, time_atp, theorem_names))
- else (message, SH_FAIL(time_isa, time_atp))
+ if success then (message, SH_OK (time_isa, time_atp, relevant_thm_names))
+ else (message, SH_FAIL (time_isa, time_atp))
end
handle Sledgehammer_HOL_Clause.TRIVIAL => ("trivial", SH_OK (0, 0, []))
| ERROR msg => ("error: " ^ msg, SH_ERROR)
@@ -375,16 +382,19 @@
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
let
open ATP_Minimal
+ open Sledgehammer_Isar
+ val thy = Proof.theory_of st
val n0 = length (these (!named_thms))
- val (prover_name, prover) = get_atp (Proof.theory_of st) args
- val minimize = minimize_theorems linear_minimize prover prover_name
+ val (prover_name, prover) = get_atp thy args
val timeout =
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o explode)
|> the_default 5
+ val params = default_params thy [("minimize_timeout", Int.toString timeout)]
+ val minimize = minimize_theorems params linear_minimize prover prover_name
val _ = log separator
in
- case minimize timeout st (these (!named_thms)) of
+ case minimize st (these (!named_thms)) of
(SOME named_thms', msg) =>
(change_data id inc_min_succs;
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
--- a/src/HOL/Sledgehammer.thy Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Sledgehammer.thy Thu Mar 25 17:56:31 2010 +0100
@@ -12,6 +12,7 @@
uses
"Tools/polyhash.ML"
"~~/src/Tools/Metis/metis.ML"
+ "Tools/Sledgehammer/sledgehammer_util.ML"
("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Mar 25 17:56:31 2010 +0100
@@ -1,71 +1,92 @@
(* Title: HOL/Tools/ATP_Manager/atp_manager.ML
Author: Fabian Immler, TU Muenchen
Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
Central manager component for ATP threads.
*)
signature ATP_MANAGER =
sig
+ type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+ type params =
+ {debug: bool,
+ verbose: bool,
+ atps: string list,
+ full_types: bool,
+ relevance_threshold: real,
+ higher_order: bool option,
+ respect_no_atp: bool,
+ follow_defs: bool,
+ isar_proof: bool,
+ timeout: Time.time,
+ minimize_timeout: Time.time}
type problem =
- {with_full_types: bool,
- subgoal: int,
- goal: Proof.context * (thm list * thm),
- axiom_clauses: (thm * (string * int)) list option,
- filtered_clauses: (thm * (string * int)) list option}
- val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
+ {subgoal: int,
+ goal: Proof.context * (thm list * thm),
+ relevance_override: relevance_override,
+ axiom_clauses: (thm * (string * int)) list option,
+ filtered_clauses: (thm * (string * int)) list option}
type prover_result =
- {success: bool,
- message: string,
- theorem_names: string list,
- runtime: int,
- proof: string,
- internal_thm_names: string Vector.vector,
- filtered_clauses: (thm * (string * int)) list}
- type prover = int -> problem -> prover_result
+ {success: bool,
+ message: string,
+ relevant_thm_names: string list,
+ atp_run_time_in_msecs: int,
+ proof: string,
+ internal_thm_names: string Vector.vector,
+ filtered_clauses: (thm * (string * int)) list}
+ type prover = params -> Time.time -> problem -> prover_result
val atps: string Unsynchronized.ref
- val get_atps: unit -> string list
val timeout: int Unsynchronized.ref
val full_types: bool Unsynchronized.ref
- val kill: unit -> unit
- val info: unit -> unit
+ val kill_atps: unit -> unit
+ val running_atps: unit -> unit
val messages: int option -> unit
val add_prover: string * prover -> theory -> theory
val get_prover: theory -> string -> prover option
- val print_provers: theory -> unit
- val sledgehammer: string list -> Proof.state -> unit
+ val available_atps: theory -> unit
+ val sledgehammer: params -> int -> relevance_override -> Proof.state -> unit
end;
structure ATP_Manager : ATP_MANAGER =
struct
-(** problems, results, and provers **)
+type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+
+(** parameters, problems, results, and provers **)
+
+(* TODO: "theory_const", "blacklist_filter", "convergence" *)
+type params =
+ {debug: bool,
+ verbose: bool,
+ atps: string list,
+ full_types: bool,
+ relevance_threshold: real,
+ higher_order: bool option,
+ respect_no_atp: bool,
+ follow_defs: bool,
+ isar_proof: bool,
+ timeout: Time.time,
+ minimize_timeout: Time.time}
type problem =
- {with_full_types: bool,
- subgoal: int,
- goal: Proof.context * (thm list * thm),
- axiom_clauses: (thm * (string * int)) list option,
- filtered_clauses: (thm * (string * int)) list option};
-
-fun problem_of_goal with_full_types subgoal goal : problem =
- {with_full_types = with_full_types,
- subgoal = subgoal,
- goal = goal,
- axiom_clauses = NONE,
- filtered_clauses = NONE};
+ {subgoal: int,
+ goal: Proof.context * (thm list * thm),
+ relevance_override: relevance_override,
+ axiom_clauses: (thm * (string * int)) list option,
+ filtered_clauses: (thm * (string * int)) list option};
type prover_result =
- {success: bool,
- message: string,
- theorem_names: string list, (*relevant theorems*)
- runtime: int, (*user time of the ATP, in milliseconds*)
- proof: string,
- internal_thm_names: string Vector.vector,
- filtered_clauses: (thm * (string * int)) list};
+ {success: bool,
+ message: string,
+ relevant_thm_names: string list,
+ atp_run_time_in_msecs: int,
+ proof: string,
+ internal_thm_names: string Vector.vector,
+ filtered_clauses: (thm * (string * int)) list};
-type prover = int -> problem -> prover_result;
+type prover = params -> Time.time -> problem -> prover_result;
(** preferences **)
@@ -74,8 +95,6 @@
val message_display_limit = 5;
val atps = Unsynchronized.ref "e spass remote_vampire";
-fun get_atps () = String.tokens (Symbol.is_ascii_blank o String.str) (! atps);
-
val timeout = Unsynchronized.ref 60;
val full_types = Unsynchronized.ref false;
@@ -218,9 +237,9 @@
(** user commands **)
-(* kill *)
+(* kill ATPs *)
-fun kill () = Synchronized.change global_state
+fun kill_atps () = Synchronized.change global_state
(fn {manager, timeout_heap, active, cancelling, messages, store} =>
let
val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active;
@@ -228,11 +247,11 @@
in state' end);
-(* info *)
+(* running_atps *)
fun seconds time = string_of_int (Time.toSeconds time) ^ "s";
-fun info () =
+fun running_atps () =
let
val {active, cancelling, ...} = Synchronized.value global_state;
@@ -287,44 +306,51 @@
fun get_prover thy name =
Option.map #1 (Symtab.lookup (Provers.get thy) name);
-fun print_provers thy = Pretty.writeln
- (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
+fun available_atps thy = Pretty.writeln
+ (Pretty.strs ("ATPs:" :: sort_strings (Symtab.keys (Provers.get thy))));
(* start prover thread *)
-fun start_prover name birth_time death_time i proof_state =
+fun start_prover (params as {timeout, ...}) birth_time death_time i
+ relevance_override proof_state name =
(case get_prover (Proof.theory_of proof_state) name of
- NONE => warning ("Unknown external prover: " ^ quote name)
+ NONE => warning ("Unknown ATP: " ^ quote name)
| SOME prover =>
let
val {context = ctxt, facts, goal} = Proof.goal proof_state;
val desc =
- "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
+ "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
val _ = Toplevel.thread true (fn () =>
let
val _ = register birth_time death_time (Thread.self (), desc);
- val problem = problem_of_goal (! full_types) i (ctxt, (facts, goal));
- val message = #message (prover (! timeout) problem)
+ val problem =
+ {subgoal = i, goal = (ctxt, (facts, goal)),
+ relevance_override = relevance_override, axiom_clauses = NONE,
+ filtered_clauses = NONE}
+ val message = #message (prover params timeout problem)
handle Sledgehammer_HOL_Clause.TRIVIAL => (* FIXME !? *)
- "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
+ "Try this command: " ^
+ Markup.markup Markup.sendback "by metis" ^ "."
| ERROR msg => ("Error: " ^ msg);
val _ = unregister message (Thread.self ());
in () end);
in () end);
-(* sledghammer for first subgoal *)
+(* Sledgehammer the given subgoal *)
-fun sledgehammer names proof_state =
+fun sledgehammer (params as {atps, timeout, ...}) i relevance_override
+ proof_state =
let
- val provers = if null names then get_atps () else names;
- val birth_time = Time.now ();
- val death_time = Time.+ (birth_time, Time.fromSeconds (! timeout));
- val _ = kill (); (*RACE wrt. other invocations of sledgehammer*)
- val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers;
- in () end;
+ val birth_time = Time.now ()
+ val death_time = Time.+ (birth_time, timeout)
+ val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
+ val _ = priority "Sledgehammering..."
+ val _ = List.app (start_prover params birth_time death_time i
+ relevance_override proof_state) atps
+ in () end
end;
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Mar 25 17:56:31 2010 +0100
@@ -6,6 +6,7 @@
signature ATP_MINIMAL =
sig
+ type params = ATP_Manager.params
type prover = ATP_Manager.prover
type prover_result = ATP_Manager.prover_result
type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
@@ -13,7 +14,7 @@
val linear_minimize : 'a minimize_fun
val binary_minimize : 'a minimize_fun
val minimize_theorems :
- (string * thm list) minimize_fun -> prover -> string -> int
+ params -> (string * thm list) minimize_fun -> prover -> string
-> Proof.state -> (string * thm list) list
-> (string * thm list) list option * string
end;
@@ -109,8 +110,8 @@
(* wrapper for calling external prover *)
-fun sledgehammer_test_theorems prover time_limit subgoalno state filtered
- name_thms_pairs =
+fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
+ timeout subgoalno state filtered name_thms_pairs =
let
val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
" theorems... ")
@@ -118,26 +119,26 @@
val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
- {with_full_types = ! ATP_Manager.full_types,
- subgoal = subgoalno,
- goal = (ctxt, (facts, goal)),
- axiom_clauses = SOME axclauses,
- filtered_clauses = filtered}
- val (result, proof) = produce_answer (prover time_limit problem)
+ {subgoal = subgoalno, goal = (ctxt, (facts, goal)),
+ relevance_override = {add = [], del = [], only = false},
+ axiom_clauses = SOME axclauses, filtered_clauses = filtered}
+ val (result, proof) = produce_answer (prover params timeout problem)
val _ = priority (string_of_result result)
in (result, proof) end
(* minimalization of thms *)
-fun minimize_theorems gen_min prover prover_name time_limit state
- name_thms_pairs =
+fun minimize_theorems (params as {minimize_timeout, ...}) gen_min prover
+ prover_name state name_thms_pairs =
let
+ val msecs = Time.toMilliseconds minimize_timeout
val _ =
priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
- " theorems, prover: " ^ prover_name ^
- ", time limit: " ^ string_of_int time_limit ^ " seconds")
- val test_thms_fun = sledgehammer_test_theorems prover time_limit 1 state
+ " theorems, ATP: " ^ prover_name ^
+ ", time limit: " ^ string_of_int msecs ^ " ms")
+ val test_thms_fun =
+ sledgehammer_test_theorems params prover minimize_timeout 1 state
fun test_thms filtered thms =
case test_thms_fun filtered thms of (Success _, _) => true | _ => false
in
@@ -157,18 +158,22 @@
val _ = priority (cat_lines
["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
in
- (SOME min_thms, "Try this command: " ^
- Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
+ (SOME min_thms,
+ "Try this command: " ^
+ Markup.markup Markup.sendback
+ ("by (metis " ^ space_implode " " min_names ^ ")")
+ ^ ".")
end
| (Timeout, _) =>
(NONE, "Timeout: You may need to increase the time limit of " ^
- string_of_int time_limit ^ " seconds. Call atp_minimize [time=...] ")
+ string_of_int msecs ^ " ms. Invoke \"atp_minimize [time=...]\".")
| (Error, msg) =>
(NONE, "Error in prover: " ^ msg)
| (Failure, _) =>
(NONE, "Failure: No proof with the theorems supplied"))
handle Sledgehammer_HOL_Clause.TRIVIAL =>
- (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+ (SOME [], "Trivial: Try this command: " ^
+ Markup.markup Markup.sendback "by metis" ^ ".")
| ERROR msg => (NONE, "Error: " ^ msg)
end
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Mar 25 17:56:31 2010 +0100
@@ -20,6 +20,7 @@
structure ATP_Wrapper : ATP_WRAPPER =
struct
+open Sledgehammer_Fact_Preprocessor
open Sledgehammer_HOL_Clause
open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
@@ -43,11 +44,11 @@
type prover_config =
{command: Path.T,
- arguments: int -> string,
+ arguments: Time.time -> string,
failure_strs: string list,
max_new_clauses: int,
- insert_theory_const: bool,
- emit_structured_proof: bool};
+ add_theory_const: bool,
+ supports_isar_proofs: bool};
(* basic template *)
@@ -64,24 +65,25 @@
else SOME "Ill-formed ATP output"
| (failure :: _) => SOME failure
-fun external_prover relevance_filter prepare write cmd args failure_strs
- produce_answer name ({with_full_types, subgoal, goal, axiom_clauses,
- filtered_clauses}: problem) =
+fun generic_prover get_facts prepare write cmd args failure_strs produce_answer
+ name ({full_types, ...} : params)
+ ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
+ : problem) =
let
(* get clauses and prepare them for writing *)
val (ctxt, (chain_ths, th)) = goal;
val thy = ProofContext.theory_of ctxt;
val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths;
- val goal_cls = #1 (Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th subgoal);
+ val goal_cls = #1 (neg_conjecture_clauses ctxt th subgoal);
val the_filtered_clauses =
(case filtered_clauses of
- NONE => relevance_filter goal goal_cls
+ NONE => get_facts relevance_override goal goal_cls
| SOME fcls => fcls);
val the_axiom_clauses =
(case axiom_clauses of
NONE => the_filtered_clauses
| SOME axcls => axcls);
- val (thm_names, clauses) =
+ val (internal_thm_names, clauses) =
prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy;
(* path to unique problem file *)
@@ -121,7 +123,7 @@
if Config.get ctxt measure_runtime then split_time s else (s, 0)
fun run_on probfile =
if File.exists cmd then
- write with_full_types probfile clauses
+ write full_types probfile clauses
|> pair (apfst split_time' (bash_output (cmd_line probfile)))
else error ("Bad executable: " ^ Path.implode cmd);
@@ -131,21 +133,24 @@
if destdir' = "" then ()
else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof;
- val (((proof, time), rc), conj_pos) =
+ val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
with_path cleanup export run_on (prob_pathname subgoal);
(* check for success and print out some information on failure *)
val failure = find_failure failure_strs proof;
val success = rc = 0 andalso is_none failure;
- val (message, real_thm_names) =
+ val (message, relevant_thm_names) =
if is_some failure then ("External prover failed.", [])
else if rc <> 0 then ("External prover failed: " ^ proof, [])
- else apfst (fn s => "Try this command: " ^ s)
- (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoal));
+ else
+ (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th,
+ subgoal));
in
{success = success, message = message,
- theorem_names = real_thm_names, runtime = time, proof = proof,
- internal_thm_names = thm_names, filtered_clauses = the_filtered_clauses}
+ relevant_thm_names = relevant_thm_names,
+ atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof,
+ internal_thm_names = internal_thm_names,
+ filtered_clauses = the_filtered_clauses}
end;
@@ -153,96 +158,87 @@
fun generic_tptp_prover
(name, {command, arguments, failure_strs, max_new_clauses,
- insert_theory_const, emit_structured_proof}) timeout =
- external_prover (get_relevant_facts max_new_clauses insert_theory_const)
- (prepare_clauses false) write_tptp_file command (arguments timeout)
- failure_strs
- (if emit_structured_proof then structured_isar_proof
- else metis_lemma_list false) name;
+ add_theory_const, supports_isar_proofs})
+ (params as {relevance_threshold, higher_order, follow_defs, isar_proof,
+ ...}) timeout =
+ generic_prover
+ (get_relevant_facts relevance_threshold higher_order follow_defs
+ max_new_clauses add_theory_const)
+ (prepare_clauses higher_order false) write_tptp_file command
+ (arguments timeout) failure_strs
+ (if supports_isar_proofs andalso isar_proof then structured_isar_proof
+ else metis_lemma_list false) name params;
-fun tptp_prover (name, p) = (name, generic_tptp_prover (name, p));
+fun tptp_prover name p = (name, generic_tptp_prover (name, p));
(** common provers **)
(* Vampire *)
-(*NB: Vampire does not work without explicit timelimit*)
-
-val vampire_failure_strs =
- ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
-val vampire_max_new_clauses = 60;
-val vampire_insert_theory_const = false;
+(* NB: Vampire does not work without explicit time limit. *)
-fun vampire_prover_config isar : prover_config =
- {command = Path.explode "$VAMPIRE_HOME/vampire",
- arguments = (fn timeout => "--output_syntax tptp --mode casc" ^
- " -t " ^ string_of_int timeout),
- failure_strs = vampire_failure_strs,
- max_new_clauses = vampire_max_new_clauses,
- insert_theory_const = vampire_insert_theory_const,
- emit_structured_proof = isar};
-
-val vampire = tptp_prover ("vampire", vampire_prover_config false);
-val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true);
+val vampire_config : prover_config =
+ {command = Path.explode "$VAMPIRE_HOME/vampire",
+ arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^
+ string_of_int (Time.toSeconds timeout)),
+ failure_strs =
+ ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"],
+ max_new_clauses = 60,
+ add_theory_const = false,
+ supports_isar_proofs = true}
+val vampire = tptp_prover "vampire" vampire_config
(* E prover *)
-val eprover_failure_strs =
- ["SZS status: Satisfiable", "SZS status Satisfiable",
- "SZS status: ResourceOut", "SZS status ResourceOut",
- "# Cannot determine problem status"];
-val eprover_max_new_clauses = 100;
-val eprover_insert_theory_const = false;
-
-fun eprover_config isar : prover_config =
- {command = Path.explode "$E_HOME/eproof",
- arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^
- " --silent --cpu-limit=" ^ string_of_int timeout),
- failure_strs = eprover_failure_strs,
- max_new_clauses = eprover_max_new_clauses,
- insert_theory_const = eprover_insert_theory_const,
- emit_structured_proof = isar};
-
-val eprover = tptp_prover ("e", eprover_config false);
-val eprover_isar = tptp_prover ("e_isar", eprover_config true);
+val e_config : prover_config =
+ {command = Path.explode "$E_HOME/eproof",
+ arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \
+ \-tAutoDev --silent --cpu-limit=" ^
+ string_of_int (Time.toSeconds timeout)),
+ failure_strs =
+ ["SZS status: Satisfiable", "SZS status Satisfiable",
+ "SZS status: ResourceOut", "SZS status ResourceOut",
+ "# Cannot determine problem status"],
+ max_new_clauses = 100,
+ add_theory_const = false,
+ supports_isar_proofs = true}
+val e = tptp_prover "e" e_config
(* SPASS *)
-val spass_failure_strs =
- ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
- "SPASS beiseite: Maximal number of loops exceeded."];
-val spass_max_new_clauses = 40;
-val spass_insert_theory_const = true;
-
-fun spass_config insert_theory_const: prover_config =
- {command = Path.explode "$SPASS_HOME/SPASS",
- arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
- " -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout),
- failure_strs = spass_failure_strs,
- max_new_clauses = spass_max_new_clauses,
- insert_theory_const = insert_theory_const,
- emit_structured_proof = false};
-
fun generic_dfg_prover
(name, ({command, arguments, failure_strs, max_new_clauses,
- insert_theory_const, ...} : prover_config)) timeout =
- external_prover
- (get_relevant_facts max_new_clauses insert_theory_const)
- (prepare_clauses true)
- write_dfg_file
- command
- (arguments timeout)
- failure_strs
- (metis_lemma_list true)
- name;
+ add_theory_const, ...} : prover_config))
+ (params as {relevance_threshold, higher_order, follow_defs, ...})
+ timeout =
+ generic_prover
+ (get_relevant_facts relevance_threshold higher_order follow_defs
+ max_new_clauses add_theory_const)
+ (prepare_clauses higher_order true) write_dfg_file command
+ (arguments timeout) failure_strs (metis_lemma_list true) name params;
fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
-val spass = dfg_prover ("spass", spass_config spass_insert_theory_const);
-val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false);
+fun spass_config_for add_theory_const : prover_config =
+ {command = Path.explode "$SPASS_HOME/SPASS",
+ arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
+ " -FullRed=0 -DocProof -TimeLimit=" ^
+ string_of_int (Time.toSeconds timeout)),
+ failure_strs =
+ ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
+ "SPASS beiseite: Maximal number of loops exceeded."],
+ max_new_clauses = 40,
+ add_theory_const = add_theory_const,
+ supports_isar_proofs = false};
+
+val spass_config = spass_config_for true
+val spass = dfg_prover ("spass", spass_config)
+
+val spass_no_tc_config = spass_config_for false
+val spass_no_tc = dfg_prover ("spass_no_tc", spass_no_tc_config)
(* remote prover invocation via SystemOnTPTP *)
@@ -251,10 +247,12 @@
fun get_systems () =
let
- val (answer, rc) = bash_output ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
+ val (answer, rc) = bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w"
in
- if rc <> 0 then error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
- else split_lines answer
+ if rc <> 0 then
+ error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
+ else
+ split_lines answer
end;
fun refresh_systems_on_tptp () =
@@ -271,27 +269,34 @@
val remote_failure_strs = ["Remote-script could not extract proof"];
-fun remote_prover_config prover_prefix args max_new insert_tc: prover_config =
- {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
- arguments = (fn timeout =>
- args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
- failure_strs = remote_failure_strs,
- max_new_clauses = max_new,
- insert_theory_const = insert_tc,
- emit_structured_proof = false};
+fun remote_prover_config prover_prefix args max_new_clauses add_theory_const
+ : prover_config =
+ {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
+ arguments = (fn timeout =>
+ args ^ " -t " ^ string_of_int (Time.toSeconds timeout) ^ " -s " ^
+ the_system prover_prefix),
+ failure_strs = remote_failure_strs,
+ max_new_clauses = max_new_clauses,
+ add_theory_const = add_theory_const,
+ supports_isar_proofs = false}
-val remote_vampire = tptp_prover ("remote_vampire", remote_prover_config
- "Vampire---9" "" vampire_max_new_clauses vampire_insert_theory_const);
+val remote_vampire =
+ tptp_prover "remote_vampire"
+ (remote_prover_config "Vampire---9" ""
+ (#max_new_clauses vampire_config) (#add_theory_const vampire_config))
-val remote_eprover = tptp_prover ("remote_e", remote_prover_config
- "EP---" "" eprover_max_new_clauses eprover_insert_theory_const);
+val remote_e =
+ tptp_prover "remote_e"
+ (remote_prover_config "EP---" ""
+ (#max_new_clauses e_config) (#add_theory_const e_config))
-val remote_spass = tptp_prover ("remote_spass", remote_prover_config
- "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const);
+val remote_spass =
+ tptp_prover "remote_spass"
+ (remote_prover_config "SPASS---" "-x"
+ (#max_new_clauses spass_config) (#add_theory_const spass_config))
val provers =
- [spass, vampire, eprover, vampire_isar, eprover_isar, spass_no_tc,
- remote_vampire, remote_spass, remote_eprover]
+ [spass, vampire, e, spass_no_tc, remote_vampire, remote_spass, remote_e]
val prover_setup = fold add_prover provers
val setup =
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 25 17:56:31 2010 +0100
@@ -346,7 +346,7 @@
fun monotonicity_message Ts extra =
let val ss = map (quote o string_for_type ctxt) Ts in
"The type" ^ plural_s_for_list ss ^ " " ^
- space_implode " " (serial_commas "and" ss) ^ " " ^
+ space_implode " " (Sledgehammer_Util.serial_commas "and" ss) ^ " " ^
(if none_true monos then
"passed the monotonicity test"
else
@@ -684,7 +684,8 @@
options
in
print ("Try again with " ^
- space_implode " " (serial_commas "and" ss) ^
+ space_implode " "
+ (Sledgehammer_Util.serial_commas "and" ss) ^
" to confirm that the " ^ das_wort_model ^
" is genuine.")
end
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 25 17:56:31 2010 +0100
@@ -24,6 +24,8 @@
open Nitpick_Nut
open Nitpick
+structure K = OuterKeyword and P = OuterParse
+
val auto = Unsynchronized.ref false;
val _ =
@@ -34,48 +36,48 @@
type raw_param = string * string list
val default_default_params =
- [("card", ["1\<midarrow>8"]),
- ("iter", ["0,1,2,4,8,12,16,24"]),
- ("bits", ["1,2,3,4,6,8,10,12"]),
- ("bisim_depth", ["7"]),
- ("box", ["smart"]),
- ("finitize", ["smart"]),
- ("mono", ["smart"]),
- ("std", ["true"]),
- ("wf", ["smart"]),
- ("sat_solver", ["smart"]),
- ("batch_size", ["smart"]),
- ("blocking", ["true"]),
- ("falsify", ["true"]),
- ("user_axioms", ["smart"]),
- ("assms", ["true"]),
- ("merge_type_vars", ["false"]),
- ("binary_ints", ["smart"]),
- ("destroy_constrs", ["true"]),
- ("specialize", ["true"]),
- ("skolemize", ["true"]),
- ("star_linear_preds", ["true"]),
- ("uncurry", ["true"]),
- ("fast_descrs", ["true"]),
- ("peephole_optim", ["true"]),
- ("timeout", ["30 s"]),
- ("tac_timeout", ["500 ms"]),
- ("sym_break", ["20"]),
- ("sharing_depth", ["3"]),
- ("flatten_props", ["false"]),
- ("max_threads", ["0"]),
- ("verbose", ["false"]),
- ("debug", ["false"]),
- ("overlord", ["false"]),
- ("show_all", ["false"]),
- ("show_skolems", ["true"]),
- ("show_datatypes", ["false"]),
- ("show_consts", ["false"]),
- ("format", ["1"]),
- ("max_potential", ["1"]),
- ("max_genuine", ["1"]),
- ("check_potential", ["false"]),
- ("check_genuine", ["false"])]
+ [("card", "1\<midarrow>8"),
+ ("iter", "0,1,2,4,8,12,16,24"),
+ ("bits", "1,2,3,4,6,8,10,12"),
+ ("bisim_depth", "7"),
+ ("box", "smart"),
+ ("finitize", "smart"),
+ ("mono", "smart"),
+ ("std", "true"),
+ ("wf", "smart"),
+ ("sat_solver", "smart"),
+ ("batch_size", "smart"),
+ ("blocking", "true"),
+ ("falsify", "true"),
+ ("user_axioms", "smart"),
+ ("assms", "true"),
+ ("merge_type_vars", "false"),
+ ("binary_ints", "smart"),
+ ("destroy_constrs", "true"),
+ ("specialize", "true"),
+ ("skolemize", "true"),
+ ("star_linear_preds", "true"),
+ ("uncurry", "true"),
+ ("fast_descrs", "true"),
+ ("peephole_optim", "true"),
+ ("timeout", "30 s"),
+ ("tac_timeout", "500 ms"),
+ ("sym_break", "20"),
+ ("sharing_depth", "3"),
+ ("flatten_props", "false"),
+ ("max_threads", "0"),
+ ("debug", "false"),
+ ("verbose", "false"),
+ ("overlord", "false"),
+ ("show_all", "false"),
+ ("show_skolems", "true"),
+ ("show_datatypes", "false"),
+ ("show_consts", "false"),
+ ("format", "1"),
+ ("max_potential", "1"),
+ ("max_genuine", "1"),
+ ("check_potential", "false"),
+ ("check_genuine", "false")]
val negated_params =
[("dont_box", "box"),
@@ -97,8 +99,8 @@
("full_descrs", "fast_descrs"),
("no_peephole_optim", "peephole_optim"),
("dont_flatten_props", "flatten_props"),
+ ("no_debug", "debug"),
("quiet", "verbose"),
- ("no_debug", "debug"),
("no_overlord", "overlord"),
("dont_show_all", "show_all"),
("hide_skolems", "show_skolems"),
@@ -119,7 +121,7 @@
(* string * 'a -> unit *)
fun check_raw_param (s, _) =
if is_known_raw_param s then ()
- else error ("Unknown parameter " ^ quote s ^ ".")
+ else error ("Unknown parameter: " ^ quote s ^ ".")
(* string -> string option *)
fun unnegate_param_name name =
@@ -139,20 +141,15 @@
| NONE => (name, value)
structure Data = Theory_Data(
- type T = {params: raw_param list}
- val empty = {params = rev default_default_params}
+ type T = raw_param list
+ val empty = default_default_params |> map (apsnd single)
val extend = I
- fun merge ({params = ps1}, {params = ps2}) : T =
- {params = AList.merge (op =) (K true) (ps1, ps2)})
+ fun merge p : T = AList.merge (op =) (K true) p)
(* raw_param -> theory -> theory *)
-fun set_default_raw_param param thy =
- let val {params} = Data.get thy in
- Data.put {params = AList.update (op =) (unnegate_raw_param param) params}
- thy
- end
+val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
(* theory -> raw_param list *)
-val default_raw_params = #params o Data.get
+val default_raw_params = Data.get
(* string -> bool *)
fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
@@ -164,26 +161,6 @@
s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^
stringify_raw_param_value (s2 :: ss)
-(* bool -> string -> string -> bool option *)
-fun bool_option_from_string option name s =
- (case s of
- "smart" => if option then NONE else raise Option
- | "false" => SOME false
- | "true" => SOME true
- | "" => SOME true
- | _ => raise Option)
- handle Option.Option =>
- let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
- error ("Parameter " ^ quote name ^ " must be assigned " ^
- space_implode " " (serial_commas "or" ss) ^ ".")
- end
-(* bool -> raw_param list -> bool option -> string -> bool option *)
-fun general_lookup_bool option raw_params default_value name =
- case AList.lookup (op =) raw_params name of
- SOME s => s |> stringify_raw_param_value
- |> bool_option_from_string option name
- | NONE => default_value
-
(* int -> string -> int *)
fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
@@ -192,14 +169,19 @@
let
val override_params = map unnegate_raw_param override_params
val raw_params = rev override_params @ rev default_params
+ (* string -> string *)
val lookup =
Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
- (* string -> string *)
- fun lookup_string name = the_default "" (lookup name)
+ val lookup_string = the_default "" o lookup
+ (* bool -> bool option -> string -> bool option *)
+ fun general_lookup_bool option default_value name =
+ case lookup name of
+ SOME s => Sledgehammer_Util.parse_bool_option option name s
+ | NONE => default_value
(* string -> bool *)
- val lookup_bool = the o general_lookup_bool false raw_params (SOME false)
+ val lookup_bool = the o general_lookup_bool false (SOME false)
(* string -> bool option *)
- val lookup_bool_option = general_lookup_bool true raw_params NONE
+ val lookup_bool_option = general_lookup_bool true NONE
(* string -> string option -> int *)
fun do_int name value =
case value of
@@ -253,7 +235,8 @@
:: map (fn (name, value) =>
(SOME (read (String.extract (name, size prefix + 1, NONE))),
value |> stringify_raw_param_value
- |> bool_option_from_string false name |> the))
+ |> Sledgehammer_Util.parse_bool_option false name
+ |> the))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
(* (string -> 'a) -> string -> ('a option * bool option) list *)
fun lookup_bool_option_assigns read prefix =
@@ -261,28 +244,13 @@
:: map (fn (name, value) =>
(SOME (read (String.extract (name, size prefix + 1, NONE))),
value |> stringify_raw_param_value
- |> bool_option_from_string true name))
+ |> Sledgehammer_Util.parse_bool_option true name))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
(* string -> Time.time option *)
fun lookup_time name =
case lookup name of
NONE => NONE
- | SOME "none" => NONE
- | SOME s =>
- let
- val msecs =
- case space_explode " " s of
- [s1, "min"] => 60000 * the (Int.fromString s1)
- | [s1, "s"] => 1000 * the (Int.fromString s1)
- | [s1, "ms"] => the (Int.fromString s1)
- | _ => 0
- in
- if msecs <= 0 then
- error ("Parameter " ^ quote name ^ " must be assigned a positive \
- \time value (e.g., \"60 s\", \"200 ms\") or \"none\".")
- else
- SOME (Time.fromMilliseconds msecs)
- end
+ | SOME s => Sledgehammer_Util.parse_time_option name s
(* string -> term list *)
val lookup_term_list =
AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt
@@ -368,22 +336,18 @@
extract_params (ProofContext.init thy) false (default_raw_params thy)
o map (apsnd single)
-(* OuterParse.token list -> string * OuterParse.token list *)
-val scan_key = Scan.repeat1 OuterParse.typ_group >> space_implode " "
-
-(* OuterParse.token list -> string list * OuterParse.token list *)
-val scan_value =
- Scan.repeat1 (OuterParse.minus >> single
- || Scan.repeat1 (Scan.unless OuterParse.minus OuterParse.name)
- || OuterParse.$$$ "," |-- OuterParse.number >> prefix ","
- >> single) >> flat
-
-(* OuterParse.token list -> raw_param * OuterParse.token list *)
-val scan_param =
- scan_key -- (Scan.option (OuterParse.$$$ "=" |-- scan_value) >> these)
-(* OuterParse.token list -> raw_param list option * OuterParse.token list *)
-val scan_params = Scan.option (OuterParse.$$$ "[" |-- OuterParse.list scan_param
- --| OuterParse.$$$ "]")
+(* P.token list -> string * P.token list *)
+val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
+(* P.token list -> string list * P.token list *)
+val parse_value =
+ Scan.repeat1 (P.minus >> single
+ || Scan.repeat1 (Scan.unless P.minus P.name)
+ || P.$$$ "," |-- P.number >> prefix "," >> single) >> flat
+(* P.token list -> raw_param * P.token list *)
+val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
+(* P.token list -> raw_param list * P.token list *)
+val parse_params =
+ Scan.optional (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]") []
(* Proof.context -> ('a -> 'a) -> 'a -> 'a *)
fun handle_exceptions ctxt f x =
@@ -423,7 +387,6 @@
| Refute.REFUTE (loc, details) =>
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
-
(* raw_param list -> bool -> int -> int -> Proof.state -> bool * Proof.state *)
fun pick_nits override_params auto i step state =
let
@@ -445,21 +408,20 @@
else (Toplevel.thread true (fn () => (go (); ())); (false, state))
end
-(* raw_param list option * int option -> Toplevel.transition
- -> Toplevel.transition *)
-fun nitpick_trans (opt_params, opt_i) =
+(* raw_param list * int -> Toplevel.transition -> Toplevel.transition *)
+fun nitpick_trans (params, i) =
Toplevel.keep (fn st =>
- (pick_nits (these opt_params) false (the_default 1 opt_i)
- (Toplevel.proof_position_of st) (Toplevel.proof_of st); ()))
+ (pick_nits params false i (Toplevel.proof_position_of st)
+ (Toplevel.proof_of st); ()))
(* raw_param -> string *)
fun string_for_raw_param (name, value) =
name ^ " = " ^ stringify_raw_param_value value
-(* raw_param list option -> Toplevel.transition -> Toplevel.transition *)
-fun nitpick_params_trans opt_params =
+(* raw_param list -> Toplevel.transition -> Toplevel.transition *)
+fun nitpick_params_trans params =
Toplevel.theory
- (fold set_default_raw_param (these opt_params)
+ (fold set_default_raw_param params
#> tap (fn thy =>
writeln ("Default parameters for Nitpick:\n" ^
(case rev (default_raw_params thy) of
@@ -469,18 +431,18 @@
params |> map string_for_raw_param
|> sort_strings |> cat_lines)))))
-(* OuterParse.token list
- -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
-val scan_nitpick_command =
- (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
-val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
+(* P.token list
+ -> (Toplevel.transition -> Toplevel.transition) * P.token list *)
+val parse_nitpick_command =
+ (parse_params -- Scan.optional P.nat 1) #>> nitpick_trans
+val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
val _ = OuterSyntax.improper_command "nitpick"
"try to find a counterexample for a given subgoal using Kodkod"
- OuterKeyword.diag scan_nitpick_command
+ K.diag parse_nitpick_command
val _ = OuterSyntax.command "nitpick_params"
"set and display the default parameters for Nitpick"
- OuterKeyword.thy_decl scan_nitpick_params_command
+ K.thy_decl parse_nitpick_params_command
(* Proof.state -> bool * Proof.state *)
fun auto_nitpick state =
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Mar 25 17:56:31 2010 +0100
@@ -194,8 +194,11 @@
else
[])
in
- if null ss then []
- else serial_commas "and" ss |> map Pretty.str |> Pretty.breaks
+ if null ss then
+ []
+ else
+ Sledgehammer_Util.serial_commas "and" ss
+ |> map Pretty.str |> Pretty.breaks
end
(* scope -> string *)
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Mar 25 17:56:31 2010 +0100
@@ -46,7 +46,6 @@
val triple_lookup :
(''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option
val is_substring_of : string -> string -> bool
- val serial_commas : string -> string list -> string list
val plural_s : int -> string
val plural_s_for_list : 'a list -> string
val flip_polarity : polarity -> polarity
@@ -233,13 +232,6 @@
not (Substring.isEmpty (snd (Substring.position needle
(Substring.full stack))))
-(* string -> string list -> string list *)
-fun serial_commas _ [] = ["??"]
- | serial_commas _ [s] = [s]
- | serial_commas conj [s1, s2] = [s1, conj, s2]
- | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
- | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
-
(* int -> string *)
fun plural_s n = if n = 1 then "" else "s"
(* 'a list -> string *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Mar 25 17:56:31 2010 +0100
@@ -9,12 +9,19 @@
type axiom_name = Sledgehammer_HOL_Clause.axiom_name
type hol_clause = Sledgehammer_HOL_Clause.hol_clause
type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
+ type relevance_override =
+ {add: Facts.ref list,
+ del: Facts.ref list,
+ only: bool}
+
val tvar_classes_of_terms : term list -> string list
val tfree_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
- val get_relevant_facts : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
- (thm * (string * int)) list
- val prepare_clauses : bool -> thm list -> thm list ->
+ val get_relevant_facts :
+ real -> bool option -> bool -> int -> bool -> relevance_override
+ -> Proof.context * (thm list * 'a) -> thm list
+ -> (thm * (string * int)) list
+ val prepare_clauses : bool option -> bool -> thm list -> thm list ->
(thm * (axiom_name * hol_clause_id)) list ->
(thm * (axiom_name * hol_clause_id)) list -> theory ->
axiom_name vector *
@@ -29,29 +36,21 @@
open Sledgehammer_Fact_Preprocessor
open Sledgehammer_HOL_Clause
-type axiom_name = axiom_name
-type hol_clause = hol_clause
-type hol_clause_id = hol_clause_id
+type relevance_override =
+ {add: Facts.ref list,
+ del: Facts.ref list,
+ only: bool}
(********************************************************************)
(* some settings for both background automatic ATP calling procedure*)
(* and also explicit ATP invocation methods *)
(********************************************************************)
-(* Translation mode can be auto-detected, or forced to be first-order or
- higher-order *)
-datatype mode = Auto | Fol | Hol;
-
-val translation_mode = Auto;
-
(*** background linkup ***)
val run_blacklist_filter = true;
(*** relevance filter parameters ***)
-val run_relevance_filter = true;
-val pass_mark = 0.5;
val convergence = 3.2; (*Higher numbers allow longer inference chains*)
-val follow_defs = false; (*Follow definitions. Makes problems bigger.*)
(***************************************************************)
(* Relevance Filtering *)
@@ -139,8 +138,8 @@
(*Inserts a dummy "constant" referring to the theory name, so that relevance
takes the given theory into account.*)
-fun const_prop_of theory_const th =
- if theory_const then
+fun const_prop_of add_theory_const th =
+ if add_theory_const then
let val name = Context.theory_name (theory_of_thm th)
val t = Const (name ^ ". 1", HOLogic.boolT)
in t $ prop_of th end
@@ -169,7 +168,7 @@
structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
-fun count_axiom_consts theory_const thy ((thm,_), tab) =
+fun count_axiom_consts add_theory_const thy ((thm,_), tab) =
let fun count_const (a, T, tab) =
let val (c, cts) = const_with_typ thy (a,T)
in (*Two-dimensional table update. Constant maps to types maps to count.*)
@@ -182,7 +181,7 @@
count_term_consts (t, count_term_consts (u, tab))
| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
| count_term_consts (_, tab) = tab
- in count_term_consts (const_prop_of theory_const thm, tab) end;
+ in count_term_consts (const_prop_of add_theory_const thm, tab) end;
(**** Actual Filtering Code ****)
@@ -214,8 +213,8 @@
let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
in Symtab.fold add_expand_pairs tab [] end;
-fun pair_consts_typs_axiom theory_const thy (thm,name) =
- ((thm,name), (consts_typs_of_term thy (const_prop_of theory_const thm)));
+fun pair_consts_typs_axiom add_theory_const thy (p as (thm, _)) =
+ (p, (consts_typs_of_term thy (const_prop_of add_theory_const thm)));
exception ConstFree;
fun dest_ConstFree (Const aT) = aT
@@ -234,9 +233,10 @@
end
handle ConstFree => false
in
- case tm of @{const Trueprop} $ (Const(@{const_name "op ="}, _) $ lhs $ rhs) =>
- defs lhs rhs
- | _ => false
+ case tm of
+ @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) =>
+ defs lhs rhs
+ | _ => false
end;
type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
@@ -263,8 +263,12 @@
end
end;
-fun relevant_clauses max_new thy ctab p rel_consts =
- let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*)
+fun relevant_clauses ctxt follow_defs max_new
+ (relevance_override as {add, del, only}) thy ctab p
+ rel_consts =
+ let val add_thms = maps (ProofContext.get_fact ctxt) add
+ val del_thms = maps (ProofContext.get_fact ctxt) del
+ fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*)
| relevant (newpairs,rejects) [] =
let val (newrels,more_rejects) = take_best max_new newpairs
val new_consts = maps #2 newrels
@@ -272,11 +276,17 @@
val newp = p + (1.0-p) / convergence
in
trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
- (map #1 newrels) @
- (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
+ map #1 newrels @
+ relevant_clauses ctxt follow_defs max_new relevance_override thy ctab
+ newp rel_consts' (more_rejects @ rejects)
end
- | relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
- let val weight = clause_weight ctab rel_consts consts_typs
+ | relevant (newrels, rejects)
+ ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
+ let
+ val weight = if member Thm.eq_thm del_thms thm then 0.0
+ else if member Thm.eq_thm add_thms thm then 1.0
+ else if only then 0.0
+ else clause_weight ctab rel_consts consts_typs
in
if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
then (trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
@@ -285,23 +295,30 @@
else relevant (newrels, ax::rejects) axs
end
in trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
- relevant ([],[])
+ relevant ([],[])
end;
-fun relevance_filter max_new theory_const thy axioms goals =
- if run_relevance_filter andalso pass_mark >= 0.1
- then
- let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
+fun relevance_filter ctxt relevance_threshold follow_defs max_new
+ add_theory_const relevance_override thy axioms goals =
+ if relevance_threshold > 0.0 then
+ let
+ val const_tab = List.foldl (count_axiom_consts add_theory_const thy)
+ Symtab.empty axioms
val goal_const_tab = get_goal_consts_typs thy goals
- val _ = trace_msg (fn () => ("Initial constants: " ^
- space_implode ", " (Symtab.keys goal_const_tab)));
- val rels = relevant_clauses max_new thy const_tab (pass_mark)
- goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms)
- in
- trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
- rels
- end
- else axioms;
+ val _ =
+ trace_msg (fn () => "Initial constants: " ^
+ commas (Symtab.keys goal_const_tab))
+ val relevant =
+ relevant_clauses ctxt follow_defs max_new relevance_override thy
+ const_tab relevance_threshold goal_const_tab
+ (map (pair_consts_typs_axiom add_theory_const thy)
+ axioms)
+ in
+ trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
+ relevant
+ end
+ else
+ axioms;
(***************************************************************)
(* Retrieving and filtering lemmas *)
@@ -526,34 +543,37 @@
likely to lead to unsound proofs.*)
fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
-fun is_first_order thy goal_cls =
- case translation_mode of
- Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
- | Fol => true
- | Hol => false
+fun is_first_order thy higher_order goal_cls =
+ case higher_order of
+ NONE => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
+ | SOME b => not b
-fun get_relevant_facts max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
+fun get_relevant_facts relevance_threshold higher_order follow_defs max_new
+ add_theory_const relevance_override
+ (ctxt, (chain_ths, th)) goal_cls =
let
val thy = ProofContext.theory_of ctxt
- val is_FO = is_first_order thy goal_cls
+ val is_FO = is_first_order thy higher_order goal_cls
val included_cls = get_all_lemmas ctxt
|> cnf_rules_pairs thy |> make_unique
|> restrict_to_logic thy is_FO
|> remove_unwanted_clauses
in
- relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
+ relevance_filter ctxt relevance_threshold follow_defs max_new
+ add_theory_const relevance_override thy included_cls
+ (map prop_of goal_cls)
end;
(* prepare for passing to writer,
create additional clauses based on the information from extra_cls *)
-fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
+fun prepare_clauses higher_order dfg goal_cls chain_ths axcls extra_cls thy =
let
(* add chain thms *)
val chain_cls =
cnf_rules_pairs thy (filter check_named (map pairname chain_ths))
val axcls = chain_cls @ axcls
val extra_cls = chain_cls @ extra_cls
- val is_FO = is_first_order thy goal_cls
+ val is_FO = is_first_order thy higher_order goal_cls
val ccls = subtract_cls goal_cls extra_cls
val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
val ccltms = map prop_of ccls
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Thu Mar 25 17:56:31 2010 +0100
@@ -51,9 +51,9 @@
conclusion variable to False.*)
fun transform_elim th =
case concl_of th of (*conclusion variable*)
- Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) =>
+ @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
- | v as Var(_, Type("prop",[])) =>
+ | v as Var(_, @{typ prop}) =>
Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
| _ => th;
@@ -76,7 +76,7 @@
fun declare_skofuns s th =
let
val nref = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
+ fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (_, T, p))) (axs, thy) =
(*Existential: declare a Skolem function, then insert into body and continue*)
let
val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
@@ -95,20 +95,20 @@
Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
- | dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx =
+ | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
(*Universal quant: insert a free variable into body and continue*)
let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
in dec_sko (subst_bound (Free (fname, T), p)) thx end
- | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
- | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
- | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
+ | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
+ | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
+ | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
| dec_sko t thx = thx (*Do nothing otherwise*)
in fn thy => dec_sko (Thm.prop_of th) ([], thy) end;
(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skofuns s th =
let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
+ fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs(_,T,p))) defs =
(*Existential: declare a Skolem function, then insert into body and continue*)
let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
@@ -123,13 +123,13 @@
in dec_sko (subst_bound (list_comb(c,args), p))
(def :: defs)
end
- | dec_sko (Const ("All",_) $ Abs (a, T, p)) defs =
+ | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
(*Universal quant: insert a free variable into body and continue*)
let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
in dec_sko (subst_bound (Free(fname,T), p)) defs end
- | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs
+ | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
| dec_sko t defs = defs (*Do nothing otherwise*)
in dec_sko (prop_of th) [] end;
@@ -156,7 +156,7 @@
fun strip_lambdas 0 th = th
| strip_lambdas n th =
case prop_of th of
- _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
+ _ $ (Const (@{const_name "op ="}, _) $ _ $ Abs (x, _, _)) =>
strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
| _ => th;
@@ -171,7 +171,7 @@
let
val thy = theory_of_cterm ct
val Abs(x,_,body) = term_of ct
- val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
+ val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
in
@@ -262,8 +262,9 @@
val (chilbert,cabs) = Thm.dest_comb ch
val thy = Thm.theory_of_cterm chilbert
val t = Thm.term_of chilbert
- val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
- | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
+ val T = case t of
+ Const (@{const_name Eps}, Type (@{type_name fun},[_,T])) => T
+ | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
val cex = Thm.cterm_of thy (HOLogic.exists_const T)
val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
@@ -289,7 +290,7 @@
map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
-(*** Blacklisting (duplicated in "Sledgehammer_Fact_Filter"?) ***)
+(*** Blacklisting (FIXME: duplicated in "Sledgehammer_Fact_Filter"?) ***)
val max_lambda_nesting = 3;
@@ -320,7 +321,8 @@
fun is_strange_thm th =
case head_of (concl_of th) of
- Const (a, _) => (a <> "Trueprop" andalso a <> "==")
+ Const (a, _) => (a <> @{const_name Trueprop} andalso
+ a <> @{const_name "=="})
| _ => false;
fun bad_for_atp th =
@@ -328,9 +330,10 @@
orelse exists_type type_has_topsort (prop_of th)
orelse is_strange_thm th;
+(* FIXME: put other record thms here, or declare as "no_atp" *)
val multi_base_blacklist =
- ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",
- "cases","ext_cases"]; (* FIXME put other record thms here, or declare as "no_atp" *)
+ ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
+ "split_asm", "cases", "ext_cases"];
(*Keep the full complexity of the original name*)
fun flatten_name s = space_implode "_X" (Long_Name.explode s);
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Thu Mar 25 17:56:31 2010 +0100
@@ -48,7 +48,7 @@
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
-(* Parameter t_full below indicates that full type information is to be
+(* Parameter "full_types" below indicates that full type information is to be
exported *)
(* If true, each function will be directly applied to as many arguments as
@@ -210,10 +210,8 @@
fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
| head_needs_hBOOL _ _ = true;
-fun wrap_type t_full (s, tp) =
- if t_full then
- type_wrapper ^ paren_pack [s, string_of_fol_type tp]
- else s;
+fun wrap_type full_types (s, tp) =
+ if full_types then type_wrapper ^ paren_pack [s, string_of_fol_type tp] else s;
fun apply ss = "hAPP" ^ paren_pack ss;
@@ -224,7 +222,7 @@
(*Apply an operator to the argument strings, using either the "apply" operator or
direct function application.*)
-fun string_of_applic t_full cma (CombConst (c, _, tvars), args) =
+fun string_of_applic full_types cma (CombConst (c, _, tvars), args) =
let val c = if c = "equal" then "c_fequal" else c
val nargs = min_arity_of cma c
val args1 = List.take(args, nargs)
@@ -232,21 +230,22 @@
Int.toString nargs ^ " but is applied to " ^
space_implode ", " args)
val args2 = List.drop(args, nargs)
- val targs = if not t_full then map string_of_fol_type tvars else []
+ val targs = if full_types then [] else map string_of_fol_type tvars
in
string_apply (c ^ paren_pack (args1@targs), args2)
end
| string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
| string_of_applic _ _ _ = error "string_of_applic";
-fun wrap_type_if t_full cnh (head, s, tp) =
- if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
+fun wrap_type_if full_types cnh (head, s, tp) =
+ if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else s;
-fun string_of_combterm (params as (t_full, cma, cnh)) t =
+fun string_of_combterm (params as (full_types, cma, cnh)) t =
let val (head, args) = strip_combterm_comb t
- in wrap_type_if t_full cnh (head,
- string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
- type_of_combterm t)
+ in wrap_type_if full_types cnh (head,
+ string_of_applic full_types cma
+ (head, map (string_of_combterm (params)) args),
+ type_of_combterm t)
end;
(*Boolean-valued terms are here converted to literals.*)
@@ -318,11 +317,11 @@
fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
-fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
+fun add_decls (full_types, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
if c = "equal" then (addtypes tvars funcs, preds)
else
let val arity = min_arity_of cma c
- val ntys = if not t_full then length tvars else 0
+ val ntys = if not full_types then length tvars else 0
val addit = Symtab.update(c, arity+ntys)
in
if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
@@ -452,12 +451,12 @@
(* TPTP format *)
-fun write_tptp_file t_full file clauses =
+fun write_tptp_file full_types file clauses =
let
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
- val params = (t_full, cma, cnh)
+ val params = (full_types, cma, cnh)
val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
val _ =
@@ -474,12 +473,12 @@
(* DFG format *)
-fun write_dfg_file t_full file clauses =
+fun write_dfg_file full_types file clauses =
let
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
- val params = (t_full, cma, cnh)
+ val params = (full_types, cma, cnh)
val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
and probname = Path.implode (Path.base file)
val axstrs = map (#1 o (clause2dfg params)) axclauses
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 25 17:56:31 2010 +0100
@@ -4,84 +4,292 @@
Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
*)
-structure Sledgehammer_Isar : sig end =
+signature SLEDGEHAMMER_ISAR =
+sig
+ type params = ATP_Manager.params
+
+ val default_params : theory -> (string * string) list -> params
+end;
+
+structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
struct
+open Sledgehammer_Util
open ATP_Manager
open ATP_Minimal
+open ATP_Wrapper
structure K = OuterKeyword and P = OuterParse
-val _ =
- OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
+fun add_to_relevance_override ns : relevance_override =
+ {add = ns, del = [], only = false}
+fun del_from_relevance_override ns : relevance_override =
+ {add = [], del = ns, only = false}
+fun only_relevance_override ns : relevance_override =
+ {add = ns, del = [], only = true}
+val default_relevance_override = add_to_relevance_override []
+fun merge_relevance_override_pairwise r1 r2 : relevance_override =
+ {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
+ only = #only r1 orelse #only r2}
+fun merge_relevance_overrides rs =
+ fold merge_relevance_override_pairwise rs default_relevance_override
-val _ =
- OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
+type raw_param = string * string list
+
+val default_default_params =
+ [("debug", "false"),
+ ("verbose", "false"),
+ ("relevance_threshold", "50"),
+ ("higher_order", "smart"),
+ ("respect_no_atp", "true"),
+ ("follow_defs", "false"),
+ ("isar_proof", "false"),
+ ("minimize_timeout", "5 s")]
-val _ =
- OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
- (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
- (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
+val negated_params =
+ [("no_debug", "debug"),
+ ("quiet", "verbose"),
+ ("partial_types", "full_types"),
+ ("first_order", "higher_order"),
+ ("ignore_no_atp", "respect_no_atp"),
+ ("dont_follow_defs", "follow_defs"),
+ ("metis_proof", "isar_proof")]
+
+val property_dependent_params = ["atps", "full_types", "timeout"]
+
+fun is_known_raw_param s =
+ AList.defined (op =) default_default_params s orelse
+ AList.defined (op =) negated_params s orelse
+ member (op =) property_dependent_params s
-val _ =
- OuterSyntax.improper_command "print_atps" "print external provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
- Toplevel.keep (print_provers o Toplevel.theory_of)));
+fun check_raw_param (s, _) =
+ if is_known_raw_param s then ()
+ else error ("Unknown parameter: " ^ quote s ^ ".")
+
+fun unnegate_raw_param (name, value) =
+ case AList.lookup (op =) negated_params name of
+ SOME name' => (name', case value of
+ ["false"] => ["true"]
+ | ["true"] => ["false"]
+ | [] => ["false"]
+ | _ => value)
+ | NONE => (name, value)
+
+structure Data = Theory_Data(
+ type T = raw_param list
+ val empty = default_default_params |> map (apsnd single)
+ val extend = I
+ fun merge p : T = AList.merge (op =) (K true) p)
-val _ =
- OuterSyntax.command "sledgehammer"
- "search for first-order proof using automatic theorem provers" K.diag
- (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
+val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
+fun default_raw_params thy =
+ [("atps", [!atps]),
+ ("full_types", [if !full_types then "true" else "false"]),
+ ("timeout", [string_of_int (!timeout) ^ " s"])] @
+ Data.get thy
-val default_minimize_prover = "remote_vampire"
-val default_minimize_time_limit = 5
+val infinity_time_in_secs = 60 * 60 * 24 * 365
+val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
-fun atp_minimize_command args thm_names state =
+fun extract_params thy default_params override_params =
let
- fun theorems_from_names ctxt =
- map (fn (name, interval) =>
+ val override_params = map unnegate_raw_param override_params
+ val raw_params = rev override_params @ rev default_params
+ val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
+ val lookup_string = the_default "" o lookup
+ fun general_lookup_bool option default_value name =
+ case lookup name of
+ SOME s => parse_bool_option option name s
+ | NONE => default_value
+ 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)
+ fun lookup_int name =
+ case lookup name of
+ NONE => 0
+ | SOME s => case Int.fromString s of
+ SOME n => n
+ | NONE => error ("Parameter " ^ quote name ^
+ " must be assigned an integer value.")
+ val debug = lookup_bool "debug"
+ val verbose = debug orelse lookup_bool "verbose"
+ val atps = lookup_string "atps" |> space_explode " "
+ val full_types = lookup_bool "full_types"
+ val relevance_threshold =
+ 0.01 * Real.fromInt (lookup_int "relevance_threshold")
+ val higher_order = lookup_bool_option "higher_order"
+ val respect_no_atp = lookup_bool "respect_no_atp"
+ val follow_defs = lookup_bool "follow_defs"
+ val isar_proof = lookup_bool "isar_proof"
+ val timeout = lookup_time "timeout"
+ val minimize_timeout = lookup_time "minimize_timeout"
+ in
+ {debug = debug, verbose = verbose, atps = atps, full_types = full_types,
+ relevance_threshold = relevance_threshold, higher_order = higher_order,
+ respect_no_atp = respect_no_atp, follow_defs = follow_defs,
+ isar_proof = isar_proof, timeout = timeout,
+ minimize_timeout = minimize_timeout}
+ end
+
+fun get_params thy = extract_params thy (default_raw_params thy)
+fun default_params thy = get_params thy o map (apsnd single)
+
+fun atp_minimize_command override_params old_style_args fact_refs state =
+ let
+ val thy = Proof.theory_of state
+ val ctxt = Proof.context_of state
+ fun theorems_from_refs ctxt =
+ map (fn fact_ref =>
let
- val thmref = Facts.Named ((name, Position.none), interval)
- val ths = ProofContext.get_fact ctxt thmref
- val name' = Facts.string_of_ref thmref
+ val ths = ProofContext.get_fact ctxt fact_ref
+ val name' = Facts.string_of_ref fact_ref
in (name', ths) end)
- fun get_time_limit_arg time_string =
- (case Int.fromString time_string of
- SOME t => t
- | NONE => error ("Invalid time limit: " ^ quote time_string))
+ fun get_time_limit_arg s =
+ (case Int.fromString s of
+ SOME t => Time.fromSeconds t
+ | NONE => error ("Invalid time limit: " ^ quote s))
fun get_opt (name, a) (p, t) =
(case name of
"time" => (p, get_time_limit_arg a)
| "atp" => (a, t)
| n => error ("Invalid argument: " ^ n))
- fun get_options args =
- fold get_opt args (default_minimize_prover, default_minimize_time_limit)
- val (prover_name, time_limit) = get_options args
+ val {atps, minimize_timeout, ...} = get_params thy override_params
+ val (atp, timeout) = fold get_opt old_style_args (hd atps, minimize_timeout)
+ val params =
+ get_params thy
+ [("atps", [atp]),
+ ("minimize_timeout",
+ [string_of_int (Time.toSeconds timeout) ^ " s"])]
val prover =
- (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
+ (case get_prover thy atp of
SOME prover => prover
- | NONE => error ("Unknown prover: " ^ quote prover_name))
- val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
+ | NONE => error ("Unknown ATP: " ^ quote atp))
+ val name_thms_pairs = theorems_from_refs ctxt fact_refs
in
- writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
- state name_thms_pairs))
+ writeln (#2 (minimize_theorems params linear_minimize prover atp state
+ name_thms_pairs))
+ end
+
+val runN = "run"
+val minimizeN = "minimize"
+val messagesN = "messages"
+val available_atpsN = "available_atps"
+val running_atpsN = "running_atps"
+val kill_atpsN = "kill_atps"
+val refresh_tptpN = "refresh_tptp"
+val helpN = "help"
+
+val addN = "add"
+val delN = "del"
+val onlyN = "only"
+
+fun hammer_away override_params subcommand opt_i relevance_override state =
+ let
+ val thy = Proof.theory_of state
+ val _ = List.app check_raw_param override_params
+ in
+ if subcommand = runN then
+ sledgehammer (get_params thy override_params) (the_default 1 opt_i)
+ relevance_override state
+ else if subcommand = minimizeN then
+ atp_minimize_command override_params [] (#add relevance_override) state
+ else if subcommand = messagesN then
+ messages opt_i
+ else if subcommand = available_atpsN then
+ available_atps thy
+ else if subcommand = running_atpsN then
+ running_atps ()
+ else if subcommand = kill_atpsN then
+ kill_atps ()
+ else if subcommand = refresh_tptpN then
+ refresh_systems_on_tptp ()
+ else
+ error ("Unknown subcommand: " ^ quote subcommand ^ ".")
end
-local structure K = OuterKeyword and P = OuterParse in
+fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) =
+ Toplevel.keep (hammer_away params subcommand opt_i relevance_override
+ o Toplevel.proof_of)
+
+fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value
+
+fun sledgehammer_params_trans params =
+ Toplevel.theory
+ (fold set_default_raw_param params
+ #> tap (fn thy =>
+ writeln ("Default parameters for Sledgehammer:\n" ^
+ (case rev (default_raw_params thy) of
+ [] => "none"
+ | params =>
+ (map check_raw_param params;
+ params |> map string_for_raw_param
+ |> sort_strings |> cat_lines)))))
-val parse_args =
- Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
-val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
+val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
+val parse_value = Scan.repeat1 P.xname
+val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
+val parse_params = Scan.optional (Args.bracks (P.list parse_param)) []
+val parse_fact_refs =
+ Scan.repeat1 (Scan.unless (P.name -- Args.colon)
+ (P.xname -- Scan.option Attrib.thm_sel)
+ >> (fn (name, interval) =>
+ Facts.Named ((name, Position.none), interval)))
+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)
+ || (P.$$$ onlyN |-- Args.colon |-- parse_fact_refs >> only_relevance_override)
+val parse_relevance_override =
+ Scan.optional (Args.parens
+ (Scan.optional (parse_fact_refs >> only_relevance_override)
+ default_relevance_override
+ -- Scan.repeat parse_relevance_chunk)
+ >> op :: >> merge_relevance_overrides)
+ default_relevance_override
+val parse_sledgehammer_command =
+ (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
+ -- Scan.option P.nat) #>> sledgehammer_trans
+val parse_sledgehammer_params_command =
+ parse_params #>> sledgehammer_params_trans
+
+val parse_minimize_args =
+ Scan.optional (Args.bracks (P.list (P.short_ident --| P.$$$ "=" -- P.xname)))
+ []
+val _ =
+ OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_atps))
+val _ =
+ OuterSyntax.improper_command "atp_info"
+ "print information about managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative running_atps))
+val _ =
+ OuterSyntax.improper_command "atp_messages"
+ "print recent messages issued by managed provers" K.diag
+ (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
+ (fn limit => Toplevel.no_timing
+ o Toplevel.imperative (fn () => messages limit)))
+val _ =
+ OuterSyntax.improper_command "print_atps" "print external provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+ Toplevel.keep (available_atps o Toplevel.theory_of)))
+val _ =
+ OuterSyntax.improper_command "atp_minimize"
+ "minimize theorem list with external prover" K.diag
+ (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) =>
+ Toplevel.no_timing o Toplevel.unknown_proof o
+ Toplevel.keep (atp_minimize_command [] args fact_refs
+ o Toplevel.proof_of)))
val _ =
- OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
- (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
- Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
-
-end
+ OuterSyntax.improper_command "sledgehammer"
+ "search for first-order proof using automatic theorem provers" K.diag
+ parse_sledgehammer_command
+val _ =
+ OuterSyntax.command "sledgehammer_params"
+ "set and display the default parameters for Sledgehammer" K.thy_decl
+ parse_sledgehammer_params_command
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Mar 25 17:56:31 2010 +0100
@@ -339,18 +339,18 @@
let
val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n")
val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt)
- fun have_or_show "show" _ = "show \""
- | have_or_show have lname = have ^ " " ^ lname ^ ": \""
+ fun have_or_show "show" _ = " show \""
+ | have_or_show have lname = " " ^ have ^ " " ^ lname ^ ": \""
fun do_line _ (lname, t, []) =
(* No deps: it's a conjecture clause, with no proof. *)
(case permuted_clause t ctms of
- SOME u => "assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
+ SOME u => " assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
| NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
[t]))
| do_line have (lname, t, deps) =
have_or_show have lname ^
string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^
- "\"\n by (metis " ^ space_implode " " deps ^ ")\n"
+ "\"\n by (metis " ^ space_implode " " deps ^ ")\n"
fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)]
| do_lines ((lname, t, deps) :: lines) =
do_line "have" (lname, t, deps) :: do_lines lines
@@ -535,18 +535,20 @@
val kill_chained = filter_out (curry (op =) chained_hint)
(* metis-command *)
-fun metis_line [] = "apply metis"
- | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
+fun metis_line [] = "by metis"
+ | metis_line xs = "by (metis " ^ space_implode " " xs ^ ")"
-(* atp_minimize [atp=<prover>] <lemmas> *)
fun minimize_line _ [] = ""
- | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
- Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^
- space_implode " " (kill_chained lemmas))
+ | minimize_line name lemmas =
+ "To minimize the number of lemmas, try this command:\n" ^
+ Markup.markup Markup.sendback
+ ("sledgehammer minimize [atps = " ^ name ^ "] (" ^
+ space_implode " " (kill_chained lemmas) ^ ")") ^ "."
fun metis_lemma_list dfg name result =
let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in
- (Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ "\n" ^
+ ("Try this command: " ^
+ Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ ".\n" ^
minimize_line name lemmas ^
(if used_conj then
""
@@ -570,8 +572,11 @@
if member (op =) tokens chained_hint then ""
else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names
in
- (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback isar_proof,
- lemma_names)
+ (* Hack: The " \n" shouldn't be part of the markup. This is a workaround
+ for a strange ProofGeneral bug, whereby the first two letters of the word
+ "proof" are not highlighted. *)
+ (one_line_proof ^ "\n\nStructured proof:" ^
+ Markup.markup Markup.sendback (" \n" ^ isar_proof), lemma_names)
end
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Mar 25 17:56:31 2010 +0100
@@ -0,0 +1,53 @@
+(* Title: HOL/Sledgehammer/sledgehammer_util.ML
+ Author: Jasmin Blanchette, TU Muenchen
+
+General-purpose functions used by the Sledgehammer modules.
+*)
+
+signature SLEDGEHAMMER_UTIL =
+sig
+ val serial_commas : string -> string list -> string list
+ val parse_bool_option : bool -> string -> string -> bool option
+ val parse_time_option : string -> string -> Time.time option
+end;
+
+structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
+struct
+
+fun serial_commas _ [] = ["??"]
+ | serial_commas _ [s] = [s]
+ | serial_commas conj [s1, s2] = [s1, conj, s2]
+ | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
+ | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
+
+fun parse_bool_option option name s =
+ (case s of
+ "smart" => if option then NONE else raise Option
+ | "false" => SOME false
+ | "true" => SOME true
+ | "" => SOME true
+ | _ => raise Option)
+ handle Option.Option =>
+ let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
+ error ("Parameter " ^ quote name ^ " must be assigned " ^
+ space_implode " " (serial_commas "or" ss) ^ ".")
+ end
+
+fun parse_time_option _ "none" = NONE
+ | parse_time_option name s =
+ let
+ val msecs =
+ case space_explode " " s of
+ [s1, "min"] => 60000 * the (Int.fromString s1)
+ | [s1, "s"] => 1000 * the (Int.fromString s1)
+ | [s1, "ms"] => the (Int.fromString s1)
+ | _ => 0
+ in
+ if msecs <= 0 then
+ error ("Parameter " ^ quote name ^ " must be assigned a positive time \
+ \value (e.g., \"60 s\", \"200 ms\") or \"none\".")
+ else
+ SOME (Time.fromMilliseconds msecs)
+ end
+
+end;