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

[Andreas Lochbihler]

Dear Lars,

On 24/07/17 15:08, Lars Hupel wrote:
> 1) Function transformers: I want to run a function transformer in
> special situations. But I can only register it globally (with
> "Code_Preproc.add_functrans"). What I use is the following pattern:
> 
> val enabled = Attrib.setup_config_bool @{binding "constructor_funs"} (K
> false)
> 
> fun functrans ctxt thms = (* implementation *)
> 
> val code_functrans = Code_Preproc.simple_functrans (fn ctxt =>
>    if Config.get ctxt enabled then
>      functrans ctxt
>    else
>      K NONE)
> 
> I'm not sure whether this is how attributes are meant to be used, but at
> least I can enable this locally. But as far as I can tell there are only
> three function transformers in total, so I'm not sure how relevant this is.
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.

> 2) "Fake local" declarations: I want to change the representation of the
> "char" type in declared code. By default, it is represented using
> numerals in a "non-free" way (i.e. there are invalid representations).
> I'd like to replace it with a free representation (bytes), but don't
> want this to affect the global theory; or at least, I'd like to avoid
> people importing my theory to be affected [0].
> 
> Here's my workaround:
> 
> ML‹
>    fun code_attribute f = Thm.declaration_attribute (fn thm =>
> Context.mapping (f thm) I)
> ›
> 
> attribute_setup "code_datatype" = ‹
>    Scan.repeat1 Args.term >> (fn terms =>
>      code_attribute (K (Code.declare_datatype_global (map dest_Const
> terms))))
> ›
> 
> Now I can use the "bundle" target:
> 
> 
> bundle char_byte_representation begin
> 
> declare [["code_datatype" char_of_byte]]
> 
> declare [[code drop: equal_char_inst.equal_char String.Char]]
> 
> (* more ... *)
> 
> declare char_byte_literals[code_unfold]
> 
> end
> 
> Importing this theory doesn't change the code setup. Only when I use
> "unbundle" the changes become permanent. However, it doesn't work
> properly in an unnamed context with "including" (this is as expected).
> There are a lot of occurrences of "code_datatype", often leading to the
> problem of artificially splitting up theories into an "abstract" and
> "implementation" part.
> 
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/...). 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?

Andreas