[isabelle-dev] [isabelle] Bug in code-setup for Imperative/HOL

[Florian Haftmann]

Hi Peter,

> 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

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130620/e728a28d/attachment.asc>