--- a/src/HOL/TPTP/MaSh_Eval.thy Mon Feb 18 18:34:55 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy Tue Feb 19 13:21:49 2013 +0100
@@ -28,6 +28,7 @@
val do_it = false (* switch to "true" to generate the files *)
val params = Sledgehammer_Isar.default_params @{context} []
val range = (1, NONE)
+val linearize = false
val dir = "List"
val prefix = "/tmp/" ^ dir ^ "/"
val prob_dir = prefix ^ "mash_problems"
@@ -42,7 +43,7 @@
ML {*
if do_it then
- evaluate_mash_suggestions @{context} params range
+ evaluate_mash_suggestions @{context} params range linearize
[MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
(SOME prob_dir)
(prefix ^ "mepo_suggestions")
--- a/src/HOL/TPTP/MaSh_Export.thy Mon Feb 18 18:34:55 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy Tue Feb 19 13:21:49 2013 +0100
@@ -33,6 +33,7 @@
val prover = hd provers
val range = (1, NONE)
val step = 1
+val linearize = false
val max_suggestions = 1024
val dir = "List"
val prefix = "/tmp/" ^ dir ^ "/"
@@ -47,21 +48,22 @@
ML {*
if do_it then
- generate_accessibility @{context} thys false (prefix ^ "mash_accessibility")
+ generate_accessibility @{context} thys linearize
+ (prefix ^ "mash_accessibility")
else
()
*}
ML {*
if do_it then
- generate_features @{context} prover thys false (prefix ^ "mash_features")
+ generate_features @{context} prover thys (prefix ^ "mash_features")
else
()
*}
ML {*
if do_it then
- generate_isar_dependencies @{context} thys false
+ generate_isar_dependencies @{context} thys linearize
(prefix ^ "mash_dependencies")
else
()
@@ -70,7 +72,7 @@
ML {*
if do_it then
generate_isar_commands @{context} prover (range, step) thys
- (prefix ^ "mash_commands")
+ linearize (prefix ^ "mash_commands")
else
()
*}
@@ -78,7 +80,7 @@
ML {*
if do_it then
generate_mepo_suggestions @{context} params (range, step) thys
- max_suggestions (prefix ^ "mepo_suggestions")
+ linearize max_suggestions (prefix ^ "mepo_suggestions")
else
()
*}
@@ -93,7 +95,7 @@
ML {*
if do_it then
- generate_prover_dependencies @{context} params range thys false
+ generate_prover_dependencies @{context} params range thys linearize
(prefix ^ "mash_prover_dependencies")
else
()
@@ -102,7 +104,7 @@
ML {*
if do_it then
generate_prover_commands @{context} params (range, step) thys
- (prefix ^ "mash_prover_commands")
+ linearize (prefix ^ "mash_prover_commands")
else
()
*}
--- a/src/HOL/TPTP/mash_eval.ML Mon Feb 18 18:34:55 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Tue Feb 19 13:21:49 2013 +0100
@@ -16,8 +16,9 @@
val MeSh_ProverN : string
val IsarN : string
val evaluate_mash_suggestions :
- Proof.context -> params -> int * int option -> string list -> string option
- -> string -> string -> string -> string -> string -> string -> unit
+ Proof.context -> params -> int * int option -> bool -> string list
+ -> string option -> string -> string -> string -> string -> string -> string
+ -> unit
end;
structure MaSh_Eval : MASH_EVAL =
@@ -39,7 +40,7 @@
fun in_range (from, to) j =
j >= from andalso (to = NONE orelse j <= the to)
-fun evaluate_mash_suggestions ctxt params range methods prob_dir_name
+fun evaluate_mash_suggestions ctxt params range linearize methods prob_dir_name
mepo_file_name mash_isar_file_name mash_prover_file_name
mesh_isar_file_name mesh_prover_file_name report_file_name =
let
--- a/src/HOL/TPTP/mash_export.ML Mon Feb 18 18:34:55 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML Tue Feb 19 13:21:49 2013 +0100
@@ -12,21 +12,21 @@
val generate_accessibility :
Proof.context -> theory list -> bool -> string -> unit
val generate_features :
- Proof.context -> string -> theory list -> bool -> string -> unit
+ Proof.context -> string -> theory list -> string -> unit
val generate_isar_dependencies :
Proof.context -> theory list -> bool -> string -> unit
val generate_prover_dependencies :
Proof.context -> params -> int * int option -> theory list -> bool -> string
-> unit
val generate_isar_commands :
- Proof.context -> string -> (int * int option) * int -> theory list -> string
- -> unit
+ Proof.context -> string -> (int * int option) * int -> theory list -> bool
+ -> string -> unit
val generate_prover_commands :
- Proof.context -> params -> (int * int option) * int -> theory list -> string
- -> unit
+ Proof.context -> params -> (int * int option) * int -> theory list -> bool
+ -> string -> unit
val generate_mepo_suggestions :
- Proof.context -> params -> (int * int option) * int -> theory list -> int
- -> string -> unit
+ Proof.context -> params -> (int * int option) * int -> theory list -> bool
+ -> int -> string -> unit
val generate_mesh_suggestions : int -> string -> string -> string -> unit
end;
@@ -51,28 +51,30 @@
|> sort (crude_thm_ord o pairself snd)
end
-fun generate_accessibility ctxt thys include_thys file_name =
+fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th))
+
+fun generate_accessibility ctxt thys linearize file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
- fun do_fact fact prevs =
+ fun do_fact (parents, fact) prevs =
let
- val s = encode_str fact ^ ": " ^ encode_strs prevs ^ "\n"
+ val parents = if linearize then prevs else parents
+ val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n"
val _ = File.append path s
in [fact] end
val facts =
all_facts ctxt
- |> not include_thys ? filter_out (has_thys thys o snd)
- |> map (snd #> nickname_of_thm)
+ |> filter_out (has_thys thys o snd)
+ |> attach_parents_to_facts []
+ |> map (apsnd (nickname_of_thm o snd))
in fold do_fact facts []; () end
-fun generate_features ctxt prover thys include_thys file_name =
+fun generate_features ctxt prover thys file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
- val facts =
- all_facts ctxt
- |> not include_thys ? filter_out (has_thys thys o snd)
+ val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
fun do_fact ((_, stature), th) =
let
val name = nickname_of_thm th
@@ -109,20 +111,22 @@
| NONE => (omitted_marker, [])
end
-fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys
+fun generate_isar_or_prover_dependencies ctxt params_opt range thys linearize
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 facts = all_facts ctxt |> filter_out (has_thys thys o snd)
val name_tabs = build_name_tables nickname_of_thm facts
fun do_fact (j, (_, th)) =
if in_range range j then
let
val name = nickname_of_thm th
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
+ val access_facts =
+ if linearize then take (j - 1) facts
+ else facts |> filter_accessible_from th
val (marker, deps) =
- smart_dependencies_of ctxt params_opt facts name_tabs th NONE
+ smart_dependencies_of ctxt params_opt access_facts name_tabs th NONE
in encode_str name ^ ": " ^ marker ^ " " ^ encode_strs deps ^ "\n" end
else
""
@@ -142,25 +146,29 @@
is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
- file_name =
+ linearize 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 name_tabs = build_name_tables nickname_of_thm facts
- fun do_fact (j, ((name, ((_, stature), th)), prevs)) =
+ fun do_fact (j, ((name, (parents, ((_, stature), th))), prevs)) =
if in_range range j then
let
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
val feats =
features_of ctxt prover (theory_of_thm th) stature [prop_of th]
val isar_deps = isar_dependencies_of name_tabs th
+ val access_facts =
+ (if linearize then take (j - 1) new_facts
+ else new_facts |> filter_accessible_from th) @ old_facts
val (marker, deps) =
- smart_dependencies_of ctxt params_opt facts name_tabs th
+ smart_dependencies_of ctxt params_opt access_facts name_tabs th
(SOME isar_deps)
+ val parents = if linearize then prevs else parents
val core =
- encode_str name ^ ": " ^ encode_strs prevs ^ "; " ^
+ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
encode_features (sort_wrt fst feats)
val query =
if is_bad_query ctxt ho_atp step j th isar_deps then ""
@@ -170,10 +178,12 @@
in query ^ update end
else
""
- val parents =
+ val new_facts =
+ new_facts |> attach_parents_to_facts old_facts
+ |> map (`(nickname_of_thm o snd o snd))
+ val hd_prevs =
map (nickname_of_thm o snd) (the_list (try List.last old_facts))
- val new_facts = new_facts |> map (`(nickname_of_thm o snd))
- val prevss = fst (split_last (parents :: map (single o fst) new_facts))
+ val prevss = fst (split_last (hd_prevs :: map (single o fst) new_facts))
val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss))
in File.write_list path lines end
@@ -184,7 +194,7 @@
generate_isar_or_prover_commands ctxt prover (SOME params)
fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...})
- (range, step) thys max_suggs file_name =
+ (range, step) thys linearize max_suggs file_name =
let
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
val path = file_name |> Path.explode
@@ -206,6 +216,7 @@
let
val suggs =
old_facts
+ |> linearize ? filter_accessible_from th
|> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
max_suggs NONE hyp_ts concl_t
|> map (nickname_of_thm o snd)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Feb 18 18:34:55 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Feb 19 13:21:49 2013 +0100
@@ -56,6 +56,7 @@
('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
-> 'a list
val crude_thm_ord : thm * thm -> order
+ val thm_less : thm * thm -> bool
val goal_of_thm : theory -> thm -> thm
val run_prover_for_mash :
Proof.context -> params -> string -> fact list -> thm -> prover_result
@@ -80,6 +81,8 @@
val mash_learn_proof :
Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
-> unit
+ val attach_parents_to_facts :
+ ('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list
val mash_learn :
Proof.context -> params -> fact_override -> thm list -> bool -> unit
val is_mash_enabled : unit -> bool
@@ -902,6 +905,8 @@
(true, "")
end)
+(* In the following functions, chunks are risers w.r.t. "thm_less_eq". *)
+
fun chunks_and_parents_for chunks th =
let
fun insert_parent new parents =
@@ -925,27 +930,30 @@
in
fold_rev do_chunk chunks ([], [])
|>> cons []
+ ||> map nickname_of_thm
end
-fun attach_parents_to_facts facts =
- let
- fun do_facts _ _ [] = []
- | do_facts _ parents [fact] = [(parents, fact)]
- | do_facts chunks parents ((fact as (_, th)) :: (facts as (_, th') :: _)) =
- let
- val chunks = app_hd (cons th) chunks
- val (chunks', parents') =
- (if thm_less_eq (th, th') andalso
- thy_name_of_thm th = thy_name_of_thm th' then
- (chunks, [th])
- else
- chunks_and_parents_for chunks th')
- ||> map nickname_of_thm
- in (parents, fact) :: do_facts chunks' parents' facts end
- in
- facts |> sort (crude_thm_ord o pairself snd)
- |> do_facts [[]] []
- end
+fun attach_parents_to_facts _ [] = []
+ | attach_parents_to_facts old_facts (facts as (_, th) :: _) =
+ let
+ fun do_facts _ [] = []
+ | do_facts (_, parents) [fact] = [(parents, fact)]
+ | do_facts (chunks, parents)
+ ((fact as (_, th)) :: (facts as (_, th') :: _)) =
+ let
+ val chunks = app_hd (cons th) chunks
+ val chunks_and_parents' =
+ if thm_less_eq (th, th') andalso
+ thy_name_of_thm th = thy_name_of_thm th' then
+ (chunks, [nickname_of_thm th])
+ else
+ chunks_and_parents_for chunks th'
+ in (parents, fact) :: do_facts chunks_and_parents' facts end
+ in
+ old_facts @ facts
+ |> do_facts (chunks_and_parents_for [[]] th)
+ |> drop (length old_facts)
+ end
fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
@@ -1046,12 +1054,12 @@
0
else
let
- val facts =
+ val new_facts =
facts |> attach_parents_to_facts
|> filter_out (is_in_access_G o snd)
val (learns, (n, _, _)) =
([], (0, next_commit_time (), false))
- |> fold learn_new_fact facts
+ |> fold learn_new_fact new_facts
in commit true learns [] []; n end
fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
| relearn_old_fact ((_, (_, status)), th)