77 (*arity theorems with theory name*) |
77 (*arity theorems with theory name*) |
78 inst_params: |
78 inst_params: |
79 (string * thm) Symtab.table Symtab.table * |
79 (string * thm) Symtab.table Symtab.table * |
80 (*constant name ~> type constructor ~> (constant name, equation)*) |
80 (*constant name ~> type constructor ~> (constant name, equation)*) |
81 (string * string) Symtab.table (*constant name ~> (constant name, type constructor)*), |
81 (string * string) Symtab.table (*constant name ~> (constant name, type constructor)*), |
82 diff_merge_classrels: (class * class) list}; |
82 diff_classrels: (class * class) list}; |
83 |
83 |
84 fun make_data |
84 fun make_data |
85 (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) = |
85 (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels) = |
86 Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels, |
86 Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels, |
87 proven_arities = proven_arities, inst_params = inst_params, |
87 proven_arities = proven_arities, inst_params = inst_params, |
88 diff_merge_classrels = diff_merge_classrels}; |
88 diff_classrels = diff_classrels}; |
|
89 |
|
90 fun diff_table tab1 tab2 = |
|
91 Symreltab.fold (fn (x, _) => if Symreltab.defined tab2 x then I else cons x) tab1 []; |
89 |
92 |
90 structure Data = Theory_Data_PP |
93 structure Data = Theory_Data_PP |
91 ( |
94 ( |
92 type T = data; |
95 type T = data; |
93 val empty = |
96 val empty = |
94 make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty), []); |
97 make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty), []); |
95 val extend = I; |
98 val extend = I; |
96 fun merge pp |
99 fun merge pp |
97 (Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1, |
100 (Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1, |
98 proven_arities = proven_arities1, inst_params = inst_params1, |
101 proven_arities = proven_arities1, inst_params = inst_params1, |
99 diff_merge_classrels = diff_merge_classrels1}, |
102 diff_classrels = diff_classrels1}, |
100 Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2, |
103 Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2, |
101 proven_arities = proven_arities2, inst_params = inst_params2, |
104 proven_arities = proven_arities2, inst_params = inst_params2, |
102 diff_merge_classrels = diff_merge_classrels2}) = |
105 diff_classrels = diff_classrels2}) = |
103 let |
106 let |
104 val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2); |
107 val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2); |
105 val params' = |
108 val params' = |
106 if null params1 then params2 |
109 if null params1 then params2 |
107 else fold_rev (fn p => if member (op =) params1 p then I else add_param pp p) params2 params1; |
110 else fold_rev (fn p => if member (op =) params1 p then I else add_param pp p) params2 params1; |
109 (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*) |
112 (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*) |
110 val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2); |
113 val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2); |
111 val proven_arities' = |
114 val proven_arities' = |
112 Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2); |
115 Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2); |
113 |
116 |
114 val classrels1 = Symreltab.keys proven_classrels1; |
117 val diff_classrels' = |
115 val classrels2 = Symreltab.keys proven_classrels2; |
118 diff_table proven_classrels1 proven_classrels2 @ |
116 val diff_merge_classrels' = |
119 diff_table proven_classrels2 proven_classrels1 @ |
117 subtract (op =) classrels1 classrels2 @ |
120 diff_classrels1 @ diff_classrels2; |
118 subtract (op =) classrels2 classrels1 @ |
|
119 diff_merge_classrels1 @ diff_merge_classrels2; |
|
120 |
121 |
121 val inst_params' = |
122 val inst_params' = |
122 (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2), |
123 (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2), |
123 Symtab.merge (K true) (#2 inst_params1, #2 inst_params2)); |
124 Symtab.merge (K true) (#2 inst_params1, #2 inst_params2)); |
124 in |
125 in |
125 make_data (axclasses', params', proven_classrels', proven_arities', inst_params', |
126 make_data |
126 diff_merge_classrels') |
127 (axclasses', params', proven_classrels', proven_arities', inst_params', diff_classrels') |
127 end; |
128 end; |
128 ); |
129 ); |
129 |
130 |
130 fun map_data f = |
131 fun map_data f = |
131 Data.map (fn Data {axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels} => |
132 Data.map (fn Data {axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels} => |
132 make_data (f (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels))); |
133 make_data (f (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels))); |
133 |
134 |
134 fun map_axclasses f = |
135 fun map_axclasses f = |
135 map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) => |
136 map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels) => |
136 (f axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels)); |
137 (f axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels)); |
137 |
138 |
138 fun map_params f = |
139 fun map_params f = |
139 map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) => |
140 map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels) => |
140 (axclasses, f params, proven_classrels, proven_arities, inst_params, diff_merge_classrels)); |
141 (axclasses, f params, proven_classrels, proven_arities, inst_params, diff_classrels)); |
141 |
142 |
142 fun map_proven_classrels f = |
143 fun map_proven_classrels f = |
143 map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) => |
144 map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels) => |
144 (axclasses, params, f proven_classrels, proven_arities, inst_params, diff_merge_classrels)); |
145 (axclasses, params, f proven_classrels, proven_arities, inst_params, diff_classrels)); |
145 |
146 |
146 fun map_proven_arities f = |
147 fun map_proven_arities f = |
147 map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) => |
148 map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels) => |
148 (axclasses, params, proven_classrels, f proven_arities, inst_params, diff_merge_classrels)); |
149 (axclasses, params, proven_classrels, f proven_arities, inst_params, diff_classrels)); |
149 |
150 |
150 fun map_inst_params f = |
151 fun map_inst_params f = |
151 map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) => |
152 map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels) => |
152 (axclasses, params, proven_classrels, proven_arities, f inst_params, diff_merge_classrels)); |
153 (axclasses, params, proven_classrels, proven_arities, f inst_params, diff_classrels)); |
153 |
154 |
154 val clear_diff_merge_classrels = |
155 val clear_diff_classrels = |
155 map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, _) => |
156 map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, _) => |
156 (axclasses, params, proven_classrels, proven_arities, inst_params, [])); |
157 (axclasses, params, proven_classrels, proven_arities, inst_params, [])); |
157 |
158 |
158 val rep_data = Data.get #> (fn Data args => args); |
159 val rep_data = Data.get #> (fn Data args => args); |
159 |
160 |
160 val axclasses_of = #axclasses o rep_data; |
161 val axclasses_of = #axclasses o rep_data; |
161 val params_of = #params o rep_data; |
162 val params_of = #params o rep_data; |
162 val proven_classrels_of = #proven_classrels o rep_data; |
163 val proven_classrels_of = #proven_classrels o rep_data; |
163 val proven_arities_of = #proven_arities o rep_data; |
164 val proven_arities_of = #proven_arities o rep_data; |
164 val inst_params_of = #inst_params o rep_data; |
165 val inst_params_of = #inst_params o rep_data; |
165 val diff_merge_classrels_of = #diff_merge_classrels o rep_data; |
166 val diff_classrels_of = #diff_classrels o rep_data; |
166 |
167 |
167 |
168 |
168 (* axclasses with parameters *) |
169 (* axclasses with parameters *) |
169 |
170 |
170 fun get_info thy c = |
171 fun get_info thy c = |