Edwin Brady
commit
e3816a7be5
|
|
@ -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][].
|
||||
|
||||
|
||||
|
||||
## 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.
|
||||
|
||||
`<LocalLeader>r` reload file
|
||||
|
||||
`<LocalLeader>t` show type
|
||||
|
||||
`<LocalLeader>d` Create an initial clause for a type declaration.
|
||||
|
||||
`<LocalLeader>b` Same as \d but for an initial typeclass method impl.
|
||||
|
||||
`<LocalLeader>md` Same as \d but for a proof clause
|
||||
|
||||
`<LocalLeader>c` case split
|
||||
|
||||
`<LocalLeader>mc` make case
|
||||
|
||||
`<LocalLeader>w` add with clause
|
||||
|
||||
`<LocalLeader>e` evaluate expression
|
||||
|
||||
`<LocalLeader>l` make lemma
|
||||
|
||||
`<LocalLeader>m` add missing clause
|
||||
|
||||
`<LocalLeader>f` refine item
|
||||
|
||||
`<LocalLeader>o` obvious proof search
|
||||
|
||||
`<LocalLeader>p` proof search
|
||||
|
||||
`<LocalLeader>i` open idris response window
|
||||
|
||||
`<LocalLeader>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/
|
||||
|
||||
|
|
@ -0,0 +1 @@
|
|||
setlocal iskeyword+='
|
||||
|
|
@ -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 "\<sum\>" conceal cchar=∑
|
||||
syntax match idrNiceOperator "\<product\>" conceal cchar=∏
|
||||
syntax match idrNiceOperator "\<sqrt\>" conceal cchar=√
|
||||
syntax match idrNiceOperator "\<pi\>" 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
|
||||
|
||||
|
|
@ -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 '<LocalLeader>_h' by default.
|
||||
|
||||
IdrisResponseWin *IdrisResponseWin*
|
||||
This opens an idris response window in a new pane.
|
||||
|
||||
Mapped to '<LocalLeader>_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 '<LocalLeader>_t' by default.
|
||||
|
||||
IdrisReload *IdrisReload*
|
||||
This reloads the file and type-checks the file in the current buffer.
|
||||
|
||||
Mapped to '<LocalLeader>_r' by default.
|
||||
|
||||
IdrisEval *IdrisEval*
|
||||
This prompts for an expression and then evaluates it in the REPL, then
|
||||
returns the result.
|
||||
|
||||
Mapped to '<LocalLeader>_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 '<LocalLeader>_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 '<LocalLeader>_d' for an ordinary top-level definition,
|
||||
'<LocalLeader>_b' for a typeclass instance definition, and
|
||||
'<LocalLeader>_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 '<LocalLeader>_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 '<LocalLeader>_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 '<LocalLeader>_o' without hints and '<LocalLeader>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 '<LocalLeader>_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 '<LocalLeader>_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:
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
au BufNewFile,BufRead *.idr setf idris2
|
||||
au BufNewFile,BufRead idris-response setf idris2
|
||||
|
|
@ -0,0 +1 @@
|
|||
au BufNewFile,BufRead *.lidr setf lidris
|
||||
|
|
@ -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(<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))
|
||||
" 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("<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 = expand("<cword>")
|
||||
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("<cword>")
|
||||
|
||||
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("<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(proof)
|
||||
let view = winsaveview()
|
||||
w
|
||||
let cline = line(".")
|
||||
let word = expand("<cword>")
|
||||
|
||||
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 <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>a 0:call search(":")<ENTER>b:call IdrisAddClause(0)<ENTER>w
|
||||
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>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>d
|
||||
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>o
|
||||
menu Idris.Proof\ Search\ with\ hints <LocalLeader>p
|
||||
|
||||
au BufHidden idris-response call IdrisHideResponseWin()
|
||||
au BufEnter idris-response call IdrisShowResponseWin()
|
||||
|
|
@ -0,0 +1,144 @@
|
|||
" indentation for idris (idris-lang.org)
|
||||
"
|
||||
" Based on haskell indentation by motemen <motemen@gmail.com>
|
||||
"
|
||||
" 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 =~ '\<let\>\s\+.\+\<in\>\s*$'
|
||||
return match(prevline, '\<let\>') + g:idris_indent_let
|
||||
endif
|
||||
|
||||
if prevline =~ '\<rewrite\>\s\+.\+\<in\>\s*$'
|
||||
return match(prevline, '\<rewrite\>') + g:idris_indent_rewrite
|
||||
endif
|
||||
|
||||
if prevline !~ '\<else\>'
|
||||
let s = match(prevline, '\<if\>.*\&.*\zs\<then\>')
|
||||
if s > 0
|
||||
return s
|
||||
endif
|
||||
|
||||
let s = match(prevline, '\<if\>')
|
||||
if s > 0
|
||||
return s + g:idris_indent_if
|
||||
endif
|
||||
endif
|
||||
|
||||
if prevline =~ '\(\<where\>\|\<do\>\|=\|[{([]\)\s*$'
|
||||
return match(prevline, '\S') + &shiftwidth
|
||||
endif
|
||||
|
||||
if prevline =~ '\<where\>\s\+\S\+.*$'
|
||||
return match(prevline, '\<where\>') + g:idris_indent_where
|
||||
endif
|
||||
|
||||
if prevline =~ '\<do\>\s\+\S\+.*$'
|
||||
return match(prevline, '\<do\>') + g:idris_indent_do
|
||||
endif
|
||||
|
||||
if prevline =~ '^\s*\<\(co\)\?data\>\s\+[^=]\+\s\+=\s\+\S\+.*$'
|
||||
return match(prevline, '=')
|
||||
endif
|
||||
|
||||
if prevline =~ '\<with\>\s\+([^)]*)\s*$'
|
||||
return match(prevline, '\S') + &shiftwidth
|
||||
endif
|
||||
|
||||
if prevline =~ '\<case\>\s\+.\+\<of\>\s*$'
|
||||
return match(prevline, '\<case\>') + g:idris_indent_case
|
||||
endif
|
||||
|
||||
if prevline =~ '^\s*\(\<namespace\>\|\<\(co\)\?data\>\)\s\+\S\+\s*$'
|
||||
return match(prevline, '\(\<namespace\>\|\<\(co\)\?data\>\)') + &shiftwidth
|
||||
endif
|
||||
|
||||
if prevline =~ '^\s*\(\<using\>\|\<parameters\>\)\s*([^(]*)\s*$'
|
||||
return match(prevline, '\(\<using\>\|\<parameters\>\)') + &shiftwidth
|
||||
endif
|
||||
|
||||
if prevline =~ '^\s*\<mutual\>\s*$'
|
||||
return match(prevline, '\<mutual\>') + &shiftwidth
|
||||
endif
|
||||
|
||||
let line = getline(v:lnum)
|
||||
|
||||
if (line =~ '^\s*}\s*' && prevline !~ '^\s*;')
|
||||
return match(prevline, '\S') - &shiftwidth
|
||||
endif
|
||||
|
||||
return match(prevline, '\S')
|
||||
endfunction
|
||||
|
|
@ -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"
|
||||
|
|
@ -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 <sfile>: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"
|
||||
|
|
@ -0,0 +1,54 @@
|
|||
"============================================================================
|
||||
"File: idris.vim
|
||||
"Description: Syntax checking plugin for syntastic.vim
|
||||
"Maintainer: raichoo <raichoo at googlemail dot com>
|
||||
"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'})
|
||||
Loading…
Reference in New Issue