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



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.

--
  Peter






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.