--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Apr 20 15:17:18 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Apr 20 16:04:49 2010 +0200
@@ -391,7 +391,7 @@
|> 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 1
+ val minimize = minimize_theorems params prover prover_name 1
val _ = log separator
in
case minimize st (these (!named_thms)) of
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Apr 20 15:17:18 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Apr 20 16:04:49 2010 +0200
@@ -15,10 +15,11 @@
overlord: bool,
atps: string list,
full_types: bool,
+ explicit_apply: bool,
respect_no_atp: bool,
relevance_threshold: real,
convergence: real,
- theory_const: bool option,
+ theory_relevant: bool option,
higher_order: bool option,
follow_defs: bool,
isar_proof: bool,
@@ -57,6 +58,7 @@
structure ATP_Manager : ATP_MANAGER =
struct
+open Sledgehammer_Util
open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
@@ -68,10 +70,11 @@
overlord: bool,
atps: string list,
full_types: bool,
+ explicit_apply: bool,
respect_no_atp: bool,
relevance_threshold: real,
convergence: real,
- theory_const: bool option,
+ theory_relevant: bool option,
higher_order: bool option,
follow_defs: bool,
isar_proof: bool,
@@ -189,14 +192,21 @@
val min_wait_time = Time.fromMilliseconds 300;
val max_wait_time = Time.fromSeconds 10;
+(* This is a workaround for Proof General's off-by-a-few sendback display bug,
+ whereby "pr" in "proof" is not highlighted. *)
+val break_into_chunks =
+ map (replace_all "\n\n" "\000") #> maps (space_explode "\000")
+
fun print_new_messages () =
- let val msgs = Synchronized.change_result global_state
- (fn {manager, timeout_heap, active, cancelling, messages, store} =>
- (messages, make_state manager timeout_heap active cancelling [] store))
- in
- if null msgs then ()
- else priority ("Sledgehammer: " ^ space_implode "\n\n" msgs)
- end;
+ case Synchronized.change_result global_state
+ (fn {manager, timeout_heap, active, cancelling, messages, store} =>
+ (messages, make_state manager timeout_heap active cancelling []
+ store)) of
+ [] => ()
+ | msgs =>
+ msgs |> break_into_chunks
+ |> (fn msg :: msgs => "Sledgehammer: " ^ msg :: msgs)
+ |> List.app priority
fun check_thread_manager params = Synchronized.change global_state
(fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
@@ -289,7 +299,7 @@
space_implode "\n\n"
("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling);
- in writeln (running ^ "\n" ^ interrupting) end;
+ in priority (running ^ "\n" ^ interrupting) end;
fun messages opt_limit =
let
@@ -298,15 +308,14 @@
val header =
"Recent ATP messages" ^
(if length store <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
- in writeln (space_implode "\n\n" (header :: #1 (chop limit store))) end;
-
+ in List.app priority (header :: break_into_chunks (#1 (chop limit store))) end
(** The Sledgehammer **)
(* named provers *)
-fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
+fun err_dup_prover name = error ("Duplicate prover: " ^ quote name ^ ".");
structure Provers = Theory_Data
(
@@ -324,8 +333,9 @@
fun get_prover thy name =
Option.map #1 (Symtab.lookup (Provers.get thy) name);
-fun available_atps thy = Pretty.writeln
- (Pretty.strs ("ATPs:" :: sort_strings (Symtab.keys (Provers.get thy))));
+fun available_atps thy =
+ priority ("Available ATPs: " ^
+ commas (sort_strings (Symtab.keys (Provers.get thy))) ^ ".")
(* start prover thread *)
@@ -333,7 +343,7 @@
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 ATP: " ^ quote name)
+ NONE => warning ("Unknown ATP: " ^ quote name ^ ".")
| SOME prover =>
let
val {context = ctxt, facts, goal} = Proof.goal proof_state;
@@ -352,7 +362,7 @@
val message = #message (prover params timeout problem)
handle Sledgehammer_HOL_Clause.TRIVIAL =>
metis_line i n []
- | ERROR msg => ("Error: " ^ msg);
+ | ERROR msg => "Error: " ^ msg ^ ".\n";
val _ = unregister params message (Thread.self ());
in () end);
in () end);
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Tue Apr 20 15:17:18 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Tue Apr 20 16:04:49 2010 +0200
@@ -9,13 +9,9 @@
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
- val linear_minimize : 'a minimize_fun
- val binary_minimize : 'a minimize_fun
val minimize_theorems :
- params -> (string * thm list) minimize_fun -> prover -> string -> int
- -> Proof.state -> (string * thm list) list
+ params -> prover -> string -> int -> Proof.state -> (string * thm list) list
-> (string * thm list) list option * string
end;
@@ -27,62 +23,24 @@
open Sledgehammer_Proof_Reconstruct
open ATP_Manager
-type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
-
(* Linear minimization algorithm *)
-fun linear_minimize p s =
+fun linear_minimize test s =
let
- fun aux [] needed = needed
- | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x)
- in aux s [] end;
-
-(* Binary minimalization *)
-
-local
- fun isplit (l, r) [] = (l, r)
- | isplit (l, r) [h] = (h :: l, r)
- | isplit (l, r) (h1 :: h2 :: t) = isplit (h1 :: l, h2 :: r) t
-in
- fun split lst = isplit ([], []) lst
-end
-
-local
- fun min _ _ [] = raise Empty
- | min _ _ [s0] = [s0]
- | min p sup s =
- let
- val (l0, r0) = split s
- in
- if p (sup @ l0) then
- min p sup l0
- else if p (sup @ r0) then
- min p sup r0
- else
- let
- val l = min p (sup @ r0) l0
- val r = min p (sup @ l) r0
- in l @ r end
- end
-in
- (* return a minimal subset v of s that satisfies p
- @pre p(s) & ~p([]) & monotone(p)
- @post v subset s & p(v) &
- forall e in v. ~p(v \ e)
- *)
- fun binary_minimize p s =
- case min p [] s of
- [x] => if p [] then [] else [x]
- | m => m
-end
+ fun aux [] p = p
+ | aux (x :: xs) (needed, result) =
+ case test (xs @ needed) of
+ SOME result => aux xs (needed, result)
+ | NONE => aux xs (x :: needed, result)
+ in aux s end
(* failure check and producing answer *)
-datatype 'a prove_result = Success of 'a | Failure | Timeout | Error
+datatype outcome = Success | Failure | Timeout | Error
-val string_of_result =
- fn Success _ => "Success"
+val string_of_outcome =
+ fn Success => "Success"
| Failure => "Failure"
| Timeout => "Timeout"
| Error => "Error"
@@ -94,26 +52,19 @@
("# Cannot determine problem status within resource limit", Timeout),
("Error", Error)]
-fun produce_answer ({success, proof, internal_thm_names, filtered_clauses, ...}
- : prover_result) =
+fun outcome_of_result (result as {success, proof, ...} : prover_result) =
if success then
- (Success (Vector.foldr (op ::) [] internal_thm_names, filtered_clauses),
- proof)
- else
- let
- val failure = failure_strings |> get_first (fn (s, t) =>
- if String.isSubstring s proof then SOME (t, proof) else NONE)
- in
- (case failure of
- SOME res => res
- | NONE => (Failure, proof))
- end
-
+ Success
+ else case get_first (fn (s, outcome) =>
+ if String.isSubstring s proof then SOME outcome
+ else NONE) failure_strings of
+ SOME outcome => outcome
+ | NONE => Failure
(* wrapper for calling external prover *)
fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
- timeout subgoal state filtered name_thms_pairs =
+ timeout subgoal state filtered_clauses name_thms_pairs =
let
val num_theorems = length name_thms_pairs
val _ = priority ("Testing " ^ string_of_int num_theorems ^
@@ -124,50 +75,61 @@
val problem =
{subgoal = subgoal, 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
-
+ axiom_clauses = SOME axclauses,
+ filtered_clauses = SOME (the_default axclauses filtered_clauses)}
+ in
+ `outcome_of_result (prover params timeout problem)
+ |>> tap (priority o string_of_outcome)
+ end
(* minimalization of thms *)
-fun minimize_theorems (params as {minimize_timeout, ...}) gen_min prover
- prover_name i state name_thms_pairs =
+fun minimize_theorems (params as {minimize_timeout, isar_proof, modulus,
+ sorts, ...})
+ prover atp_name i state name_thms_pairs =
let
val msecs = Time.toMilliseconds minimize_timeout
+ val n = length name_thms_pairs
val _ =
- priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
- " theorems, ATP: " ^ prover_name ^
- ", time limit: " ^ string_of_int msecs ^ " ms")
+ priority ("Sledgehammer minimizer: ATP " ^ quote atp_name ^
+ " with a time limit of " ^ string_of_int msecs ^ " ms.")
val test_thms_fun =
sledgehammer_test_theorems params prover minimize_timeout i state
fun test_thms filtered thms =
- case test_thms_fun filtered thms of (Success _, _) => true | _ => false
- val n = state |> Proof.raw_goal |> #goal |> prop_of |> Logic.count_prems
+ case test_thms_fun filtered thms of
+ (Success, result) => SOME result
+ | _ => NONE
+
+ val {context = ctxt, facts, goal} = Proof.goal state;
+ val n = Logic.count_prems (prop_of goal)
in
(* try prove first to check result and get used theorems *)
(case test_thms_fun NONE name_thms_pairs of
- (Success (used, filtered), _) =>
+ (Success, result as {internal_thm_names, filtered_clauses, ...}) =>
let
- val ordered_used = sort_distinct string_ord used
+ val used = internal_thm_names |> Vector.foldr (op ::) []
+ |> sort_distinct string_ord
val to_use =
- if length ordered_used < length name_thms_pairs then
- filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
+ if length used < length name_thms_pairs then
+ filter (fn (name1, _) => List.exists (curry (op =) name1) used)
+ name_thms_pairs
else name_thms_pairs
- val min_thms =
- if null to_use then []
- else gen_min (test_thms (SOME filtered)) to_use
- val min_names = sort_distinct string_ord (map fst min_thms)
+ val (min_thms, {proof, internal_thm_names, ...}) =
+ linear_minimize (test_thms (SOME filtered_clauses)) to_use
+ ([], result)
+ val n = length min_thms
val _ = priority (cat_lines
- ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
- in (SOME min_thms, metis_line i n min_names) end
+ ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
+ in
+ (SOME min_thms,
+ proof_text isar_proof true modulus sorts atp_name proof
+ internal_thm_names ctxt goal i |> fst)
+ end
| (Timeout, _) =>
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \
\option (e.g., \"timeout = " ^
string_of_int (10 + msecs div 1000) ^ " s\").")
- | (Error, msg) =>
- (NONE, "Error in prover: " ^ msg)
+ | (Error, {message, ...}) => (NONE, "ATP error: " ^ message)
| (Failure, _) =>
(* Failure sometimes mean timeout, unfortunately. *)
(NONE, "Failure: No proof was found with the current time limit. You \
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Apr 20 15:17:18 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Apr 20 16:04:49 2010 +0200
@@ -48,7 +48,7 @@
arguments: Time.time -> string,
failure_strs: string list,
max_new_clauses: int,
- prefers_theory_const: bool,
+ prefers_theory_relevant: bool,
supports_isar_proofs: bool};
@@ -67,7 +67,7 @@
| (failure :: _) => SOME failure
fun generic_prover overlord get_facts prepare write_file cmd args failure_strs
- produce_answer name ({debug, full_types, ...} : params)
+ proof_text name ({debug, full_types, explicit_apply, ...} : params)
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
: problem) =
let
@@ -128,7 +128,7 @@
if Config.get ctxt measure_runtime then split_time s else (s, 0)
fun run_on probfile =
if File.exists cmd then
- write_file debug full_types probfile clauses
+ write_file full_types explicit_apply probfile clauses
|> pair (apfst split_time' (bash_output (cmd_line probfile)))
else error ("Bad executable: " ^ Path.implode cmd ^ ".");
@@ -142,7 +142,7 @@
File.write (Path.explode (Path.implode probfile ^ "_proof"))
("% " ^ timestamp () ^ "\n" ^ proof)
- val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
+ val (((proof, atp_run_time_in_msecs), rc), _) =
with_path cleanup export run_on (prob_pathname subgoal);
(* Check for success and print out some information on failure. *)
@@ -151,9 +151,7 @@
val (message, relevant_thm_names) =
if is_some failure then ("ATP failed to find a proof.\n", [])
else if rc <> 0 then ("ATP error: " ^ proof ^ ".\n", [])
- else
- (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th,
- subgoal));
+ else proof_text name proof internal_thm_names ctxt th subgoal
in
{success = success, message = message,
relevant_thm_names = relevant_thm_names,
@@ -167,21 +165,20 @@
fun generic_tptp_prover
(name, {command, arguments, failure_strs, max_new_clauses,
- prefers_theory_const, supports_isar_proofs})
+ prefers_theory_relevant, supports_isar_proofs})
(params as {overlord, respect_no_atp, relevance_threshold, convergence,
- theory_const, higher_order, follow_defs, isar_proof,
+ theory_relevant, higher_order, follow_defs, isar_proof,
modulus, sorts, ...})
timeout =
generic_prover overlord
(get_relevant_facts respect_no_atp relevance_threshold convergence
higher_order follow_defs max_new_clauses
- (the_default prefers_theory_const theory_const))
- (prepare_clauses higher_order false) write_tptp_file command
+ (the_default prefers_theory_relevant theory_relevant))
+ (prepare_clauses higher_order false)
+ (write_tptp_file (overlord andalso not isar_proof)) command
(arguments timeout) failure_strs
- (if supports_isar_proofs andalso isar_proof then
- structured_isar_proof modulus sorts
- else
- metis_lemma_list false) name params;
+ (proof_text (supports_isar_proofs andalso isar_proof) false modulus sorts)
+ name params
fun tptp_prover name p = (name, generic_tptp_prover (name, p));
@@ -201,7 +198,7 @@
failure_strs =
["Satisfiability detected", "Refutation not found", "CANNOT PROVE"],
max_new_clauses = 60,
- prefers_theory_const = false,
+ prefers_theory_relevant = false,
supports_isar_proofs = true}
val vampire = tptp_prover "vampire" vampire_config
@@ -218,7 +215,7 @@
"SZS status: ResourceOut", "SZS status ResourceOut",
"# Cannot determine problem status"],
max_new_clauses = 100,
- prefers_theory_const = false,
+ prefers_theory_relevant = false,
supports_isar_proofs = true}
val e = tptp_prover "e" e_config
@@ -227,29 +224,32 @@
fun generic_dfg_prover
(name, ({command, arguments, failure_strs, max_new_clauses,
- prefers_theory_const, ...} : prover_config))
+ prefers_theory_relevant, ...} : prover_config))
(params as {overlord, respect_no_atp, relevance_threshold, convergence,
- theory_const, higher_order, follow_defs, ...})
+ theory_relevant, higher_order, follow_defs, ...})
timeout =
generic_prover overlord
(get_relevant_facts respect_no_atp relevance_threshold convergence
higher_order follow_defs max_new_clauses
- (the_default prefers_theory_const theory_const))
+ (the_default prefers_theory_relevant theory_relevant))
(prepare_clauses higher_order true) write_dfg_file command
- (arguments timeout) failure_strs (metis_lemma_list true) name params;
+ (arguments timeout) failure_strs (metis_proof_text false false)
+ name params
fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
+(* The "-VarWeight=3" option helps the higher-order problems, probably by
+ counteracting the presence of "hAPP". *)
val spass_config : prover_config =
{command = Path.explode "$SPASS_HOME/SPASS",
arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
- " -FullRed=0 -DocProof -TimeLimit=" ^
+ " -FullRed=0 -DocProof -VarWeight=3 -TimeLimit=" ^
string_of_int (generous_to_secs timeout)),
failure_strs =
["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
"SPASS beiseite: Maximal number of loops exceeded."],
max_new_clauses = 40,
- prefers_theory_const = true,
+ prefers_theory_relevant = true,
supports_isar_proofs = false}
val spass = dfg_prover ("spass", spass_config)
@@ -283,7 +283,7 @@
val remote_failure_strs = ["Remote-script could not extract proof"];
fun remote_prover_config prover_prefix args
- ({failure_strs, max_new_clauses, prefers_theory_const, ...}
+ ({failure_strs, max_new_clauses, prefers_theory_relevant, ...}
: prover_config) : prover_config =
{command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
arguments = (fn timeout =>
@@ -291,7 +291,7 @@
the_system prover_prefix),
failure_strs = remote_failure_strs @ failure_strs,
max_new_clauses = max_new_clauses,
- prefers_theory_const = prefers_theory_const,
+ prefers_theory_relevant = prefers_theory_relevant,
supports_isar_proofs = false}
val remote_vampire =
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Apr 20 15:17:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Apr 20 16:04:49 2010 +0200
@@ -693,13 +693,19 @@
val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
if common_thm used cls then NONE else SOME name)
in
- if null unused then ()
- else warning ("Metis: unused theorems " ^ commas_quote unused);
+ if not (common_thm used cls) then
+ warning "Metis: The goal is provable because the context is \
+ \inconsistent."
+ else if not (null unused) then
+ warning ("Metis: Unused theorems: " ^ commas_quote unused
+ ^ ".")
+ else
+ ();
case result of
(_,ith)::_ =>
- (trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith);
+ (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
[ith])
- | _ => (trace_msg (fn () => "Metis: no result");
+ | _ => (trace_msg (fn () => "Metis: No result");
[])
end
| Metis.Resolution.Satisfiable _ =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Apr 20 15:17:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Apr 20 16:04:49 2010 +0200
@@ -127,8 +127,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 theory_relevant th =
+ if theory_relevant then
let val name = Context.theory_name (theory_of_thm th)
val t = Const (name ^ ". 1", HOLogic.boolT)
in t $ prop_of th end
@@ -157,7 +157,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 theory_relevant 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.*)
@@ -170,7 +170,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 theory_relevant thm, tab) end;
(**** Actual Filtering Code ****)
@@ -201,8 +201,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 (p as (thm, _)) =
- (p, (consts_typs_of_term thy (const_prop_of theory_const thm)));
+fun pair_consts_typs_axiom theory_relevant thy (p as (thm, _)) =
+ (p, (consts_typs_of_term thy (const_prop_of theory_relevant thm)));
exception ConstFree;
fun dest_ConstFree (Const aT) = aT
@@ -254,8 +254,10 @@
fun relevant_clauses ctxt convergence follow_defs max_new
(relevance_override as {add, del, only}) thy ctab =
let
- val add_thms = maps (ProofContext.get_fact ctxt) add
- val del_thms = maps (ProofContext.get_fact ctxt) del
+ val thms_for_facts =
+ maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt)
+ val add_thms = thms_for_facts add
+ val del_thms = thms_for_facts del
fun iter p rel_consts =
let
fun relevant ([], _) [] = [] (* Nothing added this iteration *)
@@ -294,10 +296,10 @@
in iter end
fun relevance_filter ctxt relevance_threshold convergence follow_defs max_new
- theory_const relevance_override thy axioms goals =
+ theory_relevant relevance_override thy axioms goals =
if relevance_threshold > 0.0 then
let
- val const_tab = List.foldl (count_axiom_consts theory_const thy)
+ val const_tab = List.foldl (count_axiom_consts theory_relevant thy)
Symtab.empty axioms
val goal_const_tab = get_goal_consts_typs thy goals
val _ =
@@ -306,7 +308,8 @@
val relevant =
relevant_clauses ctxt convergence follow_defs max_new relevance_override
thy const_tab relevance_threshold goal_const_tab
- (map (pair_consts_typs_axiom theory_const thy) axioms)
+ (map (pair_consts_typs_axiom theory_relevant thy)
+ axioms)
in
trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
relevant
@@ -365,11 +368,11 @@
val ths = filter_out bad_for_atp ths0;
in
if Facts.is_concealed facts name orelse null ths orelse
- respect_no_atp andalso is_package_def name then I
- else
- (case find_first check_thms [name1, name2, name] of
- NONE => I
- | SOME a => cons (a, ths))
+ (respect_no_atp andalso is_package_def name) then
+ I
+ else case find_first check_thms [name1, name2, name] of
+ NONE => I
+ | SOME a => cons (a, ths)
end);
in valid_facts global_facts @ valid_facts local_facts end;
@@ -502,7 +505,7 @@
| SOME b => not b
fun get_relevant_facts respect_no_atp relevance_threshold convergence
- higher_order follow_defs max_new theory_const
+ higher_order follow_defs max_new theory_relevant
(relevance_override as {add, only, ...})
(ctxt, (chain_ths, th)) goal_cls =
if (only andalso null add) orelse relevance_threshold > 1.0 then
@@ -517,7 +520,7 @@
|> remove_unwanted_clauses
in
relevance_filter ctxt relevance_threshold convergence follow_defs max_new
- theory_const relevance_override thy included_cls
+ theory_relevant relevance_override thy included_cls
(map prop_of goal_cls)
end
@@ -527,7 +530,8 @@
let
(* add chain thms *)
val chain_cls =
- cnf_rules_pairs thy (filter check_named (map pairname chain_ths))
+ cnf_rules_pairs thy (filter check_named
+ (map (`Thm.get_name_hint) chain_ths))
val axcls = chain_cls @ axcls
val extra_cls = chain_cls @ extra_cls
val is_FO = is_first_order thy higher_order goal_cls
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Apr 20 15:17:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Apr 20 16:04:49 2010 +0200
@@ -10,7 +10,6 @@
val trace_msg: (unit -> string) -> unit
val skolem_prefix: string
val cnf_axiom: theory -> thm -> thm list
- val pairname: thm -> string * thm
val multi_base_blacklist: string list
val bad_for_atp: thm -> bool
val type_has_topsort: typ -> bool
@@ -370,7 +369,7 @@
val update_cache = ThmCache.map o apfst o Thmtab.update;
fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ())));
-(*Exported function to convert Isabelle theorems into axiom clauses*)
+(* Convert Isabelle theorems into axiom clauses. *)
fun cnf_axiom thy th0 =
let val th = Thm.transfer thy th0 in
case lookup_cache thy th of
@@ -379,11 +378,6 @@
end;
-(**** Rules from the context ****)
-
-fun pairname th = (Thm.get_name_hint th, th);
-
-
(**** Translate a set of theorems into CNF ****)
fun pair_name_cls k (n, []) = []
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue Apr 20 15:17:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue Apr 20 16:04:49 2010 +0200
@@ -4,7 +4,7 @@
Storing/printing FOL clauses and arity clauses. Typed equality is
treated differently.
-FIXME: combine with res_hol_clause!
+FIXME: combine with sledgehammer_hol_clause!
*)
signature SLEDGEHAMMER_FOL_CLAUSE =
@@ -57,12 +57,14 @@
val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list
val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
- val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table
- val add_classrel_clause_preds : classrel_clause * int Symtab.table -> int Symtab.table
+ val add_type_sort_preds: typ -> int Symtab.table -> int Symtab.table
+ val add_classrel_clause_preds :
+ classrel_clause -> int Symtab.table -> int Symtab.table
val class_of_arityLit: arLit -> class
- val add_arity_clause_preds: arity_clause * int Symtab.table -> int Symtab.table
- val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table
- val add_arity_clause_funcs: arity_clause * int Symtab.table -> int Symtab.table
+ val add_arity_clause_preds: arity_clause -> int Symtab.table -> int Symtab.table
+ val add_fol_type_funcs: fol_type -> int Symtab.table -> int Symtab.table
+ val add_arity_clause_funcs:
+ arity_clause -> int Symtab.table -> int Symtab.table
val init_functab: int Symtab.table
val dfg_sign: bool -> string -> string
val dfg_of_typeLit: bool -> type_literal -> string
@@ -102,7 +104,7 @@
val tconst_prefix = "tc_";
val class_prefix = "class_";
-fun union_all xss = List.foldl (uncurry (union (op =))) [] xss;
+fun union_all xss = fold (union (op =)) xss []
(* Provide readable names for the more common symbolic functions *)
val const_trans_table =
@@ -218,7 +220,8 @@
type name = string * string
type name_pool = string Symtab.table * string Symtab.table
-fun empty_name_pool debug = if debug then SOME (`I Symtab.empty) else NONE
+fun empty_name_pool readable_names =
+ if readable_names then SOME (`I Symtab.empty) else NONE
fun pool_map f xs =
fold_rev (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs
@@ -240,7 +243,7 @@
fun translate_first_char f s =
String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
-fun clean_short_name full_name s =
+fun readable_name full_name s =
let
val s = s |> Long_Name.base_name
|> fold remove_all ["\<^sub>", "\<^bsub>", "\<^esub>", "\<^isub>"]
@@ -249,7 +252,8 @@
(s' |> rev
|> implode
|> String.translate
- (fn c => if Char.isAlphaNum c then String.str c else ""))
+ (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
+ else ""))
^ replicate_string (String.size s - length s') "_"
val s' =
if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
@@ -267,8 +271,8 @@
| nice_name (full_name, desired_name) (SOME the_pool) =
case Symtab.lookup (fst the_pool) full_name of
SOME nice_name => (nice_name, SOME the_pool)
- | NONE => add_nice_name full_name (clean_short_name full_name desired_name)
- 0 the_pool
+ | NONE => add_nice_name full_name (readable_name full_name desired_name) 0
+ the_pool
|> apsnd SOME
(**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG
@@ -315,7 +319,7 @@
| pred_of_sort (LTFree (s,ty)) = (s,1)
(*Given a list of sorted type variables, return a list of type literals.*)
-fun add_typs Ts = List.foldl (uncurry (union (op =))) [] (map sorts_on_typs Ts);
+fun add_typs Ts = fold (union (op =)) (map sorts_on_typs Ts) []
(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
* Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
@@ -373,11 +377,11 @@
(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
fun class_pairs thy [] supers = []
| class_pairs thy subs supers =
- let val class_less = Sorts.class_less(Sign.classes_of thy)
- fun add_super sub (super,pairs) =
- if class_less (sub,super) then (sub,super)::pairs else pairs
- fun add_supers (sub,pairs) = List.foldl (add_super sub) pairs supers
- in List.foldl add_supers [] subs end;
+ let
+ val class_less = Sorts.class_less (Sign.classes_of thy)
+ fun add_super sub super = class_less (sub, super) ? cons (sub, super)
+ fun add_supers sub = fold (add_super sub) supers
+ in fold add_supers subs [] end
fun make_classrel_clause (sub,super) =
ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
@@ -402,18 +406,18 @@
arity_clause dfg (class::seen) n (tcons,ars)
fun multi_arity_clause dfg [] = []
- | multi_arity_clause dfg ((tcons,ars) :: tc_arlists) =
- arity_clause dfg [] 1 (tcons, ars) @ multi_arity_clause dfg tc_arlists
+ | multi_arity_clause dfg ((tcons, ars) :: tc_arlists) =
+ arity_clause dfg [] 1 (tcons, ars) @ multi_arity_clause dfg tc_arlists
(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
provided its arguments have the corresponding sorts.*)
fun type_class_pairs thy tycons classes =
let val alg = Sign.classes_of thy
- fun domain_sorts (tycon,class) = Sorts.mg_domain alg tycon [class]
- fun add_class tycon (class,pairs) =
- (class, domain_sorts(tycon,class))::pairs
- handle Sorts.CLASS_ERROR _ => pairs
- fun try_classes tycon = (tycon, List.foldl (add_class tycon) [] classes)
+ fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
+ fun add_class tycon class =
+ cons (class, domain_sorts tycon class)
+ handle Sorts.CLASS_ERROR _ => I
+ fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
in map try_classes tycons end;
(*Proving one (tycon, class) membership may require proving others, so iterate.*)
@@ -435,35 +439,35 @@
(*FIXME: multiple-arity checking doesn't work, as update_new is the wrong
function (it flags repeated declarations of a function, even with the same arity)*)
-fun update_many (tab, keypairs) = List.foldl (uncurry Symtab.update) tab keypairs;
+fun update_many keypairs = fold Symtab.update keypairs
-fun add_type_sort_preds (T, preds) =
- update_many (preds, map pred_of_sort (sorts_on_typs T));
+val add_type_sort_preds = update_many o map pred_of_sort o sorts_on_typs
-fun add_classrel_clause_preds (ClassrelClause {subclass,superclass,...}, preds) =
- Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
+fun add_classrel_clause_preds (ClassrelClause {subclass, superclass, ...}) =
+ Symtab.update (subclass, 1) #> Symtab.update (superclass, 1)
fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass
| class_of_arityLit (TVarLit (tclass, _)) = tclass;
-fun add_arity_clause_preds (ArityClause {conclLit,premLits,...}, preds) =
- let val classes = map (make_type_class o class_of_arityLit) (conclLit::premLits)
- fun upd (class,preds) = Symtab.update (class,1) preds
- in List.foldl upd preds classes end;
+fun add_arity_clause_preds (ArityClause {conclLit, premLits, ...}) =
+ let
+ val classes = map (make_type_class o class_of_arityLit)
+ (conclLit :: premLits)
+ in fold (Symtab.update o rpair 1) classes end;
(*** Find occurrences of functions in clauses ***)
-fun add_foltype_funcs (TyVar _, funcs) = funcs
- | add_foltype_funcs (TyFree (s, _), funcs) = Symtab.update (s, 0) funcs
- | add_foltype_funcs (TyConstr ((s, _), tys), funcs) =
- List.foldl add_foltype_funcs (Symtab.update (s, length tys) funcs) tys;
+fun add_fol_type_funcs (TyVar _) = I
+ | add_fol_type_funcs (TyFree (s, _)) = Symtab.update (s, 0)
+ | add_fol_type_funcs (TyConstr ((s, _), tys)) =
+ Symtab.update (s, length tys) #> fold add_fol_type_funcs tys
(*TFrees are recorded as constants*)
fun add_type_sort_funcs (TVar _, funcs) = funcs
| add_type_sort_funcs (TFree (a, _), funcs) =
Symtab.update (make_fixed_type_var a, 0) funcs
-fun add_arity_clause_funcs (ArityClause {conclLit,...}, funcs) =
+fun add_arity_clause_funcs (ArityClause {conclLit,...}) funcs =
let val TConsLit (_, tcons, tvars) = conclLit
in Symtab.update (tcons, length tvars) funcs end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Apr 20 15:17:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Apr 20 16:04:49 2010 +0200
@@ -34,13 +34,12 @@
val get_helper_clauses : bool -> theory -> bool ->
hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
hol_clause list
- val write_tptp_file : bool -> bool -> Path.T ->
+ val write_tptp_file : bool -> bool -> bool -> Path.T ->
hol_clause list * hol_clause list * hol_clause list * hol_clause list *
- classrel_clause list * arity_clause list ->
- int * int
+ classrel_clause list * arity_clause list -> unit
val write_dfg_file : bool -> bool -> Path.T ->
hol_clause list * hol_clause list * hol_clause list * hol_clause list *
- classrel_clause list * arity_clause list -> int * int
+ classrel_clause list * arity_clause list -> unit
end
structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
@@ -51,19 +50,19 @@
open Sledgehammer_Fact_Preprocessor
(* Parameter "full_types" below indicates that full type information is to be
-exported *)
+ exported.
-(* If true, each function will be directly applied to as many arguments as
- possible, avoiding use of the "apply" operator. Use of hBOOL is also
- minimized. *)
-val minimize_applies = true;
+ If "explicit_apply" is false, each function will be directly applied to as
+ many arguments as possible, avoiding use of the "apply" operator. Use of
+ hBOOL is also minimized.
+*)
fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
(*True if the constant ever appears outside of the top-level position in literals.
If false, the constant always receives all of its arguments and is used as a predicate.*)
-fun needs_hBOOL const_needs_hBOOL c =
- not minimize_applies orelse
+fun needs_hBOOL explicit_apply const_needs_hBOOL c =
+ explicit_apply orelse
the_default false (Symtab.lookup const_needs_hBOOL c);
@@ -174,13 +173,13 @@
end;
-fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
- let val cls = make_clause dfg thy (id, name, Axiom, th)
- in
- if isTaut cls then pairs else (name,cls)::pairs
- end;
+fun add_axiom_clause dfg thy (th, (name, id)) =
+ let val cls = make_clause dfg thy (id, name, Axiom, th) in
+ not (isTaut cls) ? cons (name, cls)
+ end
-fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) [];
+fun make_axiom_clauses dfg thy clauses =
+ fold (add_axiom_clause dfg thy) clauses []
fun make_conjecture_clauses_aux _ _ _ [] = []
| make_conjecture_clauses_aux dfg thy n (th::ths) =
@@ -212,9 +211,10 @@
val type_wrapper = "ti";
-fun head_needs_hBOOL const_needs_hBOOL (CombConst((c, _), _, _)) =
- needs_hBOOL const_needs_hBOOL c
- | head_needs_hBOOL _ _ = true;
+fun head_needs_hBOOL explicit_apply const_needs_hBOOL
+ (CombConst ((c, _), _, _)) =
+ needs_hBOOL explicit_apply const_needs_hBOOL c
+ | head_needs_hBOOL _ _ _ = true
fun wrap_type full_types (s, ty) pool =
if full_types then
@@ -224,8 +224,11 @@
else
(s, pool)
-fun wrap_type_if full_types cnh (head, s, tp) =
- if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else pair s
+fun wrap_type_if full_types explicit_apply cnh (head, s, tp) =
+ if head_needs_hBOOL explicit_apply cnh head then
+ wrap_type full_types (s, tp)
+ else
+ pair s
fun apply ss = "hAPP" ^ paren_pack ss;
@@ -253,18 +256,22 @@
| string_of_application _ _ (CombVar (name, _), args) pool =
nice_name name pool |>> (fn s => string_apply (s, args))
-fun string_of_combterm (params as (full_types, cma, cnh)) t pool =
+fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t
+ pool =
let
val (head, args) = strip_combterm_comb t
val (ss, pool) = pool_map (string_of_combterm params) args pool
val (s, pool) = string_of_application full_types cma (head, ss) pool
- in wrap_type_if full_types cnh (head, s, type_of_combterm t) pool end
+ in
+ wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t)
+ pool
+ end
(*Boolean-valued terms are here converted to literals.*)
fun boolify params c =
string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
-fun string_of_predicate (params as (_, _, cnh)) t =
+fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t =
case t of
(CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) =>
(* DFG only: new TPTP prefers infix equality *)
@@ -273,7 +280,8 @@
| _ =>
case #1 (strip_combterm_comb t) of
CombConst ((s, _), _, _) =>
- (if needs_hBOOL cnh s then boolify else string_of_combterm) params t
+ (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
+ params t
| _ => boolify params t
@@ -341,51 +349,53 @@
(** For DFG format: accumulate function and predicate declarations **)
-fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
+fun add_types tvars = fold add_fol_type_funcs tvars
-fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars), (funcs, preds)) =
+fun add_decls (full_types, explicit_apply, cma, cnh)
+ (CombConst ((c, _), _, tvars)) (funcs, preds) =
if c = "equal" then
- (addtypes tvars funcs, preds)
+ (add_types tvars funcs, preds)
else
let val arity = min_arity_of cma c
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)
- else (addtypes tvars funcs, addit preds)
+ if needs_hBOOL explicit_apply cnh c then
+ (add_types tvars (addit funcs), preds)
+ else
+ (add_types tvars funcs, addit preds)
end
- | add_decls _ (CombVar (_,ctp), (funcs, preds)) =
- (add_foltype_funcs (ctp,funcs), preds)
- | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
+ | add_decls _ (CombVar (_, ctp)) (funcs, preds) =
+ (add_fol_type_funcs ctp funcs, preds)
+ | add_decls params (CombApp (P, Q)) decls =
+ decls |> add_decls params P |> add_decls params Q
-fun add_literal_decls params (Literal (_,c), decls) = add_decls params (c,decls);
+fun add_literal_decls params (Literal (_, c)) = add_decls params c
-fun add_clause_decls params (HOLClause {literals, ...}, decls) =
- List.foldl (add_literal_decls params) decls literals
+fun add_clause_decls params (HOLClause {literals, ...}) decls =
+ fold (add_literal_decls params) literals decls
handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
fun decls_of_clauses params clauses arity_clauses =
- let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) init_functab)
- val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
- val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
- in
- (Symtab.dest (List.foldl add_arity_clause_funcs functab arity_clauses),
- Symtab.dest predtab)
- end;
+ let val functab = init_functab |> Symtab.update (type_wrapper, 2)
+ |> Symtab.update ("hAPP", 2)
+ val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1)
+ val (functab, predtab) =
+ (functab, predtab) |> fold (add_clause_decls params) clauses
+ |>> fold add_arity_clause_funcs arity_clauses
+ in (Symtab.dest functab, Symtab.dest predtab) end
-fun add_clause_preds (HOLClause {ctypes_sorts, ...}, preds) =
- List.foldl add_type_sort_preds preds ctypes_sorts
+fun add_clause_preds (HOLClause {ctypes_sorts, ...}) preds =
+ fold add_type_sort_preds ctypes_sorts preds
handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
(*Higher-order clauses have only the predicates hBOOL and type classes.*)
fun preds_of_clauses clauses clsrel_clauses arity_clauses =
- Symtab.dest
- (List.foldl add_classrel_clause_preds
- (List.foldl add_arity_clause_preds
- (List.foldl add_clause_preds Symtab.empty clauses)
- arity_clauses)
- clsrel_clauses)
-
+ Symtab.empty
+ |> fold add_clause_preds clauses
+ |> fold add_arity_clause_preds arity_clauses
+ |> fold add_classrel_clause_preds clsrel_clauses
+ |> Symtab.dest
(**********************************************************************)
(* write clauses to files *)
@@ -395,22 +405,19 @@
Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0),
("c_COMBS", 0)];
-fun count_combterm (CombConst ((c, _), _, _), ct) =
- (case Symtab.lookup ct c of NONE => ct (*no counter*)
- | SOME n => Symtab.update (c,n+1) ct)
- | count_combterm (CombVar _, ct) = ct
- | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
+fun count_combterm (CombConst ((c, _), _, _)) =
+ Symtab.map_entry c (Integer.add 1)
+ | count_combterm (CombVar _) = I
+ | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
-fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
+fun count_literal (Literal (_, t)) = count_combterm t
-fun count_clause (HOLClause {literals, ...}, ct) =
- List.foldl count_literal ct literals;
+fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
-fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}, ct) =
- if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals
- else ct;
+fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}) =
+ member (op =) user_lemmas axiom_name ? fold count_literal literals
-fun cnf_helper_thms thy = cnf_rules_pairs thy o map pairname
+fun cnf_helper_thms thy = cnf_rules_pairs thy o map (`Thm.get_name_hint)
fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
if isFO then
@@ -418,8 +425,8 @@
else
let
val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
- val ct0 = List.foldl count_clause init_counters conjectures
- val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
+ val ct = init_counters |> fold count_clause conjectures
+ |> fold (count_user_clause user_lemmas) axclauses
fun needed c = the (Symtab.lookup ct c) > 0
val IK = if needed "c_COMBI" orelse needed "c_COMBK"
then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
@@ -440,15 +447,16 @@
fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
let val (head, args) = strip_combterm_comb t
val n = length args
- val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
+ val (const_min_arity, const_needs_hBOOL) =
+ (const_min_arity, const_needs_hBOOL)
+ |> fold (count_constants_term false) args
in
case head of
CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*)
let val a = if a="equal" andalso not toplev then "c_fequal" else a
- val const_min_arity = Symtab.map_default (a, n) (Integer.min n) const_min_arity
in
- if toplev then (const_min_arity, const_needs_hBOOL)
- else (const_min_arity, Symtab.update (a,true) (const_needs_hBOOL))
+ (const_min_arity |> Symtab.map_default (a, n) (Integer.min n),
+ const_needs_hBOOL |> not toplev ? Symtab.update (a, true))
end
| _ => (const_min_arity, const_needs_hBOOL)
end;
@@ -461,64 +469,74 @@
(const_min_arity, const_needs_hBOOL) =
fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
-fun display_arity const_needs_hBOOL (c,n) =
+fun display_arity explicit_apply const_needs_hBOOL (c,n) =
trace_msg (fn () => "Constant: " ^ c ^
" arity:\t" ^ Int.toString n ^
- (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
+ (if needs_hBOOL explicit_apply const_needs_hBOOL c then
+ " needs hBOOL"
+ else
+ ""))
-fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
- if minimize_applies then
+fun count_constants explicit_apply
+ (conjectures, _, extra_clauses, helper_clauses, _, _) =
+ if not explicit_apply then
let val (const_min_arity, const_needs_hBOOL) =
fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
|> fold count_constants_clause extra_clauses
|> fold count_constants_clause helper_clauses
- val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
+ val _ = List.app (display_arity explicit_apply const_needs_hBOOL)
+ (Symtab.dest (const_min_arity))
in (const_min_arity, const_needs_hBOOL) end
else (Symtab.empty, Symtab.empty);
+fun header () =
+ "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
+ "% " ^ timestamp () ^ "\n"
+
(* TPTP format *)
-fun write_tptp_file debug full_types file clauses =
+fun write_tptp_file readable_names full_types explicit_apply file clauses =
let
fun section _ [] = []
| section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
- val pool = empty_name_pool debug
+ val pool = empty_name_pool readable_names
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
- val (cma, cnh) = count_constants clauses
- val params = (full_types, cma, cnh)
+ val (cma, cnh) = count_constants explicit_apply clauses
+ val params = (full_types, explicit_apply, cma, cnh)
val ((conjecture_clss, tfree_litss), pool) =
pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
- val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
+ val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses
pool
val classrel_clss = map tptp_classrel_clause classrel_clauses
val arity_clss = map tptp_arity_clause arity_clauses
val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
helper_clauses pool
- val _ =
- File.write_list file (
- "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
- "% " ^ timestamp () ^ "\n" ::
- section "Relevant fact" ax_clss @
- section "Type variable" tfree_clss @
- section "Conjecture" conjecture_clss @
- section "Class relationship" classrel_clss @
- section "Arity declaration" arity_clss @
- section "Helper fact" helper_clss)
- in (length axclauses + 1, length tfree_clss + length conjecture_clss)
- end;
+ in
+ File.write_list file
+ (header () ::
+ section "Relevant fact" ax_clss @
+ section "Type variable" tfree_clss @
+ section "Conjecture" conjecture_clss @
+ section "Class relationship" classrel_clss @
+ section "Arity declaration" arity_clss @
+ section "Helper fact" helper_clss)
+ end
(* DFG format *)
-fun write_dfg_file debug full_types file clauses =
+fun write_dfg_file full_types explicit_apply file clauses =
let
- val pool = empty_name_pool debug
+ (* Some of the helper functions below are not name-pool-aware. However,
+ there's no point in adding name pool support if the DFG format is on its
+ way out anyway. *)
+ val pool = NONE
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
- val (cma, cnh) = count_constants clauses
- val params = (full_types, cma, cnh)
+ val (cma, cnh) = count_constants explicit_apply clauses
+ val params = (full_types, explicit_apply, cma, cnh)
val ((conjecture_clss, tfree_litss), pool) =
pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
and probname = Path.implode (Path.base file)
@@ -526,30 +544,25 @@
val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
val (helper_clauses_strs, pool) =
pool_map (apfst fst oo dfg_clause params) helper_clauses pool
- val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
+ val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
- val _ =
- File.write_list file (
- string_of_start probname ::
- string_of_descrip probname ::
- string_of_symbols (string_of_funcs funcs)
- (string_of_preds (cl_preds @ ty_preds)) ::
- "list_of_clauses(axioms, cnf).\n" ::
- axstrs @
- map dfg_classrel_clause classrel_clauses @
- map dfg_arity_clause arity_clauses @
- helper_clauses_strs @
- ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
- tfree_clss @
- conjecture_clss @
- ["end_of_list.\n\n",
- (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
- "list_of_settings(SPASS).\n{*\nset_flag(VarWeight, 3).\n*}\nend_of_list.\n\n",
- "end_problem.\n"])
-
in
- (length axclauses + length classrel_clauses + length arity_clauses +
- length helper_clauses + 1, length tfree_clss + length conjecture_clss)
+ File.write_list file
+ (header () ::
+ string_of_start probname ::
+ string_of_descrip probname ::
+ string_of_symbols (string_of_funcs funcs)
+ (string_of_preds (cl_preds @ ty_preds)) ::
+ "list_of_clauses(axioms, cnf).\n" ::
+ axstrs @
+ map dfg_classrel_clause classrel_clauses @
+ map dfg_arity_clause arity_clauses @
+ helper_clauses_strs @
+ ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
+ tfree_clss @
+ conjecture_clss @
+ ["end_of_list.\n\n",
+ "end_problem.\n"])
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Apr 20 15:17:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Apr 20 16:04:49 2010 +0200
@@ -41,10 +41,11 @@
[("debug", "false"),
("verbose", "false"),
("overlord", "false"),
+ ("explicit_apply", "false"),
("respect_no_atp", "true"),
("relevance_threshold", "50"),
("convergence", "320"),
- ("theory_const", "smart"),
+ ("theory_relevant", "smart"),
("higher_order", "smart"),
("follow_defs", "false"),
("isar_proof", "false"),
@@ -58,9 +59,10 @@
[("no_debug", "debug"),
("quiet", "verbose"),
("no_overlord", "overlord"),
+ ("implicit_apply", "explicit_apply"),
("ignore_no_atp", "respect_no_atp"),
("partial_types", "full_types"),
- ("no_theory_const", "theory_const"),
+ ("theory_irrelevant", "theory_relevant"),
("first_order", "higher_order"),
("dont_follow_defs", "follow_defs"),
("metis_proof", "isar_proof"),
@@ -146,11 +148,12 @@
val overlord = lookup_bool "overlord"
val atps = lookup_string "atps" |> space_explode " "
val full_types = lookup_bool "full_types"
+ val explicit_apply = lookup_bool "explicit_apply"
val respect_no_atp = lookup_bool "respect_no_atp"
val relevance_threshold =
0.01 * Real.fromInt (lookup_int "relevance_threshold")
val convergence = 0.01 * Real.fromInt (lookup_int "convergence")
- val theory_const = lookup_bool_option "theory_const"
+ val theory_relevant = lookup_bool_option "theory_relevant"
val higher_order = lookup_bool_option "higher_order"
val follow_defs = lookup_bool "follow_defs"
val isar_proof = lookup_bool "isar_proof"
@@ -160,11 +163,12 @@
val minimize_timeout = lookup_time "minimize_timeout"
in
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
- full_types = full_types, respect_no_atp = respect_no_atp,
- relevance_threshold = relevance_threshold, convergence = convergence,
- theory_const = theory_const, higher_order = higher_order,
- follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus,
- sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout}
+ full_types = full_types, explicit_apply = explicit_apply,
+ respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
+ convergence = convergence, theory_relevant = theory_relevant,
+ higher_order = higher_order, follow_defs = follow_defs,
+ isar_proof = isar_proof, modulus = modulus, sorts = sorts,
+ timeout = timeout, minimize_timeout = minimize_timeout}
end
fun get_params thy = extract_params thy (default_raw_params thy)
@@ -183,27 +187,27 @@
fun get_time_limit_arg s =
(case Int.fromString s of
SOME t => Time.fromSeconds t
- | NONE => error ("Invalid time limit: " ^ quote s))
+ | 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))
+ | n => error ("Invalid argument: " ^ n ^ "."))
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.toMilliseconds timeout) ^ " ms"])]
+ (override_params @
+ [("atps", [atp]),
+ ("minimize_timeout",
+ [string_of_int (Time.toMilliseconds timeout) ^ " ms"])])
val prover =
(case get_prover thy atp of
SOME prover => prover
- | NONE => error ("Unknown ATP: " ^ quote atp))
+ | NONE => error ("Unknown ATP: " ^ quote atp ^ "."))
val name_thms_pairs = theorems_from_refs ctxt fact_refs
in
- writeln (#2 (minimize_theorems params linear_minimize prover atp i state
- name_thms_pairs))
+ priority (#2 (minimize_theorems params prover atp i state name_thms_pairs))
end
val runN = "run"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Apr 20 15:17:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Apr 20 16:04:49 2010 +0200
@@ -14,10 +14,15 @@
val strip_prefix: string -> string -> string option
val is_proof_well_formed: string -> bool
val metis_line: int -> int -> string list -> string
- val metis_lemma_list: bool -> string ->
- string * string vector * (int * int) * Proof.context * thm * int -> string * string list
- val structured_isar_proof: int -> bool -> string ->
- string * string vector * (int * int) * Proof.context * thm * int -> string * string list
+ val metis_proof_text:
+ bool -> bool -> string -> string -> string vector -> Proof.context -> thm
+ -> int -> string * string list
+ val isar_proof_text:
+ bool -> int -> bool -> string -> string -> string vector -> Proof.context
+ -> thm -> int -> string * string list
+ val proof_text:
+ bool -> bool -> int -> bool -> string -> string -> string vector
+ -> Proof.context -> thm -> int -> string * string list
end;
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
@@ -493,45 +498,22 @@
exists (fn s => String.isSubstring s proof) end_proof_strs
(* === EXTRACTING LEMMAS === *)
-(* lines have the form "cnf(108, axiom, ...",
-the number (108) has to be extracted)*)
-fun get_step_nums false extract =
+(* A list consisting of the first number in each line is returned.
+ TPTP: Interesting lines have the form "cnf(108, axiom, ...)", where the
+ number (108) is extracted.
+ DFG: Lines have the form "108[0:Inp] ...", where the first number (108) is
+ extracted. *)
+fun get_step_nums proof_extract =
let
val toks = String.tokens (not o Char.isAlphaNum)
fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok
| inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) =
Int.fromString ntok
+ | inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok (* DFG *)
| inputno _ = NONE
- val lines = split_lines extract
+ val lines = split_lines proof_extract
in map_filter (inputno o toks) lines end
-(*String contains multiple lines. We want those of the form
- "253[0:Inp] et cetera..."
- A list consisting of the first number in each line is returned. *)
-| get_step_nums true proofextract =
- let val toks = String.tokens (not o Char.isAlphaNum)
- fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
- | inputno _ = NONE
- val lines = split_lines proofextract
- in map_filter (inputno o toks) lines end
-(*extracting lemmas from tstp-output between the lines from above*)
-fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
- let
- (* get the names of axioms from their numbers*)
- fun get_axiom_names thm_names step_nums =
- let
- val last_axiom = Vector.length thm_names
- fun is_axiom n = n <= last_axiom
- fun is_conj n = n >= fst conj_count andalso
- n < fst conj_count + snd conj_count
- fun getname i = Vector.sub(thm_names, i-1)
- in
- (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
- (map getname (filter is_axiom step_nums))),
- exists is_conj step_nums)
- end
- in get_axiom_names thm_names (get_step_nums (get_proof_extract proof)) end;
-
(*Used to label theorems chained into the sledgehammer call*)
val chained_hint = "CHAINED";
val kill_chained = filter_out (curry (op =) chained_hint)
@@ -546,29 +528,33 @@
fun metis_line i n xs =
"Try this command: " ^
Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n"
-fun minimize_line _ [] = ""
- | minimize_line name xs =
+fun minimize_line _ _ [] = ""
+ | minimize_line isar_proof atp_name xs =
"To minimize the number of lemmas, try this command: " ^
Markup.markup Markup.sendback
- ("sledgehammer minimize [atp = " ^ name ^ "] (" ^
+ ("sledgehammer minimize [atp = " ^ atp_name ^
+ (if isar_proof then ", isar_proof" else "") ^ "] (" ^
space_implode " " xs ^ ")") ^ ".\n"
-fun metis_lemma_list dfg name (result as (_, _, _, _, goal, i)) =
+fun metis_proof_text isar_proof minimal atp_name proof thm_names
+ (_ : Proof.context) goal i =
let
- val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
+ val lemmas =
+ proof |> get_proof_extract
+ |> get_step_nums
+ |> filter (fn i => i <= Vector.length thm_names)
+ |> map (fn i => Vector.sub (thm_names, i - 1))
+ |> filter (fn x => x <> "??.unknown")
+ |> sort_distinct string_ord
val n = Logic.count_prems (prop_of goal)
val xs = kill_chained lemmas
in
- (metis_line i n xs ^ minimize_line name xs ^
- (if used_conj then
- ""
- else
- "\nWarning: The goal is provable because the context is inconsistent."),
+ (metis_line i n xs ^
+ (if minimal then "" else minimize_line isar_proof atp_name xs),
kill_chained lemmas)
- end;
+ end
-fun structured_isar_proof modulus sorts name
- (result as (proof, thm_names, conj_count, ctxt, goal, i)) =
+fun isar_proof_text minimal modulus sorts atp_name proof thm_names ctxt goal i =
let
(* We could use "split_lines", but it can return blank lines. *)
val lines = String.tokens (equal #"\n");
@@ -576,7 +562,8 @@
String.translate (fn c => if Char.isSpace c then "" else str c)
val extract = get_proof_extract proof
val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
- val (one_line_proof, lemma_names) = metis_lemma_list false name result
+ val (one_line_proof, lemma_names) =
+ metis_proof_text true minimal atp_name proof thm_names ctxt goal i
val tokens = String.tokens (fn c => c = #" ") one_line_proof
val isar_proof =
if member (op =) tokens chained_hint then ""
@@ -588,4 +575,8 @@
lemma_names)
end
+fun proof_text isar_proof minimal modulus sorts =
+ if isar_proof then isar_proof_text minimal modulus sorts
+ else metis_proof_text isar_proof minimal
+
end;