# HG changeset patch # User wenzelm # Date 1205600884 -3600 # Node ID 533dcb120a8e9a57b06ecd7423f4e7c4afb9ff0e # Parent e19a5a7e83f1f64088f0ad3ee4abff8434648f40 replaced obsolete FactIndex.T by Facts.T; removed unused get_thm(s)_closure; removed obsolete theorems_of, fact_index_of, lthms_containing, hide_thms; diff -r e19a5a7e83f1 -r 533dcb120a8e src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Mar 15 18:08:03 2008 +0100 +++ b/src/Pure/Isar/proof_context.ML Sat Mar 15 18:08:04 2008 +0100 @@ -29,8 +29,7 @@ val mk_const: Proof.context -> string * typ list -> term val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context - val theorems_of: Proof.context -> thm list NameSpace.table - val fact_index_of: Proof.context -> FactIndex.T + val facts_of: Proof.context -> Facts.T val transfer: theory -> Proof.context -> Proof.context val theory: (theory -> theory) -> Proof.context -> Proof.context val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context @@ -93,18 +92,14 @@ val fact_tac: thm list -> int -> tactic val some_fact_tac: Proof.context -> int -> tactic val get_thm: Proof.context -> thmref -> thm - val get_thm_closure: Proof.context -> thmref -> thm val get_thms: Proof.context -> thmref -> thm list - val get_thms_closure: Proof.context -> thmref -> thm list val valid_thms: Proof.context -> string * thm list -> bool - val lthms_containing: Proof.context -> FactIndex.spec -> (string * thm list) list val add_path: string -> Proof.context -> Proof.context val no_base_names: Proof.context -> Proof.context val qualified_names: Proof.context -> Proof.context val sticky_prefix: string -> Proof.context -> Proof.context val restore_naming: Proof.context -> Proof.context -> Proof.context val reset_naming: Proof.context -> Proof.context - val hide_thms: bool -> string list -> Proof.context -> Proof.context val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context val note_thmss: string -> ((bstring * attribute list) * (thmref * attribute list) list) list -> @@ -155,7 +150,6 @@ struct val theory_of = Context.theory_of_proof; - val init = Context.init_proof; @@ -187,12 +181,12 @@ naming: NameSpace.naming, (*local naming conventions*) syntax: LocalSyntax.T, (*local syntax*) consts: Consts.T * Consts.T, (*local/global consts*) - thms: thm list NameSpace.table * FactIndex.T, (*local thms*) - cases: (string * (RuleCases.T * bool)) list}; (*local contexts*) + facts: Facts.T, (*local facts*) + cases: (string * (RuleCases.T * bool)) list}; (*named case contexts*) -fun make_ctxt (mode, naming, syntax, consts, thms, cases) = +fun make_ctxt (mode, naming, syntax, consts, facts, cases) = Ctxt {mode = mode, naming = naming, syntax = syntax, - consts = consts, thms = thms, cases = cases}; + consts = consts, facts = facts, cases = cases}; val local_naming = NameSpace.default_naming |> NameSpace.add_path "local"; @@ -201,42 +195,41 @@ type T = ctxt; fun init thy = make_ctxt (mode_default, local_naming, LocalSyntax.init thy, - (Sign.consts_of thy, Sign.consts_of thy), - (NameSpace.empty_table, FactIndex.empty), []); + (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []); ); fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args); fun map_context f = - ContextData.map (fn Ctxt {mode, naming, syntax, consts, thms, cases} => - make_ctxt (f (mode, naming, syntax, consts, thms, cases))); + ContextData.map (fn Ctxt {mode, naming, syntax, consts, facts, cases} => + make_ctxt (f (mode, naming, syntax, consts, facts, cases))); -fun set_mode mode = map_context (fn (_, naming, syntax, consts, thms, cases) => - (mode, naming, syntax, consts, thms, cases)); +fun set_mode mode = map_context (fn (_, naming, syntax, consts, facts, cases) => + (mode, naming, syntax, consts, facts, cases)); fun map_mode f = - map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, consts, thms, cases) => - (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, consts, thms, cases)); + map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, consts, facts, cases) => + (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, consts, facts, cases)); fun map_naming f = - map_context (fn (mode, naming, syntax, consts, thms, cases) => - (mode, f naming, syntax, consts, thms, cases)); + map_context (fn (mode, naming, syntax, consts, facts, cases) => + (mode, f naming, syntax, consts, facts, cases)); fun map_syntax f = - map_context (fn (mode, naming, syntax, consts, thms, cases) => - (mode, naming, f syntax, consts, thms, cases)); + map_context (fn (mode, naming, syntax, consts, facts, cases) => + (mode, naming, f syntax, consts, facts, cases)); fun map_consts f = - map_context (fn (mode, naming, syntax, consts, thms, cases) => - (mode, naming, syntax, f consts, thms, cases)); + map_context (fn (mode, naming, syntax, consts, facts, cases) => + (mode, naming, syntax, f consts, facts, cases)); -fun map_thms f = - map_context (fn (mode, naming, syntax, consts, thms, cases) => - (mode, naming, syntax, consts, f thms, cases)); +fun map_facts f = + map_context (fn (mode, naming, syntax, consts, facts, cases) => + (mode, naming, syntax, consts, f facts, cases)); fun map_cases f = - map_context (fn (mode, naming, syntax, consts, thms, cases) => - (mode, naming, syntax, consts, thms, f cases)); + map_context (fn (mode, naming, syntax, consts, facts, cases) => + (mode, naming, syntax, consts, facts, f cases)); val get_mode = #mode o rep_context; fun restore_mode ctxt = set_mode (get_mode ctxt); @@ -258,10 +251,7 @@ fun mk_const ctxt (c, Ts) = Const (c, Consts.instance (consts_of ctxt) (c, Ts)); -val thms_of = #thms o rep_context; -val theorems_of = #1 o thms_of; -val fact_index_of = #2 o thms_of; - +val facts_of = #facts o rep_context; val cases_of = #cases o rep_context; @@ -795,10 +785,7 @@ fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts; fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => - let - val index = fact_index_of ctxt; - val facts = FactIndex.could_unify index (Term.strip_all_body goal); - in fact_tac facts i end); + fact_tac (Facts.could_unify (facts_of ctxt) (Term.strip_all_body goal)) i); (* get_thm(s) *) @@ -813,21 +800,20 @@ | retrieve_thms from_thy pick ctxt xthmref = let val thy = theory_of ctxt; - val (space, tab) = #1 (thms_of ctxt); + val local_facts = facts_of ctxt; + val space = Facts.space_of local_facts; val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref; val name = PureThy.name_of_thmref thmref; val thms = if name = "" then [Thm.transfer thy Drule.dummy_thm] else - (case Symtab.lookup tab name of + (case Facts.lookup local_facts name of SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths) | NONE => from_thy thy xthmref); in pick name thms end; val get_thm = retrieve_thms PureThy.get_thms PureThy.single_thm; -val get_thm_closure = retrieve_thms PureThy.get_thms_closure PureThy.single_thm; val get_thms = retrieve_thms PureThy.get_thms (K I); -val get_thms_closure = retrieve_thms PureThy.get_thms_closure (K I); (* valid_thms *) @@ -838,15 +824,6 @@ | SOME ths' => Thm.eq_thms (ths, ths')); -(* lthms_containing *) - -fun lthms_containing ctxt spec = - FactIndex.find (fact_index_of ctxt) spec - |> map (fn (name, ths) => - if valid_thms ctxt (name, ths) then (name, ths) - else (NameSpace.hidden (if name = "" then "unnamed" else name), ths)); - - (* name space operations *) val add_path = map_naming o NameSpace.add_path; @@ -856,35 +833,15 @@ val restore_naming = map_naming o K o naming_of; val reset_naming = map_naming (K local_naming); -fun hide_thms fully names = map_thms (fn ((space, tab), index) => - ((fold (NameSpace.hide fully) names space, tab), index)); - -(* put_thms *) +(* facts *) -fun update_thms _ ("", NONE) ctxt = ctxt - | update_thms opts ("", SOME ths) ctxt = ctxt |> map_thms (fn (facts, index) => - let - val index' = uncurry FactIndex.add_local opts ("", ths) index; - in (facts, index') end) - | update_thms _ (bname, NONE) ctxt = ctxt |> map_thms (fn ((space, tab), index) => - let - val name = full_name ctxt bname; - val tab' = Symtab.delete_safe name tab; - in ((space, tab'), index) end) - | update_thms opts (bname, SOME ths) ctxt = ctxt |> map_thms (fn ((space, tab), index) => - let - val name = full_name ctxt bname; - val space' = NameSpace.declare (naming_of ctxt) name space; - val tab' = Symtab.update (name, ths) tab; - val index' = uncurry FactIndex.add_local opts (name, ths) index; - in ((space', tab'), index') end); +fun update_thms _ (bname, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt bname)) + | update_thms do_props (bname, SOME ths) ctxt = ctxt |> map_facts + (Facts.add do_props (naming_of ctxt) (full_name ctxt bname, ths)); fun put_thms do_props thms ctxt = - ctxt |> map_naming (K local_naming) |> update_thms (do_props, false) thms |> restore_naming ctxt; - - -(* note_thmss *) + ctxt |> map_naming (K local_naming) |> update_thms do_props thms |> restore_naming ctxt; local @@ -897,7 +854,7 @@ val (res, ctxt') = fold_map app facts ctxt; val thms = PureThy.name_thms false false name (flat res); val Mode {stmt, ...} = get_mode ctxt; - in ((bname, thms), ctxt' |> update_thms (stmt, true) (bname, SOME thms)) end); + in ((bname, thms), ctxt' |> update_thms stmt (bname, SOME thms)) end); in @@ -1197,10 +1154,9 @@ fun pretty_lthms ctxt = let - val props = FactIndex.props (fact_index_of ctxt); - val facts = - (if null props then I else cons ("unnamed", props)) - (NameSpace.extern_table (#1 (thms_of ctxt))); + val local_facts = facts_of ctxt; + val props = Facts.props local_facts; + val facts = (if null props then I else cons ("unnamed", props)) (Facts.extern local_facts); in if null facts andalso not (! verbose) then [] else [Pretty.big_list "facts:" (map (pretty_fact ctxt) facts)]