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.

2 files changed, 94 insertions, 0 deletions

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