--- a/src/HOL/TPTP/atp_theory_export.ML Wed Dec 12 00:24:06 2012 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Wed Dec 12 02:47:45 2012 +0100
@@ -136,13 +136,13 @@
val atp_problem =
atp_problem
|> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
- val ths = facts |> map snd
- val all_names = ths |> map (rpair () o Thm.get_name_hint) |> Symtab.make
+ val all_names = Sledgehammer_Fact.build_all_names Thm.get_name_hint facts
val infers =
- facts |> map (fn (_, th) =>
- (fact_name_of (Thm.get_name_hint th),
- th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
- |> map fact_name_of))
+ facts
+ |> map (fn (_, th) =>
+ (fact_name_of (Thm.get_name_hint th),
+ th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
+ |> map fact_name_of))
val all_atp_problem_names =
atp_problem |> maps (map ident_of_problem_line o snd)
val infers =
--- a/src/HOL/TPTP/mash_eval.ML Wed Dec 12 00:24:06 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Wed Dec 12 02:47:45 2012 +0100
@@ -24,8 +24,6 @@
val MeShN = "MeSh"
val IsarN = "Isar"
-val all_names = map (rpair () o nickname_of) #> Symtab.make
-
fun evaluate_mash_suggestions ctxt params prob_dir_name sugg_file_name
report_file_name =
let
@@ -40,7 +38,7 @@
val lines = sugg_path |> File.read_lines
val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val facts = all_facts ctxt true false Symtab.empty [] [] css
- val all_names = all_names (facts |> map snd)
+ val all_names = build_all_names nickname_of facts
val mepo_ok = Unsynchronized.ref 0
val mash_ok = Unsynchronized.ref 0
val mesh_ok = Unsynchronized.ref 0
--- a/src/HOL/TPTP/mash_export.ML Wed Dec 12 00:24:06 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML Wed Dec 12 02:47:45 2012 +0100
@@ -28,11 +28,12 @@
structure MaSh_Export : MASH_EXPORT =
struct
+open Sledgehammer_Fact
open Sledgehammer_MePo
open Sledgehammer_MaSh
fun thy_map_from_facts ths =
- ths |> sort (thm_ord o swap o pairself snd)
+ ths |> rev
|> map (snd #> `(theory_of_thm #> Context.theory_name))
|> AList.coalesce (op =)
|> map (apsnd (map nickname_of))
@@ -45,6 +46,7 @@
fun all_facts ctxt =
let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
Sledgehammer_Fact.all_facts ctxt true false Symtab.empty [] [] css
+ |> sort (thm_ord o pairself snd)
end
fun add_thy_parent_facts thy_map thy =
@@ -59,8 +61,6 @@
val thy_name_of_fact = hd o Long_Name.explode
fun thy_of_fact thy = Context.get_theory thy o thy_name_of_fact
-val all_names = map (rpair () o nickname_of) #> Symtab.make
-
fun generate_accessibility ctxt thys include_thys file_name =
let
val path = file_name |> Path.explode
@@ -110,18 +110,16 @@
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 ths = facts |> map snd
- val all_names = all_names ths
- fun do_thm th =
+ all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd)
+ val all_names = build_all_names nickname_of facts
+ fun do_fact (_, th) =
let
val name = nickname_of th
val deps =
isar_or_prover_dependencies_of ctxt params_opt facts all_names th
val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
in File.append path s end
- in List.app do_thm ths end
+ in List.app do_fact facts end
fun generate_isar_dependencies ctxt =
generate_isar_or_prover_dependencies ctxt NONE
@@ -134,10 +132,8 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val facts = all_facts ctxt
- val (new_facts, old_facts) =
- facts |> List.partition (has_thys thys o snd)
- |>> sort (thm_ord o pairself snd)
- val all_names = all_names (map snd facts)
+ val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
+ val all_names = build_all_names nickname_of facts
fun do_fact ((_, stature), th) prevs =
let
val name = nickname_of th
@@ -171,9 +167,7 @@
val _ = File.write path ""
val prover = hd provers
val facts = all_facts ctxt
- val (new_facts, old_facts) =
- facts |> List.partition (has_thys thys o snd)
- |>> sort (thm_ord o pairself snd)
+ val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
fun do_fact (fact as (_, th)) old_facts =
let
val name = nickname_of th
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Dec 12 00:24:06 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Dec 12 02:47:45 2012 +0100
@@ -25,7 +25,8 @@
-> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
val backquote_thm : Proof.context -> thm -> string
val clasimpset_rule_table_of : Proof.context -> status Termtab.table
- val normalize_eq : term -> term
+ val build_all_names :
+ (thm -> string) -> ('a * thm) list -> string Symtab.table
val maybe_instantiate_inducts :
Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
-> (((unit -> string) * 'a) * thm) list
@@ -320,9 +321,25 @@
else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 $ t2 $ t1))
| normalize_eq t = t
-fun uniquify xs =
+val normalize_eq_etc = normalize_eq o Term_Subst.zero_var_indexes
+
+fun if_thm_before th th' =
+ if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
+
+fun build_all_names name_of facts =
+ Termtab.fold
+ (fn (_, aliases as main :: _) =>
+ fold (fn alias =>
+ Symtab.update (name_of alias,
+ name_of (if_thm_before main alias))) aliases)
+ (fold_rev (fn (_, thm) =>
+ Termtab.cons_list (normalize_eq_etc (prop_of thm), thm))
+ facts Termtab.empty)
+ Symtab.empty
+
+fun uniquify facts =
Termtab.fold (cons o snd)
- (fold (Termtab.default o `(normalize_eq o prop_of o snd)) xs
+ (fold (Termtab.default o `(normalize_eq_etc o prop_of o snd)) facts
Termtab.empty) []
fun struct_induct_rule_on th =
@@ -411,36 +428,37 @@
I
else
let
- val multi = length ths > 1
+ val n = length ths
+ val multi = n > 1
fun check_thms a =
case try (Proof_Context.get_thms ctxt) a of
NONE => false
| SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
in
- pair 1
- #> fold (fn th => fn (j, (multis, unis)) =>
- (j + 1,
- if not (member Thm.eq_thm_prop add_ths th) andalso
- is_theorem_bad_for_atps ho_atp th then
- (multis, unis)
- else
- let
- val new =
- (((fn () =>
- if name0 = "" then
- backquote_thm ctxt th
- else
- [Facts.extern ctxt facts name0,
- Name_Space.extern ctxt full_space name0]
- |> find_first check_thms
- |> the_default name0
- |> make_name reserved multi j),
- stature_of_thm global assms chained css name0
- th), th)
- in
- if multi then (new :: multis, unis)
- else (multis, new :: unis)
- end)) ths
+ pair n
+ #> fold_rev (fn th => fn (j, (multis, unis)) =>
+ (j - 1,
+ if not (member Thm.eq_thm_prop add_ths th) andalso
+ is_theorem_bad_for_atps ho_atp th then
+ (multis, unis)
+ else
+ let
+ val new =
+ (((fn () =>
+ if name0 = "" then
+ backquote_thm ctxt th
+ else
+ [Facts.extern ctxt facts name0,
+ Name_Space.extern ctxt full_space name0]
+ |> find_first check_thms
+ |> the_default name0
+ |> make_name reserved multi j),
+ stature_of_thm global assms chained css name0 th),
+ th)
+ in
+ if multi then (new :: multis, unis)
+ else (multis, new :: unis)
+ end)) ths
#> snd
end)
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Dec 12 00:24:06 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Dec 12 02:47:45 2012 +0100
@@ -54,9 +54,9 @@
val features_of :
Proof.context -> string -> theory -> stature -> term list
-> (string * real) list
- val isar_dependencies_of : unit Symtab.table -> thm -> string list option
+ val isar_dependencies_of : string Symtab.table -> thm -> string list option
val prover_dependencies_of :
- Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
+ Proof.context -> params -> string -> int -> fact list -> string Symtab.table
-> thm -> bool * string list option
val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list
val find_mash_suggestions :
@@ -296,7 +296,7 @@
local
-val version = "*** MaSh version 20121205c ***"
+val version = "*** MaSh version 20121212a ***"
exception Too_New of unit
@@ -836,7 +836,7 @@
val commit_timeout = seconds 30.0
-(* The timeout is understood in a very slack fashion. *)
+(* The timeout is understood in a very relaxed fashion. *)
fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover
auto_level run_prover learn_timeout facts =
let
@@ -844,9 +844,9 @@
fun next_commit_time () =
Time.+ (Timer.checkRealTimer timer, commit_timeout)
val {fact_G, ...} = mash_get ctxt
+ val facts = facts |> sort (thm_ord o pairself snd)
val (old_facts, new_facts) =
facts |> List.partition (is_fact_in_graph fact_G)
- ||> sort (thm_ord o pairself snd)
in
if null new_facts andalso (not run_prover orelse null old_facts) then
if auto_level < 2 then
@@ -861,9 +861,7 @@
""
else
let
- val all_names =
- Symtab.empty
- |> fold Symtab.update (facts |> map (rpair () o nickname_of o snd))
+ val all_names = build_all_names nickname_of facts
fun deps_of status th =
if status = Non_Rec_Def orelse status = Rec_Def then
SOME []
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Dec 12 00:24:06 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Dec 12 02:47:45 2012 +0100
@@ -17,7 +17,7 @@
val parse_time_option : string -> string -> Time.time option
val subgoal_count : Proof.state -> int
val reserved_isar_keyword_table : unit -> unit Symtab.table
- val thms_in_proof : unit Symtab.table option -> thm -> string list
+ val thms_in_proof : string Symtab.table option -> thm -> string list
val thms_of_name : Proof.context -> string -> thm list
val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
end;
@@ -97,7 +97,10 @@
let
val collect =
case all_names of
- SOME names => (fn s => Symtab.defined names s ? insert (op =) s)
+ SOME names =>
+ (fn s => case Symtab.lookup names s of
+ SOME s' => insert (op =) s'
+ | NONE => I)
| NONE => insert (op =)
val names =
[] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]