# HG changeset patch # User blanchet # Date 1282659851 -7200 # Node ID 4c6b65d6a1354322a4dcb993decc71aec03ac5db # Parent e85ce10cef1a439f31324c4a9e2aaddcdbb86e1b quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy") diff -r e85ce10cef1a -r 4c6b65d6a135 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 15:29:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 16:24:11 2010 +0200 @@ -13,7 +13,8 @@ val trace : bool Unsynchronized.ref val chained_prefix : string val name_thms_pair_from_ref : - Proof.context -> thm list -> Facts.ref -> string * thm list + Proof.context -> unit Symtab.table -> thm list -> Facts.ref + -> string * thm list val relevant_facts : bool -> real -> real -> bool -> int -> bool -> relevance_override -> Proof.context * (thm list * 'a) -> term list -> term @@ -39,12 +40,13 @@ (* Used to label theorems chained into the goal. *) val chained_prefix = sledgehammer_prefix ^ "chained_" -fun name_thms_pair_from_ref ctxt chained_ths xref = +fun name_thms_pair_from_ref ctxt reserved chained_ths xref = let val ths = ProofContext.get_fact ctxt xref val name = Facts.string_of_ref xref - |> forall (member Thm.eq_thm chained_ths) ths - ? prefix chained_prefix + val name = name |> Symtab.defined reserved name ? quote + |> forall (member Thm.eq_thm chained_ths) ths + ? prefix chained_prefix in (name, ths) end @@ -532,7 +534,7 @@ is_strange_theorem thm end -fun all_name_thms_pairs ctxt full_types add_thms chained_ths = +fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths = let val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); val local_facts = ProofContext.facts_of ctxt @@ -564,18 +566,19 @@ val ths = ths0 |> filter ((not o is_theorem_bad_for_atps full_types) orf member Thm.eq_thm add_thms) + fun backquotify th = + "`" ^ Print_Mode.setmp [Print_Mode.input] + (Syntax.string_of_term ctxt) (prop_of th) ^ "`" val name' = case find_first check_thms [name1, name2, name] of - SOME name' => name' - | NONE => - ths |> map (fn th => - "`" ^ Print_Mode.setmp [Print_Mode.input] - (Syntax.string_of_term ctxt) - (prop_of th) ^ "`") - |> space_implode " " + SOME name' => name' |> Symtab.defined reserved name' ? quote + | NONE => ths |> map_filter (try backquotify) |> space_implode " " in - cons (name' |> forall (member Thm.eq_thm chained_ths) ths0 - ? prefix chained_prefix, ths) + if name' = "" then + I + else + cons (name' |> forall (member Thm.eq_thm chained_ths) ths0 + ? prefix chained_prefix, ths) end) in [] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals) @@ -609,9 +612,10 @@ (ctxt, (chained_ths, _)) hyp_ts concl_t = let val add_thms = maps (ProofContext.get_fact ctxt) add + val reserved = reserved_isar_keyword_table () val axioms = - (if only then map (name_thms_pair_from_ref ctxt chained_ths) add - else all_name_thms_pairs ctxt full_types add_thms chained_ths) + (if only then map (name_thms_pair_from_ref ctxt reserved chained_ths) add + else all_name_thms_pairs ctxt reserved full_types add_thms chained_ths) |> name_thm_pairs ctxt (respect_no_atp andalso not only) |> make_unique in diff -r e85ce10cef1a -r 4c6b65d6a135 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 24 15:29:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 24 16:24:11 2010 +0200 @@ -157,8 +157,10 @@ fun run_minimize params i refs state = let val ctxt = Proof.context_of state + val reserved = reserved_isar_keyword_table () val chained_ths = #facts (Proof.goal state) - val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs + val name_thms_pairs = + map (name_thms_pair_from_ref ctxt reserved chained_ths) refs in case subgoal_count state of 0 => priority "No subgoal!" diff -r e85ce10cef1a -r 4c6b65d6a135 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 24 15:29:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 24 16:24:11 2010 +0200 @@ -613,8 +613,8 @@ "Try this command: " ^ Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "." fun minimize_line _ [] = "" - | minimize_line minimize_command facts = - case minimize_command facts of + | minimize_line minimize_command ss = + case minimize_command ss of "" => "" | command => "\nTo minimize the number of lemmas, try this: " ^ diff -r e85ce10cef1a -r 4c6b65d6a135 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Aug 24 15:29:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Aug 24 16:24:11 2010 +0200 @@ -21,6 +21,7 @@ val specialize_type : theory -> (string * typ) -> term -> term val subgoal_count : Proof.state -> int val strip_subgoal : thm -> int -> (string * typ) list * term list * term + val reserved_isar_keyword_table : unit -> unit Symtab.table end; structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = @@ -155,4 +156,8 @@ val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees in (rev (map dest_Free frees), hyp_ts, concl_t) end +fun reserved_isar_keyword_table () = + union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ()) + |> map (rpair ()) |> Symtab.make + end;