Email Gateway (Aug 18 2022 at 17:10): Email Gateway (Aug 18 2022 at 17:10):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear all,
In Isabelle2009-2, the code generator translated the theory String into the
module Stringa. In Isabelle2011, it uses String. Consequently, the SML
translations in HOL/Library/Code_Char for String.implode and String.explode to
String.implode and String.explode no longer refer to ML's built-in implode and
explode functions, but are captured by the new String module, which does not
declare such functions. Consequently, PolyML 5.4 rejects generated code that
uses String.implode and String.explode.
Surprisingly, with the @{code} antiquotation, everything seems to work fine.
Here's a small example:
theory Test imports Main Code_Char begin
definition foo where "foo = String.explode (STR ''abc'')"
export_code foo in SML file "test.ML"
ML {* @{code foo} *}
end
If I adjust the translation to
code_const explode (SML "explode")
then the raw polyml accepts the code produced by export_code, but the
antiquotation no longer works.
What do I have to do such that both work?
Regards,
Andreas
Email Gateway (Aug 18 2022 at 17:12):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
first, the appropriate solution to your problem should be
code_modulename SML
String Stringa
The reason is that all runtime services uses target language Eval rather
than SML (as noted in code generation tutorial p. 31) and typically do
not use different structures.
After some experimentation I have a feeling that code_reserved does not
exactly behave as expected, I will keep track on this.
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 17:15):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi again,
After some experimentation I have a feeling that code_reserved does not
exactly behave as expected, I will keep track on this.
the reason for this »misbevahiour« were the following lines added to
String.thy: http://isabelle.in.tum.de/reports/Isabelle/rev/0a3fa8fbcdc5
E.g. they would fix the module name »String«.
I am not able to reconstruct was my motivation was to add these, but now
they are removed for good.
Florian
signature.asc
Email Gateway (Aug 18 2022 at 17:15):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Florian,
thanks for figuring this out. I will keep your code_modulename workaround until
I switch to the development version again.
Andreas
Florian Haftmann schrieb:
Last updated: Apr 19 2024 at 04:17 UTC