repaired accessibility chains generated by MaSh exporter + tuned one function out
--- a/src/HOL/TPTP/atp_theory_export.ML Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Thu Jul 26 10:48:03 2012 +0200
@@ -123,7 +123,8 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val facts =
- Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
+ Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) false
+ Symtab.empty [] [] css_table
val atp_problem =
facts
|> map (fn ((_, loc), th) =>
--- a/src/HOL/TPTP/mash_eval.ML Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Thu Jul 26 10:48:03 2012 +0200
@@ -36,8 +36,9 @@
val slack_max_facts = max_facts_slack * the max_facts
val path = file_name |> Path.explode
val lines = path |> File.read_lines
- val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
- val facts = all_facts_of (Proof_Context.init_global thy) css_table
+ val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+ val facts =
+ all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
val all_names = all_names (facts |> map snd)
val mepo_ok = Unsynchronized.ref 0
val mash_ok = Unsynchronized.ref 0
@@ -70,7 +71,7 @@
val th =
case find_first (fn (_, th) => nickname_of th = name) facts of
SOME (_, th) => th
- | NONE => error ("No fact called \"" ^ name ^ "\"")
+ | NONE => error ("No fact called \"" ^ name ^ "\".")
val goal = goal_of_thm thy th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val isar_deps = isar_dependencies_of all_names th |> these
--- a/src/HOL/TPTP/mash_export.ML Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Thu Jul 26 10:48:03 2012 +0200
@@ -9,11 +9,11 @@
sig
type params = Sledgehammer_Provers.params
- val generate_accessibility : theory -> bool -> string -> unit
+ val generate_accessibility : Proof.context -> theory -> bool -> string -> unit
val generate_features :
Proof.context -> string -> theory -> bool -> string -> unit
val generate_isar_dependencies :
- theory -> bool -> string -> unit
+ Proof.context -> theory -> bool -> string -> unit
val generate_atp_dependencies :
Proof.context -> params -> theory -> bool -> string -> unit
val generate_commands : Proof.context -> params -> theory -> string -> unit
@@ -56,7 +56,7 @@
SOME deps => deps
| NONE => isar_dependencies_of all_names th |> these
-fun generate_accessibility thy include_thy file_name =
+fun generate_accessibility ctxt thy include_thy file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
@@ -65,24 +65,25 @@
val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
val _ = File.append path s
in [fact] end
+ val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val thy_map =
- all_facts_of (Proof_Context.init_global thy) Termtab.empty
+ all_facts ctxt false Symtab.empty [] [] css
|> not include_thy ? filter_out (has_thy thy o snd)
|> thy_map_from_facts
fun do_thy facts =
let
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 do_fact facts parents; () end
in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end
fun generate_features ctxt prover thy include_thy file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
- val css_table = clasimpset_rule_table_of ctxt
+ val css = clasimpset_rule_table_of ctxt
val facts =
- all_facts_of (Proof_Context.init_global thy) css_table
+ all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
|> not include_thy ? filter_out (has_thy thy o snd)
fun do_fact ((_, stature), th) =
let
@@ -93,12 +94,13 @@
in File.append path s end
in List.app do_fact facts end
-fun generate_isar_dependencies thy include_thy file_name =
+fun generate_isar_dependencies ctxt thy include_thy file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
+ val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val ths =
- all_facts_of (Proof_Context.init_global thy) Termtab.empty
+ all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
|> not include_thy ? filter_out (has_thy thy o snd)
|> map snd
val all_names = all_names ths
@@ -116,8 +118,9 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val prover = hd provers
+ val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val facts =
- all_facts_of (Proof_Context.init_global thy) Termtab.empty
+ all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
|> not include_thy ? filter_out (has_thy thy o snd)
val ths = facts |> map snd
val all_names = all_names ths
@@ -134,8 +137,9 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val prover = hd provers
- val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
- val facts = all_facts_of (Proof_Context.init_global thy) css_table
+ val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+ val facts =
+ all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
val (new_facts, old_facts) =
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
@@ -164,8 +168,9 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val prover = hd provers
- val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
- val facts = all_facts_of (Proof_Context.init_global thy) css_table
+ val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+ val facts =
+ all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
val (new_facts, old_facts) =
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Jul 26 10:48:03 2012 +0200
@@ -29,7 +29,9 @@
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_of : Proof.context -> status Termtab.table -> fact list
+ val all_facts :
+ Proof.context -> bool -> unit Symtab.table -> thm list -> thm list
+ -> status Termtab.table -> fact list
val nearly_all_facts :
Proof.context -> bool -> fact_override -> unit Symtab.table
-> status Termtab.table -> thm list -> term list -> term -> fact list
@@ -436,10 +438,6 @@
|> op @
end
-fun all_facts_of ctxt css =
- all_facts ctxt false Symtab.empty [] [] css
- |> rev (* partly restore the original order of facts, for MaSh *)
-
fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
concl_t =
if only andalso null add then