Hi René, > I'm currently trying to "mitigate" the changes to export_code, which > only inserts needed constants into the signature. For one theory, I > tried to use the wildcard "Theory._" -- but the then-generated code > seems to include ALL exportable definitions of some point in time. For > example, the generated code now includes the structures > Quickcheck_Exhausting and Quickcheck_Narrowing, which seems rather odd. > > The documentation states "referring to all executable constants within a > certain theory by giving name._", and I thought 'within' herer refers to > 'defined in', opposed to 'available in'.
there seems to be some confusion here. The story as supposed to be is:
* You specify some constants after export_code. Wildcards possible.
* These are implicitly augmented by their dependency. Generated code is
always self-contained in that respect!
* The new issue is that exports via signature are reduced (not to the
uttermost minimum, this will still need further refinement).
Having said that, is is quite natural that generated code also may
contain a structure named Quickcheck_Exhaustive, I guess due to the
generators which come with every datatype specification.
If you observe things which cannot be explained following this scheme, I
kindly ask for a self-contained example which demonstrates the
difference between expectation and reality.
Hope this helps,
Florian
>
>> hg id
> 8fcbfce2a2a9 tip
>
> - René
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
