Email Gateway (Aug 18 2022 at 15:23): Email Gateway (Aug 18 2022 at 15:23):From: Tjark Weber <webertj@in.tum.de>
I'm trying to generate code from a model that defines numerous sets and
relations.
Currently, I am importing theory Executable_Set (from HOL/Library).
There is a dire warning in this theory: "avoid using this at any cost!"
Is there a better option then? I'd rather not rephrase the model in
terms of lists everywhere.
With Executable_Set imported, the generated code unfortunately is not
type-correct. The code generator confuses "'a => bool" with "'a set".
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?
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.
Tjark
Example.thy
Email Gateway (Aug 18 2022 at 15:24):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Email Gateway (Aug 18 2022 at 15:25):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Tjark,
I must correct myself: they are considered, but you must issue a
manual code_datatype declaration after you have issued the signature
declaration, i.e.
setup {*
Code.add_signature_cmd ("Abs_foo_ext", ...)
*}
code_datatype Abs_foo_ext
Hope this helps,
Florian
signature.asc
Last updated: Apr 19 2024 at 01:05 UTC