[isabelle-dev] conflict between code_identifier constant and module_name

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Sep 5 09:26:04 CEST 2013

Hi Andreas,
> Two months ago, Florian replaced code_module with code_identifier
> (6646bb548c6b). Now, I am having trouble using the greater capabilities
> of code_identifier. I would like to assign a constant to a different
> module, say
> code_identifier constant replicate \<rightharpoonup> (SML) "My_Module.rep"
> Then, code generation works fine as long as there is no module_name
> involved:
> definition test where "test = replicate"
> export_code test in SML
> export_code test in SML module_name foo (* fails due to module
> dependency cycles *)
> Unfortunately, many idioms internally use module_name -- for example,
> all of the following raise errors due to module dependency cycles:
> ML {* @{code test} *}
> value [code] "test 3 (0 :: nat)"
> lemma "test = foo" quickcheck
> The same problem also occurs with type constructors. Therefore: What is
> the intended way of using code_identifier with constants?

Thanks for reporting this, this is indeed not the intended behaviour.
The code_identifier as currently implemented has the following hierarchy
of precedence:

  first code_identifier for the symbol itself
  if there is no declaration for that symbol, consider code_identifier
    for the containing module

Now Ā»code_moduleĀ« has always been implemented as some special pervasive
module-level code_identifier (previously code_modulename), which of
course is not suitable here any longer.

I will try what I can do before the release deadline to amend this.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130905/26b6aca7/attachment.sig>

More information about the isabelle-dev mailing list