Re: [isabelle] Bug in code serialiser for OCaml
- To: Andreas Lochbihler <andreas.lochbihler at kit.edu>
- Subject: Re: [isabelle] Bug in code serialiser for OCaml
- From: Lukas Bulwahn <bulwahn at in.tum.de>
- Date: Tue, 03 May 2011 08:38:33 +0200
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <4DAEF904.email@example.com>
- References: <4DAE998B.firstname.lastname@example.org> <4DAEF904.email@example.com>
- User-agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:188.8.131.52) Gecko/20110419 Thunderbird/3.1.9
On 04/20/2011 05:17 PM, Lukas Bulwahn wrote:
This issue has been resolved in the current development version with
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