[isabelle-dev] Afterthoughts on Local_Theory.subtarget_result
florian at haftmann-online.de
Tue Jan 22 22:24:23 CET 2019
as of 82f57315cade (followed-up by AFP bf62184), the still occasionally
seen Local_Theory.reset invocations are gone, conveniently replaced by
I'm considering pushing that even further: specification tools should by
contract provide a »clean« definitional extension without any artefacts
of the internal construction leaking out, i. e.
val specification: spec -> local_theory -> result * local_theory
where »spec« is the input specification and »result« a characterization
of the definitional extension with enough information to build on it in
derived tools; the resulting local_theory can be continued on directly
-- all internal construction steps are hid in a local subtarget.
The corresponding package is supposed to provide a morphism lifter for
val transform: morphism -> result -> result
hence exporting up through nested context is trivial.
This would also open up the possibility to get rid of the still seen
*_global variants for specification tools: using a combinator
Named_Target.theory_map_result: (morphism -> 'a -> 'a) ->
(local_theory -> 'a * local_theory) -> theory -> 'a * theory
any Package.spec_global can be trivially inlined as
Named_Target.theory_map_result Package.transform (Package.spec …)
So much my current understanding of affairs.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev