Dear Lars,
Well, we here at ETH have another function transformer, which can also
be activated and deactivated basically with almost the same pattern. The
only difference is that at the moment we use a command rather than a
Config value because de- and reactivation in our case has to do a bit
more than just enabling/disabling a function transformer. It also must
swap a few code equations.
Function transformers could also be declared with an attribute, although
there I'd say it's even less clear that attributes should be (ab)used
for that.
Yes, we felt like that, too. That's why we went for a command.
This is an interesting idea. For the above-mentioned function
transformer, we also have code_datatype declarations that must be
switched back and forth. The big advantage of your approach seems to me
that one can envision this alternative setup already where characters
are defined (and similarly for int/nat/set/mapping/...).
Exactly, that's another goal that could be achieved.
But I wonder
whether these bundle targets can be extended later. That is, if is some
unrelated theory, I write my own function for chars by pattern-matching
on Char. If I then import your theory, can I add further declarations
(code drop/code) to the bundle such that subsequent theories get a
consistent setup no matter whether the unbundle the bundle or not?
Currently I'm unaware of any way to extend bundles, except for something
like:
bundle bar begin
unbundle foo
end
Whether or not extending bundles is possible/canonical in Isar is a
question best answered by Makarius.
Well, originally, bundles were never meant to be extended later. That's what Makarius told
me back in 2012. Maybe the situation has changed now. But I'd say that this is crucial to
improve the current state of the art. Otherwise, we'll just have a mess with bundle names.
Independently, a localised code generator would of course be nice.
Best,
Andreas
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
