[isabelle] Bug in code serialiser for OCaml



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

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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