# HG changeset patch # User krauss # Date 1262470738 -3600 # Node ID b0d21ae2528e4ae9e34e2d9e6b3ca5a112c892c4 # Parent f66bb6536f6a65a13d04feb1e8e2e295fa2abffc more official data record Function.info diff -r f66bb6536f6a -r b0d21ae2528e src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/function.ML Sat Jan 02 23:18:58 2010 +0100 @@ -7,6 +7,8 @@ signature FUNCTION = sig + include FUNCTION_DATA + val add_function : (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Function_Common.function_config @@ -23,6 +25,8 @@ val setup : theory -> theory val get_congs : Proof.context -> thm list + + val get_info : Proof.context -> term -> info end @@ -105,15 +109,16 @@ [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) ||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros - val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps', - pinducts=snd pinducts', termination=termination', - fs=fs, R=R, defname=defname } + val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', + pinducts=snd pinducts', termination=termination', fs=fs, R=R, + defname=defname, is_partial=true } + val _ = if not is_external then () else Specification.print_consts lthy (K false) (map fst fixes) in lthy - |> Local_Theory.declaration false (add_function_data o morph_function_data cdata) + |> Local_Theory.declaration false (add_function_data o morph_function_data info) end in lthy @@ -127,14 +132,14 @@ fun gen_termination_proof prep_term raw_term_opt lthy = let val term_opt = Option.map (prep_term lthy) raw_term_opt - val data = the (case term_opt of + val info = the (case term_opt of SOME t => (import_function_data t lthy handle Option.Option => error ("Not a function: " ^ quote (Syntax.string_of_term lthy t))) | NONE => (import_last_function lthy handle Option.Option => error "Not a function")) - val FunctionCtxData { termination, R, add_simps, case_names, psimps, - pinducts, defname, ...} = data + val { termination, fs, R, add_simps, case_names, psimps, + pinducts, defname, ...} = info val domT = domain_type (fastype_of R) val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) @@ -145,6 +150,10 @@ full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) val tsimps = map remove_domain_condition psimps val tinduct = map remove_domain_condition pinducts + + val info' = { is_partial=false, defname=defname, add_simps=add_simps, + case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, + termination=termination } fun qualify n = Binding.name n |> Binding.qualify true defname in @@ -154,6 +163,7 @@ ((qualify "induct", [Attrib.internal (K (Rule_Cases.case_names case_names))]), tinduct) |> snd + |> Local_Theory.declaration false (add_function_data o morph_function_data info') end in lthy @@ -196,6 +206,8 @@ val get_congs = Function_Ctx_Tree.get_function_congs +fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t + |> the_single |> snd (* outer syntax *) diff -r f66bb6536f6a -r b0d21ae2528e src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/function_common.ML Sat Jan 02 23:18:58 2010 +0100 @@ -5,9 +5,49 @@ Common definitions and other infrastructure. *) +signature FUNCTION_DATA = +sig + +type info = + {is_partial : bool, + defname : string, + (* contains no logical entities: invariant under morphisms: *) + add_simps : (binding -> binding) -> string -> (binding -> binding) -> + Attrib.src list -> thm list -> local_theory -> thm list * local_theory, + case_names : string list, + fs : term list, + R : term, + psimps: thm list, + pinducts: thm list, + termination: thm + } + +end + +structure Function_Data : FUNCTION_DATA = +struct + +type info = + {is_partial : bool, + defname : string, + (* contains no logical entities: invariant under morphisms: *) + add_simps : (binding -> binding) -> string -> (binding -> binding) -> + Attrib.src list -> thm list -> local_theory -> thm list * local_theory, + case_names : string list, + fs : term list, + R : term, + psimps: thm list, + pinducts: thm list, + termination: thm + } + +end + structure Function_Common = struct +open Function_Data + local open Function_Lib in (* Profiling *) @@ -58,41 +98,21 @@ domintros : thm list option } - -datatype function_context_data = - FunctionCtxData of - { - defname : string, - - (* contains no logical entities: invariant under morphisms *) - add_simps : (binding -> binding) -> string -> (binding -> binding) -> - Attrib.src list -> thm list -> local_theory -> thm list * local_theory, - - case_names : string list, - - fs : term list, - R : term, - - psimps: thm list, - pinducts: thm list, - termination: thm - } - -fun morph_function_data (FunctionCtxData {add_simps, case_names, fs, R, - psimps, pinducts, termination, defname}) phi = +fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts, + termination, defname, is_partial} : info) phi = let val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi val name = Binding.name_of o Morphism.binding phi o Binding.name in - FunctionCtxData { add_simps = add_simps, case_names = case_names, - fs = map term fs, R = term R, psimps = fact psimps, - pinducts = fact pinducts, termination = thm termination, - defname = name defname } + { add_simps = add_simps, case_names = case_names, + fs = map term fs, R = term R, psimps = fact psimps, + pinducts = fact pinducts, termination = thm termination, + defname = name defname, is_partial=is_partial } end structure FunctionData = Generic_Data ( - type T = (term * function_context_data) Item_Net.T; + type T = (term * info) Item_Net.T; val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); val extend = I; fun merge tabs : T = Item_Net.merge tabs; @@ -135,7 +155,7 @@ val all_function_data = Item_Net.content o get_function -fun add_function_data (data as FunctionCtxData {fs, termination, ...}) = +fun add_function_data (data : info as {fs, termination, ...}) = FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs) #> store_termination_rule termination