# HG changeset patch # User blanchet # Date 1341956163 -7200 # Node ID 40655464a93b3d2840d5bda79c2aa94b449fecaa # Parent 06216c789ac98f63ecfc9ba26e69e51213b0239f MaSh evaluation driver diff -r 06216c789ac9 -r 40655464a93b src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Tue Jul 10 23:36:03 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Export.thy Tue Jul 10 23:36:03 2012 +0200 @@ -14,41 +14,32 @@ *} ML {* -val do_it = false; (* switch to "true" to generate the files *) -val thy = @{theory List}; -val ctxt = @{context} +val do_it = false (* switch to "true" to generate the files *) +val thy = @{theory List} *} ML {* -if do_it then - "/tmp/mash_sample_problem.out" - |> generate_mash_problem_file_for_theory thy -else - () +if do_it then generate_mash_commands thy "/tmp/mash_commands" +else () +*} + +ML {* +if do_it then generate_mash_features thy false "/tmp/mash_features" +else () *} ML {* -if do_it then - "/tmp/mash_features.out" - |> generate_mash_feature_file_for_theory thy false -else - () +if do_it then generate_mash_accessibility thy false "/tmp/mash_accessibility" +else () *} ML {* -if do_it then - "/tmp/mash_accessibility.out" - |> generate_mash_accessibility_file_for_theory thy false -else - () +if do_it then generate_mash_dependencies thy false "/tmp/mash_dependencies" +else () *} ML {* -if do_it then - "/tmp/mash_dependencies.out" - |> generate_mash_dependency_file_for_theory thy false -else - () +find_index (curry (op =) 22) [0, 0, 9, 1, 2, 3] *} end diff -r 06216c789ac9 -r 40655464a93b src/HOL/TPTP/MaSh_Import.thy --- a/src/HOL/TPTP/MaSh_Import.thy Tue Jul 10 23:36:03 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Import.thy Tue Jul 10 23:36:03 2012 +0200 @@ -9,4 +9,18 @@ uses "mash_import.ML" begin +ML {* +open MaSh_Import +*} + +ML {* +val do_it = true (* switch to "true" to generate the files *); +val thy = @{theory List} +*} + +ML {* +if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions2" +else () +*} + end diff -r 06216c789ac9 -r 40655464a93b src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Tue Jul 10 23:36:03 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jul 10 23:36:03 2012 +0200 @@ -63,6 +63,7 @@ let val ctxt = Proof_Context.init_global thy in Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] [] (Sledgehammer_Filter.clasimpset_rule_table_of ctxt) + |> rev (* try to restore the original order of facts, for MaSh *) end fun inference_term [] = NONE diff -r 06216c789ac9 -r 40655464a93b src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Tue Jul 10 23:36:03 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Tue Jul 10 23:36:03 2012 +0200 @@ -7,12 +7,17 @@ signature MASH_EXPORT = sig - val generate_mash_accessibility_file_for_theory : - theory -> bool -> string -> unit - val generate_mash_feature_file_for_theory : theory -> bool -> string -> unit - val generate_mash_dependency_file_for_theory : - theory -> bool -> string -> unit - val generate_mash_problem_file_for_theory : theory -> string -> unit + type stature = ATP_Problem_Generate.stature + + val non_tautological_facts_of : + theory -> (((unit -> string) * stature) * thm) list + val theory_ord : theory * theory -> order + val thm_ord : thm * thm -> order + val dependencies_of : string list -> thm -> string list + val generate_mash_accessibility : theory -> bool -> string -> unit + val generate_mash_features : theory -> bool -> string -> unit + val generate_mash_dependencies : theory -> bool -> string -> unit + val generate_mash_commands : theory -> string -> unit end; structure MaSh_Export : MASH_EXPORT = @@ -29,8 +34,6 @@ if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse c = #")" orelse c = #"," then String.str c - else if c = #"'" then - "~" else (* fixed width, in case more digits follow *) "\\" ^ stringN_of_int 3 (Char.ord c) @@ -189,7 +192,7 @@ val dependencies_of = map fact_name_of oo theorems_mentioned_in_proof_term o SOME -fun generate_mash_accessibility_file_for_theory thy include_thy file_name = +fun generate_mash_accessibility thy include_thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" @@ -212,7 +215,7 @@ val _ = List.app (do_thy o snd) thy_ths in () end -fun generate_mash_feature_file_for_theory thy include_thy file_name = +fun generate_mash_features thy include_thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" @@ -228,7 +231,7 @@ val _ = List.app do_fact facts in () end -fun generate_mash_dependency_file_for_theory thy include_thy file_name = +fun generate_mash_dependencies thy include_thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" @@ -246,7 +249,7 @@ val _ = List.app do_thm ths in () end -fun generate_mash_problem_file_for_theory thy file_name = +fun generate_mash_commands thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" diff -r 06216c789ac9 -r 40655464a93b src/HOL/TPTP/mash_import.ML --- a/src/HOL/TPTP/mash_import.ML Tue Jul 10 23:36:03 2012 +0200 +++ b/src/HOL/TPTP/mash_import.ML Tue Jul 10 23:36:03 2012 +0200 @@ -8,8 +8,141 @@ signature MASH_IMPORT = sig + val import_and_evaluate_mash_suggestions : + Proof.context -> theory -> string -> unit end; structure MaSh_Import : MASH_IMPORT = struct + +val unescape_meta = + let + fun un accum [] = String.implode (rev accum) + | un accum (#"\\" :: d1 :: d2 :: d3 :: cs) = + (case Int.fromString (String.implode [d1, d2, d3]) of + SOME n => un (Char.chr n :: accum) cs + | NONE => "" (* error *)) + | un _ (#"\\" :: _) = "" (* error *) + | un accum (c :: cs) = un (c :: accum) cs + in un [] o String.explode end + +val of_fact_name = unescape_meta + +val freezeT = Type.legacy_freeze_type; + +fun freeze (t $ u) = freeze t $ freeze u + | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t) + | freeze (Var ((s, _), T)) = Free (s, freezeT T) + | freeze (Const (s, T)) = Const (s, freezeT T) + | freeze (Free (s, T)) = Free (s, freezeT T) + | freeze t = t + +val prover_name = ATP_Systems.spassN +val max_relevant = 40 +val slack_max_relevant = 2 * max_relevant +val timeout = 2 + +fun import_and_evaluate_mash_suggestions ctxt thy file_name = + let + val params as {relevance_thresholds, ...} = + Sledgehammer_Isar.default_params ctxt + [("strict", "true"), + ("slice", "false"), + ("timeout", string_of_int timeout), + ("preplay_timeout", "0"), + ("minimize", "true")] + val is_built_in_const = + Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name + val relevance_fudge = + Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name + val relevance_override = {add = [], del = [], only = false} + val path = file_name |> Path.explode + val lines = path |> File.read_lines + val facts = non_tautological_facts_of thy + val all_names = facts |> map (Thm.get_name_hint o snd) + val i = 1 + fun run_sh facts goal = + let + val facts = + facts |> take max_relevant + |> map Sledgehammer_Provers.Untranslated_Fact + val problem = + {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = 1, + facts = facts} + val prover = + Sledgehammer_Run.get_minimizing_prover ctxt + Sledgehammer_Provers.Normal prover_name + in prover params (K (K (K ""))) problem end + fun meng_facts goal = + let val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i in + Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds + slack_max_relevant is_built_in_const relevance_fudge + relevance_override [] hyp_ts concl_t + end + fun find_sugg facts sugg = + find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts + fun sugg_facts facts = + map_filter (find_sugg facts o of_fact_name) + #> take slack_max_relevant + #> map (apfst (apfst (fn name => name ()))) + fun hybrid_facts fs1 fs2 = + let + val fact_eq = (op =) o pairself fst + fun score_in f fs = + case find_index (curry fact_eq f) fs of + ~1 => length fs + | j => j + fun score_of f = score_in f fs1 + score_in f fs2 + in + union fact_eq fs1 fs2 + |> map (`score_of) + |> sort (int_ord o pairself fst) + |> map snd + |> take max_relevant + end + fun with_index facts s = + (find_index (fn ((s', _), _) => s = s') facts + 1, s) + fun index_string (j, s) = s ^ "@" ^ string_of_int j + fun print_res label facts {outcome, run_time, used_facts, ...} = + tracing (" " ^ label ^ ": " ^ + (if is_none outcome then + "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ + space_implode " " + (used_facts |> map (with_index facts o fst) + |> sort (int_ord o pairself fst) + |> map index_string) + else + "Failure: " ^ space_implode " " (map (fst o fst) facts) )) + fun solve_goal name suggs = + let + val name = of_fact_name name + val _ = tracing ("Goal: " ^ name) + val th = + case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of + SOME (_, th) => th + | NONE => error ("No fact called \"" ^ name ^ "\"") + val deps = dependencies_of all_names th + val goal = th |> prop_of |> freeze |> cterm_of thy |> Goal.init + val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) + val deps_facts = sugg_facts facts deps + val meng_facts = meng_facts goal facts + val mash_facts = sugg_facts facts suggs + val hybrid_facts = hybrid_facts meng_facts mash_facts + val deps_res = run_sh deps_facts goal + val meng_res = run_sh meng_facts goal + val mash_res = run_sh mash_facts goal + val hybrid_res = run_sh hybrid_facts goal + in + print_res "Dependencies" deps_facts deps_res; + print_res "Meng & Paulson" meng_facts meng_res; + print_res "MaSh" mash_facts mash_res; + print_res "Hybrid" hybrid_facts hybrid_res + end + val explode_suggs = space_explode " " #> filter_out (curry (op =) "") + fun do_line line = + case space_explode ":" line of + [goal_name, suggs] => solve_goal goal_name (explode_suggs suggs) + | _ => () + in List.app do_line lines end + end;