The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

> The Unicode character range 0x1D2C through 0x1D50 contains superscripted
> versions of the Latin alphabet (lower case).  These could be very useful
> in notations -- for example, I wanted to create a superscripted "op" to
> denote the opposite of a category, since I use contravariant functors
> a lot.
> 
> Coq seems to react rather strangely to characters in this region.  It
> will let me define a notation involving these characters, and will use
> it correctly when pretty-printing.  However, if I attempt to use the
> notation I have defined in a Gallina term, it will either go into an
> infinite loop (100% CPU) and/or report a lexer error.
> 
> I tried to patch Coq to fix this, but the root cause seems to be the
> tables in lib/unicodetable.ml which classify characters, and these
> tables appear to have been machine-generated by some program which is
> not part of Coq.  Is this true? 

Yes, from 8.3, the unicode table used by Coq is generated by the
camomile library from the standard official classification schemes of
unicode symbols (PropList.txt). I just checked and it turns out that
camomile is actually not up-to-date (it uses version 3.2.0 of the
standard, which does not specify the 0x01D00-0x01D7F range while the
last version is 5.2.0, which at least specifies characters from the
range 0x1D2C-0x1D61).

> If so, are the rules governing the use of Unicode characters beyond
> Coq's control?

No, in principle, nothing prevents Coq to assign to Unicode characters
properties that are not considered by the standard or that are
different from the standard.

The specific properties that Coq is interested and that it extracts
from the unicode standard properties are "being a letter", "being a
lowercase letter", "being an uppercase letter", "being acceptable
after the first letter of an identifier" (e.g. letter, subscript and
superscript, ...), "being a symbol".

The table being currently incomplete, you can safely update it and
move the 0x01D2C-0x01D61 range from the "cn" block to the appropriate
block in unicodetable.ml, at least for you own purpose if not
following the standard, or as a contributed patch if following the
standard given at http://www.unicode.org/Public/UNIDATA/PropList.txt
(current version) http://www.unicode.org/reports/tr49/Categories.txt
(development version). [Actually, I think that Yann Régis-Gianas has a
script to generate the table from the official data, so you could ask
him.]

> My plan was to add a vernacular command to allow the user to classify or
> reclassify character ranges, similar to what is done in TeX.

Updating the table would be enough in the present case, but I'm pretty
sure that changing the official status of a character might be
convenient in some cases.

Hugo