summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--README.md1
-rw-r--r--ale_linters/idris/idris.vim87
-rw-r--r--doc/ale-idris.txt23
-rw-r--r--doc/ale.txt3
-rw-r--r--test/command_callback/test_idris_command_callbacks.vader42
-rw-r--r--test/handler/test_idris_handler.vader52
6 files changed, 208 insertions, 0 deletions
diff --git a/README.md b/README.md
index 5d2e7983..305430d8 100644
--- a/README.md
+++ b/README.md
@@ -84,6 +84,7 @@ name. That seems to be the fairest way to arrange this table.
| Handlebars | [ember-template-lint](https://github.com/rwjblue/ember-template-lint) |
| Haskell | [ghc](https://www.haskell.org/ghc/), [stack-ghc](https://haskellstack.org/), [stack-build](https://haskellstack.org/), [ghc-mod](https://github.com/DanielG/ghc-mod), [stack-ghc-mod](https://github.com/DanielG/ghc-mod), [hlint](https://hackage.haskell.org/package/hlint), [hdevtools](https://hackage.haskell.org/package/hdevtools) |
| HTML | [HTMLHint](http://htmlhint.com/), [proselint](http://proselint.com/), [tidy](http://www.html-tidy.org/) |
+| Idris | [idris](http://www.idris-lang.org/) |
| Java | [checkstyle](http://checkstyle.sourceforge.net), [javac](http://www.oracle.com/technetwork/java/javase/downloads/index.html) |
| JavaScript | [eslint](http://eslint.org/), [jscs](http://jscs.info/), [jshint](http://jshint.com/), [flow](https://flowtype.org/), [standard](http://standardjs.com/), [prettier](https://github.com/prettier/prettier) (and `prettier-eslint`, `prettier-standard`), [xo](https://github.com/sindresorhus/xo)
| JSON | [jsonlint](http://zaa.ch/jsonlint/) |
diff --git a/ale_linters/idris/idris.vim b/ale_linters/idris/idris.vim
new file mode 100644
index 00000000..115d04fc
--- /dev/null
+++ b/ale_linters/idris/idris.vim
@@ -0,0 +1,87 @@
+" Author: Scott Bonds <scott@ggr.com>
+" Description: default Idris compiler
+
+call ale#Set('idris_idris_executable', 'idris')
+call ale#Set('idris_idris_options', '--total --warnpartial --warnreach --warnipkg')
+
+function! ale_linters#idris#idris#GetExecutable(buffer) abort
+ return ale#Var(a:buffer, 'idris_idris_executable')
+endfunction
+
+function! ale_linters#idris#idris#GetCommand(buffer) abort
+ let l:options = ale#Var(a:buffer, 'idris_idris_options')
+
+ return ale#Escape(ale_linters#idris#idris#GetExecutable(a:buffer))
+ \ . (!empty(l:options) ? ' ' . l:options : '')
+ \ . ' --check %s'
+endfunction
+
+function! ale_linters#idris#idris#Handle(buffer, lines) abort
+ " This was copied almost verbatim from ale#handlers#haskell#HandleGHCFormat
+
+ " Look for lines like the following:
+ " foo.idr:2:6:When checking right hand side of main with expected type
+ " bar.idr:11:11-13:
+ let l:pattern = '\v^([a-zA-Z]?:?[^:]+):(\d+):(\d+)(-\d+)?:(.*)?$'
+ let l:output = []
+
+ let l:corrected_lines = []
+
+ for l:line in a:lines
+ if len(matchlist(l:line, l:pattern)) > 0
+ call add(l:corrected_lines, l:line)
+ elseif len(l:corrected_lines) > 0
+ if l:line is# ''
+ let l:corrected_lines[-1] .= ' ' " turn a blank line into a space
+ else
+ let l:corrected_lines[-1] .= l:line
+ endif
+ let l:corrected_lines[-1] = substitute(l:corrected_lines[-1], '\s\+', ' ', 'g')
+ endif
+ endfor
+
+ for l:line in l:corrected_lines
+ let l:match = matchlist(l:line, l:pattern)
+
+ if len(l:match) == 0
+ continue
+ endif
+
+ if !ale#path#IsBufferPath(a:buffer, l:match[1])
+ continue
+ endif
+
+ let l:errors = matchlist(l:match[5], '\v([wW]arning|[eE]rror) - ?(.*)')
+
+ if len(l:errors) > 0
+ let l:ghc_type = l:errors[1]
+ let l:text = l:errors[2]
+ else
+ let l:ghc_type = ''
+ let l:text = l:match[5][:0] is# ' ' ? l:match[5][1:] : l:match[5]
+ endif
+
+ if l:ghc_type is? 'Warning'
+ let l:type = 'W'
+ else
+ let l:type = 'E'
+ endif
+
+ call add(l:output, {
+ \ 'lnum': l:match[2] + 0,
+ \ 'col': l:match[3] + 0,
+ \ 'text': l:text,
+ \ 'type': l:type,
+ \})
+ endfor
+
+ return l:output
+endfunction
+
+call ale#linter#Define('idris', {
+\ 'name': 'idris',
+\ 'executable_callback': 'ale_linters#idris#idris#GetExecutable',
+\ 'command_callback': 'ale_linters#idris#idris#GetCommand',
+\ 'callback': 'ale_linters#idris#idris#Handle',
+\})
+
diff --git a/doc/ale-idris.txt b/doc/ale-idris.txt
new file mode 100644
index 00000000..c7500b0d
--- /dev/null
+++ b/doc/ale-idris.txt
@@ -0,0 +1,23 @@
+===============================================================================
+ALE Idris Integration *ale-idris-options*
+
+===============================================================================
+idris *ale-idris-idris*
+
+g:ale_idris_idris_executable *g:ale_idris_idris_executable*
+ *b:ale_idris_idris_executable*
+ Type: |String|
+ Default: `'idris'`
+
+ This variable can be changed to change the path to idris.
+
+
+g:ale_idris_idris_options *g:ale_idris_idris_options*
+ *b:ale_idris_idris_options*
+ Type: |String|
+ Default: `'--total --warnpartial --warnreach --warnipkg'`
+
+ This variable can be changed to modify flags given to idris.
+
+===============================================================================
+ vim:tw=78:ts=2:sts=2:sw=2:ft=help:norl:
diff --git a/doc/ale.txt b/doc/ale.txt
index 869a5576..eb31b829 100644
--- a/doc/ale.txt
+++ b/doc/ale.txt
@@ -49,6 +49,8 @@ CONTENTS *ale-contents*
html..................................|ale-html-options|
htmlhint............................|ale-html-htmlhint|
tidy................................|ale-html-tidy|
+ idris.................................|ale-idris-options|
+ idris...............................|ale-idris-idris|
java..................................|ale-java-options|
checkstyle..........................|ale-java-checkstyle|
javac...............................|ale-java-javac|
@@ -191,6 +193,7 @@ The following languages and tools are supported.
* Handlebars: 'ember-template-lint'
* Haskell: 'ghc', 'stack-ghc', 'stack-build', 'ghc-mod', 'stack-ghc-mod', 'hlint', 'hdevtools'
* HTML: 'HTMLHint', 'proselint', 'tidy'
+* Idris: 'idris'
* Java: 'javac'
* JavaScript: 'eslint', 'jscs', 'jshint', 'flow', 'prettier', 'prettier-eslint', 'xo'
* JSON: 'jsonlint'
diff --git a/test/command_callback/test_idris_command_callbacks.vader b/test/command_callback/test_idris_command_callbacks.vader
new file mode 100644
index 00000000..03a69f39
--- /dev/null
+++ b/test/command_callback/test_idris_command_callbacks.vader
@@ -0,0 +1,42 @@
+Before:
+ Save g:ale_idris_idris_executable
+ Save g:ale_idris_idris_options
+
+ unlet! g:ale_idris_idris_executable
+ unlet! b:ale_idris_idris_executable
+ unlet! g:ale_idris_idris_options
+ unlet! b:ale_idris_idris_options
+
+ runtime ale_linters/idris/idris.vim
+
+After:
+ Restore
+ unlet! b:command_tail
+ unlet! b:ale_idris_idris_executable
+ unlet! b:ale_idris_idris_options
+ call ale#linter#Reset()
+
+Execute(The executable should be configurable):
+ AssertEqual 'idris', ale_linters#idris#idris#GetExecutable(bufnr(''))
+
+ let b:ale_idris_idris_executable = 'foobar'
+
+ AssertEqual 'foobar', ale_linters#idris#idris#GetExecutable(bufnr(''))
+
+Execute(The executable should be used in the command):
+ AssertEqual
+ \ ale#Escape('idris') . ' --total --warnpartial --warnreach --warnipkg --check %s',
+ \ ale_linters#idris#idris#GetCommand(bufnr(''))
+
+ let b:ale_idris_idris_executable = 'foobar'
+
+ AssertEqual
+ \ ale#Escape('foobar') . ' --total --warnpartial --warnreach --warnipkg --check %s',
+ \ ale_linters#idris#idris#GetCommand(bufnr(''))
+
+Execute(The options should be configurable):
+ let b:ale_idris_idris_options = '--something'
+
+ AssertEqual
+ \ ale#Escape('idris') . ' --something --check %s',
+ \ ale_linters#idris#idris#GetCommand(bufnr(''))
diff --git a/test/handler/test_idris_handler.vader b/test/handler/test_idris_handler.vader
new file mode 100644
index 00000000..1c20be7b
--- /dev/null
+++ b/test/handler/test_idris_handler.vader
@@ -0,0 +1,52 @@
+Before:
+ runtime ale_linters/idris/idris.vim
+
+Execute(The idris handler should parse messages that reference a single column):
+ call ale#test#SetFilename('/tmp/foo.idr')
+
+ AssertEqual
+ \ [
+ \ {
+ \ 'lnum': 4,
+ \ 'col': 5,
+ \ 'type': 'E',
+ \ 'text': 'When checking right hand side of main with expected type IO () When checking an application of function Prelude.Monad.>>=: Type mismatch between IO () (Type of putStrLn _) and _ -> _ (Is putStrLn _ applied to too many arguments?) Specifically: Type mismatch between IO and \uv => _ -> uv'
+ \ }
+ \ ],
+ \ ale_linters#idris#idris#Handle(bufnr(''), [
+ \ '/tmp/foo.idr:4:5:',
+ \ 'When checking right hand side of main with expected type',
+ \ ' IO ()',
+ \ '',
+ \ 'When checking an application of function Prelude.Monad.>>=:',
+ \ ' Type mismatch between',
+ \ ' IO () (Type of putStrLn _)',
+ \ ' and',
+ \ ' _ -> _ (Is putStrLn _ applied to too many arguments?)',
+ \ '',
+ \ ' Specifically:',
+ \ ' Type mismatch between',
+ \ ' IO',
+ \ ' and',
+ \ ' \uv => _ -> uv',
+ \ ])
+
+Execute(The idris handler should parse messages that reference a column range):
+ call ale#test#SetFilename('/tmp/foo.idr')
+
+ AssertEqual
+ \ [
+ \ {
+ \ 'lnum': 11,
+ \ 'col': 11,
+ \ 'type': 'E',
+ \ 'text': 'When checking right hand side of Main.case block in main at /tmp/foo.idr:10:10 with expected type IO () Last statement in do block must be an expression'
+ \ }
+ \ ],
+ \ ale_linters#idris#idris#Handle(bufnr(''), [
+ \ '/tmp/foo.idr:11:11-13:',
+ \ 'When checking right hand side of Main.case block in main at /tmp/foo.idr:10:10 with expected type',
+ \ ' IO ()',
+ \ '',
+ \ 'Last statement in do block must be an expression',
+ \ ])