Re: [isabelle] Code generation for composite terms

Hi Andreas,

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

this was my slip, I have been referring to the predicate compiler

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

The approach with a big tuple seems suitable, indeed.

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.