[isabelle-dev] [isabelle] Bug in code-setup for Imperative/HOL
florian.haftmann at informatik.tu-muenchen.de
Thu Jun 20 08:29:03 CEST 2013
> 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.
thanks for pointing this out.
> 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.
The technical complication here is that -> is an infix operator, but the
code_type etc. printing machinery can only print free infix operators
properly, not half-instantiated ones like unit -> _. A generalisation
is not worth the effort here, so the parentheses are fine.
Note the same complication also applies to product types, e.g in
definition foo :: "'a Heap * 'b Heap" where
"foo = undefined"
export_code foo in SML
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev