# HG changeset patch # User blanchet # Date 1356623352 -3600 # Node ID 4d0997abce796f08857ffa0d6c11cded3e33d88f # Parent f104b10af6e7f04e5589e59926e913667e98dba5 improved thm order hack, in case the default names are overridden diff -r f104b10af6e7 -r 4d0997abce79 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Thu Dec 27 15:46:27 2012 +0100 +++ b/src/HOL/TPTP/mash_eval.ML Thu Dec 27 16:49:12 2012 +0100 @@ -46,7 +46,7 @@ val lines = sugg_path |> File.read_lines val css = clasimpset_rule_table_of ctxt val facts = all_facts ctxt true false Symtab.empty [] [] css - val all_names = build_all_names nickname_of facts + val all_names = build_all_names nickname_of_thm facts fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) fun index_string (j, s) = s ^ "@" ^ string_of_int j fun str_of_res label facts ({outcome, run_time, used_facts, ...} @@ -74,7 +74,7 @@ let val (name, suggs) = extract_query line val th = - case find_first (fn (_, th) => nickname_of th = name) facts of + case find_first (fn (_, th) => nickname_of_thm th = name) facts of SOME (_, th) => th | NONE => error ("No fact called \"" ^ name ^ "\".") val goal = goal_of_thm (Proof_Context.theory_of ctxt) th @@ -107,7 +107,7 @@ fun prove heading get facts = let fun nickify ((_, stature), th) = - ((K (escape_meta (nickname_of th)), stature), th) + ((K (escape_meta (nickname_of_thm th)), stature), th) val facts = facts |> map (get #> nickify) diff -r f104b10af6e7 -r 4d0997abce79 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Thu Dec 27 15:46:27 2012 +0100 +++ b/src/HOL/TPTP/mash_export.ML Thu Dec 27 16:49:12 2012 +0100 @@ -59,7 +59,7 @@ val facts = all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd) - |> map (snd #> nickname_of) + |> map (snd #> nickname_of_thm) in fold do_fact facts []; () end fun generate_features ctxt prover thys include_thys file_name = @@ -71,7 +71,7 @@ |> not include_thys ? filter_out (has_thys thys o snd) fun do_fact ((_, stature), th) = let - val name = nickname_of th + val name = nickname_of_thm th val feats = features_of ctxt prover (theory_of_thm th) stature [prop_of th] val s = @@ -96,11 +96,11 @@ val path = file_name |> Path.explode val facts = all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd) - val all_names = build_all_names nickname_of facts + val all_names = build_all_names nickname_of_thm facts fun do_fact (j, (_, th)) = if in_range range j then let - val name = nickname_of th + val name = nickname_of_thm th val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) val deps = isar_or_prover_dependencies_of ctxt params_opt facts all_names th @@ -128,7 +128,7 @@ val path = file_name |> Path.explode val facts = all_facts ctxt val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) - val all_names = build_all_names nickname_of facts + val all_names = build_all_names nickname_of_thm facts fun do_fact (j, ((name, ((_, stature), th)), prevs)) = if in_range range j then let @@ -149,8 +149,9 @@ in query ^ update end else "" - val parents = map (nickname_of o snd) (the_list (try List.last old_facts)) - val new_facts = new_facts |> map (`(nickname_of o snd)) + val parents = + map (nickname_of_thm o snd) (the_list (try List.last old_facts)) + val new_facts = new_facts |> map (`(nickname_of_thm o snd)) val prevss = fst (split_last (parents :: map (single o fst) new_facts)) val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss)) in File.write_list path lines end @@ -168,10 +169,10 @@ val path = file_name |> Path.explode val facts = all_facts ctxt val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) - val all_names = build_all_names nickname_of facts + val all_names = build_all_names nickname_of_thm facts fun do_fact ((_, th), old_facts) = let - val name = nickname_of th + val name = nickname_of_thm th val goal = goal_of_thm (Proof_Context.theory_of ctxt) th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 val isar_deps = isar_dependencies_of all_names th @@ -184,7 +185,7 @@ old_facts |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t - |> map (nickname_of o snd) + |> map (nickname_of_thm o snd) in escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" end end fun accum x (yss as ys :: _) = (x :: ys) :: yss diff -r f104b10af6e7 -r 4d0997abce79 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 27 15:46:27 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 27 16:49:12 2012 +0100 @@ -40,7 +40,7 @@ Proof.context -> bool -> int -> string list * (string * real) list -> (string * real) list val mash_unlearn : Proof.context -> unit - val nickname_of : thm -> string + val nickname_of_thm : thm -> string val find_suggested_facts : (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list val mesh_facts : @@ -403,7 +403,7 @@ val local_prefix = "local" ^ Long_Name.separator -fun nickname_of th = +fun nickname_of_thm th = if Thm.has_name_hint th then let val hint = Thm.get_name_hint th in (* FIXME: There must be a better way to detect local facts. *) @@ -417,7 +417,7 @@ fun find_suggested_facts suggs facts = let - fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact) + fun add_fact (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact) val tab = Symtab.empty |> fold add_fact facts fun find_sugg (name, weight) = Symtab.lookup tab name |> Option.map (rpair weight) @@ -489,8 +489,12 @@ fun thm_ord p = case theory_ord (pairself theory_of_thm p) of EQUAL => - (* Hack to put "xxx_def" before "xxxI" and "xxxE" *) - string_ord (pairself nickname_of (swap p)) + let val q = pairself nickname_of_thm p in + (* Hack to put "xxx_def" before "xxxI" and "xxxE" *) + case bool_ord (pairself (String.isSuffix "_def") (swap q)) of + EQUAL => string_ord q + | ord => ord + end | ord => ord val freezeT = Type.legacy_freeze_type @@ -604,7 +608,7 @@ val prover_dependency_default_max_facts = 50 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) -val typedef_deps = [@{thm CollectI} |> nickname_of] +val typedef_deps = [@{thm CollectI} |> nickname_of_thm] (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) val typedef_ths = @@ -614,12 +618,12 @@ type_definition.Abs_cases type_definition.Rep_induct type_definition.Abs_induct type_definition.Rep_range type_definition.Abs_image} - |> map nickname_of + |> map nickname_of_thm fun is_size_def [dep] th = (case first_field ".recs" dep of SOME (pref, _) => - (case first_field ".size" (nickname_of th) of + (case first_field ".size" (nickname_of_thm th) of SOME (pref', _) => pref = pref' | NONE => false) | NONE => false) @@ -649,8 +653,9 @@ val goal = goal_of_thm thy th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) - fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th) - fun is_dep dep (_, th) = nickname_of th = dep + fun nickify ((_, stature), th) = + ((fn () => nickname_of_thm th, stature), th) + fun is_dep dep (_, th) = nickname_of_thm th = dep fun add_isar_dep facts dep accum = if exists (is_dep dep) accum then accum @@ -663,11 +668,11 @@ (max_facts |> the_default prover_dependency_default_max_facts) NONE hyp_ts concl_t |> fold (add_isar_dep facts) (these isar_deps) - |> map fix_name + |> map nickify in if verbose andalso auto_level = 0 then let val num_facts = length facts in - "MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of th) ^ + "MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of_thm th) ^ " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ "." |> Output.urgent_message @@ -697,7 +702,7 @@ fun maximal_in_graph access_G facts = let - val facts = [] |> fold (cons o nickname_of o snd) facts + val facts = [] |> fold (cons o nickname_of_thm o snd) facts val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts fun insert_new seen name = not (Symtab.defined seen name) ? insert (op =) name @@ -726,7 +731,7 @@ in find_maxes Symtab.empty ([], Graph.maximals access_G) end fun is_fact_in_graph access_G (_, th) = - can (Graph.get_node access_G) (nickname_of th) + can (Graph.get_node access_G) (nickname_of_thm th) val weight_raw_mash_facts = weight_mepo_facts val weight_mash_facts = weight_raw_mash_facts @@ -825,7 +830,7 @@ val thy = Proof_Context.theory_of ctxt val name = freshish_name () val feats = features_of ctxt prover thy (Local, General) [t] - val deps = used_ths |> map nickname_of + val deps = used_ths |> map nickname_of_thm in peek_state ctxt (fn {access_G, ...} => let val parents = maximal_in_graph access_G facts in @@ -863,7 +868,7 @@ "" else let - val all_names = build_all_names nickname_of facts + val all_names = build_all_names nickname_of_thm facts fun deps_of status th = if status = Non_Rec_Def orelse status = Rec_Def then SOME [] @@ -911,7 +916,7 @@ | learn_new_fact ((_, stature as (_, status)), th) (adds, (parents, n, next_commit, _)) = let - val name = nickname_of th + val name = nickname_of_thm th val feats = features_of ctxt prover (theory_of_thm th) stature [prop_of th] val deps = deps_of status th |> these @@ -946,7 +951,7 @@ | relearn_old_fact ((_, (_, status)), th) ((reps, flops), (n, next_commit, _)) = let - val name = nickname_of th + val name = nickname_of_thm th val (n, reps, flops) = case deps_of status th of SOME deps => (n + 1, (name, deps) :: reps, flops) @@ -968,7 +973,7 @@ let val max_isar = 1000 * max_dependencies fun kind_of_proof th = - try (Graph.get_node access_G) (nickname_of th) + try (Graph.get_node access_G) (nickname_of_thm th) |> the_default Isar_Proof fun priority_of (_, th) = random_range 0 max_isar