From 63922a1d1ea22c58be758d188068f33491411c0c Mon Sep 17 00:00:00 2001 From: Adam Stankiewicz Date: Mon, 4 Mar 2019 10:14:37 +0100 Subject: Add idris support, closes #265 --- ftplugin/idris.vim | 346 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 346 insertions(+) create mode 100644 ftplugin/idris.vim (limited to 'ftplugin') diff --git a/ftplugin/idris.vim b/ftplugin/idris.vim new file mode 100644 index 00000000..ce18060d --- /dev/null +++ b/ftplugin/idris.vim @@ -0,0 +1,346 @@ +if exists('g:polyglot_disabled') && index(g:polyglot_disabled, 'idris') != -1 + finish +endif + +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)) + return system("idris --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 = s:IdrisCommand(":l", file) + if (! (tc is "")) + call IWrite(tc) + else + if (a:q==0) + echo "Successfully reloaded " . file + call IWrite("") + 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 tc = IdrisReloadToLine(cline) + if (! (tc is "")) + echo tc + else + let ty = s:IdrisCommand(":t", word) + call IWrite(ty) + endif + return tc +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() + let tc = IdrisReload(1) + + if (a:hint==0) + let hints = "" + else + let hints = input ("Hints: ") + endif + + if (tc is "") + let result = s:IdrisCommand(":ps!", cline, word, hints) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + endif + endif +endfunction + +function! IdrisMakeLemma() + let view = winsaveview() + w + let cline = line(".") + let word = s:currentQueryObject() + let tc = IdrisReload(1) + + if (tc is "") + let result = s:IdrisCommand(":ml!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + call search(word, "b") + endif + endif +endfunction + +function! IdrisRefine() + let view = winsaveview() + w + let cline = line(".") + let word = expand("") + let tc = IdrisReload(1) + + let name = input ("Name: ") + + if (tc is "") + let result = s:IdrisCommand(":ref!", cline, word, name) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + endif + endif +endfunction + +function! IdrisAddMissing() + let view = winsaveview() + w + let cline = line(".") + let word = expand("") + let tc = IdrisReload(1) + + if (tc is "") + let result = s:IdrisCommand(":am!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + endif + endif +endfunction + +function! IdrisCaseSplit() + let view = winsaveview() + let cline = line(".") + let word = expand("") + let tc = IdrisReloadToLine(cline) + + if (tc is "") + let result = s:IdrisCommand(":cs!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + endif + endif +endfunction + +function! IdrisMakeWith() + let view = winsaveview() + w + let cline = line(".") + let word = s:currentQueryObject() + let tc = IdrisReload(1) + + if (tc is "") + let result = s:IdrisCommand(":mw!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + call search("_") + endif + endif +endfunction + +function! IdrisMakeCase() + let view = winsaveview() + w + let cline = line(".") + let word = s:currentQueryObject() + let tc = IdrisReload(1) + + if (tc is "") + let result = s:IdrisCommand(":mc!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + call search("_") + endif + endif +endfunction + +function! IdrisAddClause(proof) + let view = winsaveview() + w + let cline = line(".") + let word = expand("") + let tc = IdrisReloadToLine(cline) + + if (tc is "") + 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 + endif +endfunction + +function! IdrisEval() + w + let tc = IdrisReload(1) + if (tc is "") + let expr = input ("Expression: ") + let result = s:IdrisCommand(expr) + call IWrite(" = " . result) + endif +endfunction + +nnoremap t :call IdrisShowType() +nnoremap r :call IdrisReload(0) +nnoremap c :call IdrisCaseSplit() +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 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.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() -- cgit v1.2.3