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

[Florian Haftmann]

Hi Brian,

thanks for reporting this.  I hope to eliminate this problem within this
day.

Hope this helps,
	Florian

Brian Huffman schrieb:
> 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
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090608/4aa801fb/attachment-0001.pgp>