Re: [isabelle] Code generation for composite terms



Hi Florian,

On 24/04/14 13:42, Florian Haftmann wrote:
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?

AFAIK, quickcheck achieves a similar effect by forking the theory,
adding definitions (or even axiomatizations), generating code and
throwing it away afterwards.  If I understand right, your business is
also about testing, so this should also be applicable to your scenario.
We have been unable to find these temporary definitions in Quickcheck. The three generators random, exhaustive and narrowing package everything that is needed for testing in in a single term. Then, they call some version of Code_Thingol.dynamic_value which uses Code_Target.ensure_value to get the intermediate representation of the generated code. Finally, they run the code either with the usual mechanism from Code_Runtime or with Narrowing_Generators.value.

In principle, we could also stuff all our data into a large single term and then decompose it in the generated test driver again. Do you recommend that we follow this way? Or do you think that separate definitions are superior?

Cheers,
Andreas




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