diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..2095d5d --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/doc/ diff --git a/autoload/idris2.vim b/autoload/idris2.vim new file mode 100644 index 0000000..2a53e7b --- /dev/null +++ b/autoload/idris2.vim @@ -0,0 +1,293 @@ +" 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)) + " Vim does not support ANSI escape codes natively, so we need to disable + " automatic colouring + return system("idris2 --no-color --find-ipkg " . shellescape(expand('%:p')) . " --client " . idriscmd) +endfunction + +function! idris2#docFold(lineNum) + let line = getline(a:lineNum) + + if line =~ "^\s*|||" + return "1" + endif + + return "0" +endfunction + +function! idris2#fold(lineNum) + return idris2#docFold(a:lineNum) +endfunction + +setlocal foldmethod=expr +setlocal foldexpr=idris2#fold(v:lnum) + +" creates a response window (if doesn't exist) and its scratch buffer (if +" doesn't exist) +function! idris2#responseWin() + if (!bufexists("idris-response")) + botright 10new idris-response + setlocal bufhidden=hide buftype=nofile nobuflisted noswapfile + let g:idris_respwin = "active" + wincmd p + elseif (bufexists("idris-response") && g:idris_respwin == "hidden") + botright 10new + keepjumps buffer idris-response + let g:idris_respwin = "active" + wincmd p + endif +endfunction + +function! idris2#onHideResponseWin() + let g:idris_respwin = "hidden" +endfunction + +function! idris2#write(str) + let bufname = "idris-response" + if (bufexists(bufname)) + let nr = bufwinnr(bufname) + let origin_nr = bufwinnr("%") + let save_cursor = getcurpos() + + if nr != -1 + " go to open window of response buffer if it exists + exec "keepjumps " . nr . "wincmd w" + else + " open buffer in current window. This assumes the current buffer is not + " modified + keepjumps buffer idris-response + endif + + " set buffer text to argument + keepjumps %delete + let resp = split(a:str, '\n') + call append(1, resp) + + " return to previous file + if nr != -1 + exec "keepjumps " . origin_nr . "wincmd w" + else + keepjumps buffer # + call setpos('.', save_cursor) + endif + + else + " if buffer does not exist, just echo the output + echo a:str + endif +endfunction + +function! idris2#reload(q) + write + let file = expand('%:p') + let tc = system("idris2 --no-color --find-ipkg " . shellescape(file) . " --client ''") + if (! (tc is "")) + call idris2#write(tc) + else + if (a:q==0) + call idris2#write("Successfully reloaded " . file) + endif + endif + return tc +endfunction + +function! idris2#reloadToLine(cline) + return idris2#reload(1) + "write + "let file = expand("%:p") + "let tc = s:idrisCommand(":lto", a:cline, file) + "if (! (tc is "")) + " call idris2#write(tc) + "endif + "return tc +endfunction + +function! idris2#showType() + write + let word = s:currentQueryObject() + let cline = line(".") + let ccol = col(".") + let ty = s:idrisCommand(":t", word) + call idris2#write(ty) +endfunction + +function! idris2#showDoc() + write + let word = expand("") + let ty = s:idrisCommand(":doc", word) + call idris2#write(ty) +endfunction + +function! idris2#proofSearch(hint) + let view = winsaveview() + write + 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 idris2#write(result) + else + e + call winrestview(view) + endif +endfunction + +function! idris2#generateDef() + let view = winsaveview() + write + let cline = line(".") + let word = s:currentQueryObject() + + let result = s:idrisCommand(":gd!", cline, word) + if (! (result is "")) + call idris2#write(result) + else + e + call winrestview(view) + endif +endfunction + +function! idris2#makeLemma() + let view = winsaveview() + write + let cline = line(".") + let word = s:currentQueryObject() + + let result = s:idrisCommand(":ml!", cline, word) + if (! (result is "")) + call idris2#write(result) + else + e + call winrestview(view) + call search(word, "b") + endif +endfunction + +function! idris2#refine() + let view = winsaveview() + write + let cline = line(".") + let word = expand("") + let name = input ("Name: ") + + let result = s:idrisCommand(":ref!", cline, word, name) + if (! (result is "")) + call idris2#write(result) + else + e + call winrestview(view) + endif +endfunction + +function! idris2#addMissing() + let view = winsaveview() + write + let cline = line(".") + let word = expand("") + + let result = s:idrisCommand(":am!", cline, word) + if (! (result is "")) + call idris2#write(result) + else + e + call winrestview(view) + endif +endfunction + +function! idris2#caseSplit() + write + let view = winsaveview() + let cline = line(".") + let ccol = col(".") + let word = expand("") + let result = s:idrisCommand(":cs!", cline, ccol, word) + if (! (result is "")) + call idris2#write(result) + else + e + call winrestview(view) + endif +endfunction + +function! idris2#makeWith() + let view = winsaveview() + write + let cline = line(".") + let word = s:currentQueryObject() + let tc = idris2#reload(1) + + let result = s:idrisCommand(":mw!", cline, word) + if (! (result is "")) + call idris2#write(result) + else + e + call winrestview(view) + call search("_") + endif +endfunction + +function! idris2#makeCase() + let view = winsaveview() + write + let cline = line(".") + let word = s:currentQueryObject() + + let result = s:idrisCommand(":mc!", cline, word) + if (! (result is "")) + call idris2#write(result) + else + e + call winrestview(view) + call search("_") + endif +endfunction + +function! idris2#addClause(proof) + let view = winsaveview() + write + 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 idris2#write(result) + else + e + call winrestview(view) + call search(word) + + endif +endfunction + +function! idris2#eval() + write + let expr = input ("Expression: ") + let result = s:idrisCommand(expr) + call idris2#write(" = " . result) +endfunction + diff --git a/autoload/idris2/indent.vim b/autoload/idris2/indent.vim new file mode 100644 index 0000000..a33a57e --- /dev/null +++ b/autoload/idris2/indent.vim @@ -0,0 +1,87 @@ +function! idris2#indent#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/ftplugin/idris2.vim b/ftplugin/idris2.vim index 4ef20e5..92f3c67 100644 --- a/ftplugin/idris2.vim +++ b/ftplugin/idris2.vim @@ -1,7 +1,3 @@ -if bufname('%') == "idris-response" - finish -endif - if exists("b:did_ftplugin") finish endif @@ -11,309 +7,34 @@ 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 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)) - " Vim does not support ANSI escape codes natively, so we need to disable - " automatic colouring - return system("idris2 --no-color --find-ipkg " . shellescape(expand('%:p')) . " --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 --no-color --find-ipkg " . shellescape(file) . " --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() +nnoremap t :call idris2#showType() +nnoremap r :call idris2#reload(0) +nnoremap c :call idris2#caseSplit() +nnoremap a 0:call search(":")b:call idris2#addClause(0)w +nnoremap d 0:call search(":")b:call idris2#addClause(0)w +nnoremap b 0:call idris2#addClause(0) +nnoremap m :call idris2#addMissing() +nnoremap md 0:call search(":")b:call idris2#addClause(1)w +nnoremap f :call idris2#refine() +nnoremap o :call idris2#proofSearch(0) +nnoremap s :call idris2#proofSearch(0) +nnoremap g :call idris2#generateDef() +nnoremap p :call idris2#proofSearch(1) +nnoremap l :call idris2#makeLemma() +nnoremap e :call idris2#eval() +nnoremap w 0:call idris2#makeWith() +nnoremap mc :call idris2#makeCase() +nnoremap i 0:call idris2#responseWin() +nnoremap h :call idris2#showDoc() menu Idris.Reload r menu Idris.Show\ Type t @@ -327,5 +48,7 @@ menu Idris.Add\ missing\ cases m menu Idris.Proof\ Search s menu Idris.Proof\ Search\ with\ hints p -au BufHidden idris-response call IdrisHideResponseWin() -au BufEnter idris-response call IdrisShowResponseWin() +augroup idris_responsewin + autocmd! + au BufHidden idris-response call idris2#onHideResponseWin() +augroup end diff --git a/indent/idris2.vim b/indent/idris2.vim index ae496f8..f14a5e2 100644 --- a/indent/idris2.vim +++ b/indent/idris2.vim @@ -53,92 +53,5 @@ if !exists('g:idris_indent_do') let g:idris_indent_do = 3 endif -setlocal indentexpr=GetIdrisIndent() +setlocal indentexpr=idris2#indent#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