Re: [isabelle] Code generation for composite terms
On 24/04/14 13:42, Florian Haftmann wrote:
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
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
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.
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and