# HG changeset patch # User blanchet # Date 1406287357 -7200 # Node ID 2f46999395e233f42f1d7d943ba5eee1a2b1d1c8 # Parent 9bfa4cb2fee6f5feecb98f47f39ba1c90ed83d84# Parent 0c267a7a23f2b75216049431ddff26d058b9fed5 merge diff -r 0c267a7a23f2 -r 2f46999395e2 src/HOL/TPTP/atp_theory_export.ML --- 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) ^ " " ^ diff -r 0c267a7a23f2 -r 2f46999395e2 src/HOL/Tools/ATP/atp_systems.ML --- 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 () = diff -r 0c267a7a23f2 -r 2f46999395e2 src/HOL/Tools/BNF/bnf_def.ML --- 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. *) diff -r 0c267a7a23f2 -r 2f46999395e2 src/HOL/Tools/BNF/bnf_def_tactics.ML --- 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. *) diff -r 0c267a7a23f2 -r 2f46999395e2 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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. *) diff -r 0c267a7a23f2 -r 2f46999395e2 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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] diff -r 0c267a7a23f2 -r 2f46999395e2 src/HOL/Tools/BNF/bnf_fp_util.ML --- 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. *) diff -r 0c267a7a23f2 -r 2f46999395e2 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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)) diff -r 0c267a7a23f2 -r 2f46999395e2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- 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) diff -r 0c267a7a23f2 -r 2f46999395e2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- 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" diff -r 0c267a7a23f2 -r 2f46999395e2 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- 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" diff -r 0c267a7a23f2 -r 2f46999395e2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- 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 ^ " " ^ ")" diff -r 0c267a7a23f2 -r 2f46999395e2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- 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,