From 0c76381c7176253e218517f108d461b10afe0f5a 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 941e4e3c..98ee4934 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -89,6 +89,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..7c1bf44c --- /dev/null +++ b/assets/syntaxes/02_Extra/Idris2 @@ -0,0 +1 @@ +Subproject commit 7c1bf44c4f9092b7b1e274b1332cf32a089b2b99 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 @@ +[38;2;117;113;94m-- some code in Idris[0m +[38;2;249;38;114mmodule[0m[38;2;248;248;242m [0m[38;2;166;226;46mXX.X'''[0m + +[38;2;249;38;114mimport[0m[38;2;248;248;242m [0m[38;2;166;226;46mData.Nat[0m + +[38;2;249;38;114mdata[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mX[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mA[0m[38;2;248;248;242m [0m[38;2;249;38;114m|[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mB[0m + +[38;2;249;38;114mnamespace[0m[38;2;248;248;242m [0m[38;2;166;226;46mX[0m +[38;2;248;248;242m [0m[38;2;117;113;94m||| Documentation[0m +[38;2;248;248;242m [0m[38;2;249;38;114mrecord[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mY[0m[38;2;248;248;242m [0m[38;2;249;38;114mwhere[0m +[38;2;248;248;242m [0m[38;2;249;38;114m[[0m[38;2;248;248;242mnoHints[0m[38;2;249;38;114m][0m +[38;2;248;248;242m [0m[38;2;249;38;114mconstructor[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mMkY'[0m +[38;2;248;248;242m [0m[38;2;166;226;46mfield1[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m +[38;2;248;248;242m [0m[38;2;248;248;242m{[0m[38;2;249;38;114mauto[0m[38;2;248;248;242m [0m[3;38;2;253;151;31mx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m}[0m + +[38;2;249;38;114mnamespace[0m[38;2;248;248;242m [0m[38;2;166;226;46mX'[0m[38;2;248;248;242m [0m[38;2;249;38;114m{[0m +[38;2;248;248;242m [0m[38;2;249;38;114mparameters[0m[38;2;248;248;242m [0m[38;2;248;248;242m([0m[3;38;2;253;151;31mx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mA[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[3;38;2;102;217;239mMaybe[0m[38;2;248;248;242m b[0m[38;2;249;38;114m)[0m[38;2;248;248;242m)[0m +[38;2;248;248;242m [0m[38;2;166;226;46mx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m +[38;2;249;38;114m}[0m + +[38;2;166;226;46mu[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239m()[0m +[38;2;248;248;242mu [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[3;38;2;102;217;239m()[0m + +[38;2;166;226;46mk[0m[38;2;248;248;242m, [0m[38;2;166;226;46mw[0m[38;2;248;248;242m, [0m[38;2;166;226;46mu[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mChar[0m +[38;2;248;248;242mk [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255m\NUL[0m[38;2;190;132;255m'[0m +[38;2;248;248;242mw [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255mw[0m[38;2;190;132;255m'[0m + +[38;2;248;248;242mx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114m[[0m[38;2;190;132;255m1[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m3[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;230;219;116m"[0m[38;2;230;219;116msdf[0m[38;2;248;248;242m\{[0m[38;2;248;248;242md[0m[38;2;248;248;242m}[0m[38;2;230;219;116m"[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m0xFF[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m0o77[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m0b10_1[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m100_100[0m[38;2;249;38;114m][0m + +[38;2;166;226;46mf[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mInt[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mInt[0m +[38;2;248;248;242mf [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114mif[0m[38;2;248;248;242m x [0m[38;2;249;38;114m>[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114mthen[0m[38;2;248;248;242m x [0m[38;2;249;38;114melse[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[3;38;2;102;217;239m()[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mSS[0m[38;2;248;248;242m [0m[38;2;249;38;114m`[0m[38;2;249;38;114melem[0m[38;2;249;38;114m`[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mS[0m[38;2;248;248;242m [0m[38;2;249;38;114m$[0m[38;2;248;248;242m [0m[38;2;249;38;114mdo[0m +[38;2;248;248;242m x [0m[38;2;249;38;114m<-[0m[38;2;248;248;242m a [0m[38;2;249;38;114m[[0m[38;2;190;132;255m1[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m2[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m3[0m[38;2;249;38;114m][0m +[38;2;248;248;242m [0m[38;2;249;38;114mlet[0m[38;2;248;248;242m ukuk [0m[38;2;249;38;114m=[0m[38;2;248;248;242m akak[0m +[38;2;248;248;242m [0m[38;2;249;38;114mrewrite[0m[38;2;248;248;242m [0m[38;2;249;38;114m$[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mWow[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mWow[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mWow[0m[38;2;248;248;242m [0m[38;2;166;226;46mWow.[0m[3;38;2;102;217;239mWow[0m[38;2;248;248;242m b [0m[3;38;2;102;217;239mW[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[3;38;2;102;217;239mW[0m[38;2;249;38;114m)[0m +[38;2;248;248;242m pure [0m[38;2;249;38;114m$[0m[38;2;248;248;242m f [0m[3;38;2;102;217;239mA[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mB[0m[38;2;248;248;242m c [0m[3;38;2;102;217;239mD[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[3;38;2;102;217;239mEE[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mE[0m + +[38;2;166;226;46m(&&&)[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m +[38;2;248;248;242mz [0m[38;2;249;38;114m&&&[0m[38;2;248;248;242m y [0m[38;2;249;38;114m=[0m[38;2;248;248;242m d [0m[38;2;249;38;114m+[0m[38;2;248;248;242m [0m[38;2;248;248;242m?foo[0m +[38;2;249;38;114m([0m[38;2;248;248;242m&&&[0m[38;2;249;38;114m)[0m[38;2;248;248;242m x y [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;248;248;242m?asfda[0m + +[38;2;249;38;114mpublic[0m[38;2;248;248;242m [0m[38;2;249;38;114mexport[0m[38;2;248;248;242m [0m[38;2;249;38;114mcovering[0m +[38;2;166;226;46m(.fun)[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mX[0m[38;2;248;248;242m a [0m[3;38;2;102;217;239mY[0m[38;2;248;248;242m b [0m[38;2;249;38;114m=>[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m +[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[38;2;249;38;114m.[0m[38;2;248;248;242mfun [0m[38;2;249;38;114m=[0m[38;2;248;248;242m haha[0m[38;2;249;38;114m.[0m[38;2;248;248;242mfun haha [0m[38;2;249;38;114m.[0m[38;2;248;248;242mN[0m +[38;2;249;38;114m([0m[38;2;249;38;114m.[0m[38;2;248;248;242mfun[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m ahah [0m[38;2;249;38;114m$[0m[38;2;248;248;242m [0m[38;2;249;38;114m\case[0m +[38;2;248;248;242m x[0m[38;2;249;38;114m@[0m[38;2;249;38;114m([0m[38;2;248;248;242mx[0m[38;2;249;38;114m,[0m[38;2;248;248;242m y[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[38;2;249;38;114m=>[0m[38;2;248;248;242m [0m[38;2;166;226;46mPrelude.Types.[0m[38;2;248;248;242mahahah[0m + +[38;2;166;226;46m(.N)[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m +[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[38;2;249;38;114m.[0m[38;2;248;248;242mN [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mZ[0m +[38;2;249;38;114m([0m[38;2;249;38;114m.[0m[38;2;248;248;242mN[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[3;38;2;102;217;239mS[0m[38;2;248;248;242m n[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[38;2;249;38;114m.[0m[38;2;248;248;242mN[0m[38;2;249;38;114m)[0m[38;2;248;248;242m n[0m + +[38;2;166;226;46mxx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mName[0m +[38;2;248;248;242mxx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114m`{[0m[38;2;166;226;46mFull.[0m[3;38;2;102;217;239mName[0m[38;2;249;38;114m}[0m + +[38;2;249;38;114minfixr[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114m^^^[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;249;38;114m&&&[0m + +[38;2;166;226;46mxxx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[38;2;248;248;242m?[0m +[38;2;248;248;242mxxx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114mcase[0m[38;2;248;248;242m x [0m[38;2;249;38;114mof[0m +[38;2;248;248;242m [0m[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[38;2;249;38;114m=>[0m[38;2;248;248;242m lalalaCamelCase[0m +[38;2;248;248;242m z [0m[38;2;249;38;114m=>[0m[38;2;248;248;242m alalalCamelCase[0m + +[38;2;166;226;46mff[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mTTImp[0m +[38;2;248;248;242mff [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114mlet[0m[38;2;248;248;242m x [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114min[0m[38;2;248;248;242m val[0m +[38;2;248;248;242mff [0m[38;2;190;132;255m_[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114m`([0m[38;2;249;38;114mlet[0m[38;2;248;248;242m x [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114min[0m[38;2;248;248;242m [0m[38;2;249;38;114m~[0m[38;2;248;248;242mval [0m[38;2;249;38;114m^~^[0m[38;2;248;248;242m [0m[38;2;249;38;114m~[0m[38;2;249;38;114m([0m[38;2;248;248;242mabc[0m[38;2;249;38;114m)[0m[38;2;249;38;114m)[0m +[38;2;248;248;242mff [0m[38;2;190;132;255m_[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m f [0m[38;2;249;38;114m`([0m[38;2;249;38;114mlet[0m[38;2;248;248;242m x [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114min[0m[38;2;248;248;242m [0m[38;2;249;38;114m~[0m[38;2;248;248;242mval [0m[38;2;249;38;114m^~^[0m[38;2;248;248;242m [0m[38;2;249;38;114m~[0m[38;2;249;38;114m([0m[38;2;248;248;242mabc[0m[38;2;249;38;114m)[0m[38;2;249;38;114m)[0m[38;2;248;248;242m x[0m + +[38;2;249;38;114m%language[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mElabReflection[0m +[38;2;249;38;114m%runElab[0m[38;2;248;248;242m [0m[38;2;166;226;46mX.[0m[38;2;248;248;242msf ads[0m + +[38;2;249;38;114m%macro[0m[38;2;248;248;242m [0m[38;2;249;38;114m%inline[0m +[38;2;166;226;46mfff[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mList[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mDecl[0m +[38;2;248;248;242mfff [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114m`[[0m +[38;2;248;248;242m [0m[38;2;166;226;46mf[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m + +[38;2;248;248;242m f [0m[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m haha [0m[38;2;249;38;114m%runElab[0m[38;2;248;248;242m [0m[38;2;249;38;114m%search[0m[38;2;248;248;242m [0m[38;2;249;38;114m@[0m[38;2;249;38;114m{[0m[38;2;249;38;114m%World[0m[38;2;249;38;114m}[0m +[38;2;249;38;114m][0m + +[38;2;249;38;114mprivate[0m[38;2;248;248;242m [0m[38;2;249;38;114minfixr[0m[38;2;248;248;242m [0m[38;2;190;132;255m4[0m[38;2;248;248;242m [0m[38;2;249;38;114m^--^[0m + +[38;2;249;38;114m([0m[38;2;249;38;114m^--^[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m +[38;2;249;38;114m([0m[38;2;249;38;114m^--^[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mZ[0m +[38;2;248;248;242mx [0m[38;2;249;38;114m^--^[0m[38;2;248;248;242m y [0m[38;2;249;38;114m=[0m[38;2;248;248;242m x [0m[38;2;249;38;114m+[0m[38;2;248;248;242m y[0m + +[38;2;166;226;46mx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[38;2;248;248;242m([0m[3;38;2;253;151;31my[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mVect[0m[38;2;248;248;242m n [0m[38;2;249;38;114m([0m[3;38;2;102;217;239mMaybe[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[3;38;2;102;217;239mMaybe[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[38;2;248;248;242m&&&[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;249;38;114m)[0m[38;2;249;38;114m)[0m[38;2;248;248;242m)[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m +[38;2;248;248;242m [0m[38;2;248;248;242m{[0m[3;38;2;253;151;31mx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m}[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[38;2;248;248;242m{[0m[38;2;249;38;114mauto[0m[38;2;248;248;242m [0m[3;38;2;253;151;31m_[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mMonoid[0m[38;2;248;248;242m a[0m[38;2;248;248;242m}[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m +[38;2;248;248;242m [0m[38;2;248;248;242m{[0m[38;2;249;38;114mdefault [0m[38;2;249;38;114m4[0m[38;2;248;248;242m [0m[3;38;2;253;151;31mxx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m}[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m +[38;2;248;248;242m [0m[38;2;248;248;242m{[0m[38;2;249;38;114mdefault [0m[38;2;249;38;114m(f x Y)[0m[38;2;248;248;242m [0m[3;38;2;253;151;31mxx'[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m}[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m +[38;2;248;248;242m [0m[3;38;2;102;217;239mString[0m +[38;2;248;248;242mx [0m[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mS[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;248;248;242m?foo[0m +[38;2;248;248;242mx y [0m[38;2;190;132;255m_[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;230;219;116m"[0m[38;2;230;219;116ma b [0m[38;2;248;248;242m\{[0m[38;2;248;248;242mshow [0m[38;2;249;38;114m$[0m[38;2;248;248;242m [0m[38;2;249;38;114mlet[0m[38;2;248;248;242m x [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114min[0m[38;2;248;248;242m y[0m[38;2;248;248;242m}[0m[38;2;230;219;116m y >>= z[0m[38;2;230;219;116m"[0m + +[38;2;166;226;46mmultiline[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mString[0m +[38;2;248;248;242mmultiline [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;230;219;116m"[0m[38;2;230;219;116m"[0m[38;2;230;219;116m"[0m +[38;2;230;219;116m A multiline string[0m[38;2;190;132;255m\NUL[0m +[38;2;230;219;116m [0m[38;2;230;219;116m"[0m[38;2;230;219;116m"[0m[38;2;230;219;116m"[0m + +[38;2;166;226;46mf'[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m +[38;2;248;248;242mf' [0m[38;2;249;38;114m=[0m[38;2;248;248;242m x' [0m[38;2;190;132;255m4[0m + +[38;2;166;226;46mx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mChar[0m +[38;2;248;248;242mx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255m\BEL[0m[38;2;190;132;255m'[0m +[38;2;248;248;242mx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255m\\[0m[38;2;190;132;255m'[0m +[38;2;248;248;242mx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255m\'[0m[38;2;190;132;255m'[0m +[38;2;248;248;242mx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255m\o755[0m[38;2;190;132;255m'[0m +[38;2;248;248;242mx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255ma[0m[38;2;190;132;255m'[0m + +[38;2;166;226;46mxx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mInt[0m +[38;2;248;248;242mxx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m0o7_5_5[0m 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