[isabelle-dev] Bug report: code generation with class constant called "open"

[Brian Huffman]

Hi all,

I recently tried to make some changes to the topological_space class
in RealVector.thy (I moved the definition of "open" here from
Library/Topology_Euclidean_Space.thy). Here is the declaration of the
syntactic class for the "open" predicate:

class "open" = fixes "open" :: "'a set => bool"

I made sure to put [code del] on every instance definition of "open",
but HOL/ex/Codegenerator_Test still fails. Here is the error message:

*** Error: Identifier expected but open was found (line 2204 of
"generated code")
*** Error: : expected but open was found (line 2204 of "generated code")
*** Error: <identifier> expected but open was found (line 2204 of
"generated code")
*** Error: } expected but : was found (line 2204 of "generated code")
*** Error: end expected but : was found (line 2204 of "generated code")
*** Error: Start of signature expected but ( was found (line 2204 of
"generated code")
*** Error: ; expected but ( was found (line 2204 of "generated code")
*** Exception- Fail "Static errors (pass 1)" raised
*** At command "export_code".

By doing "export_code * in SML module_name CodegenTest file -" I found
the offending bit of SML:

type 'a opena = {open : ('a -> bool) -> bool};
fun opena (A_:'a opena) = #open A_;

Evidently types are renamed to avoid clashes with SML keywords, but
record selectors are not.

I'll wait to push my changes until this is fixed.

- Brian