Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generator forgets to rename type variable...

view this post on Zulip Email Gateway (Aug 19 2022 at 12:34):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 12:44):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
See now http://isabelle.in.tum.de/reports/Isabelle/rev/89d5b69e5a08
where normalizing of type variable names is done more extensively.

Cheers,
Florian
signature.asc

Last updated: Apr 24 2024 at 20:16 UTC