# HG changeset patch # User blanchet # Date 1342593843 -7200 # Node ID f5b160f9859e24041c2c3c1e26e772ca6644d210 # Parent dcf3160376ae87f7f72017fc7b2d46e16aceba4d more work on MaSh diff -r dcf3160376ae -r f5b160f9859e src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:03 2012 +0200 @@ -34,7 +34,7 @@ val isaN = "Isa" val iterN = "Iter" val mashN = "MaSh" -val iter_mashN = "Iter+MaSh" +val meshN = "Mesh" val max_facts_slack = 2 @@ -49,7 +49,7 @@ 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 mesh_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 @@ -57,7 +57,7 @@ map_filter (find_sugg facts o of_fact_name) #> take (max_facts_slack * the max_facts) #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t - fun hybrid_facts fsp = + fun mesh_facts fsp = let val (fs1, fs2) = fsp |> pairself (map (apfst (apfst (fn name => name ())))) @@ -117,14 +117,13 @@ 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 iter_mash_facts = hybrid_facts (iter_facts, mash_facts) + 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 - val iter_mash_s = prove iter_mash_ok iter_mashN iter_mash_facts goal + val mesh_s = prove mesh_ok meshN mesh_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] + ["Goal " ^ string_of_int j ^ ": " ^ name, iter_s, mash_s, mesh_s, isa_s] |> cat_lines |> tracing end val explode_suggs = space_explode " " #> filter_out (curry (op =) "") @@ -150,7 +149,7 @@ ["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 meshN mesh_ok n, total_of isaN isa_ok n] |> cat_lines |> tracing end diff -r dcf3160376ae -r f5b160f9859e src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 18 08:44:03 2012 +0200 @@ -28,9 +28,6 @@ Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list - val all_facts : - Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list - -> status Termtab.table -> fact list val all_facts_of : theory -> fact list val nearly_all_facts : Proof.context -> bool -> fact_override -> thm list -> term list -> term diff -r dcf3160376ae -r f5b160f9859e src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:03 2012 +0200 @@ -30,14 +30,14 @@ val generate_isa_dependencies : theory -> bool -> string -> unit val generate_atp_dependencies : Proof.context -> params -> theory -> bool -> string -> unit - - val reset : unit -> unit - val can_suggest_facts : unit -> bool -(* ### val suggest_facts : ... *) - val can_learn_thy : theory -> bool - val learn_thy : theory -> real -> unit - val learn_proof : theory -> term -> thm list -> unit - + val mash_reset : unit -> unit + val mash_can_suggest_facts : unit -> bool + val mash_suggest_facts : + theory -> params -> string -> int -> term list -> term -> fact list + -> fact list * fact list + val mash_can_learn_thy : theory -> bool + val mash_learn_thy : theory -> real -> unit + val mash_learn_proof : theory -> term -> thm list -> unit val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> term -> fact list -> fact list @@ -56,17 +56,17 @@ (*** Low-level communication with MaSh ***) -fun mash_reset () = +fun mash_RESET () = tracing "MaSh RESET" -fun mash_add fact (access, feats, deps) = +fun mash_ADD fact (access, feats, deps) = tracing ("MaSh ADD " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^ space_implode " " feats ^ "; " ^ space_implode " " deps) -fun mash_del fact = +fun mash_DEL fact = tracing ("MaSh DEL " ^ fact) -fun mash_suggest fact (access, feats) = +fun mash_SUGGEST fact (access, feats) = tracing ("MaSh SUGGEST " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^ space_implode " " feats) @@ -365,18 +365,21 @@ (*** High-level communication with MaSh ***) -fun reset () = () +fun mash_reset () = () -fun can_suggest_facts () = true +fun mash_can_suggest_facts () = true -fun can_learn_thy thy = true +fun mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts = + (facts, []) -fun learn_thy thy timeout = () +fun mash_can_learn_thy thy = true -fun learn_proof thy t ths = () +fun mash_learn_thy thy timeout = () + +fun mash_learn_proof thy t ths = () fun relevant_facts ctxt params prover max_facts - ({add, only, ...} : fact_override) hyp_ts concl_t facts = + ({add, only, ...} : fact_override) hyp_ts concl_t facts = if only then facts else if max_facts <= 0 then @@ -388,10 +391,14 @@ ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @ (accepts |> filter_out (member Thm.eq_thm_prop ths o snd))) |> take max_facts + 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 mesh_facts = iter_facts in - facts - |> iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts - concl_t + mesh_facts |> not (null add_ths) ? prepend_facts add_ths end