# HG changeset patch # User blanchet # Date 1355276865 -3600 # Node ID 3c6ac2da2f4519f918e3eaf114db8fc7aa10e0cc # Parent 8ec31bdb9d36bd5d7a1210301953b81914a0d01e merge aliased theorems in MaSh dependencies, modulo symmetry of equality diff -r 8ec31bdb9d36 -r 3c6ac2da2f45 src/HOL/TPTP/atp_theory_export.ML --- 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 = diff -r 8ec31bdb9d36 -r 3c6ac2da2f45 src/HOL/TPTP/mash_eval.ML --- 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 diff -r 8ec31bdb9d36 -r 3c6ac2da2f45 src/HOL/TPTP/mash_export.ML --- 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 diff -r 8ec31bdb9d36 -r 3c6ac2da2f45 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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 diff -r 8ec31bdb9d36 -r 3c6ac2da2f45 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 [] diff -r 8ec31bdb9d36 -r 3c6ac2da2f45 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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]