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

[Lars Hupel]

Dear users of the code generator,

last week I spoke with Florian about some fundamental properties of the
code generator.

Many Isabelle users are also "power users" of the code generator; in the
sense that they exploit many of its facilities (code printing, various
attributes, ...). These days the setup is really powerful and can be
tweaked in many ways.

However, only few bits of the code generator is actually localized: Off
the top of my head, this only applies to some of the attributes
("[code]" etc.). There are a lot of commands that only work in a global
context and have a permanent effect on the theory.

This has led to a problem: My work currently requires gathering code
equations for some constants. Afterwards, I need to prove some things
about them, which I do with either "code_simp" or "eval" – however, this
requires a different setup. To make matters worse, the gathering of the
code equations also requires special setup.

I'd like to share with you two strategies to cope with this situation.
This can serve as the basis for further discussion how to localize the
code generator.

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.

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.

Cheers
Lars



[0] This is not a theoretical problem, see AFP/e0065e482c76.