commit e3816a7be58b4f8cadf10038314fe8ee9b01daa2 Author: Edwin Brady Date: Sat Feb 22 20:32:56 2020 +0000 Initial version Mostly copied from idris-vim diff --git a/README.md b/README.md new file mode 100644 index 0000000..ea03240 --- /dev/null +++ b/README.md @@ -0,0 +1,125 @@ +Idris 2 mode for vim +==================== + +This is an [Idris 2][] mode for vim which features syntax highlighting, +indentation and optional syntax checking via [Syntastic][]. If you need a REPL +I recommend using [Vimshell][]. + +![Screenshot](http://raichoo.github.io/images/vim.png) + +## Installation + +I recommend using [Pathogen][] for installation. Simply clone +this repo into your `~/.vim/bundle` directory and you are ready to go. + + cd ~/.vim/bundle + git clone https://github.com/idris-hackers/idris-vim.git + +### Manual Installation + +Copy content into your `~/.vim` directory. + +Be sure that the following lines are in your +`.vimrc` + + + syntax on + filetype on + filetype plugin indent on + +## Features + +Apart from syntax highlighting, indentation, and unicode character concealing, +idris-vim offers some neat interactive editing features. For more information on +how to use it, read this blog article by Edwin Brady on [Interactive Idris editing with vim][]. + +## Interactive Editing Commands + +[Idris][] mode for vim offers interactive editing capabilities, the following +commands are supported. + +`r` reload file + +`t` show type + +`d` Create an initial clause for a type declaration. + +`b` Same as \d but for an initial typeclass method impl. + +`md` Same as \d but for a proof clause + +`c` case split + +`mc` make case + +`w` add with clause + +`e` evaluate expression + +`l` make lemma + +`m` add missing clause + +`f` refine item + +`o` obvious proof search + +`p` proof search + +`i` open idris response window + +`h` show documentation + +## Configuration + +### Indentation + +To configure indentation in `idris-vim` you can use the following variables: + +* `let g:idris_indent_if = 3` + + if bool + >>>then ... + >>>else ... + +* `let g:idris_indent_case = 5` + + case xs of + >>>>>[] => ... + >>>>>(y::ys) => ... + +* `let g:idris_indent_let = 4` + + let x = 0 in + >>>>x + +* `let g:idris_indent_where = 6` + + where f : Int -> Int + >>>>>>f x = x + +* `let g:idris_indent_do = 3` + + do x <- a + >>>y <- b + +* `let g:idris_indent_rewrite = 8` + + rewrite prf in expr + >>>>>>>>x + +### Concealing + +Concealing with unicode characters is off by default, but `let g:idris_conceal = 1` turns it on. + +### Tab Characters + +If you simply must use tab characters, and would prefer that the ftplugin not set expandtab add `let g:idris_allow_tabchar = 1`. + + +[Idris]: http://www.idris-lang.org +[Syntastic]: https://github.com/scrooloose/syntastic +[Vimshell]: https://github.com/Shougo/vimshell.vim +[Pathogen]: https://github.com/tpope/vim-pathogen +[Interactive Idris editing with vim]: http://edwinb.wordpress.com/2013/10/28/interactive-idris-editing-with-vim/ + diff --git a/after/ftplugin/idris2.vim b/after/ftplugin/idris2.vim new file mode 100644 index 0000000..8468b65 --- /dev/null +++ b/after/ftplugin/idris2.vim @@ -0,0 +1 @@ +setlocal iskeyword+=' diff --git a/after/syntax/idris2.vim b/after/syntax/idris2.vim new file mode 100644 index 0000000..7165bb0 --- /dev/null +++ b/after/syntax/idris2.vim @@ -0,0 +1,78 @@ +" This script allows for unicode concealing of certain characters +" For instance -> goes to → +" +" It needs vim >= 7.3, set nocompatible, set enc=utf-8 +" +" If you want to turn this on, let g:idris_conceal = 1 + +if !exists('g:idris_conceal') || !has('conceal') || &enc != 'utf-8' + finish +endif + +" vim: set fenc=utf-8: +syntax match idrNiceOperator "\\\ze[[:alpha:][:space:]_([]" conceal cchar=λ +syntax match idrNiceOperator "<-" conceal cchar=← +syntax match idrNiceOperator "->" conceal cchar=→ +syntax match idrNiceOperator "\" conceal cchar=∑ +syntax match idrNiceOperator "\" conceal cchar=∏ +syntax match idrNiceOperator "\" conceal cchar=√ +syntax match idrNiceOperator "\" conceal cchar=π +syntax match idrNiceOperator "==" conceal cchar=≡ +syntax match idrNiceOperator "\/=" conceal cchar=≠ + + +let s:extraConceal = 1 + +let s:doubleArrow = 1 +" Set this to 0 to use the more technically correct arrow from bar + +" Some windows font don't support some of the characters, +" so if they are the main font, we don't load them :) +if has("win32") + let s:incompleteFont = [ 'Consolas' + \ , 'Lucida Console' + \ , 'Courier New' + \ ] + let s:mainfont = substitute( &guifont, '^\([^:,]\+\).*', '\1', '') + for s:fontName in s:incompleteFont + if s:mainfont ==? s:fontName + let s:extraConceal = 0 + break + endif + endfor +endif + +if s:extraConceal + syntax match idrNiceOperator "Void" conceal cchar=⊥ + + " Match greater than and lower than w/o messing with Kleisli composition + syntax match idrNiceOperator "<=\ze[^<]" conceal cchar=≤ + syntax match idrNiceOperator ">=\ze[^>]" conceal cchar=≥ + + if s:doubleArrow + syntax match idrNiceOperator "=>" conceal cchar=⇒ + else + syntax match idrNiceOperator "=>" conceal cchar=↦ + endif + + syntax match idrNiceOperator "=\zs<<" conceal cchar=« + + syntax match idrNiceOperator "++" conceal cchar=⧺ + syntax match idrNiceOperator "::" conceal cchar=∷ + syntax match idrNiceOperator "-<" conceal cchar=↢ + syntax match idrNiceOperator ">-" conceal cchar=↣ + syntax match idrNiceOperator "-<<" conceal cchar=⤛ + syntax match idrNiceOperator ">>-" conceal cchar=⤜ + + " Only replace the dot, avoid taking spaces around. + syntax match idrNiceOperator /\s\.\s/ms=s+1,me=e-1 conceal cchar=∘ + syntax match idrNiceOperator "\.\." conceal cchar=‥ + + syntax match idrNiceOperator "`elem`" conceal cchar=∈ + syntax match idrNiceOperator "`notElem`" conceal cchar=∉ +endif + +hi link idrNiceOperator Operator +hi! link Conceal Operator +setlocal conceallevel=2 + diff --git a/doc/idris2-vim.txt b/doc/idris2-vim.txt new file mode 100644 index 0000000..a1b96ee --- /dev/null +++ b/doc/idris2-vim.txt @@ -0,0 +1,154 @@ +*idris2-vim.txt* Last change 2020 February 22 +=============================================================================== +=============================================================================== + @@@@ @@@@@@@@ @@@@@@@@ @@@@ @@@@@@ @@ @@ @@@@ @@ @@ + @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@@ @@@ + @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@@@ @@@@ + @@ @@ @@ @@@@@@@@ @@ @@@@@@ @@@@@@@ @@ @@ @@ @@ @@@ @@ + @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ + @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ + @@@@ @@@@@@@@ @@ @@ @@@@ @@@@@@ @@@ @@@@ @@ @@ +=============================================================================== +CONTENTS *idris-vim-contents* + + 1. Features: |idris-vim-features| + 2. Requirements: |idris-vim-requirements| + 3. Functions: |idris-vim-functions| + 4. Troubleshooting |idris-vim-troubleshooting| + 5. Examples: |idris-vim-examples| + 6. Information: |idris-vim-information| + +=============================================================================== +FEATURES *idris-vim-features* + + * Syntax Highlighting + * Indentation + * Unicode Concealing + * Syntax Checking (via Syntastic(https://github.com/scrooloose/syntastic)) + * Interactive Editing via the REPL + +=============================================================================== +REQUIREMENTS *idris-vim-requirements* + + * Idris2 (https://github.com/edwinb/Idris2/) + + OPTIONAL: + + * Syntastic(https://github.com/scrooloose/syntastic) for syntax checking + * Vimshell(https://github.com/Shougo/vimshell.vim) for a REPL + +=============================================================================== +FUNCTIONS *idris-vim-functions* + +All of the functions in idris-vim are essentially just calls back to the REPL, +so documentation for each of them is also available there. + +IdrisDocumentation *IdrisDocumentation* + Shows internal documentation of the primitive under the cursor. + + Mapped to '_h' by default. + +IdrisResponseWin *IdrisResponseWin* + This opens an idris response window in a new pane. + + Mapped to '_i' by default. + +IdrisShowType *IdrisShowType* + This shows the type of the name under the cursor (or, if the cursor happens + to be over a metavariable, a bit more information about its context). + + Mapped to '_t' by default. + +IdrisReload *IdrisReload* + This reloads the file and type-checks the file in the current buffer. + + Mapped to '_r' by default. + +IdrisEval *IdrisEval* + This prompts for an expression and then evaluates it in the REPL, then + returns the result. + + Mapped to '_e' by default. + +IdrisCaseSplit *IdrisCaseSplit* + When the cursor is over a variable in a pattern match clause or case + expression, this splits the variable into all well-typed patterns. + + Mapped to '_c' by default + +IdrisAddClause *IdrisAddClause* + When the cursor is at a type declaration this creates a new clause for that + signature. + + By default mapped to '_d' for an ordinary top-level definition, + '_b' for a typeclass instance definition, and + '_md' to add a pattern-matching proof clause. + +IdrisAddMissing: *IdrisAddMissing* + When the cursor is over a function, this adds all clauses necessary to make + that function cover all inputs. This also eliminates clauses which would + lead to unification errors from appearing. + + Mapped to '_m' by default + +IdrisRefine: *IdrisRefine* + Refines the item the cursor is over (applies the name and fills in any + arguments which can be filled in via unification) + + Mapped to '_f' by default + +IdrisProofSearch: *IdrisProofSearch* + This attempts to find a value for the metavariable it was called on by + looking at the rest of the code. It can also be called with hints, which + are functions that can apply to help solve for the metavariable. + + Mapped to '_o' without hints and 'p' with hints by + default + +IdrisMakeWith: *IdrisMakeWith* + When the cursor is over a pattern clause and this is called, it creates a + new with clause. + + Mapped to '_w' by default + +IdrisMakeLemma: *IdrisMakeLemma* + When the cursor is over a metavariable and this is called, it creates a new + top-level definition to solve the metavariable. + + Mapped to '_l' by default + +=============================================================================== +TROUBLESHOOTING *idris-vim-troubleshooting* + +If this isn't working for you, make sure that: + + * There is an Idris REPL running + * For syntax checking, you have syntastic installed + * The plugins mappings exists and don't conflict with anything else installed + (You can use ':map' to check. There should be mappings similar to + '\h * :call IdrisShowDoc()'.) + * Vim recognizes you're in an idris file (you can use ':verb set ft' to check) + +If none of this works, check to issue tracker on github and if nothing is +there create an issue with a detailed description of the problem. + +=============================================================================== +EXAMPLES *idris-vim-examples* + +Some excellent tutorials/examples for interactive editing using the above +functions can be found at: + http://edwinb.wordpress.com/2013/10/28/interactive-idris-editing-with-vim/ +and + http://www.scribd.com/doc/214031954/60/Interactive-Editing-in-Vim + +=============================================================================== +INFORMATION *idris-vim-information* + +Author: edwinb +Repo: https://github.com/idris-hackers/idris-vim + +Documentation by japesinator + +=============================================================================== +=============================================================================== +" vim:ft=help:et:ts=2:sw=2:sts=2:norl: diff --git a/ftdetect/idris2.vim b/ftdetect/idris2.vim new file mode 100644 index 0000000..3f57c9d --- /dev/null +++ b/ftdetect/idris2.vim @@ -0,0 +1,2 @@ +au BufNewFile,BufRead *.idr setf idris2 +au BufNewFile,BufRead idris-response setf idris2 diff --git a/ftdetect/lidris.vim b/ftdetect/lidris.vim new file mode 100644 index 0000000..ea1e7f6 --- /dev/null +++ b/ftdetect/lidris.vim @@ -0,0 +1 @@ +au BufNewFile,BufRead *.lidr setf lidris diff --git a/ftplugin/idris2.vim b/ftplugin/idris2.vim new file mode 100644 index 0000000..9458996 --- /dev/null +++ b/ftplugin/idris2.vim @@ -0,0 +1,330 @@ +if bufname('%') == "idris-response" + finish +endif + +if exists("b:did_ftplugin") + finish +endif + +setlocal shiftwidth=2 +setlocal tabstop=2 +if !exists("g:idris_allow_tabchar") || g:idris_allow_tabchar == 0 + setlocal expandtab +endif +setlocal comments=s1:{-,mb:-,ex:-},:\|\|\|,:-- +setlocal commentstring=--%s +setlocal iskeyword+=? +setlocal wildignore+=*.ibc + +let idris_response = 0 +let b:did_ftplugin = 1 + +" Text near cursor position that needs to be passed to a command. +" Refinment of `expand()` to accomodate differences between +" a (n)vim word and what Idris requires. +function! s:currentQueryObject() + let word = expand("") + if word =~ '^?' + " Cut off '?' that introduces a hole identifier. + let word = strpart(word, 1) + endif + return word +endfunction + +function! s:IdrisCommand(...) + let idriscmd = shellescape(join(a:000)) +" echo("idris2 " . expand ('%:t') . " --client " . idriscmd) + return system("idris2 " . expand ('%:t') . " --client " . idriscmd) +endfunction + +function! IdrisDocFold(lineNum) + let line = getline(a:lineNum) + + if line =~ "^\s*|||" + return "1" + endif + + return "0" +endfunction + +function! IdrisFold(lineNum) + return IdrisDocFold(a:lineNum) +endfunction + +setlocal foldmethod=expr +setlocal foldexpr=IdrisFold(v:lnum) + +function! IdrisResponseWin() + if (!bufexists("idris-response")) + botright 10split + badd idris-response + b idris-response + let g:idris_respwin = "active" + set buftype=nofile + wincmd k + elseif (bufexists("idris-response") && g:idris_respwin == "hidden") + botright 10split + b idris-response + let g:idris_respwin = "active" + wincmd k + endif +endfunction + +function! IdrisHideResponseWin() + let g:idris_respwin = "hidden" +endfunction + +function! IdrisShowResponseWin() + let g:idris_respwin = "active" +endfunction + +function! IWrite(str) + if (bufexists("idris-response")) + let save_cursor = getcurpos() + b idris-response + %delete + let resp = split(a:str, '\n') + call append(1, resp) + b # + call setpos('.', save_cursor) + else + echo a:str + endif +endfunction + +function! IdrisReload(q) + w + let file = expand("%:p") + let tc = system("idris2 " . expand ('%:t') . " --client ''") + if (! (tc is "")) + call IWrite(tc) + else + if (a:q==0) + call IWrite("Successfully reloaded " . file) + endif + endif + return tc +endfunction + +function! IdrisReloadToLine(cline) + return IdrisReload(1) + "w + "let file = expand("%:p") + "let tc = s:IdrisCommand(":lto", a:cline, file) + "if (! (tc is "")) + " call IWrite(tc) + "endif + "return tc +endfunction + +function! IdrisShowType() + w + let word = s:currentQueryObject() + let cline = line(".") + let ccol = col(".") + let ty = s:IdrisCommand(":t", word) + call IWrite(ty) +endfunction + +function! IdrisShowDoc() + w + let word = expand("") + let ty = s:IdrisCommand(":doc", word) + call IWrite(ty) +endfunction + +function! IdrisProofSearch(hint) + let view = winsaveview() + w + let cline = line(".") + let word = s:currentQueryObject() + + if (a:hint==0) + let hints = "" + else + let hints = input ("Hints: ") + endif + + let result = s:IdrisCommand(":ps!", cline, word, hints) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + endif +endfunction + +function! IdrisGenerateDef() + let view = winsaveview() + w + let cline = line(".") + let word = s:currentQueryObject() + + let result = s:IdrisCommand(":gd!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + endif +endfunction + +function! IdrisMakeLemma() + let view = winsaveview() + w + let cline = line(".") + let word = s:currentQueryObject() + + let result = s:IdrisCommand(":ml!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + call search(word, "b") + endif +endfunction + +function! IdrisRefine() + let view = winsaveview() + w + let cline = line(".") + let word = expand("") + let name = input ("Name: ") + + let result = s:IdrisCommand(":ref!", cline, word, name) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + endif +endfunction + +function! IdrisAddMissing() + let view = winsaveview() + w + let cline = line(".") + let word = expand("") + + let result = s:IdrisCommand(":am!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + endif +endfunction + +function! IdrisCaseSplit() + w + let view = winsaveview() + let cline = line(".") + let ccol = col(".") + let word = expand("") + let result = s:IdrisCommand(":cs!", cline, ccol, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + endif +endfunction + +function! IdrisMakeWith() + let view = winsaveview() + w + let cline = line(".") + let word = s:currentQueryObject() + let tc = IdrisReload(1) + + let result = s:IdrisCommand(":mw!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + call search("_") + endif +endfunction + +function! IdrisMakeCase() + let view = winsaveview() + w + let cline = line(".") + let word = s:currentQueryObject() + + let result = s:IdrisCommand(":mc!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + call search("_") + endif +endfunction + +function! IdrisAddClause(proof) + let view = winsaveview() + w + let cline = line(".") + let word = expand("") + + if (a:proof==0) + let fn = ":ac!" + else + let fn = ":apc!" + endif + + let result = s:IdrisCommand(fn, cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + call search(word) + + endif +endfunction + +function! IdrisEval() + w + let expr = input ("Expression: ") + let result = s:IdrisCommand(expr) + call IWrite(" = " . result) +endfunction + +nnoremap t :call IdrisShowType() +nnoremap r :call IdrisReload(0) +nnoremap c :call IdrisCaseSplit() +nnoremap a 0:call search(":")b:call IdrisAddClause(0)w +nnoremap d 0:call search(":")b:call IdrisAddClause(0)w +nnoremap b 0:call IdrisAddClause(0) +nnoremap m :call IdrisAddMissing() +nnoremap md 0:call search(":")b:call IdrisAddClause(1)w +nnoremap f :call IdrisRefine() +nnoremap o :call IdrisProofSearch(0) +nnoremap s :call IdrisProofSearch(0) +nnoremap g :call IdrisGenerateDef() +nnoremap p :call IdrisProofSearch(1) +nnoremap l :call IdrisMakeLemma() +nnoremap e :call IdrisEval() +nnoremap w 0:call IdrisMakeWith() +nnoremap mc :call IdrisMakeCase() +nnoremap i 0:call IdrisResponseWin() +nnoremap h :call IdrisShowDoc() + +menu Idris.Reload r +menu Idris.Show\ Type t +menu Idris.Evaluate e +menu Idris.-SEP0- : +menu Idris.Add\ Clause d +menu Idris.Generate\ Definition g +menu Idris.Add\ with w +menu Idris.Case\ Split c +menu Idris.Add\ missing\ cases m +menu Idris.Proof\ Search o +menu Idris.Proof\ Search\ with\ hints p + +au BufHidden idris-response call IdrisHideResponseWin() +au BufEnter idris-response call IdrisShowResponseWin() diff --git a/indent/idris2.vim b/indent/idris2.vim new file mode 100644 index 0000000..ae496f8 --- /dev/null +++ b/indent/idris2.vim @@ -0,0 +1,144 @@ +" indentation for idris (idris-lang.org) +" +" Based on haskell indentation by motemen +" +" author: raichoo (raichoo@googlemail.com) +" +" Modify g:idris_indent_if and g:idris_indent_case to +" change indentation for `if'(default 3) and `case'(default 5). +" Example (in .vimrc): +" > let g:idris_indent_if = 2 + +if exists('b:did_indent') + finish +endif + +let b:did_indent = 1 + +if !exists('g:idris_indent_if') + " if bool + " >>>then ... + " >>>else ... + let g:idris_indent_if = 3 +endif + +if !exists('g:idris_indent_case') + " case xs of + " >>>>>[] => ... + " >>>>>(y::ys) => ... + let g:idris_indent_case = 5 +endif + +if !exists('g:idris_indent_let') + " let x : Nat = O in + " >>>>x + let g:idris_indent_let = 4 +endif + +if !exists('g:idris_indent_rewrite') + " rewrite prf in expr + " >>>>>>>>x + let g:idris_indent_rewrite = 8 +endif + +if !exists('g:idris_indent_where') + " where f : Nat -> Nat + " >>>>>>f x = x + let g:idris_indent_where = 6 +endif + +if !exists('g:idris_indent_do') + " do x <- a + " >>>y <- b + let g:idris_indent_do = 3 +endif + +setlocal indentexpr=GetIdrisIndent() +setlocal indentkeys=!^F,o,O,} + +function! GetIdrisIndent() + let prevline = getline(v:lnum - 1) + + if prevline =~ '\s\+(\s*.\+\s\+:\s\+.\+\s*)\s\+->\s*$' + return match(prevline, '(') + elseif prevline =~ '\s\+{\s*.\+\s\+:\s\+.\+\s*}\s\+->\s*$' + return match(prevline, '{') + endif + + if prevline =~ '[!#$%&*+./<>?@\\^|~-]\s*$' + let s = match(prevline, '[:=]') + if s > 0 + return s + 2 + else + return match(prevline, '\S') + endif + endif + + if prevline =~ '[{([][^})\]]\+$' + return match(prevline, '[{([]') + endif + + if prevline =~ '\\s\+.\+\\s*$' + return match(prevline, '\') + g:idris_indent_let + endif + + if prevline =~ '\\s\+.\+\\s*$' + return match(prevline, '\') + g:idris_indent_rewrite + endif + + if prevline !~ '\' + let s = match(prevline, '\.*\&.*\zs\') + if s > 0 + return s + endif + + let s = match(prevline, '\') + if s > 0 + return s + g:idris_indent_if + endif + endif + + if prevline =~ '\(\\|\\|=\|[{([]\)\s*$' + return match(prevline, '\S') + &shiftwidth + endif + + if prevline =~ '\\s\+\S\+.*$' + return match(prevline, '\') + g:idris_indent_where + endif + + if prevline =~ '\\s\+\S\+.*$' + return match(prevline, '\') + g:idris_indent_do + endif + + if prevline =~ '^\s*\<\(co\)\?data\>\s\+[^=]\+\s\+=\s\+\S\+.*$' + return match(prevline, '=') + endif + + if prevline =~ '\\s\+([^)]*)\s*$' + return match(prevline, '\S') + &shiftwidth + endif + + if prevline =~ '\\s\+.\+\\s*$' + return match(prevline, '\') + g:idris_indent_case + endif + + if prevline =~ '^\s*\(\\|\<\(co\)\?data\>\)\s\+\S\+\s*$' + return match(prevline, '\(\\|\<\(co\)\?data\>\)') + &shiftwidth + endif + + if prevline =~ '^\s*\(\\|\\)\s*([^(]*)\s*$' + return match(prevline, '\(\\|\\)') + &shiftwidth + endif + + if prevline =~ '^\s*\\s*$' + return match(prevline, '\') + &shiftwidth + endif + + let line = getline(v:lnum) + + if (line =~ '^\s*}\s*' && prevline !~ '^\s*;') + return match(prevline, '\S') - &shiftwidth + endif + + return match(prevline, '\S') +endfunction diff --git a/syntax/idris2.vim b/syntax/idris2.vim new file mode 100644 index 0000000..fddf1ea --- /dev/null +++ b/syntax/idris2.vim @@ -0,0 +1,89 @@ +" syntax highlighting for idris (idris-lang.org) +" +" Heavily modified version of the haskell syntax +" highlighter to support idris. +" +" author: raichoo (raichoo@googlemail.com) + +if exists("b:current_syntax") + finish +endif + +syn match idrisTypeDecl "[a-zA-Z][a-zA-z0-9_']*\s\+:\s\+" + \ contains=idrisIdentifier,idrisOperators +syn region idrisParens matchgroup=idrisDelimiter start="(" end=")" contains=TOP,idrisTypeDecl +syn region idrisBrackets matchgroup=idrisDelimiter start="\[" end="]" contains=TOP,idrisTypeDecl +syn region idrisBlock matchgroup=idrisDelimiter start="{" end="}" contains=TOP,idrisTypeDecl +syn keyword idrisModule module namespace +syn keyword idrisImport import +syn keyword idrisRefl refl +syn keyword idrisDeprecated class instance +syn keyword idrisStructure codata data record dsl interface implementation +syn keyword idrisWhere where +syn keyword idrisVisibility public abstract private export +syn keyword idrisBlock parameters mutual postulate using +syn keyword idrisTotality total partial covering +syn keyword idrisImplicit implicit +syn keyword idrisAnnotation auto impossible static constructor +syn keyword idrisStatement do case of rewrite with proof +syn keyword idrisLet let in +syn match idrisSyntax "\(pattern \+\|term \+\)\?syntax" +syn keyword idrisConditional if then else +syn match idrisTactic contained "\<\(intros\?\|rewrite\|exact\|refine\|trivial\|let\|focus\|try\|compute\|solve\|attack\|reflect\|fill\|applyTactic\)\>" +syn match idrisNumber "\<[0-9]\+\>\|\<0[xX][0-9a-fA-F]\+\>\|\<0[oO][0-7]\+\>" +syn match idrisFloat "\<[0-9]\+\.[0-9]\+\([eE][-+]\=[0-9]\+\)\=\>" +syn match idrisDelimiter "[,;]" +syn keyword idrisInfix prefix infix infixl infixr +syn match idrisOperators "\([-!#$%&\*\+./<=>\?@\\^|~:]\|\<_\>\)" +syn match idrisType "\<[A-Z][a-zA-Z0-9_']*\>" +syn keyword idrisTodo TODO FIXME XXX HACK contained +syn match idrisLineComment "---*\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=idrisTodo,@Spell +syn match idrisDocComment "|||\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=idrisTodo,@Spell +syn match idrisMetaVar "?[a-z][A-Za-z0-9_']*" +syn match idrisLink "%\(lib\|link\|include\)" +syn match idrisDirective "%\(access\|assert_total\|default\|elim\|error_reverse\|hide\|name\|reflection\|error_handlers\|language\|flag\|dynamic\|provide\|inline\|used\|no_implicit\|hint\|extern\|unqualified\|error_handler\)" +syn keyword idrisDSL lambda variable index_first index_next +syn match idrisChar "'[^'\\]'\|'\\.'\|'\\u[0-9a-fA-F]\{4}'" +syn match idrisBacktick "`[A-Za-z][A-Za-z0-9_']*`" +syn region idrisString start=+"+ skip=+\\\\\|\\"+ end=+"+ contains=@Spell +syn region idrisBlockComment start="{-" end="-}" contains=idrisBlockComment,idrisTodo,@Spell +syn region idrisProofBlock start="\(default\s\+\)\?\(proof\|tactics\) *{" end="}" contains=idrisTactic +syn match idrisIdentifier "[a-zA-Z][a-zA-z0-9_']*" contained + +highlight def link idrisDeprecated Error +highlight def link idrisIdentifier Identifier +highlight def link idrisImport Structure +highlight def link idrisModule Structure +highlight def link idrisStructure Structure +highlight def link idrisStatement Statement +highlight def link idrisDSL Statement +highlight def link idrisBlock Statement +highlight def link idrisAnnotation Statement +highlight def link idrisWhere Structure +highlight def link idrisLet Structure +highlight def link idrisTotality Statement +highlight def link idrisImplicit Statement +highlight def link idrisSyntax Statement +highlight def link idrisVisibility Statement +highlight def link idrisConditional Conditional +highlight def link idrisProofBlock Macro +highlight def link idrisRefl Macro +highlight def link idrisTactic Identifier +highlight def link idrisLink Statement +highlight def link idrisDirective Statement +highlight def link idrisNumber Number +highlight def link idrisFloat Float +highlight def link idrisDelimiter Delimiter +highlight def link idrisInfix PreProc +highlight def link idrisOperators Operator +highlight def link idrisType Include +highlight def link idrisDocComment Comment +highlight def link idrisLineComment Comment +highlight def link idrisBlockComment Comment +highlight def link idrisTodo Todo +highlight def link idrisMetaVar Macro +highlight def link idrisString String +highlight def link idrisChar String +highlight def link idrisBacktick Operator + +let b:current_syntax = "idris" diff --git a/syntax/lidris.vim b/syntax/lidris.vim new file mode 100644 index 0000000..d662b51 --- /dev/null +++ b/syntax/lidris.vim @@ -0,0 +1,22 @@ +" Vim syntax file +" Language: Literate Idris +" Maintainer: Idris Hackers (https://github.com/idris-hackers/idris-vim) +" Last Change: 2014 Mar 4 +" Version: 0.1 +" +" This is just a minimal adaption of the Literate Haskell syntax file. + + +" Read Idris highlighting. +if version < 600 + syntax include @idrisTop :p:h/idris.vim +else + syntax include @idrisTop syntax/idris.vim +endif + +" Recognize blocks of Bird tracks, highlight as Idris. +syntax region lidrisBirdTrackBlock start="^>" end="\%(^[^>]\)\@=" contains=@idrisTop,lidrisBirdTrack +syntax match lidrisBirdTrack "^>" contained +hi def link lidrisBirdTrack Comment + +let b:current_syntax = "lidris" diff --git a/syntax_checkers/idris/idris2.vim b/syntax_checkers/idris/idris2.vim new file mode 100644 index 0000000..aba3722 --- /dev/null +++ b/syntax_checkers/idris/idris2.vim @@ -0,0 +1,54 @@ +"============================================================================ +"File: idris.vim +"Description: Syntax checking plugin for syntastic.vim +"Maintainer: raichoo +"License: This program is free software. It comes without any warranty, +" to the extent permitted by applicable law. You can redistribute +" it and/or modify it under the terms of the Do What The Fuck You +" Want To Public License, Version 2, as published by Sam Hocevar. +" See http://sam.zoy.org/wtfpl/COPYING for more details. +" +"============================================================================ + +if exists("g:loaded_syntastic_idris_idris_checker") + finish +endif +let g:loaded_syntastic_idris_idris_checker=1 + +function! SyntaxCheckers_idris_idris_IsAvailable() + return executable("idris") +endfunction + +if !exists("g:syntastic_idris_options") + let g:syntastic_idris_options = " " +endif + +function! SyntaxCheckers_idris_idris_GetLocList() dict + let makeprg = self.makeprgBuild({ + \ 'exe': 'idris', + \ 'args': "--client ':l". g:syntastic_idris_options, + \ 'post_args': "'", + \ 'filetype': 'idris', + \ 'subchecker': 'idris' }) + + let errorformat = + \ '"%f" (line %l\, column %c\):,' . + \ 'user error (%f\:%l\:%m\),' . + \ '%E%f:%l:%c: error: %m,' . + \ '%E%f:%l:%c-%*[0-9]: error: %m,' . + \ '%W%f:%l:%c: warning: %m,' . + \ '%W%f:%l:%c-%*[0-9]: warning: %m,' . + \ '%E%f:%l:%c:%m,' . + \ '%E%f:%l:%c-%*[0-9]:%m,' . + \ '%C%m,' . + \ '%m' + + return SyntasticMake({ + \ 'makeprg': makeprg, + \ 'errorformat': errorformat, + \ 'postprocess': ['compressWhitespace'] }) +endfunction + +call g:SyntasticRegistry.CreateAndRegisterChecker({ + \ 'filetype': 'idris', + \ 'name': 'idris'})