[isabelle-dev] conflict between code_identifier constant and module_name

[Florian Haftmann]

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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>