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,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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