[isabelle-dev] Towards a "localized" code generator

[Andreas Lochbihler]

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