if exists('b:current_syntax')
  finish
endif
let b:current_syntax = 'quox'

setlocal iskeyword+=#
setlocal iskeyword+=-
setlocal iskeyword+='

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