Re: [isabelle] Code generation for composite terms

Hi Andreas,

> 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.

The first half of this sentence is the reason for the second half ;-).

> 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.

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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