Re: [isabelle-dev] Afterthoughts on Local_Theory.subtarget_result

2019-01-31 Thread Makarius 
On 22/01/2019 22:24, Florian Haftmann wrote:
> 
> 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.

This looks clean and canonical. At least we have Local_Theory.reset out
of the way in visible Isabelle/ML tool implementations: it is still
present inside Local_Theory.close_target, though.

I wonder what happens when that is removed: presumably it requires a lot
of fine-tuning to make everything work again without that hidden reset.


Makarius



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Afterthoughts on Local_Theory.subtarget_result

2019-01-22 Thread Florian Haftmann 
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