--- a/src/HOL/TPTP/MaSh_Eval.thy Wed Jul 18 08:44:05 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Eval.thy Wed Jul 18 08:44:05 2012 +0200
@@ -5,7 +5,7 @@
header {* MaSh Evaluation Driver *}
theory MaSh_Eval
-imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d"
+imports Complex_Main
uses "mash_eval.ML"
begin
@@ -20,14 +20,14 @@
*}
ML {*
-val do_it = false (* switch to "true" to generate the files *);
-val thy = @{theory Nat};
+val do_it = false (* switch to "true" to generate the files *)
+val thy = @{theory Nat}
val params = Sledgehammer_Isar.default_params @{context} []
*}
ML {*
if do_it then
- evaluate_mash_suggestions @{context} params thy "/Users/blanchet/tum/mash/mash/results/natNB200ATP-15.pred"
+ evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions"
else
()
*}
--- a/src/HOL/TPTP/MaSh_Export.thy Wed Jul 18 08:44:05 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy Wed Jul 18 08:44:05 2012 +0200
@@ -5,7 +5,7 @@
header {* MaSh Exporter *}
theory MaSh_Export
-imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d"
+imports Complex_Main
uses "mash_export.ML"
begin
@@ -18,9 +18,10 @@
*}
ML {*
-val do_it = false (* switch to "true" to generate the files *);
-val thy = @{theory List};
-val params = Sledgehammer_Isar.default_params @{context} []
+val do_it = false (* switch to "true" to generate the files *)
+val thy = @{theory List}
+val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
+val prover = hd provers
*}
ML {*
@@ -32,14 +33,28 @@
ML {*
if do_it then
- generate_features @{context} thy false "/tmp/mash_features"
+ generate_features @{context} prover thy false "/tmp/mash_features"
else
()
*}
ML {*
if do_it then
- generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
+ generate_isar_dependencies thy false "/tmp/mash_dependencies"
+else
+ ()
+*}
+
+ML {*
+if do_it then
+ generate_commands @{context} prover thy "/tmp/mash_commands"
+else
+ ()
+*}
+
+ML {*
+if do_it then
+ generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
else
()
*}
@@ -51,18 +66,5 @@
()
*}
-ML {*
-if do_it then
- generate_commands @{context} thy "/tmp/mash_commands"
-else
- ()
-*}
-
-ML {*
-if do_it then
- generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
-else
- ()
-*}
end
--- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:05 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:05 2012 +0200
@@ -27,7 +27,7 @@
val max_facts_slack = 2
val all_names =
- filter_out (is_likely_tautology_or_too_meta)
+ filter_out is_likely_tautology_or_too_meta
#> map (rpair () o Thm.get_name_hint) #> Symtab.make
fun evaluate_mash_suggestions ctxt params thy file_name =
--- a/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:05 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:05 2012 +0200
@@ -12,9 +12,9 @@
val generate_accessibility : theory -> bool -> string -> unit
val generate_features :
Proof.context -> string -> theory -> bool -> string -> unit
- val generate_isa_dependencies :
+ val generate_isar_dependencies :
theory -> bool -> string -> unit
- val generate_prover_dependencies :
+ val generate_atp_dependencies :
Proof.context -> params -> theory -> bool -> string -> unit
val generate_commands : Proof.context -> string -> theory -> string -> unit
val generate_iter_suggestions :
@@ -50,7 +50,7 @@
fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact
val all_names =
- filter_out (is_likely_tautology_or_too_meta)
+ filter_out is_likely_tautology_or_too_meta
#> map (rpair () o Thm.get_name_hint) #> Symtab.make
fun generate_accessibility thy include_thy file_name =
@@ -71,7 +71,7 @@
val thy = thy_of_fact thy (hd facts)
val parents = parent_facts thy thy_map
in fold do_fact facts parents; () end
- in fold_rev (fn (_, facts) => K (do_thy facts)) thy_map () end
+ in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end
fun generate_features ctxt prover thy include_thy file_name =
let
@@ -90,7 +90,7 @@
in File.append path s end
in List.app do_fact facts end
-fun generate_isa_dependencies thy include_thy file_name =
+fun generate_isar_dependencies thy include_thy file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
@@ -107,8 +107,8 @@
in File.append path s end
in List.app do_thm ths end
-fun generate_prover_dependencies ctxt (params as {provers, max_facts, ...}) thy
- include_thy file_name =
+fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy
+ include_thy file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
@@ -119,7 +119,7 @@
val ths = facts |> map snd
val all_names = all_names ths
fun is_dep dep (_, th) = Thm.get_name_hint th = dep
- fun add_isa_dep facts dep accum =
+ fun add_isar_dep facts dep accum =
if exists (is_dep dep) accum then
accum
else case find_first (is_dep dep) facts of
@@ -135,21 +135,21 @@
val deps =
case isabelle_dependencies_of all_names th of
[] => []
- | isa_dep as [_] => isa_dep (* can hardly beat that *)
- | isa_deps =>
+ | isar_dep as [_] => isar_dep (* can hardly beat that *)
+ | isar_deps =>
let
val facts =
facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
val facts =
facts |> iterative_relevant_facts ctxt params prover
(the max_facts) NONE hyp_ts concl_t
- |> fold (add_isa_dep facts) isa_deps
+ |> fold (add_isar_dep facts) isar_deps
|> map fix_name
in
case run_prover_for_mash ctxt params prover facts goal of
{outcome = NONE, used_facts, ...} =>
used_facts |> map fst |> sort string_ord
- | _ => isa_deps
+ | _ => isar_deps
end
val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
in File.append path s end