--- 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
--- 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
--- 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