106 val t' = Morphism.term (#morphism dep) t; |
106 val t' = Morphism.term (#morphism dep) t; |
107 in if t aconv t' then NONE else SOME (v, t') end); |
107 in if t aconv t' then NONE else SOME (v, t') end); |
108 in SOME (dep, (substT, subst)) end); |
108 in SOME (dep, (substT, subst)) end); |
109 |
109 |
110 |
110 |
111 (* general setup *) |
111 (* presentation *) |
112 |
112 |
113 fun setup_presentation f = |
113 fun export_enabled (context: Thy_Info.presentation_context) = |
114 Theory.setup (Thy_Info.add_presentation (fn context => fn thy => |
114 Options.bool (#options context) "export_theory"; |
115 if Options.bool (#options context) "export_theory" then f context thy else ())); |
|
116 |
115 |
117 fun export_body thy name body = |
116 fun export_body thy name body = |
118 if XML.is_empty_body body then () |
117 if XML.is_empty_body body then () |
119 else Export.export thy (Path.binding0 (Path.make ["theory", name])) body; |
118 else Export.export thy (Path.binding0 (Path.make ["theory", name])) body; |
120 |
119 |
121 |
120 val _ = (Theory.setup o Thy_Info.add_presentation) (fn context => fn thy => |
122 (* presentation *) |
|
123 |
|
124 val _ = setup_presentation (fn context => fn thy => |
|
125 let |
121 let |
|
122 val rep_tsig = Type.rep_tsig (Sign.tsig_of thy); |
|
123 val consts = Sign.consts_of thy; |
|
124 val thy_ctxt = Proof_Context.init_global thy; |
|
125 |
|
126 val pos_properties = Thy_Info.adjust_pos_properties context; |
|
127 |
|
128 val enabled = export_enabled context; |
|
129 |
|
130 |
|
131 (* strict parents *) |
|
132 |
126 val parents = Theory.parents_of thy; |
133 val parents = Theory.parents_of thy; |
127 val rep_tsig = Type.rep_tsig (Sign.tsig_of thy); |
134 val _ = |
128 |
135 Export.export thy \<^path_binding>\<open>theory/parents\<close> |
129 val thy_ctxt = Proof_Context.init_global thy; |
136 (XML.Encode.string (cat_lines (map Context.theory_long_name parents))); |
130 |
|
131 val pos_properties = Thy_Info.adjust_pos_properties context; |
|
132 |
137 |
133 |
138 |
134 (* spec rules *) |
139 (* spec rules *) |
135 |
140 |
136 fun spec_rule_content {pos, name, rough_classification, terms, rules} = |
141 fun spec_rule_content {pos, name, rough_classification, terms, rules} = |
160 let |
165 let |
161 val xname = Name_Space.extern_shortest thy_ctxt space name; |
166 val xname = Name_Space.extern_shortest thy_ctxt space name; |
162 val {serial, pos, ...} = Name_Space.the_entry space name; |
167 val {serial, pos, ...} = Name_Space.the_entry space name; |
163 in make_entity_markup name xname pos serial end; |
168 in make_entity_markup name xname pos serial end; |
164 |
169 |
165 fun export_entities export_name export get_space decls = |
170 fun export_entities export_name get_space decls export = |
166 let |
171 let |
167 val parent_spaces = map get_space parents; |
172 val parent_spaces = map get_space parents; |
168 val space = get_space thy; |
173 val space = get_space thy; |
169 in |
174 in |
170 (decls, []) |-> fold (fn (name, decl) => |
175 (decls, []) |-> fold (fn (name, decl) => |
171 if exists (fn space => Name_Space.declared space name) parent_spaces then I |
176 if exists (fn space => Name_Space.declared space name) parent_spaces then I |
172 else |
177 else |
173 (case export name decl of |
178 (case export name decl of |
174 NONE => I |
179 NONE => I |
175 | SOME body => |
180 | SOME make_body => |
176 cons (#serial (Name_Space.the_entry space name), |
181 let |
177 XML.Elem (entity_markup space name, body)))) |
182 val i = #serial (Name_Space.the_entry space name); |
|
183 val body = if enabled then make_body () else []; |
|
184 in cons (i, XML.Elem (entity_markup space name, body)) end)) |
178 |> sort (int_ord o apply2 #1) |> map #2 |
185 |> sort (int_ord o apply2 #1) |> map #2 |
179 |> export_body thy export_name |
186 |> export_body thy export_name |
180 end; |
187 end; |
181 |
188 |
182 |
189 |
184 |
191 |
185 val encode_type = |
192 val encode_type = |
186 let open XML.Encode Term_XML.Encode |
193 let open XML.Encode Term_XML.Encode |
187 in triple encode_syntax (list string) (option typ) end; |
194 in triple encode_syntax (list string) (option typ) end; |
188 |
195 |
189 fun export_type c (Type.LogicalType n) = |
196 val _ = |
190 SOME (encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE)) |
197 export_entities "types" Sign.type_space (Name_Space.dest_table (#types rep_tsig)) |
191 | export_type c (Type.Abbreviation (args, U, false)) = |
198 (fn c => |
192 SOME (encode_type (get_syntax_type thy_ctxt c, args, SOME U)) |
199 (fn Type.LogicalType n => |
193 | export_type _ _ = NONE; |
200 SOME (fn () => |
194 |
201 encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE)) |
195 val _ = |
202 | Type.Abbreviation (args, U, false) => |
196 export_entities "types" export_type Sign.type_space |
203 SOME (fn () => |
197 (Name_Space.dest_table (#types rep_tsig)); |
204 encode_type (get_syntax_type thy_ctxt c, args, SOME U)) |
|
205 | _ => NONE)); |
198 |
206 |
199 |
207 |
200 (* consts *) |
208 (* consts *) |
201 |
209 |
202 val consts = Sign.consts_of thy; |
|
203 val encode_term = Term_XML.Encode.term consts; |
210 val encode_term = Term_XML.Encode.term consts; |
204 |
211 |
205 val encode_const = |
212 val encode_const = |
206 let open XML.Encode Term_XML.Encode |
213 let open XML.Encode Term_XML.Encode |
207 in pair encode_syntax (pair (list string) (pair typ (pair (option encode_term) bool))) end; |
214 in pair encode_syntax (pair (list string) (pair typ (pair (option encode_term) bool))) end; |
208 |
215 |
209 fun export_const c (T, abbrev) = |
216 val _ = |
210 let |
217 export_entities "consts" Sign.const_space (#constants (Consts.dest consts)) |
211 val syntax = get_syntax_const thy_ctxt c; |
218 (fn c => fn (T, abbrev) => |
212 val U = Logic.unvarifyT_global T; |
219 SOME (fn () => |
213 val U0 = Type.strip_sorts U; |
220 let |
214 val abbrev' = abbrev |
221 val syntax = get_syntax_const thy_ctxt c; |
215 |> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts); |
222 val U = Logic.unvarifyT_global T; |
216 val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0)); |
223 val U0 = Type.strip_sorts U; |
217 val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0); |
224 val trim_abbrev = |
218 in encode_const (syntax, (args, (U0, (abbrev', propositional)))) end; |
225 Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts; |
219 |
226 val abbrev' = Option.map trim_abbrev abbrev; |
220 val _ = |
227 val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0)); |
221 export_entities "consts" (SOME oo export_const) Sign.const_space |
228 val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0); |
222 (#constants (Consts.dest consts)); |
229 in encode_const (syntax, (args, (U0, (abbrev', propositional)))) end)); |
223 |
230 |
224 |
231 |
225 (* axioms *) |
232 (* axioms *) |
226 |
233 |
227 fun standard_prop used extra_shyps raw_prop raw_proof = |
234 fun standard_prop used extra_shyps raw_prop raw_proof = |
291 end; |
298 end; |
292 |
299 |
293 fun export_thm (thm_id, thm_name) = |
300 fun export_thm (thm_id, thm_name) = |
294 let |
301 let |
295 val markup = entity_markup_thm (#serial thm_id, thm_name); |
302 val markup = entity_markup_thm (#serial thm_id, thm_name); |
296 val thm = Global_Theory.get_thm_name thy (thm_name, Position.none); |
303 val body = |
297 in XML.Elem (markup, encode_thm thm_id thm) end; |
304 if enabled then |
|
305 Global_Theory.get_thm_name thy (thm_name, Position.none) |
|
306 |> encode_thm thm_id |
|
307 else []; |
|
308 in XML.Elem (markup, body) end; |
298 |
309 |
299 val _ = export_body thy "thms" (map export_thm (Global_Theory.dest_thm_names thy)); |
310 val _ = export_body thy "thms" (map export_thm (Global_Theory.dest_thm_names thy)); |
300 |
311 |
301 |
312 |
302 (* type classes *) |
313 (* type classes *) |
303 |
314 |
304 val encode_class = |
315 val encode_class = |
305 let open XML.Encode Term_XML.Encode |
316 let open XML.Encode Term_XML.Encode |
306 in pair (list (pair string typ)) (list (encode_axiom Name.context)) end; |
317 in pair (list (pair string typ)) (list (encode_axiom Name.context)) end; |
307 |
318 |
308 fun export_class name = |
319 val _ = |
309 (case try (Axclass.get_info thy) name of |
320 export_entities "classes" Sign.class_space |
310 NONE => ([], []) |
321 (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig))))) |
311 | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms)) |
322 (fn name => fn () => SOME (fn () => |
312 |> encode_class |> SOME; |
323 (case try (Axclass.get_info thy) name of |
313 |
324 NONE => ([], []) |
314 val _ = |
325 | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms)) |
315 export_entities "classes" (fn name => fn () => export_class name) |
326 |> encode_class)); |
316 Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig))))); |
|
317 |
327 |
318 |
328 |
319 (* sort algebra *) |
329 (* sort algebra *) |
320 |
330 |
321 local |
331 val _ = |
322 val prop = encode_axiom Name.context o Logic.varify_global; |
332 if enabled then |
323 |
333 let |
324 val encode_classrel = |
334 val prop = encode_axiom Name.context o Logic.varify_global; |
325 let open XML.Encode |
335 |
326 in list (pair prop (pair string string)) end; |
336 val encode_classrel = |
327 |
337 let open XML.Encode |
328 val encode_arities = |
338 in list (pair prop (pair string string)) end; |
329 let open XML.Encode Term_XML.Encode |
339 |
330 in list (pair prop (triple string (list sort) string)) end; |
340 val encode_arities = |
331 in |
341 let open XML.Encode Term_XML.Encode |
332 val export_classrel = |
342 in list (pair prop (triple string (list sort) string)) end; |
333 maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel; |
343 |
334 |
344 val export_classrel = |
335 val export_arities = map (`Logic.mk_arity) #> encode_arities; |
345 maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel; |
336 |
346 |
337 val {classrel, arities} = |
347 val export_arities = map (`Logic.mk_arity) #> encode_arities; |
338 Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents) |
348 |
339 (#2 (#classes rep_tsig)); |
349 val {classrel, arities} = |
340 end; |
350 Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents) |
341 |
351 (#2 (#classes rep_tsig)); |
342 val _ = if null classrel then () else export_body thy "classrel" (export_classrel classrel); |
352 in |
343 val _ = if null arities then () else export_body thy "arities" (export_arities arities); |
353 if null classrel then () else export_body thy "classrel" (export_classrel classrel); |
|
354 if null arities then () else export_body thy "arities" (export_arities arities) |
|
355 end |
|
356 else (); |
344 |
357 |
345 |
358 |
346 (* locales *) |
359 (* locales *) |
347 |
360 |
348 fun encode_locale used = |
361 fun encode_locale used = |
349 let open XML.Encode Term_XML.Encode in |
362 let open XML.Encode Term_XML.Encode in |
350 triple (list (pair string sort)) (list (pair (pair string typ) encode_syntax)) |
363 triple (list (pair string sort)) (list (pair (pair string typ) encode_syntax)) |
351 (list (encode_axiom used)) |
364 (list (encode_axiom used)) |
352 end; |
365 end; |
353 |
366 |
354 fun export_locale loc = |
367 val _ = |
355 let |
368 export_entities "locales" Locale.locale_space (get_locales thy) |
356 val {typargs, args, axioms} = locale_content thy loc; |
369 (fn loc => fn () => SOME (fn () => |
357 val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context; |
370 let |
358 in encode_locale used (typargs, args, axioms) end |
371 val {typargs, args, axioms} = locale_content thy loc; |
359 handle ERROR msg => |
372 val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context; |
360 cat_error msg ("The error(s) above occurred in locale " ^ |
373 in encode_locale used (typargs, args, axioms) end |
361 quote (Locale.markup_name thy_ctxt loc)); |
374 handle ERROR msg => |
362 |
375 cat_error msg ("The error(s) above occurred in locale " ^ |
363 val _ = |
376 quote (Locale.markup_name thy_ctxt loc)))); |
364 export_entities "locales" (fn loc => fn () => SOME (export_locale loc)) |
|
365 Locale.locale_space (get_locales thy); |
|
366 |
377 |
367 |
378 |
368 (* locale dependencies *) |
379 (* locale dependencies *) |
369 |
380 |
370 fun encode_locale_dependency (dep: Locale.locale_dependency, subst) = |
381 fun encode_locale_dependency (dep: Locale.locale_dependency, subst) = |
374 val encode_subst = |
385 val encode_subst = |
375 pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) (term consts))); |
386 pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) (term consts))); |
376 in pair string (pair string (pair (list (pair string bool)) encode_subst)) end; |
387 in pair string (pair string (pair (list (pair string bool)) encode_subst)) end; |
377 |
388 |
378 val _ = |
389 val _ = |
379 get_dependencies parents thy |
390 if enabled then |
380 |> map_index (fn (i, dep) => |
391 get_dependencies parents thy |> map_index (fn (i, dep) => |
|
392 let |
|
393 val xname = string_of_int (i + 1); |
|
394 val name = Long_Name.implode [Context.theory_name thy, xname]; |
|
395 val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep)); |
|
396 val body = encode_locale_dependency dep; |
|
397 in XML.Elem (markup, body) end) |
|
398 |> export_body thy "locale_dependencies" |
|
399 else (); |
|
400 |
|
401 |
|
402 (* constdefs *) |
|
403 |
|
404 val _ = |
|
405 if enabled then |
381 let |
406 let |
382 val xname = string_of_int (i + 1); |
407 val constdefs = |
383 val name = Long_Name.implode [Context.theory_name thy, xname]; |
408 Defs.dest_constdefs (map Theory.defs_of (Theory.parents_of thy)) (Theory.defs_of thy) |
384 val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep)); |
409 |> sort_by #1; |
385 val body = encode_locale_dependency dep; |
410 val encode = |
386 in XML.Elem (markup, body) end) |
411 let open XML.Encode |
387 |> export_body thy "locale_dependencies"; |
412 in list (pair string string) end; |
388 |
413 in if null constdefs then () else export_body thy "constdefs" (encode constdefs) end |
389 |
414 else (); |
390 (* constdefs *) |
|
391 |
|
392 val constdefs = |
|
393 Defs.dest_constdefs (map Theory.defs_of (Theory.parents_of thy)) (Theory.defs_of thy) |
|
394 |> sort_by #1; |
|
395 |
|
396 val encode_constdefs = |
|
397 let open XML.Encode |
|
398 in list (pair string string) end; |
|
399 |
|
400 val _ = |
|
401 if null constdefs then () else export_body thy "constdefs" (encode_constdefs constdefs); |
|
402 |
415 |
403 |
416 |
404 (* spec rules *) |
417 (* spec rules *) |
405 |
418 |
406 val encode_specs = |
419 val encode_specs = |