From a2fa57272f93c71b64ecbb7896d4893784ca5fbb Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 5 Nov 2023 22:15:02 +0100
Subject: [PATCH] first

---
 ftdetect/quox.vim |  1 +
 syntax/quox.vim   | 73 +++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 74 insertions(+)
 create mode 100644 ftdetect/quox.vim
 create mode 100644 syntax/quox.vim

diff --git a/ftdetect/quox.vim b/ftdetect/quox.vim
new file mode 100644
index 0000000..6057629
--- /dev/null
+++ b/ftdetect/quox.vim
@@ -0,0 +1 @@
+au BufNewFile,BufRead *.quox setf quox
diff --git a/syntax/quox.vim b/syntax/quox.vim
new file mode 100644
index 0000000..df6590e
--- /dev/null
+++ b/syntax/quox.vim
@@ -0,0 +1,73 @@
+set isk+=-,#
+
+
+syn match quoxDelim /[\[\](){};]/
+syn match quoxDelim /\<_\>/
+hi def link quoxDelim Delimiter
+
+" [todo] don't match these inside longer symbols!!
+syn match quoxSymbol /⇒\|=>\?\|∷\|::\?\|,/
+syn keyword quoxSymbol λ fun comp
+syn match quoxSymbol /\%(\<\%(δ\|dfun\)\>\|@\)\s*/ nextgroup=quoxDimension
+syn match quoxSymbol /\<coe\>\s*/ nextgroup=quoxTypeLine
+hi def link quoxSymbol Keyword
+
+syn match quoxTypeLine /(/ contained nextgroup=quoxDimension
+hi link quoxTypeLine quoxDelim
+
+syn keyword quoxBuiltinType String Nat IOState Type
+syn match quoxBuiltinType /×\|\*\*\|≡\|==\|→\|->\|\k\@<!ℕ\k\@!/
+syn match quoxBuiltinType /★/
+syn match quoxBuiltinType /\<Eq\>\s*/ nextgroup=quoxTypeLine
+hi def link quoxBuiltinType Type
+
+syn keyword quoxBuiltinVal fst snd
+hi def link quoxBuiltinVal Function
+
+syn match quoxNat /\<\d\%(\%(\d\|_\)*\d\)\?\>/
+syn match quoxNat /\c\<0x\x\%(\%(\x\|_\)*\x\)\?\>/
+hi def link quoxNat Number
+
+syn region quoxString start=+"+ end=+"+ skip=+\\"+ contains=quoxCharEsc
+hi def link quoxString String
+
+syn match quoxTag /'\k\+/
+syn region quoxTag start=+'"+ end=+"+ skip=+\\"+ contains=quoxCharEsc
+hi def link quoxTag Constant
+
+syn match quoxCharEsc /\\\%(\\\|"\|x\x\+;\|[nt]\)/ contained
+hi def link quoxCharEsc SpecialChar
+
+syn match quoxQty /\<[01#ω]\./
+hi def link quoxQty Special
+
+syn match quoxDef /\<\%(def\|postulate\)[01#ω]\?\>/ contains=quoxQtySuffix
+syn match quoxQtySuffix /[01#ω]\>/ contained
+hi def link quoxDef Label
+hi def link quoxQtySuffix quoxQty
+
+syn keyword quoxNamespace namespace
+hi def link quoxNamespace Type
+
+syn match   quoxCase /\<case[01#ω]\?\>/ contains=quoxQtySuffix
+syn keyword quoxCase return of
+hi def link quoxCase Conditional
+
+syn match quoxDimension /\%([𝑖𝑗𝑘𝑙]\|\k\)\+/ contained
+hi def link quoxDimension PreProc
+
+syn region quoxComment start=+{-+ end=+-}+ contains=quoxComment
+syn match quoxComment /--.*$/
+hi def link quoxComment Comment
+
+syn keyword quoxLoad load
+hi def link quoxLoad Include
+
+syn region quoxAttr matchgroup=quoxDelim start=+#\[+ end=+\]+ contains=TOP
+syn region quoxAttrBrack start=+\[+ end=+\]+ matchgroup=quoxDelim contained containedin=quoxAttr
+syn keyword quoxAttrName fail main compile-scheme contained containedin=quoxAttr
+hi def link quoxAttrName PreProc
+
+syn match quoxDisplace /[⁰¹²³⁴⁵⁶⁷⁸⁹]\+/
+syn match quoxDisplace /\^\d\+/
+hi def link quoxDisplace Special