Added TLA+ grammar & queries

This commit is contained in:
Andrew Helwer 2021-08-18 12:48:01 -04:00 committed by Stephan Seitz
parent 37ee5b784e
commit 5821a85165
7 changed files with 163 additions and 0 deletions

View file

@ -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)

1
ftdetect/tlaplus.vim Normal file
View file

@ -0,0 +1 @@
au BufRead,BufNewFile *.tla set filetype=tla

View file

@ -185,6 +185,9 @@
"teal": {
"revision": "fcc5f6f4d194dede4e676834ff28a506e39e17b4"
},
"tlaplus": {
"revision": "36e7863609f5fbb4b0e39b1a035f5b3245f974f6"
},
"toml": {
"revision": "8bd2056818b21860e3d756b5a58c4f6e05fb744e"
},

View file

@ -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",

View file

@ -0,0 +1,5 @@
[
(extramodular_text)
(block_comment)
(non_terminal_proof)
] @fold

View file

@ -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)

View file

@ -0,0 +1,4 @@
[
(comment)
(block_comment)
] @comment