# HG changeset patch # User blanchet # Date 1342593843 -7200 # Node ID 902ab51dd12a762232667d813a25575248025ebc # Parent a3cb8901d60cb023ded911d351f6ab04f3abbd01 renaming diff -r a3cb8901d60c -r 902ab51dd12a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/IsaMakefile Wed Jul 18 08:44:03 2012 +0200 @@ -1150,8 +1150,8 @@ $(LOG)/HOL-TPTP.gz: $(OUT)/HOL \ TPTP/ATP_Problem_Import.thy \ TPTP/ATP_Theory_Export.thy \ + TPTP/MaSh_Eval.thy \ TPTP/MaSh_Export.thy \ - TPTP/MaSh_Import.thy \ TPTP/ROOT.ML \ TPTP/THF_Arith.thy \ TPTP/TPTP_Parser.thy \ @@ -1164,8 +1164,8 @@ TPTP/TPTP_Parser_Test.thy \ TPTP/atp_problem_import.ML \ TPTP/atp_theory_export.ML \ + TPTP/mash_eval.ML \ TPTP/mash_export.ML \ - TPTP/mash_import.ML \ TPTP/sledgehammer_tactics.ML @$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP diff -r a3cb8901d60c -r 902ab51dd12a src/HOL/TPTP/MaSh_Eval.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/MaSh_Eval.thy Wed Jul 18 08:44:03 2012 +0200 @@ -0,0 +1,35 @@ +(* Title: HOL/TPTP/MaSh_Eval.thy + Author: Jasmin Blanchette, TU Muenchen +*) + +header {* MaSh Evaluation Driver *} + +theory MaSh_Eval +imports Complex_Main +uses "mash_eval.ML" +begin + +sledgehammer_params + [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, + lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] + +declare [[sledgehammer_instantiate_inducts]] + +ML {* +open MaSh_Eval +*} + +ML {* +val do_it = false (* switch to "true" to generate the files *); +val thy = @{theory List}; +val params = Sledgehammer_Isar.default_params @{context} [] +*} + +ML {* +if do_it then + evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions_list" +else + () +*} + +end diff -r a3cb8901d60c -r 902ab51dd12a src/HOL/TPTP/MaSh_Import.thy --- a/src/HOL/TPTP/MaSh_Import.thy Wed Jul 18 08:44:03 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -(* Title: HOL/TPTP/MaSh_Import.thy - Author: Jasmin Blanchette, TU Muenchen -*) - -header {* MaSh Importer *} - -theory MaSh_Import -imports MaSh_Export -uses "mash_import.ML" -begin - -sledgehammer_params - [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, - lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] - -declare [[sledgehammer_instantiate_inducts]] - -ML {* -open MaSh_Import -*} - -ML {* -val do_it = false (* switch to "true" to generate the files *); -val thy = @{theory List}; -val params = Sledgehammer_Isar.default_params @{context} [] -*} - -ML {* -if do_it then - import_and_evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions_list" -else - () -*} - -end diff -r a3cb8901d60c -r 902ab51dd12a src/HOL/TPTP/mash_eval.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:03 2012 +0200 @@ -0,0 +1,156 @@ +(* Title: HOL/TPTP/mash_eval.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Evaluate proof suggestions from MaSh (Machine-learning for Sledgehammer). +*) + +signature MASH_EVAL = +sig + type params = Sledgehammer_Provers.params + + val evaluate_mash_suggestions : + Proof.context -> params -> theory -> string -> unit +end; + +structure MaSh_Eval : MASH_EVAL = +struct + +open Sledgehammer_Filter_MaSh + +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 isaN = "Isa" +val iterN = "Iter" +val mashN = "MaSh" +val iter_mashN = "Iter+MaSh" + +val max_relevant_slack = 2 + +fun evaluate_mash_suggestions ctxt params thy file_name = + let + val {provers, max_relevant, slice, type_enc, lam_trans, timeout, ...} = + Sledgehammer_Isar.default_params ctxt [] + val prover_name = hd provers + val path = file_name |> Path.explode + val lines = path |> File.read_lines + val facts = all_non_tautological_facts_of thy + val all_names = facts |> map (Thm.get_name_hint o snd) + val iter_ok = Unsynchronized.ref 0 + val mash_ok = Unsynchronized.ref 0 + val iter_mash_ok = Unsynchronized.ref 0 + val isa_ok = Unsynchronized.ref 0 + fun find_sugg facts sugg = + find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts + fun sugg_facts hyp_ts concl_t facts = + map_filter (find_sugg facts o of_fact_name) + #> take (max_relevant_slack * the max_relevant) + #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t + #> map (apfst (apfst (fn name => name ()))) + fun iter_mash_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 (the 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 str_of_res label facts {outcome, run_time, used_facts, ...} = + " " ^ label ^ ": " ^ + (if is_none outcome then + "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ + (used_facts |> map (with_index facts o fst) + |> sort (int_ord o pairself fst) + |> map index_string + |> space_implode " ") ^ + (if length facts < the max_relevant then + " (of " ^ string_of_int (length facts) ^ ")" + else + "") + else + "Failure: " ^ + (facts |> map (fst o fst) + |> take (the max_relevant) + |> tag_list 1 + |> map index_string + |> space_implode " ")) + fun prove ok heading facts goal = + let + val facts = facts |> take (the max_relevant) + val res as {outcome, ...} = run_prover ctxt params facts goal + val _ = if is_none outcome then ok := !ok + 1 else () + in str_of_res heading facts res end + fun solve_goal j name suggs = + let + val name = of_fact_name 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 isa_deps = isabelle_dependencies_of all_names th + val goal = goal_of_thm thy th + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 + val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) + val isa_facts = sugg_facts hyp_ts concl_t facts isa_deps + val iter_facts = + iter_facts ctxt params (max_relevant_slack * the max_relevant) goal + facts + val mash_facts = sugg_facts hyp_ts concl_t facts suggs + val iter_mash_facts = iter_mash_facts iter_facts mash_facts + val iter_s = prove iter_ok iterN iter_facts goal + val mash_s = prove mash_ok mashN mash_facts goal + val iter_mash_s = prove iter_mash_ok iter_mashN iter_mash_facts goal + val isa_s = prove isa_ok isaN isa_facts goal + in + ["Goal " ^ string_of_int j ^ ": " ^ name, iter_s, mash_s, iter_mash_s, + isa_s] + |> cat_lines |> tracing + end + val explode_suggs = space_explode " " #> filter_out (curry (op =) "") + fun do_line (j, line) = + case space_explode ":" line of + [goal_name, suggs] => solve_goal j goal_name (explode_suggs suggs) + | _ => () + fun total_of heading ok n = + " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ + Real.fmt (StringCvt.FIX (SOME 1)) + (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)" + val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts + val options = + [prover_name, string_of_int (the max_relevant) ^ " facts", + "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc, + the_default "smart" lam_trans, ATP_Util.string_from_time timeout, + "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] + val n = length lines + in + tracing " * * *"; + tracing ("Options: " ^ commas options); + List.app do_line (tag_list 1 lines); + ["Successes (of " ^ string_of_int n ^ " goals)", + total_of iterN iter_ok n, + total_of mashN mash_ok n, + total_of iter_mashN iter_mash_ok n, + total_of isaN isa_ok n] + |> cat_lines |> tracing + end + +end; diff -r a3cb8901d60c -r 902ab51dd12a src/HOL/TPTP/mash_import.ML --- a/src/HOL/TPTP/mash_import.ML Wed Jul 18 08:44:03 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,157 +0,0 @@ -(* Title: HOL/TPTP/mash_import.ML - Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 - -Import proof suggestions from MaSh (Machine-learning for Sledgehammer) and -evaluate them. -*) - -signature MASH_IMPORT = -sig - type params = Sledgehammer_Provers.params - - val import_and_evaluate_mash_suggestions : - Proof.context -> params -> theory -> string -> unit -end; - -structure MaSh_Import : MASH_IMPORT = -struct - -open Sledgehammer_Filter_MaSh - -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 isaN = "Isabelle" -val iterN = "Iterative" -val mashN = "MaSh" -val iter_mashN = "Iter+MaSh" - -val max_relevant_slack = 2 - -fun import_and_evaluate_mash_suggestions ctxt params thy file_name = - let - val {provers, max_relevant, slice, type_enc, lam_trans, timeout, ...} = - Sledgehammer_Isar.default_params ctxt [] - val prover_name = hd provers - val path = file_name |> Path.explode - val lines = path |> File.read_lines - val facts = all_non_tautological_facts_of thy - val all_names = facts |> map (Thm.get_name_hint o snd) - val iter_ok = Unsynchronized.ref 0 - val mash_ok = Unsynchronized.ref 0 - val iter_mash_ok = Unsynchronized.ref 0 - val isa_ok = Unsynchronized.ref 0 - fun find_sugg facts sugg = - find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts - fun sugg_facts hyp_ts concl_t facts = - map_filter (find_sugg facts o of_fact_name) - #> take (max_relevant_slack * the max_relevant) - #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t - #> map (apfst (apfst (fn name => name ()))) - fun iter_mash_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 (the 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 str_of_res label facts {outcome, run_time, used_facts, ...} = - " " ^ label ^ ": " ^ - (if is_none outcome then - "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ - (used_facts |> map (with_index facts o fst) - |> sort (int_ord o pairself fst) - |> map index_string - |> space_implode " ") ^ - (if length facts < the max_relevant then - " (of " ^ string_of_int (length facts) ^ ")" - else - "") - else - "Failure: " ^ - (facts |> map (fst o fst) - |> take (the max_relevant) - |> tag_list 1 - |> map index_string - |> space_implode " ")) - fun prove ok heading facts goal = - let - val facts = facts |> take (the max_relevant) - val res as {outcome, ...} = run_prover ctxt params facts goal - val _ = if is_none outcome then ok := !ok + 1 else () - in str_of_res heading facts res end - fun solve_goal j name suggs = - let - val name = of_fact_name 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 isa_deps = isabelle_dependencies_of all_names th - val goal = goal_of_thm thy th - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 - val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) - val isa_facts = sugg_facts hyp_ts concl_t facts isa_deps - val iter_facts = - iter_facts ctxt params (max_relevant_slack * the max_relevant) goal - facts - val mash_facts = sugg_facts hyp_ts concl_t facts suggs - val iter_mash_facts = iter_mash_facts iter_facts mash_facts - val iter_s = prove iter_ok iterN iter_facts goal - val mash_s = prove mash_ok mashN mash_facts goal - val iter_mash_s = prove iter_mash_ok iter_mashN iter_mash_facts goal - val isa_s = prove isa_ok isaN isa_facts goal - in - ["Goal " ^ string_of_int j ^ ": " ^ name, iter_s, mash_s, iter_mash_s, - isa_s] - |> cat_lines |> tracing - end - val explode_suggs = space_explode " " #> filter_out (curry (op =) "") - fun do_line (j, line) = - case space_explode ":" line of - [goal_name, suggs] => solve_goal j goal_name (explode_suggs suggs) - | _ => () - fun total_of heading ok n = - " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ - Real.fmt (StringCvt.FIX (SOME 1)) - (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)" - val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts - val options = - [prover_name, string_of_int (the max_relevant) ^ " facts", - "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc, - the_default "smart" lam_trans, ATP_Util.string_from_time timeout, - "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] - val n = length lines - in - tracing " * * *"; - tracing ("Options: " ^ commas options); - List.app do_line (tag_list 1 lines); - ["Successes (of " ^ string_of_int n ^ " goals)", - total_of iterN iter_ok n, - total_of mashN mash_ok n, - total_of iter_mashN iter_mash_ok n, - total_of isaN isa_ok n] - |> cat_lines |> tracing - end - -end;