Feature request: sanitize DK identifiers that are illegal in Rocq

[melanie-taprogge]

Summary

The DK-to-Rocq exporter can emit Rocq declarations whose names are not legal
Rocq identifiers.

In minimal-example.zip, DK accepts a name such as 1_p0, but Rocq cannot parse an identifier starting with a digit.

Steps to reproduce

cd minimal-example
./run.sh

The DK input is:

1_p0 : Type.

Expected behavior

The Rocq exporter should produce a legal fresh Rocq identifier, for example:

Axiom lp_1_p0 : Type.

The exact sanitization scheme is not important, but the generated file should
be accepted by Rocq and should avoid collisions.

Actual behavior

The generated Rocq is:

Axiom 1_p0 : Type.

coqc rejects this file with a syntax error.

Request

Please consider adding Rocq identifier sanitization to the DK-to-Rocq exporter
for names that are legal in Lambdapi/DK but illegal in Rocq.

Observed version

Observed with Lambdapi 3.0.0-72-g1e3b2ba.

[fblanqui]

There are several difficulties here:

• Automatic renaming is not super nice as it may not be easy for users to trace identifier names back to lp/dk. And it is not modular as you may generate names that may clash with other user symbols. Instead, you can use the option --renaming to explicit renamings yourself (see https://lambdapi.readthedocs.io/en/latest/options.html#export).
• To avoid useless renamings, we need to implement a function checking whether an identifier is a valid Rocq identifier.

[fblanqui]

After https://rocq-prover.org/doc/V9.2.0/refman/language/core/basic.html#syntax-and-lexical-conventions:

"Identifiers, written ident, are sequences of letters, digits, _ and ', that do not start with a digit or '. That is, they are recognized by the following grammar (except that the string _ is reserved; it is not a valid identifier):

ident ::= first_letter subsequent_letter*
first_letter ::= a .. z​ | A .. Z | _ | ​unicode_letter
subsequent_letter ::= first_letter​ | digit​ | ' | ​unicode_id_part

All characters are meaningful. In particular, identifiers are case-sensitive. unicode_letter non-exhaustively includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical letter-like symbols and non-breaking space. unicode_id_part non-exhaustively includes symbols for prime letters and subscripts."

[fblanqui]

On the other hand, Dedukti identifiers are:

let letter = ['a'-'z' 'A'-'Z' '0'-'9' '_' '!' '?' '\'' '+' '*' '~' '&' '^' '@' '=' '$' '%' '/' '<' '|' '-' '\\' '>']
let mident = ['a'-'z' 'A'-'Z' '0'-'9' '_']+
let ident = letter+

[fblanqui]

What do you propose to do if an identifier starts with a digit? Prefix it with "_"?

[fblanqui]

Hi Melanie. With #1397, I fail whenever there is an id containing some unicode character or that is invalid.