[isabelle] Code generator forgets to rename type variables for constants with code_abort



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"
code_datatype Foo
definition foo :: "unit => 'in foo" where [code del]: "foo _ = Foo"
code_abort 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.

Best,
Andreas




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