Re: [isabelle] Bug in code serialiser for OCaml

On 04/20/2011 05:17 PM, Lukas Bulwahn wrote:
On 04/20/2011 10:30 AM, Andreas Lochbihler wrote:
Dear all,

the OCaml code generator in Isabelle2011 seems to get confused with functions named like \<A>. For example:

primrec \<A>  :: "nat => nat" where
  "\<A> 0 = 0"
| "\<A> (Suc a) = \<A> a"

export_code \<A> in OCaml file -

produces the following definition for \<A>:

let rec a = function Arith.Zero_nat -> Arith.Zero_nat
            | Arith.Suc a -> a a;;

Obviously, the self-application "a a" in the Suc case is wrong. The code serialiser for OCaml forgets to rename the parameter a to a fresh value. The serialisers for SML, Haskell and Scala all rename the parameter a to aa.

Florian is the expert on this topic.
But I can look at this minor problem (and probably fix it) in case Florian does not have time to fix it.


This issue has been resolved in the current development version with changeset 1a82b0400b2a.


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