Added TLA+ grammar & queries

7 files changed, 163 insertions, 0 deletions

diff --git a/README.md b/README.md
index af4000b28..3adc18b5b 100644
--- a/README.md
+++ b/README.md
@@ -206,6 +206,7 @@ We are looking for maintainers to add more parsers and to write query files for
 - [x] [svelte](https://github.com/Himujjal/tree-sitter-svelte) (maintained by @elianiva)
 - [ ] [swift](https://github.com/tree-sitter/tree-sitter-swift)
 - [x] [teal](https://github.com/euclidianAce/tree-sitter-teal) (maintained by @euclidianAce)
+- [x] [tlaplus](https://github.com/tlaplus-community/tree-sitter-tlaplus/) (maintained by @ahelwer)
 - [x] [toml](https://github.com/ikatyang/tree-sitter-toml) (maintained by @tk-shirasaka)
 - [x] [tsx](https://github.com/tree-sitter/tree-sitter-typescript) (maintained by @steelsojka)
 - [x] [turtle](https://github.com/BonaBeavis/tree-sitter-turtle) (maintained by @bonabeavis)
diff --git a/ftdetect/tlaplus.vim b/ftdetect/tlaplus.vim
new file mode 100644
index 000000000..a60919b21
--- /dev/null
+++ b/ftdetect/tlaplus.vim
@@ -0,0 +1 @@
+au BufRead,BufNewFile *.tla set filetype=tla
diff --git a/lockfile.json b/lockfile.json
index 3a29bac89..b5d2521b0 100644
--- a/lockfile.json
+++ b/lockfile.json
@@ -185,6 +185,9 @@
   "teal": {
     "revision": "fcc5f6f4d194dede4e676834ff28a506e39e17b4"
   },
+  "tlaplus": {
+    "revision": "36e7863609f5fbb4b0e39b1a035f5b3245f974f6"
+  },
   "toml": {
     "revision": "8bd2056818b21860e3d756b5a58c4f6e05fb744e"
   },
diff --git a/lua/nvim-treesitter/parsers.lua b/lua/nvim-treesitter/parsers.lua
index 50887c323..72bee00e5 100644
--- a/lua/nvim-treesitter/parsers.lua
+++ b/lua/nvim-treesitter/parsers.lua
@@ -391,6 +391,15 @@ list.hcl = {
 --   }
 -- }
 
+list.tlaplus = {
+  install_info = {
+    url = "https://github.com/tlaplus-community/tree-sitter-tlaplus",
+    files = { "src/parser.c", "src/scanner.cc" }
+  },
+  maintainers = { "@ahelwer" },
+  filetype = "tlaplus"
+}
+
 list.toml = {
   install_info = {
     url = "https://github.com/ikatyang/tree-sitter-toml",
diff --git a/queries/tlaplus/folds.scm b/queries/tlaplus/folds.scm
new file mode 100644
index 000000000..2ca0168c0
--- /dev/null
+++ b/queries/tlaplus/folds.scm
@@ -0,0 +1,5 @@
+[
+  (extramodular_text)
+  (block_comment)
+  (non_terminal_proof)
+] @fold
diff --git a/queries/tlaplus/highlights.scm b/queries/tlaplus/highlights.scm
new file mode 100644
index 000000000..521f44f42
--- /dev/null
+++ b/queries/tlaplus/highlights.scm
@@ -0,0 +1,140 @@
+; highlights.scm
+
+; Keywords
+[
+  "ACTION"
+  "ASSUME"
+  "ASSUMPTION"
+  "AXIOM"
+  "BY"
+  "CASE"
+  "CHOOSE"
+  "CONSTANT"
+  "CONSTANTS"
+  "COROLLARY"
+  "DEF"
+  "DEFINE"
+  "DEFS"
+  "DOMAIN"
+  "ELSE"
+  "ENABLED"
+  "EXCEPT"
+  "EXTENDS"
+  "HAVE"
+  "HIDE"
+  "IF"
+  "IN"
+  "INSTANCE"
+  "LAMBDA"
+  "LEMMA"
+  "LET"
+  "LOCAL"
+  "MODULE"
+  "NEW"
+  "OBVIOUS"
+  "OMITTED"
+  "ONLY"
+  "OTHER"
+  "PICK"
+  "PROOF"
+  "PROPOSITION"
+  "PROVE"
+  "QED"
+  "RECURSIVE"
+  "SF_"
+  "STATE"
+  "SUBSET"
+  "SUFFICES"
+  "TAKE"
+  "TEMPORAL"
+  "THEN"
+  "THEOREM"
+  "UNCHANGED"
+  "UNION"
+  "USE"
+  "VARIABLE"
+  "VARIABLES"
+  "WF_"
+  "WITH"
+  "WITNESS"
+] @keyword
+[
+  (forall)
+  (exists)
+  (temporal_forall)
+  (temporal_exists)
+  (set_in)
+  (def_eq)
+  (gets)
+  (maps_to)
+  (all_map_to)
+  (case_box)
+  (case_arrow)
+  (label_as)
+] @keyword.function
+
+; Literals
+(number) @number
+(string) @string
+(boolean) @boolean
+(primitive_value_set) @type
+
+; Comments
+(comment) @comment
+(block_comment) @comment
+(unit (single_line) @comment)
+(extramodular_text) @text
+
+; Namespaces
+(module name: (identifier) @namespace)
+(extends (identifier_ref) @namespace)
+(instance (identifier_ref) @namespace)
+(module_definition name: (identifier) @namespace)
+
+; Constants, Variables, and Operators
+(variable_declaration (identifier) @variable)
+(constant_declaration (identifier) @constant)
+(operator_definition name: (_) @function.macro)
+(function_definition name: (identifier) @function)
+(bound_prefix_op symbol: (_) @operator)
+(bound_infix_op symbol: (_) @operator)
+(bound_postfix_op symbol: (_) @operator)
+
+; Parameters
+(operator_definition parameter: (identifier) @parameter)
+(operator_definition (operator_declaration name: (_) @parameter))
+(module_definition parameter: (identifier) @parameter)
+(module_definition (operator_declaration name: (_) @parameter))
+(function_definition (quantifier_bound (identifier) @parameter))
+(function_definition (quantifier_bound (tuple_of_identifiers (identifier) @parameter)))
+(lambda (identifier) @parameter)
+
+; Punctuation and Delimiters
+[
+  (langle_bracket)
+  (rangle_bracket)
+  (rangle_bracket_sub)
+  "{"
+  "}"
+  "["
+  "]"
+  "]_"
+  "("
+  ")"
+] @punctuation.bracket
+[
+  ","
+  ":"
+  "<"
+  ">"
+  "!"
+] @punctuation.delimiter
+(bullet_conj) @punctuation.special
+(bullet_disj) @punctuation.special
+(prev_func_val) @punctuation.special
+
+; Proofs
+(proof_step_id (level) @number)
+(proof_step_id (name) @symbol)
+(proof_step_ref (level) @number)
+(proof_step_ref (name) @symbol)
diff --git a/queries/tlaplus/injections.scm b/queries/tlaplus/injections.scm
new file mode 100644
index 000000000..24bda1cba
--- /dev/null
+++ b/queries/tlaplus/injections.scm
@@ -0,0 +1,4 @@
+[
+  (comment)
+  (block_comment)
+] @comment