# HG changeset patch # User blanchet # Date 1342593845 -7200 # Node ID 2250197977dc366dbb2896e735d5b63e4659019e # Parent 271a4a6af734188f315045d144715a029c8e00ea repair MaSh exporter diff -r 271a4a6af734 -r 2250197977dc src/HOL/TPTP/MaSh_Eval.thy --- 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 () *} diff -r 271a4a6af734 -r 2250197977dc src/HOL/TPTP/MaSh_Export.thy --- 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 diff -r 271a4a6af734 -r 2250197977dc src/HOL/TPTP/mash_eval.ML --- 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 = diff -r 271a4a6af734 -r 2250197977dc src/HOL/TPTP/mash_export.ML --- 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