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

[Lars Hupel]

Dear Andreas,

> 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. Possibly instead we could have a command

functrans_setup "constructor_funs" = ‹
  (* implementation *)
›

... akin to simprocs. Of course, this would need to work in bundles as
well. (simprocs do work in bundles)

> 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.

With locales, it would be possible, but of course they come with their
own sets of issues. The beauty of a localized tool is that it would work
uniformly across bundles and locales, so users can pick and choose.

Cheers
Lars