Add linter for Idris (#838)

* Add linter for Idris

* Fix parsing warnings and column ranges in Idris linter

* Make Idris linter configurable. Fix help tag.

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/) |

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',
+\})
+

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:

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'

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(''))

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',
+  \ ])