Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Bug in code serialiser for OCaml

Email Gateway (Aug 18 2022 at 17:36):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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.

Andreas

Email Gateway (Aug 18 2022 at 17:36):

From: Lukas Bulwahn <bulwahn@in.tum.de>
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

Email Gateway (Aug 18 2022 at 17:41):

From: Lukas Bulwahn <bulwahn@in.tum.de>
This issue has been resolved in the current development version with
changeset 1a82b0400b2a.

Lukas

Last updated: Nov 21 2024 at 12:39 UTC