# HG changeset patch # User blanchet # Date 1342593844 -7200 # Node ID 3c4e10606567542b4e93d2c5222569bdc7d46a82 # Parent cde455ec128f181f20f70811905cdd2fe5ba431a implemented MaSh QUERY operation diff -r cde455ec128f -r 3c4e10606567 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200 @@ -39,10 +39,8 @@ val mash_ok = Unsynchronized.ref 0 val mesh_ok = Unsynchronized.ref 0 val isar_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) + fun sugg_facts hyp_ts concl_t suggs = + suggested_facts suggs #> take (max_facts_slack * the max_facts) #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t fun mesh_facts fsp = @@ -88,8 +86,9 @@ 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 = + fun solve_goal (j, line) = let + val (name, suggs) = extract_query line val th = case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of SOME (_, th) => th @@ -98,12 +97,12 @@ 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 isar_facts = sugg_facts hyp_ts concl_t facts isar_deps + val isar_facts = facts |> sugg_facts hyp_ts concl_t isar_deps val iter_facts = Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params prover_name (max_facts_slack * the max_facts) NONE hyp_ts concl_t facts - val mash_facts = sugg_facts hyp_ts concl_t facts suggs + val mash_facts = facts |> sugg_facts hyp_ts concl_t suggs val mesh_facts = mesh_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 @@ -114,13 +113,6 @@ isar_s] |> cat_lines |> tracing end - val explode_suggs = - space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta - fun do_line (j, line) = - case space_explode ":" line of - [goal_name, suggs] => - solve_goal j (unescape_meta goal_name) (explode_suggs suggs) - | _ => () fun total_of heading ok n = " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1)) @@ -135,7 +127,7 @@ in tracing " * * *"; tracing ("Options: " ^ commas options); - List.app do_line (tag_list 1 lines); + List.app solve_goal (tag_list 1 lines); ["Successes (of " ^ string_of_int n ^ " goals)", total_of iterN iter_ok n, total_of mashN mash_ok n, diff -r cde455ec128f -r 3c4e10606567 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 @@ -19,6 +19,8 @@ val escape_metas : string list -> string val unescape_meta : string -> string val unescape_metas : string -> string list + val extract_query : string -> string * string list + val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list val all_non_tautological_facts_of : theory -> status Termtab.table -> fact list val theory_ord : theory * theory -> order @@ -36,12 +38,12 @@ Proof.context -> (string * string list * string list * string list) list -> unit val mash_DEL : Proof.context -> string list -> string list -> unit - val mash_SUGGEST : Proof.context -> string list -> string list -> string list + val mash_QUERY : Proof.context -> string list * string list -> string list val mash_reset : Proof.context -> unit val mash_can_suggest_facts : Proof.context -> bool val mash_suggest_facts : - Proof.context -> params -> string -> int -> term list -> term -> fact list - -> fact list * fact list + Proof.context -> params -> string -> term list -> term -> fact list + -> fact list val mash_can_learn_thy : Proof.context -> theory -> bool val mash_learn_thy : Proof.context -> theory -> real -> unit val mash_learn_proof : Proof.context -> theory -> term -> thm list -> unit @@ -92,6 +94,17 @@ val unescape_meta = unmeta_chars [] o String.explode val unescape_metas = map unescape_meta o space_explode " " +val explode_suggs = + space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta +fun extract_query line = + case space_explode ":" line of + [goal_name, suggs] => (unescape_meta goal_name, explode_suggs suggs) + | _ => ("", explode_suggs line) + +fun find_suggested facts sugg = + find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts +fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs + val thy_feature_prefix = "y_" val thy_feature_name_of = prefix thy_feature_prefix @@ -278,6 +291,32 @@ (*** Low-level communication with MaSh ***) +fun run_mash ctxt save write_cmds read_preds = + let + val temp_dir = getenv "ISABELLE_TMP" + val serial = serial_string () + val cmd_file = temp_dir ^ "/mash_commands." ^ serial + val cmd_path = Path.explode cmd_file + val pred_file = temp_dir ^ "/mash_preds." ^ serial + val log_file = temp_dir ^ "/mash_log." ^ serial + val command = + getenv "MASH_HOME" ^ "/mash.py --inputFile " ^ cmd_file ^ + " --outputDir " ^ mash_dir () ^ " --predictions " ^ pred_file ^ + " --log " ^ log_file ^ (if save then " --saveModel" else "") ^ + " > /dev/null" + val _ = File.write cmd_path "" + val _ = write_cmds (File.append cmd_path) + val _ = trace_msg ctxt (fn () => " running " ^ command) + val _ = Isabelle_System.bash command + in read_preds (fn () => File.read_lines (Path.explode pred_file)) end + +fun str_of_update (fact, access, feats, deps) = + "! " ^ escape_meta fact ^ ": " ^ escape_metas access ^ "; " ^ + escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" + +fun str_of_query (access, feats) = + "? " ^ escape_metas access ^ "; " ^ escape_metas feats + fun mash_RESET ctxt = let val path = mash_dir () |> Path.explode in trace_msg ctxt (K "MaSh RESET"); @@ -287,39 +326,20 @@ end fun mash_ADD _ [] = () - | mash_ADD ctxt records = - let - val temp_dir = getenv "ISABELLE_TMP" - val serial = serial_string () - val cmd_file = temp_dir ^ "/mash_commands." ^ serial - val cmd_path = Path.explode cmd_file - val pred_file = temp_dir ^ "/mash_preds." ^ serial - val log_file = temp_dir ^ "/mash_log." ^ serial - val _ = File.write cmd_path "" - val _ = - trace_msg ctxt (fn () => - "MaSh ADD " ^ space_implode " " (map #1 records)) - fun append_record (fact, access, feats, deps) = - "! " ^ escape_meta fact ^ ": " ^ escape_metas access ^ "; " ^ - escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" - |> File.append cmd_path - val command = - getenv "MASH_HOME" ^ "/mash.py --inputFile " ^ cmd_file ^ - " --outputDir " ^ mash_dir () ^ " --predictions " ^ pred_file ^ - " --log " ^ log_file ^ " --saveModel > /dev/null" - val _ = trace_msg ctxt (fn () => "Run: " ^ command) - val _ = List.app append_record records - val _ = Isabelle_System.bash command - in () end + | mash_ADD ctxt upds = + (trace_msg ctxt (fn () => "MaSh ADD " ^ space_implode " " (map #1 upds)); + run_mash ctxt true (fn append => List.app (append o str_of_update) upds) + (K ())) fun mash_DEL ctxt facts feats = trace_msg ctxt (fn () => "MaSh DEL " ^ escape_metas facts ^ "; " ^ escape_metas feats) -fun mash_SUGGEST ctxt access feats = - (trace_msg ctxt (fn () => - "MaSh SUGGEST " ^ escape_metas access ^ "; " ^ escape_metas feats); - []) +fun mash_QUERY ctxt (query as (_, feats)) = + (trace_msg ctxt (fn () => "MaSh SUGGEST " ^ space_implode " " feats); + run_mash ctxt false (fn append => append (str_of_query query)) + (fn preds => snd (extract_query (List.last (preds ())))) + handle List.Empty => []) (*** High-level communication with MaSh ***) @@ -385,13 +405,14 @@ fun mash_can_suggest_facts (_ : Proof.context) = not (Symtab.is_empty (#thy_facts (mash_get ()))) -fun mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts = +fun mash_suggest_facts ctxt params prover hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt - val access = accessibility_of thy (#thy_facts (mash_get ())) + val thy_facts = #thy_facts (mash_get ()) + val access = accessibility_of thy thy_facts val feats = features_of thy General (concl_t :: hyp_ts) - val suggs = mash_SUGGEST ctxt access feats - in (facts, []) end + val suggs = mash_QUERY ctxt (access, feats) + in suggested_facts suggs facts end fun mash_can_learn_thy (_ : Proof.context) thy = not (Symtab.defined (#dirty_thys (mash_get ())) (Context.theory_name thy)) @@ -436,18 +457,18 @@ let val ths = facts |> map snd val all_names = ths |> map Thm.get_name_hint - fun do_fact ((_, (_, status)), th) (prevs, records) = + fun do_fact ((_, (_, status)), th) (prevs, upds) = let val name = Thm.get_name_hint th val feats = features_of thy status [prop_of th] val deps = isabelle_dependencies_of all_names th - val record = (name, prevs, feats, deps) - in ([name], record :: records) end + val upd = (name, prevs, feats, deps) + in ([name], upd :: upds) end val parents = parent_facts thy thy_facts - val (_, records) = (parents, []) |> fold do_fact new_facts + val (_, upds) = (parents, []) |> fold do_fact new_facts val new_thy_facts = new_facts |> thy_facts_from_thms fun trans {dirty_thys, thy_facts} = - (mash_ADD ctxt (rev records); + (mash_ADD ctxt (rev upds); {dirty_thys = dirty_thys, thy_facts = thy_facts |> add_thy_facts_from_thys new_thy_facts}) in mash_map trans end @@ -485,8 +506,9 @@ val iter_facts = iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts concl_t facts - val (mash_facts, mash_rejected) = - mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts + val (mash_facts, mash_antifacts) = + facts |> mash_suggest_facts ctxt params prover hyp_ts concl_t + |> chop max_facts val mesh_facts = iter_facts (* ### *) in mesh_facts