Email Gateway (Nov 21 2022 at 10:41): Email Gateway (Nov 21 2022 at 10:41):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi,
What is the current "state-of-the-art" for generating executable code for
functions defined in locales? I have done some searching and came across
the following thread on this mailing list from 14 years ago:
https://fa.isabelle.narkive.com/yg28DBD6/isabelle-code-generation-for-functions-defined-in-locales
Florian's answer there appears to work (albeit "where" is now "rewrites").
However this technique is also quite cumbrous, especially as the number of
functions defined within the scope of a locale grows. Is there a more
streamlined approach to handling this today?
Thanks,
Dominic
Email Gateway (Nov 21 2022 at 11:53):From: Peter Lammich <lammich@in.tum.de>
Nowadays, you can use global_interpretation, and manually list all constants
in the defines part... But the basic problem of having to write boilerplate
for every constant persists. While ad hoc solutions for simple cases are
certainly possible (https://www.isa-
afp.org/theories/collections/#Locale_Code_Ex), I understand that a general
solution accounting for the full power of locale expressions would be
problematic.
Peter Lammich
Email Gateway (Nov 21 2022 at 13:08):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Many thanks, Peter, for the speedy reply! I will look into defines for
global_interpretation.
Email Gateway (Nov 21 2022 at 13:23):From: Mohammad Abdulaziz <mohammad.abdulaziz8@gmail.com>
Hi Peter,
do you have pointers to limitations of a fully general solution?
best,
Mohammad
OpenPGP_0x1524AD6775B326EC.asc
OpenPGP_signature
Email Gateway (Nov 21 2022 at 16:34):From: Peter Lammich <lammich@in.tum.de>
no. I vaguely remember a discussion with Makarius (or maybe Florian)
some 12 years ago, who doubted that
https://www.isa-afp.org/theories/collections/#Locale_Code_Ex can be done
in a clean way ...
Last updated: Apr 20 2024 at 04:19 UTC