path: root/ftplugin/idris.vim

let s:base = expand("<sfile>:h:h")
let Filter = { _, v -> stridx(v, s:base) == -1 && stridx(v, $VIMRUNTIME) == -1 && v !~ "after" }
let files = filter(globpath(&rtp, 'ftplugin/idris.vim', 1, 1), Filter)
if len(files) > 0
  exec 'source ' . files[0]
  finish
endif
if !exists('g:polyglot_disabled') || index(g:polyglot_disabled, 'idris') == -1

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))
  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("<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()
  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("<cword>")
  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("<cword>")
  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("<cword>")
  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("<cword>")
  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 <buffer> <silent> <LocalLeader>t :call IdrisShowType()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>r :call IdrisReload(0)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>c :call IdrisCaseSplit()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>d 0:call search(":")<ENTER>b:call IdrisAddClause(0)<ENTER>w
nnoremap <buffer> <silent> <LocalLeader>b 0:call IdrisAddClause(0)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>m :call IdrisAddMissing()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>md 0:call search(":")<ENTER>b:call IdrisAddClause(1)<ENTER>w
nnoremap <buffer> <silent> <LocalLeader>f :call IdrisRefine()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>o :call IdrisProofSearch(0)<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>d
menu Idris.Add\ with <LocalLeader>w
menu Idris.Case\ Split <LocalLeader>c
menu Idris.Add\ missing\ cases <LocalLeader>m
menu Idris.Proof\ Search <LocalLeader>o
menu Idris.Proof\ Search\ with\ hints <LocalLeader>p

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

endif