3 |
3 |
4 A package for general recursive function definitions. |
4 A package for general recursive function definitions. |
5 Common definitions and other infrastructure. |
5 Common definitions and other infrastructure. |
6 *) |
6 *) |
7 |
7 |
|
8 signature FUNCTION_DATA = |
|
9 sig |
|
10 |
|
11 type info = |
|
12 {is_partial : bool, |
|
13 defname : string, |
|
14 (* contains no logical entities: invariant under morphisms: *) |
|
15 add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
|
16 Attrib.src list -> thm list -> local_theory -> thm list * local_theory, |
|
17 case_names : string list, |
|
18 fs : term list, |
|
19 R : term, |
|
20 psimps: thm list, |
|
21 pinducts: thm list, |
|
22 termination: thm |
|
23 } |
|
24 |
|
25 end |
|
26 |
|
27 structure Function_Data : FUNCTION_DATA = |
|
28 struct |
|
29 |
|
30 type info = |
|
31 {is_partial : bool, |
|
32 defname : string, |
|
33 (* contains no logical entities: invariant under morphisms: *) |
|
34 add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
|
35 Attrib.src list -> thm list -> local_theory -> thm list * local_theory, |
|
36 case_names : string list, |
|
37 fs : term list, |
|
38 R : term, |
|
39 psimps: thm list, |
|
40 pinducts: thm list, |
|
41 termination: thm |
|
42 } |
|
43 |
|
44 end |
|
45 |
8 structure Function_Common = |
46 structure Function_Common = |
9 struct |
47 struct |
|
48 |
|
49 open Function_Data |
10 |
50 |
11 local open Function_Lib in |
51 local open Function_Lib in |
12 |
52 |
13 (* Profiling *) |
53 (* Profiling *) |
14 val profile = Unsynchronized.ref false; |
54 val profile = Unsynchronized.ref false; |
56 cases : thm, |
96 cases : thm, |
57 termination : thm, |
97 termination : thm, |
58 domintros : thm list option |
98 domintros : thm list option |
59 } |
99 } |
60 |
100 |
61 |
101 fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts, |
62 datatype function_context_data = |
102 termination, defname, is_partial} : info) phi = |
63 FunctionCtxData of |
|
64 { |
|
65 defname : string, |
|
66 |
|
67 (* contains no logical entities: invariant under morphisms *) |
|
68 add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
|
69 Attrib.src list -> thm list -> local_theory -> thm list * local_theory, |
|
70 |
|
71 case_names : string list, |
|
72 |
|
73 fs : term list, |
|
74 R : term, |
|
75 |
|
76 psimps: thm list, |
|
77 pinducts: thm list, |
|
78 termination: thm |
|
79 } |
|
80 |
|
81 fun morph_function_data (FunctionCtxData {add_simps, case_names, fs, R, |
|
82 psimps, pinducts, termination, defname}) phi = |
|
83 let |
103 let |
84 val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi |
104 val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi |
85 val name = Binding.name_of o Morphism.binding phi o Binding.name |
105 val name = Binding.name_of o Morphism.binding phi o Binding.name |
86 in |
106 in |
87 FunctionCtxData { add_simps = add_simps, case_names = case_names, |
107 { add_simps = add_simps, case_names = case_names, |
88 fs = map term fs, R = term R, psimps = fact psimps, |
108 fs = map term fs, R = term R, psimps = fact psimps, |
89 pinducts = fact pinducts, termination = thm termination, |
109 pinducts = fact pinducts, termination = thm termination, |
90 defname = name defname } |
110 defname = name defname, is_partial=is_partial } |
91 end |
111 end |
92 |
112 |
93 structure FunctionData = Generic_Data |
113 structure FunctionData = Generic_Data |
94 ( |
114 ( |
95 type T = (term * function_context_data) Item_Net.T; |
115 type T = (term * info) Item_Net.T; |
96 val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); |
116 val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); |
97 val extend = I; |
117 val extend = I; |
98 fun merge tabs : T = Item_Net.merge tabs; |
118 fun merge tabs : T = Item_Net.merge tabs; |
99 ); |
119 ); |
100 |
120 |
133 import_function_data t' ctxt' |
153 import_function_data t' ctxt' |
134 end |
154 end |
135 |
155 |
136 val all_function_data = Item_Net.content o get_function |
156 val all_function_data = Item_Net.content o get_function |
137 |
157 |
138 fun add_function_data (data as FunctionCtxData {fs, termination, ...}) = |
158 fun add_function_data (data : info as {fs, termination, ...}) = |
139 FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs) |
159 FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs) |
140 #> store_termination_rule termination |
160 #> store_termination_rule termination |
141 |
161 |
142 |
162 |
143 (* Simp rules for termination proofs *) |
163 (* Simp rules for termination proofs *) |