Re: [isabelle] Bug in code serialiser for OCaml
On 04/20/2011 10:30 AM, Andreas Lochbihler wrote:
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 archive was generated by a fusion of
Pipermail (Mailman edition) and