--- 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 *)
--- 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