[isabelle] Code generator forgets to rename type variables for constants with code_abort
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Code generator forgets to rename type variables for constants with code_abort
- From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
- Date: Tue, 19 Nov 2013 18:05:19 +0100
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.0
Dear developers of the code generator,
Isabelle's code generator normally normalises the names of type variables to 'a, 'b, 'c in
the type signature. Apparently, it does not so if the constant has been declared as
code_abort. For OCaml, this can produce code that does not compile, because the type
variable name uses a reserved word (tested with ocamlc version 3.12.1). Here's an example:
theory Scratch imports Main begin
typedecl 'in foo
consts Foo :: "'in foo"
definition foo :: "unit => 'in foo" where [code del]: "foo _ = Foo"
definition bar :: "unit foo" where "bar = foo ()"
export_code bar in OCaml (* OCaml does not like type variables called 'in *)
Obviously, one can fix this by changing the type signature at the definition of foo, but I
would prefer to use consistent names for my type variables.
This archive was generated by a fusion of
Pipermail (Mailman edition) and