# HG changeset patch # User blanchet # Date 1342593844 -7200 # Node ID 89674e5a4d35eac445e25becc4a953cedf476129 # Parent 7c78f14d20cffae170cd470336b35dc4f573126c make tracing an option diff -r 7c78f14d20cf -r 89674e5a4d35 src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Wed Jul 18 08:44:04 2012 +0200 @@ -31,7 +31,7 @@ open Sledgehammer_Provers val trace = - Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false) + Attrib.setup_config_bool @{binding sledgehammer_filter_iter_trace} (K false) fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator diff -r 7c78f14d20cf -r 89674e5a4d35 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 @@ -14,8 +14,11 @@ type relevance_fudge = Sledgehammer_Provers.relevance_fudge type prover_result = Sledgehammer_Provers.prover_result + val trace : bool Config.T val escape_meta : string -> string val escape_metas : string list -> string + val unescape_meta : string -> string + val unescape_metas : string -> string list val all_non_tautological_facts_of : theory -> status Termtab.table -> fact list val theory_ord : theory * theory -> order @@ -28,18 +31,20 @@ val goal_of_thm : theory -> thm -> thm val run_prover : Proof.context -> params -> fact list -> thm -> prover_result val thy_name_of_fact : string -> string - val mash_RESET : unit -> unit - val mash_ADD : (string * string list * string list * string list) list -> unit - val mash_DEL : string list -> string list -> unit - val mash_SUGGEST : string list -> string list -> string list - val mash_reset : unit -> unit - val mash_can_suggest_facts : unit -> bool + val mash_RESET : Proof.context -> unit + val mash_ADD : + 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_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 - val mash_can_learn_thy : theory -> bool - val mash_learn_thy : Proof.context -> real -> unit - val mash_learn_proof : theory -> term -> thm list -> unit + val mash_can_learn_thy : Proof.context -> theory -> bool + val mash_learn_thy : Proof.context -> theory -> real -> unit + val mash_learn_proof : Proof.context -> term -> thm list -> unit val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> term -> fact list -> fact list @@ -55,6 +60,10 @@ open Sledgehammer_Filter_Iter open Sledgehammer_Provers +val trace = + Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false) +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () + val mash_dir = "mash" val model_file = "model" val state_file = "state" @@ -63,11 +72,10 @@ getenv "ISABELLE_HOME_USER" ^ "/" ^ mash_dir ^ "/" ^ file |> Path.explode -val fresh_fact_prefix = Long_Name.separator (*** Isabelle helpers ***) -fun escape_meta_char c = +fun meta_char c = if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse c = #")" orelse c = #"," then String.str c @@ -75,8 +83,18 @@ (* fixed width, in case more digits follow *) "\\" ^ stringN_of_int 3 (Char.ord c) -val escape_meta = String.translate escape_meta_char +fun unmeta_chars accum [] = String.implode (rev accum) + | unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) = + (case Int.fromString (String.implode [d1, d2, d3]) of + SOME n => unmeta_chars (Char.chr n :: accum) cs + | NONE => "" (* error *)) + | unmeta_chars _ (#"\\" :: _) = "" (* error *) + | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs + +val escape_meta = String.translate meta_char val escape_metas = map escape_meta #> space_implode " " +val unescape_meta = unmeta_chars [] o String.explode +val unescape_metas = map unescape_meta o space_explode " " val thy_feature_prefix = "y_" @@ -254,18 +272,6 @@ Sledgehammer_Provers.Normal (hd provers) in prover params (K (K (K ""))) problem end -(* ### -fun compute_accessibility thy thy_facts = - let - fun add_facts (f :: fs) prevs = (f, prevs) :: add_facts fs [th] - fun add_thy facts = - let - val thy = theory_of_thm (hd facts) - val parents = parent_facts thy_facts thy - in add_facts facts parents end - in fold (add_thy o snd) thy_facts end -*) - fun accessibility_of thy thy_facts = case Symtab.lookup thy_facts (Context.theory_name thy) of SOME (fact :: _) => [fact] @@ -276,36 +282,37 @@ (*** Low-level communication with MaSh ***) -fun mash_RESET () = (warning "MaSh RESET"; File.rm (mk_path model_file)) +fun mash_RESET ctxt = + (trace_msg ctxt (K "MaSh RESET"); File.write (mk_path model_file) "") -val mash_ADD = +fun mash_ADD ctxt = let fun add_record (fact, access, feats, deps) = let val s = escape_meta fact ^ ": " ^ escape_metas access ^ "; " ^ escape_metas feats ^ "; " ^ escape_metas deps - in warning ("MaSh ADD " ^ s) end + in trace_msg ctxt (fn () => "MaSh ADD " ^ s) end in List.app add_record end -fun mash_DEL facts feats = - warning ("MaSh DEL " ^ escape_metas facts ^ "; " ^ escape_metas feats) +fun mash_DEL ctxt facts feats = + trace_msg ctxt (fn () => + "MaSh DEL " ^ escape_metas facts ^ "; " ^ escape_metas feats) -fun mash_SUGGEST access feats = - (warning ("MaSh SUGGEST " ^ escape_metas access ^ "; " ^ escape_metas feats); +fun mash_SUGGEST ctxt access feats = + (trace_msg ctxt (fn () => + "MaSh SUGGEST " ^ escape_metas access ^ "; " ^ escape_metas feats); []) (*** High-level communication with MaSh ***) type mash_state = - {fresh : int, - dirty_thys : unit Symtab.table, + {dirty_thys : unit Symtab.table, thy_facts : string list Symtab.table} val empty_state = - {fresh = 0, - dirty_thys = Symtab.empty, + {dirty_thys = Symtab.empty, thy_facts = Symtab.empty} local @@ -318,31 +325,30 @@ in (true, case try File.read_lines path of - SOME (fresh_line :: dirty_line :: facts_lines) => + SOME (dirty_line :: facts_lines) => let fun dirty_thys_of_line line = - Symtab.make (line |> space_explode " " |> map (rpair ())) + Symtab.make (line |> unescape_metas |> map (rpair ())) fun add_facts_line line = - case space_explode " " line of + case unescape_metas line of thy :: facts => Symtab.update_new (thy, facts) | _ => I (* shouldn't happen *) in - {fresh = Int.fromString fresh_line |> the_default 0, - dirty_thys = dirty_thys_of_line dirty_line, + {dirty_thys = dirty_thys_of_line dirty_line, thy_facts = fold add_facts_line facts_lines Symtab.empty} end | _ => empty_state) end -fun mash_save ({fresh, dirty_thys, thy_facts} : mash_state) = +fun mash_save ({dirty_thys, thy_facts} : mash_state) = let val path = mk_path state_file - val dirty_line = (dirty_thys |> Symtab.keys |> escape_metas) ^ "\n" + val dirty_line = (escape_metas (Symtab.keys dirty_thys)) ^ "\n" fun fact_line_for (thy, facts) = escape_metas (thy :: facts) ^ "\n" in - File.write path (string_of_int fresh ^ "\n" ^ dirty_line); + File.write path dirty_line; Symtab.fold (fn thy_fact => fn () => - File.append path (fact_line_for thy_fact)) thy_facts + File.append path (fact_line_for thy_fact)) thy_facts () end val global_state = @@ -353,27 +359,27 @@ fun mash_map f = Synchronized.change global_state (mash_load ##> (f #> tap mash_save)) -fun mash_peek f = Synchronized.change global_state (mash_load ##> tap f) - fun mash_get () = Synchronized.change_result global_state (mash_load #> `snd) -fun mash_reset () = +fun mash_reset ctxt = Synchronized.change global_state (fn _ => - (mash_RESET (); File.rm (mk_path state_file); (true, empty_state))) + (mash_RESET ctxt; File.write (mk_path state_file) ""; + (true, empty_state))) end -fun mash_can_suggest_facts () = not (Symtab.is_empty (#thy_facts (mash_get ()))) +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 = let val thy = Proof_Context.theory_of ctxt val access = accessibility_of thy (#thy_facts (mash_get ())) val feats = features_of thy General (concl_t :: hyp_ts) - val suggs = mash_SUGGEST access feats + val suggs = mash_SUGGEST ctxt access feats in (facts, []) end -fun mash_can_learn_thy thy = +fun mash_can_learn_thy (_ : Proof.context) thy = not (Symtab.defined (#dirty_thys (mash_get ())) (Context.theory_name thy)) fun is_fact_in_thy_facts thy_facts fact = @@ -401,60 +407,55 @@ | NONE => Symtab.update_new (thy, new_facts) in old |> Symtab.fold add_thy new end -fun mash_learn_thy ctxt timeout = +fun mash_learn_thy ctxt thy timeout = let - val thy = Proof_Context.theory_of ctxt val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val facts = all_non_tautological_facts_of thy css_table val {thy_facts, ...} = mash_get () fun is_old (_, th) = is_fact_in_thy_facts thy_facts (Thm.get_name_hint th) val (old_facts, new_facts) = facts |> List.partition is_old ||> sort (thm_ord o pairself snd) - val ths = facts |> map snd - val all_names = ths |> map Thm.get_name_hint - fun do_fact ((_, (_, status)), th) (prevs, records) = + in + if null new_facts then + () + else 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 parents = parent_facts thy thy_facts - val (_, records) = (parents, []) |> fold_rev do_fact new_facts - val new_thy_facts = new_facts |> thy_facts_from_thms - fun trans {fresh, dirty_thys, thy_facts} = - (mash_ADD records; - {fresh = fresh, dirty_thys = dirty_thys, - thy_facts = thy_facts |> add_thy_facts_from_thys new_thy_facts}) - in mash_map trans end + val ths = facts |> map snd + val all_names = ths |> map Thm.get_name_hint + fun do_fact ((_, (_, status)), th) (prevs, records) = + 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 parents = parent_facts thy thy_facts + val (_, records) = (parents, []) |> fold_rev do_fact new_facts + val new_thy_facts = new_facts |> thy_facts_from_thms + fun trans {dirty_thys, thy_facts} = + (mash_ADD ctxt records; + {dirty_thys = dirty_thys, + thy_facts = thy_facts |> add_thy_facts_from_thys new_thy_facts}) + in mash_map trans end + end -(* ### -fun compute_accessibility thy thy_facts = - let - fun add_facts (f :: fs) prevs = (f, prevs) :: add_facts fs [th] - fun add_thy facts = - let - val thy = theory_of_thm (hd facts) - val parents = parent_facts thy_facts thy - in add_facts facts parents end - in fold (add_thy o snd) thy_facts end -*) - -fun mash_learn_proof thy t ths = - mash_map (fn state as {fresh, dirty_thys, thy_facts} => - let val deps = ths |> map Thm.get_name_hint in - if forall (is_fact_in_thy_facts thy_facts) deps then - let - val fact = fresh_fact_prefix ^ string_of_int fresh - val access = accessibility_of thy thy_facts - val feats = features_of thy General [t] - in - mash_ADD [(fact, access, feats, deps)]; - {fresh = fresh + 1, dirty_thys = dirty_thys, thy_facts = thy_facts} - end - else - state - end) +fun mash_learn_proof ctxt t ths = + let val thy = Proof_Context.theory_of ctxt in + mash_map (fn state as {dirty_thys, thy_facts} => + let val deps = ths |> map Thm.get_name_hint in + if forall (is_fact_in_thy_facts thy_facts) deps then + let + val fact = ATP_Util.timestamp () (* should be fairly fresh *) + val access = accessibility_of thy thy_facts + val feats = features_of thy General [t] + in + mash_ADD ctxt [(fact, access, feats, deps)]; + {dirty_thys = dirty_thys, thy_facts = thy_facts} + end + else + state + end) + end fun relevant_facts ctxt params prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = diff -r 7c78f14d20cf -r 89674e5a4d35 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 18 08:44:04 2012 +0200 @@ -36,8 +36,7 @@ val running_proversN = "running_provers" val kill_proversN = "kill_provers" val refresh_tptpN = "refresh_tptp" -val mash_resetN = "mash_reset" -val mash_learnN = "mash_learn" +val reset_mashN = "reset_mash" val auto = Unsynchronized.ref false @@ -377,10 +376,8 @@ kill_provers () else if subcommand = refresh_tptpN then refresh_systems_on_tptp () - else if subcommand = mash_resetN then - mash_reset () - else if subcommand = mash_learnN then - () (* TODO: implement *) + else if subcommand = reset_mashN then + mash_reset ctxt else error ("Unknown subcommand: " ^ quote subcommand ^ ".") end