Re: [isabelle] Code Generation for Executable Sets

Hi Tjark,

> Currently, I am importing theory Executable_Set (from HOL/Library).
> There is a dire warning in this theory: "avoid using this at any cost!"
> My own functions are generated with the former type, while functions
> from Executable_Set expect the latter.  (The problem shows up when one
> tries to type-check code generated from the attached theory.)
> Fortunately, it seems that I can work around this issue by using
> Code.add_signature_cmd.  Is this the suggested solution?

yes, indeed.

> Unfortunately, I haven't yet figured out how to extend this workaround
> to records with fields of set type (again, see the attached theory).
> Any advice would be appreciated.

Unfortunately, currently there is no possibility to do so (in theory, it
should be sufficient to add suitable declaration for Abs_* and Rep_*,
but these are not considered for datatype constructors at the moment).

An alternative could be to use the fset type from theory Fset.thy which
is logically a copy of set but executable for finite sets;  although
this still involves a manual transfer, it is less involved than
transferring to lists.

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.