Hi all, as of 82f57315cade (followed-up by AFP bf62184), the still occasionally seen Local_Theory.reset invocations are gone, conveniently replaced by Local_Theory.subtarget_result.
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
results
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.
Cheers,
Florian
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
