coq: Add some common keywords and improve recognition of Set and qualified identifiers (#2158)

. is not an operator in Coq: in this specific usage, it is only meant to build a qualified name, so this rule really corresponds to a proper lexical rule in Coq

Unlike most languages, Coq has a large set of special words that are not reserved: they may still be used as identifiers. For example Prop is a special word, which currently gets highlighted as such in Equations.Prop.Equations, but it should be recognized as a regular name there. Because of how flexible the syntax of Coq is, it's not straightforward to disambiguate things with just a bunch of regexes, so we have to rely on heuristics. Skipping qualified names from being recognized as keywords is an easy win.

3 files changed, 152 insertions, 20 deletions

diff --git a/tests/examplefiles/coq/coq_RelationClasses.output b/tests/examplefiles/coq/coq_RelationClasses.output
index d186d8a6..aed490a6 100644
--- a/tests/examplefiles/coq/coq_RelationClasses.output
+++ b/tests/examplefiles/coq/coq_RelationClasses.output
@@ -267,11 +267,7 @@
 ' '           Text
 'Export'      Keyword.Namespace
 ' '           Text
-'Coq'         Name
-'.'           Operator
-'Classes'     Name
-'.'           Operator
-'Init'        Name
+'Coq.Classes.Init' Name
 '.'           Operator
 '\n'          Text
 
@@ -279,11 +275,7 @@
 ' '           Text
 'Import'      Keyword.Namespace
 ' '           Text
-'Coq'         Name
-'.'           Operator
-'Program'     Name
-'.'           Operator
-'Basics'      Name
+'Coq.Program.Basics' Name
 '.'           Operator
 '\n'          Text
 
@@ -291,11 +283,7 @@
 ' '           Text
 'Import'      Keyword.Namespace
 ' '           Text
-'Coq'         Name
-'.'           Operator
-'Program'     Name
-'.'           Operator
-'Tactics'     Name
+'Coq.Program.Tactics' Name
 '.'           Operator
 '\n'          Text
 
@@ -303,11 +291,7 @@
 ' '           Text
 'Import'      Keyword.Namespace
 ' '           Text
-'Coq'         Name
-'.'           Operator
-'Relations'   Name
-'.'           Operator
-'Relation_Definitions' Name
+'Coq.Relations.Relation_Definitions' Name
 '.'           Operator
 '\n\n'        Text
 
diff --git a/tests/examplefiles/coq/coq_test b/tests/examplefiles/coq/coq_test
new file mode 100644
index 00000000..29c920f0
--- /dev/null
+++ b/tests/examplefiles/coq/coq_test
@@ -0,0 +1,12 @@
+From Coq Require Import Arith.
+Require Import Equations.Prop.Equations.
+Set Implicit Arguments.
+Set Primitive Projections.
+Unset Printing All.
+Scheme tree_forest_rec := Induction for tree Sort Set
+  with forest_tree_rec := Induction for forest Sort Set.
+Fail Definition x : unit := 3.
+admit.
+Equations? neg (b : bool) : bool :=
+neg true := false;
+neg false := true.
diff --git a/tests/examplefiles/coq/coq_test.output b/tests/examplefiles/coq/coq_test.output
new file mode 100644
index 00000000..8091beec
--- /dev/null
+++ b/tests/examplefiles/coq/coq_test.output
@@ -0,0 +1,136 @@
+'From'        Keyword.Namespace
+' '           Text
+'Coq'         Name
+' '           Text
+'Require'     Keyword.Namespace
+' '           Text
+'Import'      Keyword.Namespace
+' '           Text
+'Arith'       Name
+'.'           Operator
+'\n'          Text
+
+'Require'     Keyword.Namespace
+' '           Text
+'Import'      Keyword.Namespace
+' '           Text
+'Equations.Prop.Equations' Name
+'.'           Operator
+'\n'          Text
+
+'Set'         Keyword.Namespace
+' '           Text
+'Implicit'    Keyword.Namespace
+' '           Text
+'Arguments'   Keyword.Namespace
+'.'           Operator
+'\n'          Text
+
+'Set'         Keyword.Namespace
+' '           Text
+'Primitive'   Name
+' '           Text
+'Projections' Keyword.Namespace
+'.'           Operator
+'\n'          Text
+
+'Unset'       Keyword.Namespace
+' '           Text
+'Printing'    Keyword.Namespace
+' '           Text
+'All'         Keyword.Namespace
+'.'           Operator
+'\n'          Text
+
+'Scheme'      Keyword.Namespace
+' '           Text
+'tree_forest_rec' Name
+' '           Text
+':='          Operator
+' '           Text
+'Induction'   Name
+' '           Text
+'for'         Keyword
+' '           Text
+'tree'        Name
+' '           Text
+'Sort'        Name
+' '           Text
+'Set'         Keyword.Type
+'\n  '        Text
+'with'        Keyword
+' '           Text
+'forest_tree_rec' Name
+' '           Text
+':='          Operator
+' '           Text
+'Induction'   Name
+' '           Text
+'for'         Keyword
+' '           Text
+'forest'      Name
+' '           Text
+'Sort'        Name
+' '           Text
+'Set'         Keyword.Type
+'.'           Operator
+'\n'          Text
+
+'Fail'        Keyword.Namespace
+' '           Text
+'Definition'  Keyword.Namespace
+' '           Text
+'x'           Name
+' '           Text
+':'           Operator
+' '           Text
+'unit'        Name
+' '           Text
+':='          Operator
+' '           Text
+'3'           Literal.Number.Integer
+'.'           Operator
+'\n'          Text
+
+'admit'       Keyword.Pseudo
+'.'           Operator
+'\n'          Text
+
+'Equations?'  Keyword.Namespace
+' '           Text
+'neg'         Name
+' '           Text
+'('           Operator
+'b'           Name
+' '           Text
+':'           Operator
+' '           Text
+'bool'        Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'bool'        Name
+' '           Text
+':='          Operator
+'\n'          Text
+
+'neg'         Name
+' '           Text
+'true'        Name.Builtin.Pseudo
+' '           Text
+':='          Operator
+' '           Text
+'false'       Name.Builtin.Pseudo
+';'           Operator
+'\n'          Text
+
+'neg'         Name
+' '           Text
+'false'       Name.Builtin.Pseudo
+' '           Text
+':='          Operator
+' '           Text
+'true'        Name.Builtin.Pseudo
+'.'           Operator
+'\n'          Text