From b8313da5a87a375e444796c1daaf5019cf6ff0b2 Mon Sep 17 00:00:00 2001
From: Niklas Gruhn <niklas@gruhn.me>
Date: Thu, 21 Nov 2024 00:56:24 +0100
Subject: [PATCH] Add language support for Quint (#11898)

Co-authored-by: Michael Davis <mcarsondavis@gmail.com>
---
 book/src/generated/lang-support.md   |  1 +
 languages.toml                       | 14 +++++
 runtime/queries/quint/highlights.scm | 94 ++++++++++++++++++++++++++++
 3 files changed, 109 insertions(+)
 create mode 100644 runtime/queries/quint/highlights.scm

diff --git a/book/src/generated/lang-support.md b/book/src/generated/lang-support.md
index 20f861a5d..28f25ba3f 100644
--- a/book/src/generated/lang-support.md
+++ b/book/src/generated/lang-support.md
@@ -169,6 +169,7 @@
 | purescript | ✓ | ✓ |  | `purescript-language-server` |
 | python | ✓ | ✓ | ✓ | `ruff`, `jedi-language-server`, `pylsp` |
 | qml | ✓ |  | ✓ | `qmlls` |
+| quint | ✓ |  |  | `quint-language-server` |
 | r | ✓ |  |  | `R` |
 | racket | ✓ |  | ✓ | `racket` |
 | regex | ✓ |  |  |  |
diff --git a/languages.toml b/languages.toml
index 84171af3f..ea6e6893f 100644
--- a/languages.toml
+++ b/languages.toml
@@ -84,6 +84,7 @@ pyright = { command = "pyright-langserver", args = ["--stdio"], config = {} }
 basedpyright = { command = "basedpyright-langserver", args = ["--stdio"], config = {} }
 pylyzer = { command = "pylyzer", args = ["--server"] }
 qmlls = { command = "qmlls" }
+quint-language-server = { command = "quint-language-server", args = ["--stdio"] }
 r = { command = "R", args = ["--no-echo", "-e", "languageserver::run()"] }
 racket = { command = "racket", args = ["-l", "racket-langserver"] }
 regols = { command = "regols" }
@@ -3893,6 +3894,19 @@ indent = { tab-width = 4, unit = "    " }
 name = "cylc"
 source = { git = "https://github.com/elliotfontaine/tree-sitter-cylc", rev = "30dd40d9bf23912e4aefa93eeb4c7090bda3d0f6" }
 
+[[language]]
+name = "quint"
+scope = "source.quint"
+file-types = ["qnt"]
+language-servers = ["quint-language-server"]
+comment-token = "//"
+block-comment-tokens = { start = "/*", end = "*/" }
+indent = { tab-width = 2, unit = "  " }
+
+[[grammar]]
+name = "quint"
+source = { git = "https://github.com/gruhn/tree-sitter-quint", rev = "eebbd01edfeff6404778c92efe5554e42e506a18" }
+
 [[language]]
 name = "spade"
 scope = "source.spade"
diff --git a/runtime/queries/quint/highlights.scm b/runtime/queries/quint/highlights.scm
new file mode 100644
index 000000000..edb56fbad
--- /dev/null
+++ b/runtime/queries/quint/highlights.scm
@@ -0,0 +1,94 @@
+[
+  "module"
+  "type"
+  "assume"
+  "const"
+  "var"
+  "val"
+  "nondet"
+  "def"
+  "pure"
+  "action"
+  "temporal"
+  "run"
+] @keyword
+
+(match_expr "match" @keyword.control.conditional)
+
+(if_else_condition 
+  "if" @keyword.control.conditional
+  "else" @keyword.control.conditional)
+
+(import "import" @keyword.control.import)
+(import "as" @keyword.control.import)
+(import "from" @keyword.control.import)
+(export "export" @keyword.control.import)
+(export "as" @keyword.control.import)
+
+[
+  "true"
+  "false"
+  "Int"
+  "Nat"
+  "Bool"
+] @constant.builtin
+
+[
+  ";"
+  "."
+  ","
+] @punctuation.delimiter
+
+[
+  "-"
+  "+"
+  "*"
+  "/"
+  "%"
+  "<"
+  "<="
+  "="
+  "=="
+  "!="
+  "=>"
+  ">"
+  ">="
+  "^"
+  "->"
+] @operator
+
+(infix_and "and" @operator)
+(infix_or "or" @operator)
+(infix_iff "iff" @operator)
+(infix_implies "implies" @operator)
+
+(braced_and "and" @keyword)
+(braced_or "or" @keyword)
+(braced_all "all" @keyword)
+(braced_any "any" @keyword)
+
+[
+  "("
+  ")"
+  "["
+  "]"
+  "{"
+  "}"
+] @punctuation.bracket
+
+(polymorphic_type 
+  (type) @type.parameter)
+
+(variant_constructor) @type.enum.variant
+
+(type) @type
+(int_literal) @constant.numeric.integer
+(comment) @comment
+(string) @string
+
+(operator_application
+  operator: (qualified_identifier) @function)
+
+(operator_definition
+  name: (qualified_identifier) @function
+  arguments: (typed_argument_list))