# HG changeset patch # User blanchet # Date 1355603672 -3600 # Node ID 89c0d2f13ccad3d8bfa0563e7e1f7f4a4a07ddbf # Parent a719106124d806bfca71a056758e8af1e7c77257 MaSh exporter can now export subsets of the facts, as consecutive ranges diff -r a719106124d8 -r 89c0d2f13cca src/HOL/TPTP/MaSh_Eval.thy --- a/src/HOL/TPTP/MaSh_Eval.thy Sat Dec 15 21:26:10 2012 +0100 +++ b/src/HOL/TPTP/MaSh_Eval.thy Sat Dec 15 21:34:32 2012 +0100 @@ -41,7 +41,7 @@ ML {* if do_it then - evaluate_mash_suggestions @{context} params (SOME prob_dir) + evaluate_mash_suggestions @{context} params (1, NONE) (SOME prob_dir) (prefix ^ "mash_suggestions") (prefix ^ "mash_eval") else () diff -r a719106124d8 -r 89c0d2f13cca src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Sat Dec 15 21:26:10 2012 +0100 +++ b/src/HOL/TPTP/MaSh_Export.thy Sat Dec 15 21:34:32 2012 +0100 @@ -79,7 +79,7 @@ ML {* if do_it then - generate_prover_dependencies @{context} params thys false + generate_prover_dependencies @{context} params (1, NONE) thys false (prefix ^ "mash_prover_dependencies") else () @@ -87,7 +87,7 @@ ML {* if do_it then - generate_prover_commands @{context} params thys + generate_prover_commands @{context} params (1, NONE) thys (prefix ^ "mash_prover_commands") else () diff -r a719106124d8 -r 89c0d2f13cca src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Sat Dec 15 21:26:10 2012 +0100 +++ b/src/HOL/TPTP/mash_eval.ML Sat Dec 15 21:34:32 2012 +0100 @@ -10,7 +10,8 @@ type params = Sledgehammer_Provers.params val evaluate_mash_suggestions : - Proof.context -> params -> string option -> string -> string -> unit + Proof.context -> params -> int * int option -> string option -> string + -> string -> unit end; structure MaSh_Eval : MASH_EVAL = @@ -28,7 +29,10 @@ val MeShN = "MeSh" val IsarN = "Isar" -fun evaluate_mash_suggestions ctxt params prob_dir_name sugg_file_name +fun in_range (from, to) j = + j >= from andalso (to = NONE orelse j <= the to) + +fun evaluate_mash_suggestions ctxt params range prob_dir_name sugg_file_name report_file_name = let val report_path = report_file_name |> Path.explode @@ -70,63 +74,68 @@ |> space_implode " ")) end fun solve_goal (j, line) = - let - val (name, suggs) = extract_query line - val th = - case find_first (fn (_, th) => nickname_of th = name) facts of - SOME (_, th) => th - | NONE => error ("No fact called \"" ^ name ^ "\".") - val goal = goal_of_thm (Proof_Context.theory_of ctxt) th - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 - val isar_deps = isar_dependencies_of all_names th |> these - val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) - val mepo_facts = - mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts - concl_t facts - |> weight_mepo_facts - val (mash_facts, mash_unks) = - find_mash_suggestions slack_max_facts suggs facts [] [] - |>> weight_mash_facts - val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))] - val mesh_facts = mesh_facts slack_max_facts mess - val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts - (* adapted from "mirabelle_sledgehammer.ML" *) - fun set_file_name heading (SOME dir) = + if in_range range j then + let + val (name, suggs) = extract_query line + val th = + case find_first (fn (_, th) => nickname_of th = name) facts of + SOME (_, th) => th + | NONE => error ("No fact called \"" ^ name ^ "\".") + val goal = goal_of_thm (Proof_Context.theory_of ctxt) th + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 + val isar_deps = isar_dependencies_of all_names th |> these + val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) + val mepo_facts = + mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts + concl_t facts + |> weight_mepo_facts + val (mash_facts, mash_unks) = + find_mash_suggestions slack_max_facts suggs facts [] [] + |>> weight_mash_facts + val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))] + val mesh_facts = mesh_facts slack_max_facts mess + val isar_facts = + find_suggested_facts (map (rpair 1.0) isar_deps) facts + (* adapted from "mirabelle_sledgehammer.ML" *) + fun set_file_name heading (SOME dir) = + let + val prob_prefix = + "goal_" ^ string_of_int j ^ "__" ^ escape_meta name ^ "__" ^ + heading + in + Config.put dest_dir dir + #> Config.put problem_prefix (prob_prefix ^ "__") + #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) + end + | set_file_name _ NONE = I + fun prove ok heading get facts = let - val prob_prefix = - "goal_" ^ string_of_int j ^ "__" ^ escape_meta name ^ "__" ^ - heading - in - Config.put dest_dir dir - #> Config.put problem_prefix (prob_prefix ^ "__") - #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) - end - | set_file_name _ NONE = I - fun prove ok heading get facts = - let - fun nickify ((_, stature), th) = ((K (nickname_of th), stature), th) - val facts = - facts - |> map get - |> maybe_instantiate_inducts ctxt hyp_ts concl_t - |> take (the max_facts) - |> map nickify - val ctxt = ctxt |> set_file_name heading prob_dir_name - val res as {outcome, ...} = - run_prover_for_mash ctxt params prover facts goal - val _ = if is_none outcome then ok := !ok + 1 else () - in str_of_res heading facts res end - val [mepo_s, mash_s, mesh_s, isar_s] = - [fn () => prove mepo_ok MePoN fst mepo_facts, - fn () => prove mash_ok MaShN fst mash_facts, - fn () => prove mesh_ok MeShN I mesh_facts, - fn () => prove isar_ok IsarN fst isar_facts] - |> (* Par_List. *) map (fn f => f ()) - in - ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s, - isar_s] - |> cat_lines |> print - end + fun nickify ((_, stature), th) = + ((K (nickname_of th), stature), th) + val facts = + facts + |> map get + |> maybe_instantiate_inducts ctxt hyp_ts concl_t + |> take (the max_facts) + |> map nickify + val ctxt = ctxt |> set_file_name heading prob_dir_name + val res as {outcome, ...} = + run_prover_for_mash ctxt params prover facts goal + val _ = if is_none outcome then ok := !ok + 1 else () + in str_of_res heading facts res end + val [mepo_s, mash_s, mesh_s, isar_s] = + [fn () => prove mepo_ok MePoN fst mepo_facts, + fn () => prove mash_ok MaShN fst mash_facts, + fn () => prove mesh_ok MeShN I mesh_facts, + fn () => prove isar_ok IsarN fst isar_facts] + |> (* Par_List. *) map (fn f => f ()) + in + ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s, + isar_s] + |> cat_lines |> print + end + else + () fun total_of heading ok n = " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1)) diff -r a719106124d8 -r 89c0d2f13cca src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Sat Dec 15 21:26:10 2012 +0100 +++ b/src/HOL/TPTP/mash_export.ML Sat Dec 15 21:34:32 2012 +0100 @@ -16,11 +16,12 @@ val generate_isar_dependencies : Proof.context -> theory list -> bool -> string -> unit val generate_prover_dependencies : - Proof.context -> params -> theory list -> bool -> string -> unit + Proof.context -> params -> int * int option -> theory list -> bool -> string + -> unit val generate_isar_commands : Proof.context -> string -> theory list -> string -> unit val generate_prover_commands : - Proof.context -> params -> theory list -> string -> unit + Proof.context -> params -> int * int option -> theory list -> string -> unit val generate_mepo_suggestions : Proof.context -> params -> theory list -> int -> string -> unit end; @@ -32,6 +33,9 @@ open Sledgehammer_MePo open Sledgehammer_MaSh +fun in_range (from, to) j = + j >= from andalso (to = NONE orelse j <= the to) + fun thy_map_from_facts ths = ths |> rev |> map (snd #> `(theory_of_thm #> Context.theory_name)) @@ -108,24 +112,28 @@ | NONE => isar_dependencies_of all_names th) |> these -fun generate_isar_or_prover_dependencies ctxt params_opt thys include_thys +fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys file_name = let val path = file_name |> Path.explode val facts = all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd) val all_names = build_all_names nickname_of facts - fun do_fact (_, th) = - let - val name = nickname_of th - val deps = - isar_or_prover_dependencies_of ctxt params_opt facts all_names th NONE - in escape_meta name ^ ": " ^ escape_metas deps ^ "\n" end - val lines = Par_List.map do_fact facts + fun do_fact (j, (_, th)) = + if in_range range j then + let + val name = nickname_of th + val deps = + isar_or_prover_dependencies_of ctxt params_opt facts all_names th + NONE + in escape_meta name ^ ": " ^ escape_metas deps ^ "\n" end + else + "" + val lines = Par_List.map do_fact (tag_list 1 facts) in File.write_list path lines end fun generate_isar_dependencies ctxt = - generate_isar_or_prover_dependencies ctxt NONE + generate_isar_or_prover_dependencies ctxt NONE (1, NONE) fun generate_prover_dependencies ctxt params = generate_isar_or_prover_dependencies ctxt (SOME params) @@ -134,38 +142,42 @@ Thm.legacy_get_kind th = "" orelse null isar_deps orelse is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th) -fun generate_isar_or_prover_commands ctxt prover params_opt thys file_name = +fun generate_isar_or_prover_commands ctxt prover params_opt range thys + file_name = let val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover val path = file_name |> Path.explode val facts = all_facts ctxt val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) val all_names = build_all_names nickname_of facts - fun do_fact ((name, ((_, stature), th)), prevs) = - let - val feats = - features_of ctxt prover (theory_of_thm th) stature [prop_of th] - val isar_deps = isar_dependencies_of all_names th - val deps = - isar_or_prover_dependencies_of ctxt params_opt facts all_names th - (SOME isar_deps) - val core = - escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^ - encode_features feats - val query = - if is_bad_query ctxt ho_atp th (these isar_deps) then "" - else "? " ^ core ^ "\n" - val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n" - in query ^ update end + fun do_fact (j, ((name, ((_, stature), th)), prevs)) = + if in_range range j then + let + val feats = + features_of ctxt prover (theory_of_thm th) stature [prop_of th] + val isar_deps = isar_dependencies_of all_names th + val deps = + isar_or_prover_dependencies_of ctxt params_opt facts all_names th + (SOME isar_deps) + val core = + escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^ + encode_features feats + val query = + if is_bad_query ctxt ho_atp th (these isar_deps) then "" + else "? " ^ core ^ "\n" + val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n" + in query ^ update end + else + "" val thy_map = old_facts |> thy_map_from_facts val parents = fold (add_thy_parent_facts thy_map) thys [] val new_facts = new_facts |> map (`(nickname_of o snd)) val prevss = fst (split_last (parents :: map (single o fst) new_facts)) - val lines = Par_List.map do_fact (new_facts ~~ prevss) + val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss)) in File.write_list path lines end fun generate_isar_commands ctxt prover = - generate_isar_or_prover_commands ctxt prover NONE + generate_isar_or_prover_commands ctxt prover NONE (1, NONE) fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) = generate_isar_or_prover_commands ctxt prover (SOME params)