# HG changeset patch # User wenzelm # Date 1343325546 -7200 # Node ID 4e2ee88276d22bc8c126d5e63549b93c134dbfa9 # Parent 619531d87ce4c5471ffc6c33c015f7524bd4089d# Parent 784c6f63d79ce2ea3f9a0d11940b07dde3aee95a merged diff -r 784c6f63d79c -r 4e2ee88276d2 doc-src/TutorialI/Documents/documents.tex diff -r 784c6f63d79c -r 4e2ee88276d2 src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Thu Jul 26 19:57:33 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Export.thy Thu Jul 26 19:59:06 2012 +0200 @@ -26,7 +26,7 @@ ML {* if do_it then - generate_accessibility thy false "/tmp/mash_accessibility" + generate_accessibility @{context} thy false "/tmp/mash_accessibility" else () *} @@ -40,14 +40,14 @@ ML {* if do_it then - generate_isar_dependencies thy false "/tmp/mash_dependencies" + generate_isar_dependencies @{context} thy false "/tmp/mash_dependencies" else () *} ML {* if do_it then - generate_commands @{context} prover thy "/tmp/mash_commands" + generate_commands @{context} params thy "/tmp/mash_commands" else () *} diff -r 784c6f63d79c -r 4e2ee88276d2 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Thu Jul 26 19:57:33 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Thu Jul 26 19:59:06 2012 +0200 @@ -123,7 +123,8 @@ val path = file_name |> Path.explode val _ = File.write path "" val facts = - Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table + Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) false + Symtab.empty [] [] css_table val atp_problem = facts |> map (fn ((_, loc), th) => diff -r 784c6f63d79c -r 4e2ee88276d2 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Thu Jul 26 19:57:33 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Thu Jul 26 19:59:06 2012 +0200 @@ -36,8 +36,9 @@ val slack_max_facts = max_facts_slack * the max_facts val path = file_name |> Path.explode val lines = path |> File.read_lines - val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = all_facts_of (Proof_Context.init_global thy) css_table + val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt + val facts = + all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css val all_names = all_names (facts |> map snd) val mepo_ok = Unsynchronized.ref 0 val mash_ok = Unsynchronized.ref 0 @@ -70,7 +71,7 @@ val th = case find_first (fn (_, th) => nickname_of th = name) facts of SOME (_, th) => th - | NONE => error ("No fact called \"" ^ name ^ "\"") + | NONE => error ("No fact called \"" ^ name ^ "\".") val goal = goal_of_thm thy th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 val isar_deps = isar_dependencies_of all_names th |> these diff -r 784c6f63d79c -r 4e2ee88276d2 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Thu Jul 26 19:57:33 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Thu Jul 26 19:59:06 2012 +0200 @@ -9,14 +9,14 @@ sig type params = Sledgehammer_Provers.params - val generate_accessibility : theory -> bool -> string -> unit + val generate_accessibility : Proof.context -> theory -> bool -> string -> unit val generate_features : Proof.context -> string -> theory -> bool -> string -> unit val generate_isar_dependencies : - theory -> bool -> string -> unit + Proof.context -> theory -> bool -> string -> unit val generate_atp_dependencies : Proof.context -> params -> theory -> bool -> string -> unit - val generate_commands : Proof.context -> string -> theory -> string -> unit + val generate_commands : Proof.context -> params -> theory -> string -> unit val generate_mepo_suggestions : Proof.context -> params -> theory -> int -> string -> unit end; @@ -37,6 +37,12 @@ fun has_thy thy th = Context.theory_name thy = Context.theory_name (theory_of_thm th) +fun all_non_technical_facts ctxt thy = + let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in + all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css + |> filter_out (is_thm_technical o snd) + end + fun parent_facts thy thy_map = let fun add_last thy = @@ -51,7 +57,12 @@ val all_names = map (rpair () o nickname_of) #> Symtab.make -fun generate_accessibility thy include_thy file_name = +fun smart_dependencies_of ctxt params prover facts all_names th = + case atp_dependencies_of ctxt params prover 0 facts all_names th of + SOME deps => deps + | NONE => isar_dependencies_of all_names th |> these + +fun generate_accessibility ctxt thy include_thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" @@ -61,23 +72,22 @@ val _ = File.append path s in [fact] end val thy_map = - all_facts_of (Proof_Context.init_global thy) Termtab.empty + all_non_technical_facts ctxt thy |> not include_thy ? filter_out (has_thy thy o snd) |> thy_map_from_facts fun do_thy facts = let val thy = thy_of_fact thy (hd facts) val parents = parent_facts thy thy_map - in fold do_fact facts parents; () end + in fold_rev do_fact facts parents; () end in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end fun generate_features ctxt prover thy include_thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" - val css_table = clasimpset_rule_table_of ctxt val facts = - all_facts_of (Proof_Context.init_global thy) css_table + all_non_technical_facts ctxt thy |> not include_thy ? filter_out (has_thy thy o snd) fun do_fact ((_, stature), th) = let @@ -88,12 +98,12 @@ in File.append path s end in List.app do_fact facts end -fun generate_isar_dependencies thy include_thy file_name = +fun generate_isar_dependencies ctxt thy include_thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" val ths = - all_facts_of (Proof_Context.init_global thy) Termtab.empty + all_non_technical_facts ctxt thy |> not include_thy ? filter_out (has_thy thy o snd) |> map snd val all_names = all_names ths @@ -112,27 +122,24 @@ val _ = File.write path "" val prover = hd provers val facts = - all_facts_of (Proof_Context.init_global thy) Termtab.empty + all_non_technical_facts ctxt thy |> not include_thy ? filter_out (has_thy thy o snd) val ths = facts |> map snd val all_names = all_names ths fun do_thm th = let val name = nickname_of th - val deps = - case atp_dependencies_of ctxt params prover 0 facts all_names th of - SOME deps => deps - | NONE => isar_dependencies_of all_names th |> these + val deps = smart_dependencies_of ctxt params prover facts all_names th val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" in File.append path s end in List.app do_thm ths end -fun generate_commands ctxt prover thy file_name = +fun generate_commands ctxt (params as {provers, ...}) thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" - val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = all_facts_of (Proof_Context.init_global thy) css_table + val prover = hd provers + val facts = all_non_technical_facts ctxt thy val (new_facts, old_facts) = facts |> List.partition (has_thy thy o snd) |>> sort (thm_ord o pairself snd) @@ -142,13 +149,13 @@ let val name = nickname_of th val feats = features_of ctxt prover thy stature [prop_of th] - val deps = isar_dependencies_of all_names th |> these + val deps = smart_dependencies_of ctxt params prover facts all_names th val kind = Thm.legacy_get_kind th - val core = escape_metas prevs ^ "; " ^ escape_metas feats + val core = + escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^ + escape_metas feats val query = if kind <> "" then "? " ^ core ^ "\n" else "" - val update = - "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^ - escape_metas deps ^ "\n" + val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n" val _ = File.append path (query ^ update) in [name] end val thy_map = old_facts |> thy_map_from_facts @@ -161,8 +168,7 @@ val path = file_name |> Path.explode val _ = File.write path "" val prover = hd provers - val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = all_facts_of (Proof_Context.init_global thy) css_table + val facts = all_non_technical_facts ctxt thy val (new_facts, old_facts) = facts |> List.partition (has_thy thy o snd) |>> sort (thm_ord o pairself snd) diff -r 784c6f63d79c -r 4e2ee88276d2 src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Thu Jul 26 19:57:33 2012 +0200 +++ b/src/HOL/Tools/SMT/smt_solver.ML Thu Jul 26 19:59:06 2012 +0200 @@ -52,8 +52,8 @@ local fun make_cmd command options problem_path proof_path = space_implode " " ( - map File.shell_quote (command () @ options) @ - [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path]) + "(exec 2>&1;" :: map File.shell_quote (command () @ options) @ + [File.shell_path problem_path, ")", ">", File.shell_path proof_path]) fun trace_and ctxt msg f x = let val _ = SMT_Config.trace_msg ctxt (fn () => msg) () @@ -99,7 +99,7 @@ val ls = rev (snd (chop_while (equal "") (rev res))) val _ = SMT_Config.trace_msg ctxt (pretty "Result:") ls - val _ = null ls andalso return_code <> 0 andalso + val _ = return_code <> 0 andalso raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) in ls end diff -r 784c6f63d79c -r 4e2ee88276d2 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Jul 26 19:57:33 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Jul 26 19:59:06 2012 +0200 @@ -29,7 +29,9 @@ Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list - val all_facts_of : Proof.context -> status Termtab.table -> fact list + val all_facts : + Proof.context -> bool -> unit Symtab.table -> thm list -> thm list + -> status Termtab.table -> fact list val nearly_all_facts : Proof.context -> bool -> fact_override -> unit Symtab.table -> status Termtab.table -> thm list -> term list -> term -> fact list @@ -436,10 +438,6 @@ |> op @ end -fun all_facts_of ctxt css = - all_facts ctxt false Symtab.empty [] [] css - |> rev (* partly restore the original order of facts, for MaSh *) - fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts concl_t = if only andalso null add then diff -r 784c6f63d79c -r 4e2ee88276d2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Jul 26 19:57:33 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Jul 26 19:59:06 2012 +0200 @@ -162,21 +162,22 @@ #> (fn (name, value) => if is_known_raw_param name then (name, value) - else if is_prover_list ctxt name andalso null value then - ("provers", [name]) - else if can (type_enc_from_string Strict) name andalso null value then - ("type_enc", [name]) - else if can (trans_lams_from_string ctxt any_type_enc) name andalso - null value then - ("lam_trans", [name]) - else if member (op =) fact_filters name then - ("fact_filter", [name]) - else if can Int.fromString name then - ("max_facts", [name]) + else if null value then + if is_prover_list ctxt name then + ("provers", [name]) + else if can (type_enc_from_string Strict) name then + ("type_enc", [name]) + else if can (trans_lams_from_string ctxt any_type_enc) name then + ("lam_trans", [name]) + else if member (op =) fact_filters name then + ("fact_filter", [name]) + else if is_some (Int.fromString name) then + ("max_facts", [name]) + else + error ("Unknown parameter: " ^ quote name ^ ".") else error ("Unknown parameter: " ^ quote name ^ ".")) - (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are read correctly. *) val implode_param = strip_spaces_except_between_idents o space_implode " " diff -r 784c6f63d79c -r 4e2ee88276d2 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jul 26 19:57:33 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jul 26 19:59:06 2012 +0200 @@ -45,6 +45,7 @@ val atp_dependencies_of : Proof.context -> params -> string -> int -> fact list -> unit Symtab.table -> thm -> string list option + val is_thm_technical : thm -> bool val mash_CLEAR : Proof.context -> unit val mash_ADD : Proof.context -> bool @@ -399,6 +400,14 @@ | _ => NONE end +val technical_theories = + ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick", + "New_DSequence", "New_Random_Sequence", "Quickcheck", + "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"] + +val is_thm_technical = + member (op =) technical_theories o Context.theory_name o theory_of_thm + (*** Low-level communication with MaSh ***) @@ -700,14 +709,6 @@ (true, "") end) -val evil_theories = - ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick", - "New_DSequence", "New_Random_Sequence", "Quickcheck", - "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"] - -fun fact_has_evil_theory (_, th) = - member (op =) evil_theories (Context.theory_name (theory_of_thm th)) - fun sendback sub = Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub) @@ -722,7 +723,7 @@ Time.+ (Timer.checkRealTimer timer, commit_timeout) val {fact_G} = mash_get ctxt val (old_facts, new_facts) = - facts |> filter_out fact_has_evil_theory + facts |> filter_out (is_thm_technical o snd) |> List.partition (is_fact_in_graph fact_G) ||> sort (thm_ord o pairself snd) in diff -r 784c6f63d79c -r 4e2ee88276d2 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 26 19:57:33 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 26 19:59:06 2012 +0200 @@ -775,9 +775,9 @@ val args = arguments ctxt full_proof extra slice_timeout (ord, ord_info, sel_weights) val command = - File.shell_path command0 ^ " " ^ args ^ " " ^ - File.shell_path prob_file - |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1" + "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ + File.shell_path prob_file ^ ")" + |> enclose "TIMEFORMAT='%3R'; { time " " ; }" val _ = atp_problem |> lines_for_atp_problem format ord ord_info diff -r 784c6f63d79c -r 4e2ee88276d2 src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Thu Jul 26 19:57:33 2012 +0200 +++ b/src/HOL/Tools/try0.ML Thu Jul 26 19:59:06 2012 +0200 @@ -77,12 +77,13 @@ if mode <> Auto_Try orelse run_if_auto_try then let val attrs = attrs_text attrs quad in do_generic timeout_opt - (name ^ (if all_goals andalso - nprems_of (#goal (Proof.goal st)) > 1 then - "[1]" - else - "") ^ - attrs) I (#goal o Proof.goal) + (name ^ attrs ^ + (if all_goals andalso + nprems_of (#goal (Proof.goal st)) > 1 then + " [1]" + else + "")) + I (#goal o Proof.goal) (apply_named_method_on_first_goal (name ^ attrs) (Proof.theory_of st)) st end