[isabelle] Code generation for composite terms
We are trying to implement an evaluation system for Isabelle2013-2 that can generate code
in different target languages, run generated functions on some input data, and process the
result. Our goal is to automate testing of adaptations of the code generator setup
(code_printing). To that end, we would like the code generator to generate the function to
test and the test data.
Unfortunately, the test data is not an Isabelle constant, the most prominent example are
literal numbers like "42 :: code_numeral". However, export_code and its ML equivalent only
accept constants, not general terms like "42". Therefore, we'd like to know how we can
generate code for such terms.
We had a look at how "value [code]" achieves to evaluate arbitrary terms. After studying
the sources, it seems to us that Code_Thingol.ensure_value does the necessary wrapping by
introducing a code dependency "dummy_pattern = <term to evaluate>", then builds the code
graph and removes "dummy_pattern" and the dependency again. This looks a bit hacky (I
don't see a way to generalise this to multiple terms to evaluate) and uses lots of
functions that Code_Thingol does not export. So, I wonder whether that is one way to go.
If we had to do it manually, we would define constants for the arguments and feed them to
the export_code command. However, in an automated system, our asynchronous testing command
then would become a theory transformation that pollutes the name space if many test cases
are run. Is there a simpler solution? For example, making a bunch of definitions solely
for the invocation of the code generator that are forgotton afterwards again?
Or are there simpler solutions that we have overlooked?
Thanks in advance for any suggestions and ideas,
This archive was generated by a fusion of
Pipermail (Mailman edition) and