Email Gateway (Aug 19 2022 at 11:17): Email Gateway (Aug 19 2022 at 11:17):From: Peter Lammich <lammich@in.tum.de>
Hi List,
I just discovered a bug in the code-setup of Imperative/HOL.
For SML/OCaml/Scala, the "code_type" command binds the type
"'a Heap" to "unit -> _".
However, when generating code for a function of type "'a Heap => _", the
code-generator will generate a signature of type
"unit -> 'a -> _".
The correct signature would be
"(unit -> 'a) -> _".
When compiling the code, this results in an error (Mismatch between
structure and signature).
Adding parantheses in the code_type-command solves the problem:
code_type Heap (SML "(unit/ ->/ _)")
I have added this fix as changeset f6d1ca0c6faf.
However, conceptually, I think the code-generator's pretty-printer
should care about the parantheses, and not the user who assumes that
what he specifies as code_type is actually interpreted as a type, and
not somehow intermixed with other types.
Last updated: Apr 19 2024 at 12:27 UTC