idris2-vim/ftplugin/idris2.vim

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(<cword>)` to accomodate differences between
" a (n)vim word and what Idris requires.
function! s:currentQueryObject()
  let word = expand("<cword>")
  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"
    setlocal buftype=nofile bufhidden=hide noswapfile
    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)
  let view = winsaveview()
  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
  call winrestview(view)
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)
  elseif (a:q==0)
    call IWrite("Successfully reloaded " . file)
  endif
  return tc
endfunction

function! IdrisShowType(imp)
  w
  let word = s:currentQueryObject()
  let cline = line(".")
  let ccol = col(".")
  let ty = s:IdrisCommand(a:imp ? ":ti" : ":t", word)
  call IWrite(ty)
endfunction

function! IdrisShowDoc()
  w
  let word = expand("<cword>")
  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 = s:currentQueryObject()
  let name = input ("Name: ")

  let result = s:IdrisCommand(":refine!", cline, word, name)
  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("<cword>")
  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()
  let view = winsaveview()
  w
  let cline = line(".")
  let word = expand("<cword>")

  let result = s:IdrisCommand(":ac!", 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 <buffer> <silent> <LocalLeader>t :call IdrisShowType(0)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>T :call IdrisShowType(1)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>r :call IdrisReload(0)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>c :call IdrisCaseSplit()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>a 0:call search(":")<ENTER>b:call IdrisAddClause()<ENTER>w
nnoremap <buffer> <silent> <LocalLeader>f :call IdrisRefine()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>o :call IdrisProofSearch(0)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>s :call IdrisProofSearch(0)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>g :call IdrisGenerateDef()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>p :call IdrisProofSearch(1)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>l :call IdrisMakeLemma()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>e :call IdrisEval()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>w 0:call IdrisMakeWith()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>mc :call IdrisMakeCase()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>i 0:call IdrisResponseWin()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>h :call IdrisShowDoc()<ENTER>

menu Idris.Reload <LocalLeader>r
menu Idris.Show\ Type <LocalLeader>t
menu Idris.Evaluate <LocalLeader>e
menu Idris.-SEP0- :
menu Idris.Add\ Clause <LocalLeader>a
menu Idris.Generate\ Definition <LocalLeader>g
menu Idris.Add\ with <LocalLeader>w
menu Idris.Case\ Split <LocalLeader>c
menu Idris.Add\ missing\ cases <LocalLeader>m
menu Idris.Proof\ Search <LocalLeader>s
menu Idris.Proof\ Search\ with\ hints <LocalLeader>p

au BufHidden idris-response call IdrisHideResponseWin()
au BufEnter idris-response call IdrisShowResponseWin()