From 44562f7020ad1c5b130051cc9e014fae04a8894e Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Tue, 24 Dec 2024 19:19:07 +0300
Subject: [PATCH] [ new ] Add support for Idris 2 programming language

---
 .gitmodules                                   |   3 +
 CHANGELOG.md                                  |   1 +
 assets/syntaxes/02_Extra/Idris2               |   1 +
 .../syntax-tests/highlighted/Idris2/test.idr  | 107 ++++++++++++++++++
 tests/syntax-tests/source/Idris2/LICENSE.md   |   7 ++
 tests/syntax-tests/source/Idris2/test.idr     | 107 ++++++++++++++++++
 6 files changed, 226 insertions(+)
 create mode 160000 assets/syntaxes/02_Extra/Idris2
 create mode 100644 tests/syntax-tests/highlighted/Idris2/test.idr
 create mode 100644 tests/syntax-tests/source/Idris2/LICENSE.md
 create mode 100644 tests/syntax-tests/source/Idris2/test.idr

diff --git a/.gitmodules b/.gitmodules
index fe159da8..36060a72 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -263,3 +263,6 @@
 [submodule "assets/syntaxes/02_Extra/CFML"]
 	path = assets/syntaxes/02_Extra/CFML
 	url = https://github.com/jcberquist/sublimetext-cfml.git
+[submodule "assets/syntaxes/02_Extra/Idris2"]
+	path = assets/syntaxes/02_Extra/Idris2
+	url = https://github.com/buzden/sublime-syntax-idris2
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4941340e..316ae669 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -70,6 +70,7 @@
 - Adds support for pipe delimiter for CSV #3115 (@pratik-m)
 - Add syntax mapping for `/etc/pacman.conf` #2961 (@cyqsimon)
 - Associate `uv.lock` with `TOML` syntax, see #3132 (@fepegar)
+- Add support for [Idris 2 programming language](https://www.idris-lang.org/) #3150 (@buzden)
 
 ## Themes
 
diff --git a/assets/syntaxes/02_Extra/Idris2 b/assets/syntaxes/02_Extra/Idris2
new file mode 160000
index 00000000..a3d7f5a8
--- /dev/null
+++ b/assets/syntaxes/02_Extra/Idris2
@@ -0,0 +1 @@
+Subproject commit a3d7f5a884cdc2dabf3a9c8193580c613b939cdc
diff --git a/tests/syntax-tests/highlighted/Idris2/test.idr b/tests/syntax-tests/highlighted/Idris2/test.idr
new file mode 100644
index 00000000..04691268
--- /dev/null
+++ b/tests/syntax-tests/highlighted/Idris2/test.idr
@@ -0,0 +1,107 @@
+-- some code in Idris
+module XX.X'''
+
+import Data.Nat
+
+data X = A | B
+
+namespace X
+  ||| Documentation
+  record Y where
+    [noHints]
+    constructor MkY'
+    field1 : Nat
+    {auto x : Nat}
+
+namespace X' {
+  parameters (x : A (Maybe b))
+    x : Nat
+}
+
+u : ()
+u = ()
+
+k, w, u : Char
+k = '\NUL'
+w = 'w'
+
+x = [1, 0, 3, "sdf\{d}", 0xFF, 0o77, 0b10_1, 100_100]
+
+f : Int -> Int
+f = if x > 0 then x else 0 () SS `elem` S $ do
+  x <- a [1, 2, 3]
+  let ukuk = akak
+  rewrite $ Wow Wow Wow Wow.Wow b W (W)
+  pure $ f A B c D (EE) E
+
+(&&&) : Nat -> Nat -> Nat
+z &&& y = d + ?foo
+(&&&) x y = ?asfda
+
+public export covering
+(.fun) : X a Y b => Nat -> Nat
+Z .fun = haha.fun haha .N
+(.fun) Z = ahah $ \case
+  x@(x, y) => Prelude.Types.ahahah
+
+(.N) : Nat -> Nat
+Z .N = Z
+(.N) (S n) = (.N) n
+
+xx : Name
+xx = `{Full.Name}
+
+infixr 0 ^^^, &&&
+
+xxx : ?
+xxx = case x of
+  Z => lalalaCamelCase
+  z => alalalCamelCase
+
+ff : Nat -> TTImp
+ff 0 = let x = 0 in val
+ff _ = `(let x = 0 in ~val ^~^ ~(abc))
+ff _ = f `(let x = 0 in ~val ^~^ ~(abc)) x
+
+%language ElabReflection
+%runElab X.sf ads
+
+%macro %inline
+fff : List Decl
+fff = `[
+  f : Nat -> Nat
+
+  f Z = haha %runElab %search @{%World}
+]
+
+private infixr 4 ^--^
+
+(^--^) : Nat -> Nat -> Nat
+(^--^) Z Z = Z
+x ^--^ y = x + y
+
+x : (y : Vect n (Maybe (Maybe (&&&) Nat))) ->
+    {x : Nat} -> {auto _ : Monoid a} ->
+    {default 4 xx : Nat} ->
+    {default (f x Y) xx' : Nat} ->
+    String
+x Z S = ?foo
+x y _ = "a b \{show $ let x = 0 in y} y >>= z"
+
+multiline : String
+multiline = """
+  A multiline string\NUL
+  """
+
+f' : Nat -> Nat
+f' = x' 4
+
+x : Char
+x = '\BEL'
+x = '\\'
+x = '\''
+x = '\o755'
+x = 'a'
+
+xx : Int
+xx = 0o7_5_5
diff --git a/tests/syntax-tests/source/Idris2/LICENSE.md b/tests/syntax-tests/source/Idris2/LICENSE.md
new file mode 100644
index 00000000..2d9d6206
--- /dev/null
+++ b/tests/syntax-tests/source/Idris2/LICENSE.md
@@ -0,0 +1,7 @@
+The `test.idr` file has been added from https://github.com/buzden/sublime-syntax-idris2 under the following license:
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
diff --git a/tests/syntax-tests/source/Idris2/test.idr b/tests/syntax-tests/source/Idris2/test.idr
new file mode 100644
index 00000000..1fada03d
--- /dev/null
+++ b/tests/syntax-tests/source/Idris2/test.idr
@@ -0,0 +1,107 @@
+-- some code in Idris
+module XX.X'''
+
+import Data.Nat
+
+data X = A | B
+
+namespace X
+  ||| Documentation
+  record Y where
+    [noHints]
+    constructor MkY'
+    field1 : Nat
+    {auto x : Nat}
+
+namespace X' {
+  parameters (x : A (Maybe b))
+    x : Nat
+}
+
+u : ()
+u = ()
+
+k, w, u : Char
+k = '\NUL'
+w = 'w'
+
+x = [1, 0, 3, "sdf\{d}", 0xFF, 0o77, 0b10_1, 100_100]
+
+f : Int -> Int
+f = if x > 0 then x else 0 () SS `elem` S $ do
+  x <- a [1, 2, 3]
+  let ukuk = akak
+  rewrite $ Wow Wow Wow Wow.Wow b W (W)
+  pure $ f A B c D (EE) E
+
+(&&&) : Nat -> Nat -> Nat
+z &&& y = d + ?foo
+(&&&) x y = ?asfda
+
+public export covering
+(.fun) : X a Y b => Nat -> Nat
+Z .fun = haha.fun haha .N
+(.fun) Z = ahah $ \case
+  x@(x, y) => Prelude.Types.ahahah
+
+(.N) : Nat -> Nat
+Z .N = Z
+(.N) (S n) = (.N) n
+
+xx : Name
+xx = `{Full.Name}
+
+infixr 0 ^^^, &&&
+
+xxx : ?
+xxx = case x of
+  Z => lalalaCamelCase
+  z => alalalCamelCase
+
+ff : Nat -> TTImp
+ff 0 = let x = 0 in val
+ff _ = `(let x = 0 in ~val ^~^ ~(abc))
+ff _ = f `(let x = 0 in ~val ^~^ ~(abc)) x
+
+%language ElabReflection
+%runElab X.sf ads
+
+%macro %inline
+fff : List Decl
+fff = `[
+  f : Nat -> Nat
+
+  f Z = haha %runElab %search @{%World}
+]
+
+private infixr 4 ^--^
+
+(^--^) : Nat -> Nat -> Nat
+(^--^) Z Z = Z
+x ^--^ y = x + y
+
+x : (y : Vect n (Maybe (Maybe (&&&) Nat))) ->
+    {x : Nat} -> {auto _ : Monoid a} ->
+    {default 4 xx : Nat} ->
+    {default (f x Y) xx' : Nat} ->
+    String
+x Z S = ?foo
+x y _ = "a b \{show $ let x = 0 in y} y >>= z"
+
+multiline : String
+multiline = """
+  A multiline string\NUL
+  """
+
+f' : Nat -> Nat
+f' = x' 4
+
+x : Char
+x = '\BEL'
+x = '\\'
+x = '\''
+x = '\o755'
+x = 'a'
+
+xx : Int
+xx = 0o7_5_5