# HG changeset patch # User Lars Hupel # Date 1491413021 -7200 # Node ID 3c628937899db6d6baba56f15bc8ec84980b3632 # Parent faeccede95349eafcc993396bc30626be599d289 use Item_Net to store inductive info diff -r faeccede9534 -r 3c628937899d src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Wed Apr 05 22:29:09 2017 +0200 +++ b/src/HOL/Library/Countable.thy Wed Apr 05 19:23:41 2017 +0200 @@ -176,7 +176,7 @@ (case HOLogic.dest_Trueprop (Thm.concl_of typedef_thm) of (_ $ _ $ _ $ (_ $ Const (n, _))) => n | _ => raise Match) - val induct_info = Inductive.the_inductive ctxt pred_name + val induct_info = Inductive.the_inductive_global ctxt pred_name val pred_names = #names (fst induct_info) val induct_thms = #inducts (snd induct_info) val alist = pred_names ~~ induct_thms diff -r faeccede9534 -r 3c628937899d src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Wed Apr 05 22:29:09 2017 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Wed Apr 05 19:23:41 2017 +0200 @@ -150,7 +150,7 @@ let val thy = Proof_Context.theory_of ctxt; val ({names, ...}, {raw_induct, intrs, elims, ...}) = - Inductive.the_inductive ctxt (Sign.intern_const thy s); + Inductive.the_inductive_global ctxt (Sign.intern_const thy s); val ind_params = Inductive.params_of raw_induct; val raw_induct = atomize_induct ctxt raw_induct; val elims = map (atomize_induct ctxt) elims; @@ -591,7 +591,7 @@ let val thy = Proof_Context.theory_of ctxt; val ({names, ...}, {raw_induct, intrs, elims, ...}) = - Inductive.the_inductive ctxt (Sign.intern_const thy s); + Inductive.the_inductive_global ctxt (Sign.intern_const thy s); val raw_induct = atomize_induct ctxt raw_induct; val elims = map (atomize_induct ctxt) elims; val intrs = map (atomize_intr ctxt) intrs; diff -r faeccede9534 -r 3c628937899d src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Wed Apr 05 22:29:09 2017 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Apr 05 19:23:41 2017 +0200 @@ -155,7 +155,7 @@ let val thy = Proof_Context.theory_of ctxt; val ({names, ...}, {raw_induct, intrs, elims, ...}) = - Inductive.the_inductive ctxt (Sign.intern_const thy s); + Inductive.the_inductive_global ctxt (Sign.intern_const thy s); val ind_params = Inductive.params_of raw_induct; val raw_induct = atomize_induct ctxt raw_induct; val elims = map (atomize_induct ctxt) elims; diff -r faeccede9534 -r 3c628937899d src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Wed Apr 05 22:29:09 2017 +0200 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Wed Apr 05 19:23:41 2017 +0200 @@ -265,7 +265,7 @@ val no_compilation = ([], ([], [])) fun fetch_pred_data ctxt name = - (case try (Inductive.the_inductive ctxt) name of + (case try (Inductive.the_inductive_global ctxt) name of SOME (info as (_, result)) => let val thy = Proof_Context.theory_of ctxt @@ -293,7 +293,7 @@ in PredData.map (Graph.map_node name (map_pred_data add)) end fun is_inductive_predicate ctxt name = - is_some (try (Inductive.the_inductive ctxt) name) + is_some (try (Inductive.the_inductive_global ctxt) name) fun depending_preds_of ctxt (key, value) = let diff -r faeccede9534 -r 3c628937899d src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Wed Apr 05 22:29:09 2017 +0200 +++ b/src/HOL/Tools/inductive.ML Wed Apr 05 19:23:41 2017 +0200 @@ -25,7 +25,8 @@ induct: thm, inducts: thm list, intrs: thm list, eqs: thm list} val transform_result: morphism -> inductive_result -> inductive_result type inductive_info = {names: string list, coind: bool} * inductive_result - val the_inductive: Proof.context -> string -> inductive_info + val the_inductive: Proof.context -> term -> inductive_info + val the_inductive_global: Proof.context -> string -> inductive_info val print_inductives: bool -> Proof.context -> unit val get_monos: Proof.context -> thm list val mono_add: attribute @@ -202,12 +203,15 @@ type inductive_info = {names: string list, coind: bool} * inductive_result; +val empty_infos = + Item_Net.init (op = o apply2 (#names o fst)) (#preds o snd) + val empty_equations = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of); datatype data = Data of - {infos: inductive_info Symtab.table, + {infos: inductive_info Item_Net.T, monos: thm list, equations: thm Item_Net.T}; @@ -217,11 +221,11 @@ structure Data = Generic_Data ( type T = data; - val empty = make_data (Symtab.empty, [], empty_equations); + val empty = make_data (empty_infos, [], empty_equations); val extend = I; fun merge (Data {infos = infos1, monos = monos1, equations = equations1}, Data {infos = infos2, monos = monos2, equations = equations2}) = - make_data (Symtab.merge (K true) (infos1, infos2), + make_data (Item_Net.merge (infos1, infos2), Thm.merge_thms (monos1, monos2), Item_Net.merge (equations1, equations2)); ); @@ -235,26 +239,34 @@ let val {infos, monos, ...} = rep_data ctxt; val space = Consts.space_of (Proof_Context.consts_of ctxt); + val consts = + Item_Net.content infos + |> maps (fn ({names, ...}, result) => map (rpair result) names) in [Pretty.block (Pretty.breaks (Pretty.str "(co)inductives:" :: map (Pretty.mark_str o #1) - (Name_Space.markup_entries verbose ctxt space (Symtab.dest infos)))), + (Name_Space.markup_entries verbose ctxt space consts))), Pretty.big_list "monotonicity rules:" (map (Thm.pretty_thm_item ctxt) monos)] end |> Pretty.writeln_chunks; (* inductive info *) -fun the_inductive ctxt name = - (case Symtab.lookup (#infos (rep_data ctxt)) name of - NONE => error ("Unknown (co)inductive predicate " ^ quote name) - | SOME info => info); +fun the_inductive ctxt term = + Item_Net.retrieve (#infos (rep_data ctxt)) term + |> the_single -fun put_inductives names info = +fun the_inductive_global ctxt name = + #infos (rep_data ctxt) + |> Item_Net.content + |> filter (fn ({names, ...}, _) => member op = names name) + |> the_single + +fun put_inductives info = map_data (fn (infos, monos, equations) => - (fold (fn name => Symtab.update (name, info)) names infos, monos, equations)); + (Item_Net.update info infos, monos, equations)); (* monotonicity rules *) @@ -1133,7 +1145,7 @@ val lthy4 = lthy3 |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => let val result' = transform_result phi result; - in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end); + in put_inductives ({names = cnames, coind = coind}, result') end); in (result, lthy4) end; @@ -1218,7 +1230,7 @@ |> Named_Target.theory_init |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd |> Local_Theory.exit; - val info = #2 (the_inductive ctxt' name); + val info = #2 (the_inductive_global ctxt' name); in (info, Proof_Context.theory_of ctxt') end; diff -r faeccede9534 -r 3c628937899d src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Wed Apr 05 22:29:09 2017 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Wed Apr 05 19:23:41 2017 +0200 @@ -149,7 +149,7 @@ | is_meta (Const (@{const_name Pure.imp}, _) $ _ $ Q) = is_meta Q | is_meta (Const (@{const_name Trueprop}, _) $ t) = (case head_of t of - Const (s, _) => can (Inductive.the_inductive ctxt) s + Const (s, _) => can (Inductive.the_inductive_global ctxt) s | _ => true) | is_meta _ = false; @@ -493,7 +493,7 @@ fun add_ind_realizers name rsets thy = let val (_, {intrs, induct, raw_induct, elims, ...}) = - Inductive.the_inductive (Proof_Context.init_global thy) name; + Inductive.the_inductive_global (Proof_Context.init_global thy) name; val vss = sort (int_ord o apply2 length) (subsets (map fst (relevant_vars (Thm.concl_of (hd intrs))))) in