--- a/src/HOL/TPTP/atp_theory_export.ML Thu Jul 24 23:18:01 2014 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Fri Jul 25 13:22:37 2014 +0200
@@ -51,12 +51,11 @@
val thy = Proof_Context.theory_of ctxt
val prob_file = File.tmp_path (Path.explode "prob")
val atp = atp_of_format format
- val {exec, arguments, proof_delims, known_failures, ...} =
- get_atp thy atp ()
+ val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp ()
val ord = effective_term_order ctxt atp
val _ = problem |> lines_of_atp_problem format ord (K [])
|> File.write_list prob_file
- val exec = exec ()
+ val exec = exec false
val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
val command =
File.shell_path (Path.explode path) ^ " " ^
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Jul 24 23:18:01 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 25 13:22:37 2014 +0200
@@ -14,11 +14,9 @@
type slice_spec = (int * string) * atp_format * string * string * bool
type atp_config =
- {exec : unit -> string list * string list,
- arguments :
- Proof.context -> bool -> string -> Time.time -> string
- -> term_order * (unit -> (string * int) list)
- * (unit -> (string * real) list) -> string,
+ {exec : bool -> string list * string list,
+ arguments : Proof.context -> bool -> string -> Time.time -> string ->
+ term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
proof_delims : (string * string) list,
known_failures : (atp_failure * string) list,
prem_role : atp_formula_role,
@@ -48,10 +46,9 @@
val spass_H2NuVS0Red2 : string
val spass_H2SOS : string
val spass_extra_options : string Config.T
- val remote_atp :
- string -> string -> string list -> (string * string) list
- -> (atp_failure * string) list -> atp_formula_role
- -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config)
+ val remote_atp : string -> string -> string list -> (string * string) list ->
+ (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) ->
+ string * (unit -> atp_config)
val add_atp : string * (unit -> atp_config) -> theory -> theory
val get_atp : theory -> string -> (unit -> atp_config)
val supported_atps : theory -> string list
@@ -76,11 +73,9 @@
type slice_spec = (int * string) * atp_format * string * string * bool
type atp_config =
- {exec : unit -> string list * string list,
- arguments :
- Proof.context -> bool -> string -> Time.time -> string
- -> term_order * (unit -> (string * int) list)
- * (unit -> (string * real) list) -> string,
+ {exec : bool -> string list * string list,
+ arguments : Proof.context -> bool -> string -> Time.time -> string ->
+ term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
proof_delims : (string * string) list,
known_failures : (atp_failure * string) list,
prem_role : atp_formula_role,
@@ -213,7 +208,6 @@
(* E *)
fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> LESS
-fun is_e_at_least_1_9 () = string_ord (getenv "E_VERSION", "1.9") <> LESS
val e_smartN = "smart"
val e_autoN = "auto"
@@ -267,9 +261,9 @@
|> implode) ^
"),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
\1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
- \FIFOWeight(PreferProcessed))'"
+ \FIFOWeight(PreferProcessed))' "
else
- "-xAuto"
+ "-xAuto "
val e_ord_weights =
map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
@@ -279,25 +273,26 @@
fun e_term_order_info_arguments false false _ = ""
| e_term_order_info_arguments gen_weights gen_prec ord_info =
let val ord_info = ord_info () in
- (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' "
- else "") ^
- (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' "
- else "")
+ (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^
+ (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "")
end
val e_config : atp_config =
- {exec = (fn () => (["E_HOME"],
- if is_e_at_least_1_9 () then ["eprover"] else ["eproof_ram", "eproof"])),
- arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout => fn file_name =>
+ {exec = fn full_proofs => (["E_HOME"],
+ if full_proofs orelse not (is_e_at_least_1_8 ()) then ["eproof_ram", "eproof"]
+ else ["eprover"]),
+ arguments = fn ctxt => fn full_proofs => fn heuristic => fn timeout => fn file_name =>
fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
(if is_e_at_least_1_8 () then "--auto-schedule " else "") ^
"--tstp-in --tstp-out --silent " ^
- e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
- e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
+ e_selection_weight_arguments ctxt heuristic sel_weights ^
+ e_term_order_info_arguments gen_weights gen_prec ord_info ^
"--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
"--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
- (if is_e_at_least_1_9 () then " --proof-object=3"
- else " --output-level=5 --pcl-shell-level=" ^ (if full_proof then "0" else "2")) ^
+ (if full_proofs orelse not (is_e_at_least_1_8 ()) then
+ " --output-level=5 --pcl-shell-level=" ^ (if full_proofs then "0" else "2")
+ else
+ " --proof-object=1") ^
" " ^ file_name,
proof_delims =
[("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
@@ -511,20 +506,20 @@
val vampire_config : atp_config =
{exec = K (["VAMPIRE_HOME"], ["vampire"]),
- arguments = fn _ => fn full_proof => fn sos => fn timeout => fn file_name =>
+ arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name =>
fn _ =>
"--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
" --proof tptp --output_axiom_names on" ^
(if is_vampire_at_least_1_8 () then
(* Cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
- (if full_proof then
+ (if full_proofs then
" --forced_options splitting=off:equality_proxy=off:general_splitting=off\
\:inequality_splitting=0:naming=0"
else
"")
else
"") ^
- " --thanks \"Andrei and Krystof\" --input_file " ^ file_name
+ " --thanks \"Andrei et al.\" --input_file " ^ file_name
|> sos = sosN ? prefix "--sos on ",
proof_delims =
[("=========== Refutation ==========",
@@ -766,7 +761,7 @@
fun is_atp_installed thy name =
let val {exec, ...} = get_atp thy name () in
- exists (fn var => getenv var <> "") (fst (exec ()))
+ exists (fn var => getenv var <> "") (fst (exec false))
end
fun refresh_systems_on_tptp () =
--- a/src/HOL/Tools/BNF/bnf_def.ML Thu Jul 24 23:18:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Jul 25 13:22:37 2014 +0200
@@ -1,7 +1,8 @@
(* Title: HOL/Tools/BNF/bnf_def.ML
Author: Dmitriy Traytel, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2012
+ Author: Martin Desharnais, TU Muenchen
+ Copyright 2012, 2013, 2014
Definition of bounded natural functors.
*)
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Thu Jul 24 23:18:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Fri Jul 25 13:22:37 2014 +0200
@@ -1,7 +1,8 @@
(* Title: HOL/Tools/BNF/bnf_def_tactics.ML
Author: Dmitriy Traytel, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2012
+ Author: Martin Desharnais, TU Muenchen
+ Copyright 2012, 2013, 2014
Tactics for definition of bounded natural functors.
*)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Jul 24 23:18:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Jul 25 13:22:37 2014 +0200
@@ -1,6 +1,7 @@
(* Title: HOL/Tools/BNF/bnf_fp_def_sugar.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2012, 2013
+ Author: Martin Desharnais, TU Muenchen
+ Copyright 2012, 2013, 2014
Sugared datatype and codatatype constructions.
*)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Jul 24 23:18:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Jul 25 13:22:37 2014 +0200
@@ -1,6 +1,7 @@
(* Title: HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2012
+ Author: Martin Desharnais, TU Muenchen
+ Copyright 2012, 2013, 2014
Tactics for datatype and codatatype sugar.
*)
@@ -232,15 +233,14 @@
fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss
dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs =
rtac dtor_rel_coinduct 1 THEN
- EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
- fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
+ EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
+ fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
(rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
- (dtac (rotate_prems (~1) ((cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct] @{thm
- arg_cong2}) RS iffD1)) THEN'
- atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac assm THEN'
- REPEAT_DETERM o etac conjE))) 1 THEN
- unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels
- @ simp_thms') THEN
+ (dtac (rotate_prems (~1) (cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct]
+ @{thm arg_cong2} RS iffD1)) THEN'
+ atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac assm THEN'
+ REPEAT_DETERM o etac conjE))) 1 THEN
+ unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels @ simp_thms') THEN
unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def
rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl]
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Jul 24 23:18:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jul 25 13:22:37 2014 +0200
@@ -1,7 +1,8 @@
(* Title: HOL/Tools/BNF/bnf_fp_util.ML
Author: Dmitriy Traytel, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2012, 2013
+ Author: Martin Desharnais, TU Muenchen
+ Copyright 2012, 2013, 2014
Shared library for the datatype and codatatype constructions.
*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Jul 24 23:18:01 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Jul 25 13:22:37 2014 +0200
@@ -203,10 +203,9 @@
if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name
else remotify_prover_if_supported_and_not_already_remote ctxt name
-(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
- timeout, it makes sense to put E first. *)
+(* The first ATP of the list is used by Auto Sledgehammer. *)
fun default_provers_param_value mode ctxt =
- [eN, spassN, z3N, e_sineN, vampireN]
+ [eN, spassN, z3N, vampireN, e_sineN]
|> map_filter (remotify_prover_if_not_installed ctxt)
(* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
|> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu Jul 24 23:18:01 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Jul 25 13:22:37 2014 +0200
@@ -21,6 +21,7 @@
structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
struct
+open Sledgehammer_Util
open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
@@ -35,10 +36,12 @@
val slack = seconds 0.025
fun minimize_isar_step_dependencies ctxt preplay_data
- (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =
+ (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meths as meth :: _, comment)) =
(case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
Played time =>
let
+ val gfs0 = filter (influence_proof_method ctxt meth o thms_of_name ctxt) gfs00
+
fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)
fun minimize_facts _ min_facts [] time = (min_facts, time)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Thu Jul 24 23:18:01 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jul 25 13:22:37 2014 +0200
@@ -218,8 +218,6 @@
|> Config.put show_sorts false
|> Config.put show_consts false
- val register_fixes = map Free #> fold Variable.auto_fixes
-
fun add_str s' = apfst (suffix s')
fun of_indent ind = replicate_string (ind * indent_size) " "
@@ -246,7 +244,7 @@
|> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
|> simplify_spaces
|> maybe_quote),
- ctxt |> Variable.auto_fixes term)
+ ctxt |> perhaps (try (Variable.auto_fixes term)))
fun using_facts [] [] = ""
| using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
@@ -266,7 +264,7 @@
maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
fun add_frees xs (s, ctxt) =
- (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
+ (s ^ space_implode " and " (map of_free xs), ctxt |> fold Variable.auto_fixes (map Free xs))
fun add_fix _ [] = I
| add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Jul 24 23:18:01 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri Jul 25 13:22:37 2014 +0200
@@ -36,6 +36,7 @@
val is_proof_method_direct : proof_method -> bool
val string_of_proof_method : Proof.context -> string list -> proof_method -> string
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
+ val influence_proof_method : Proof.context -> proof_method -> thm list -> bool
val string_of_play_outcome : play_outcome -> string
val play_outcome_ord : play_outcome * play_outcome -> order
val one_line_proof_text : Proof.context -> int -> one_line_params -> string
@@ -121,7 +122,8 @@
end
| Simp_Method => Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps global_facts)
| Simp_Size_Method =>
- Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps @{thms size_ne_size_imp_ne})
+ Simplifier.asm_full_simp_tac
+ (silence_methods ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))
| _ =>
Method.insert_tac global_facts THEN'
(case meth of
@@ -135,6 +137,16 @@
| Presburger_Method => Cooper.tac true [] [] ctxt
| Algebra_Method => Groebner.algebra_tac [] [] ctxt))
+val simp_based_methods =
+ [Simp_Method, Simp_Size_Method, Auto_Method, Fastforce_Method, Force_Method]
+
+fun influence_proof_method ctxt meth ths =
+ not (member (op =) simp_based_methods meth) orelse
+ let val ctxt' = silence_methods ctxt in
+ (* unfortunate pointer comparison -- but it's always safe to consider a theorem useful *)
+ not (pointer_eq (ctxt' addsimps ths, ctxt'))
+ end
+
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
| string_of_play_outcome (Play_Timed_Out time) =
if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Jul 24 23:18:01 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Jul 25 13:22:37 2014 +0200
@@ -143,6 +143,7 @@
val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
best_max_new_mono_instances, ...} = get_atp thy name ()
+ val full_proofs = isar_proofs |> the_default (mode = Minimize)
val local_name = perhaps (try (unprefix remote_prefix)) name
val waldmeister_new = (local_name = waldmeister_newN)
val spass = (local_name = spassN orelse local_name = spass_pirateN)
@@ -162,7 +163,7 @@
Path.append (Path.explode dest_dir) problem_file_name
else
error ("No such directory: " ^ quote dest_dir ^ ".")
- val exec = exec ()
+ val exec = exec full_proofs
val command0 =
(case find_first (fn var => getenv var <> "") (fst exec) of
SOME var =>
@@ -276,9 +277,8 @@
fun ord_info () = atp_problem_term_order_info atp_problem
val ord = effective_term_order ctxt name
- val full_proof = isar_proofs |> the_default (mode = Minimize)
val args =
- arguments ctxt full_proof extra slice_timeout (File.shell_path prob_path)
+ arguments ctxt full_proofs extra slice_timeout (File.shell_path prob_path)
(ord, ord_info, sel_weights)
val command =
"(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu Jul 24 23:18:01 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Jul 25 13:22:37 2014 +0200
@@ -130,7 +130,7 @@
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
- preplay_timeout, ...} : params)
+ minimize, preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state goal facts =
let
val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
@@ -144,7 +144,7 @@
max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
- slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
+ slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
expect = ""}
val problem =
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,