Extraction does not like double underscore in identifier names

[samuelgruetter]

When I extract Coq code generated by hs-to-coq back to Haskell using Coq's Extraction command, I get a lot of warnings like this:

Warning: The identifier arg_0__ contains __ which is reserved for the
extraction [extraction-reserved-identifier,extraction]

The extracted code seemed to work nevertheless, but probably just because I was lucky.

Is extracting back to Haskell part of the "hs-to-coq story"? If yes, it would be nice to fix this.

(You could reproduce this by running make in https://github.com/samuelgruetter/riscv-coq/tree/bcbb77c369bd25ff8b5fa96be0a73c99abe39b44 with its dependency bbv as a sibling directory, but probably this happens on almost any file generated by hs-to-coq when you extract it to Haskell).

Coq version: 8.7.2 hs-to-coq version: 79e6380fb7c8514e7619a5c97a3c04d330fff348

[nomeata]

You can quench the warning with

Set Warnings "-extraction-reserved-identifier".

(this is what we do).

Do you happen to know for what and how Coq uses __ during extraction?

[samuelgruetter]

Nice "solution" :wink:

And no I don't know what __ is used for, except for this:

__ :: any
__ = Prelude.error "Logical or arity value used"

but that wouldn't clash with arg_0__.

Is there any way hs-to-coq could use the same function arg names as the original Coq source instead of arg_0__? (just curious, not really important)

[nomeata]

Is there any way hs-to-coq could use the same function arg names as the original Coq source instead of arg_0__? (just curious, not really important)

In some cases, yes. In general, no. Consider

n = 50

foo 0 = 42 + n
foo n = 42 + n

What is the name of foo’s first argument? If we make it n, then we shadow the global n and that breaks the first equation.