Added TLA+ grammar & queries

3 files changed, 149 insertions, 0 deletions

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