Re: [isabelle] Bug in code serialiser for OCaml



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.

Lukas

Andreas







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