[isabelle] Code generation for composite terms



Hi,

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,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.