Changing subscript highlighting

[cpitclaudel]

Hi all,

company-coq got subscript highlighting a few months after fstar-mode got it, and in hindsight I feel that it works a bit better there. Unlike fstar-mode (which requires an underscore), company-coq highlights all numbers at the end of variable names as subscripts. Concretely, that means that you can write x1 instead of x_1 to get x₁.

Quick statistics suggest that fstar-mode's _<number> syntax isn't used very often in F* code in the wild, while identifiers with a number at the end are pretty common (see table below). And in fact, when the _<number> syntax is used, it isn't always obvious that a subscript was actually desired (e.g. lemma_intro_modifies_0, division_definition_lemma_1, lognot_lemma_1). In the entire ulib/ directory, I could find only four examples of short variable names using the _<number> syntax: s_1, s_2, qj_1, and qj_2. The only other cases that I could find where _ are used for subscripting are the int_8, int_16 etc. types.

How would we feel about changing F* mode to highlight x1 as x₁? To prevent confusion, this would mean ceasing to highlight x_1 as x₁ (otherwise it wouldn't be possible to distinguish x1 an x_1). Of course, it'd remain easy to turn off subscripts highlighting entirely, and it would also be relatively easy to locally hide the _, if desired.

[File name]                            [x1]     [x_1]
FStar.All.fst                          3        0
FStar.Array.fst                        136      0
FStar.Axiomatic.Array.fst              41       0
FStar.BitVector.fst                    0        8
FStar.Buffer.Quantifiers.fst           50       10
FStar.Buffer.fst                       1739     376
FStar.Bytes.fst                        0        0
FStar.Classical.fst                    0        5
FStar.Constructive.fst                 19       0
FStar.Crypto.fst                       3        0
FStar.DependentMap.fst                 144      0
FStar.ErasedLogic.fst                  8        0
FStar.Fin.fst                          22       0
FStar.FunctionalExtensionality.fst     0        0
FStar.Ghost.fst                        12       0
FStar.Heap.fst                         80       0
FStar.HyperHeap.fst                    147      0
FStar.HyperStack.fst                   187      6
FStar.IndefiniteDescription.fst        0        0
FStar.Int.Cast.fst                     249      0
FStar.Int.fst                          19       0
FStar.Int128.fst                       12       0
FStar.Int16.fst                        12       0
FStar.Int31.fst                        12       0
FStar.Int32.fst                        12       0
FStar.Int63.fst                        12       0
FStar.Int64.fst                        12       0
FStar.Int8.fst                         12       0
FStar.Integers.fst                     3        22
FStar.List.Tot.Base.fst                109      0
FStar.List.Tot.Properties.fst          435      0
FStar.List.Tot.fst                     0        0
FStar.List.fst                         164      0
FStar.MRef.fst                         37       0
FStar.Map.fst                          108      0
FStar.MarkovsPrinciple.fst             0        0
FStar.Math.Lemmas.fst                  117      52
FStar.Math.Lib.fst                     9        3
FStar.Monotonic.RRef.fst               38       0
FStar.Monotonic.Seq.fst                255      63
FStar.Mul.fst                          0        0
FStar.OrdMap.fst                       81       0
FStar.OrdMapProps.fst                  0        0
FStar.OrdSet.fst                       278      0
FStar.OrdSetProps.fst                  31       0
FStar.PredicateExtensionality.fst      12       0
FStar.PropositionalExtensionality.fst  6        0
FStar.Reader.fst                       30       0
FStar.Relational.Comp.fst              169      0
FStar.Relational.Relational.fst        54       0
FStar.Relational.State.fst             4        0
FStar.ST.fst                           19       0
FStar.Seq.Base.fst                     153      0
FStar.Seq.Properties.fst               535      4
FStar.Seq.fst                          0        0
FStar.Set.fst                          102      0
FStar.Squash.fst                       0        0
FStar.SquashEffect.fst                 0        0
FStar.SquashProperties.fst             37       0
FStar.StrongExcludedMiddle.fst         0        0
FStar.Struct.fst                       1253     84
FStar.StructNG.fst                     1269     71
FStar.TSet.fst                         88       0
FStar.Tcp.fst                          0        0
FStar.TwoLevelHeap.fst                 35       0
FStar.UInt.fst                         289      61
FStar.UInt128.fst                      14       0
FStar.UInt16.fst                       14       0
FStar.UInt31.fst                       14       0
FStar.UInt32.fst                       14       0
FStar.UInt63.fst                       14       0
FStar.UInt64.fst                       14       0
FStar.UInt8.fst                        14       0
FStar.Universe.fst                     5        0
FStar.Util.fst                         0        0
FStar.WellFounded.fst                  5        0
prims.fst                              104      1

[msprotz]

One of the reasons we haven't completely bought into it is because it looks nice in Emacs but not when you copy/paste it into a code snippet in a LaTeX paper. But I'll let others with more experience writing massive files chime in with their opinion :).

[cpitclaudel]

One of the reasons we haven't completely bought into it is because it looks nice in Emacs but not when you copy/paste it into a code snippet in a LaTeX paper.

Meh. You're using the wrong tools :P https://github.com/cpitclaudel/esh/raw/master/example/reference.pdf

Jokes aside, you're right; hence I'm proposing to drop that special syntax and instead highlight the one that's currently used.

[cpitclaudel]

Here's what the proposal looks like, concretely:

Now:

After:

[kyoDralliam]

I'm not exactly fond of the x_n syntax in the source code (when debugging the code in the terminal there are already too many _) so I would be rather happy if I could just write xn and still have the subscript highlight.

[cpitclaudel]

Done! Please report any issues you run across :)