Idris2 & Vim channels & Vim plugin development

This time, lets look into Vim channels. The channel.txt -documentation is superb and I would really have no need to write this. You might be interested in knowing what kind of a task it is though. Going through implementing something for Vim.

Easiest way to start with this is to run the demoserver.py script that you find from $VIMRUNTIME/tools. Then do this:

let channel = ch_open('localhost:8765')
echo ch_evalexpr(channel, 'hello!')

To run this write that script into a Vim buffer, then VISUAL-yank it and type :@*.

The terminal where you've opened the demoserver.py should show you the following or similar, depending on what you wrote to evalexpr.

received: [1,"hello"]

sending [1, "what?"]
received: [2,"hello"]

sending [2, "what?"]
received: [3,"hello!"]

sending [3, "got it"]

So it does what we want it to do. Lets check inside the script and see if we can make something out of it. Inside the read-handler there's a putrid surprise left for the reader:

try:
    data = self.request.recv(4096).decode('utf-8')
except socket.error:
    print("=== socket error ===")
    break
except IOError:
    print("=== socket closed ===")
    break
if data == '':
    print("=== socket closed ===")
    break
try:
    decoded = json.loads(data)
except ValueError:
    print("json decoding failed")
    decoded = [-1, '']

Eww. It's reading a fixed-size message from Vim, discards the rest of it and then stumbles on the truncated part on the subsequent reads.

It takes at least 20 lines to write a quirky fix and 2000 lines to provide a proper fix somebody ought have already provided into the standard libraries because json protocols are popular these days.

I was thinking of writing an Idris IDE-protocol driver in Python. Yeah no, lets leave Python3 aside and do things in vimscript.

Btw. There's a nice online book that teaches you vimscript. I've read this at least once and I read parts of it again while writing this.

Protocol we implement

The Idris IDE protocol messages start with 6-character hexadecimal number that communicates how long the message packet is. It's good to start by finding out how to translate the hexadecimal header.

It appears to be easy as there are methods for hexadecimal conversion.

echo str2nr('023029', 16)
echo printf('%06x', 2341)

And it's also straightforward to get the length of a string.

echo strlen("foo")

Next lets try start Idris2 through Vim.

let w:output = ""
func! IdrisHandle(channel, msg)
  let w:output = (w:output . a:msg)
endfunc

let job = job_start("idris2 --ide-mode", {"mode":"raw", "callback":"IdrisHandle"})
let w:channel = job_getchannel(job)
let output = ch_readraw(channel)

call ch_close(channel)
call job_stop(job)

The :echo output should show:

000018(:protocol-version 2 0)

An another useful command is put =output if you want to write the results of a variable to examine it for a longer while.

Now we have to decode and encode the first layer of these messages.

func! Read6HexMessage()
    while strlen(w:output) < 6
        let data = ch_readraw(w:channel, {"timeout":2000})
        let w:output = w:output . data
        if strlen(data) == 0
            return ""
        endif
    endwhile
    let kount = str2nr(strpart(w:output, 0, 6), 16)
    while strlen(w:output) < kount + 6
        let data = ch_readraw(w:channel, {"timeout":2000})
        let w:output = w:output . data
        if strlen(data) == 0
            return ""
        endif
    endwhile
    let msg = strpart(w:output, 6, kount)
    let w:output = strpart(w:output, 6+kount)
    return msg
endfunc

func! Write6HexMessage(msg)
    let kount = printf('%06x', strlen(a:msg))
    call ch_sendraw(w:channel, kount . a:msg)
endfunc

The Read6HexMessage is waiting for more if the message isn't long enough to be read. To not hung up we step if the program doesn't progress, by checking whether there was more data received.

Later when writing this I realised the messages drop without the callback. Apparently I need to add 'drop':'never' when opening the channel. But it still didn't work with the very first command, so I went async with this.

Next we would like to interpret what's in each message. The command syntax for the Idris IDE is quite simple:

A ::= NUM | '"' STR '"' | ':' ALPHA+
S ::= A | '(' S* ')' | nil

After few trials I ended up with the following readers and writers for the command syntax:

func! FromSExpr(msg)
    let start = 0
    let sexpr = []
    let context = []
    while 1
        let start = start + strlen(matchstr(a:msg, '^\_s\+', start))
        let head = matchstr(a:msg, '^:[:\-a-zA-Z]\+\|^(\|^)\|^\d\+\|^nil\|^"\([^"]\|\"\)\{-}"', start)
        if head =~ '^('
            call add(context, sexpr)
            let sexpr = []
        elseif head =~ '^)' && len(context) > 0
            let top = remove(context, -1)
            call add(top, sexpr)
            let sexpr = top
        elseif head =~ '^:'
            call add(sexpr, {'command':strpart(head, 1)})
        elseif head =~ '^\d'
            call add(sexpr, str2nr(head))
        elseif head =~ '^"'
            let item = substitute(strpart(head, 1, strlen(head) - 2), '\\"', '"', 'g')
            call add(sexpr, item)
        elseif head =~ '^nil'
            call add(sexpr, [])
        elseif start == strlen(a:msg) && len(context) == 0
            if len(sexpr) == 1
                return remove(sexpr, 0)
            else
                return {'syntax_error':start, 'sexpr':sexpr, 'context':context, 'msg':(a:msg)}
            endif
        else
            return {'syntax_error':start, 'sexpr':sexpr, 'context':context, 'msg':(a:msg)}
        endif
        let start = start + strlen(head)
    endwhile
endfunc

func! IsSyntaxError(item)
    if type(a:item) == v:t_dict
        return has_key(a:item, 'syntax_error')
    endif
    return 0
endfunc

func! IsList(item)
    return type(a:item) == v:t_list
endfunc

func! IsString(item)
    return type(a:item) == v:t_string
endfunc

func! IsNumber(item)
    return type(a:item) == v:t_number
endfunc

func! IsCommand(item)
    if type(a:item) == v:t_dict
        return has_key(a:item, 'command')
    endif
endfunc

func! ToSExpr(item)
    if IsList(a:item)
        let forms = []
        for subitem in a:item
            call add(forms, ToSExpr(subitem))
        endfor
        return '(' . join(forms, ' ') . ')'
    elseif IsString(a:item)
        return '"' . substitute(a:item, '"', '\"', 'g') . '"'
    elseif IsNumber(a:item)
        return printf("%d", a:item)
    elseif IsCommand(a:item)
        return ":" . (a:item)['command']
    endif
endfunc

Now we are able to communicate with the IDE prompt:

let msg = ToSExpr([[{'command':'load-file'}, "Test"], 1]) . "\n"
call Write6HexMessage(msg)

let msg = ToSExpr([[{'command':'type-of'}, "test"], 2]) . "\n"
call Write6HexMessage(msg)

The results go to the w:output.

I am quite not certain about what I received as the output, so lets continue with the IDE-mode of earlier Idris that we know to work:

let w:output = ""
let w:channel = v:null
let w:output = v:null
func! IdrisHandle(channel, msg)
  let w:output = (w:output . a:msg)
  if 6 <= strlen(w:output)
    let kount = str2nr(strpart(w:output, 0, 6), 16)
    if kount + 6 <= strlen(w:output)
        let data = strpart(w:output, 6, kount)
        let w:output = strpart(w:output, 6+kount)
        call IdrisMessage(FromSExpr(data))
    endif
  endif
endfunc

let w:messages = []
func! IdrisMessage(msg)
    call add(w:messages, a:msg)
endfunc

func! IdrisStart()
    let w:messages = []
    let w:output = ""
    let w:job = job_start("idris --ide-mode", {'mode':'raw', 'callback':'IdrisHandle'})
    let w:channel = job_getchannel(w:job)
endfunc

func! IdrisStop()
    call ch_close(w:channel)
    call job_stop(w:job)
endfunc

Now we are done with the main interface. This didn't all come out at the first iteration. Lot of small fixes were added while working on this.

Next we start peeking inside the original idris-vim -plugin.

Response window

The first thing that's needed is the response window. Obviously we'd have already needed it.

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

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

function! IWrite(str)
  if (bufexists("idris-response"))
    let win_view = winsaveview()
    let save_cursor = getcurpos()
    b idris-response
    %delete
    let resp = split(a:str, '\n')
    let n = len(resp)
    let c = 0
    while c < n
        call setbufline("idris-response", c+1, resp[c])
        let c = c + 1
    endwhile
    b #
    call setpos('.', save_cursor)
    call winrestview(win_view)
  else
    echo a:str
  endif
endfunction

function! IAppend(str)
  if (bufexists("idris-response"))
    let win_view = winsaveview()
    let save_cursor = getcurpos()
    b idris-response
    let resp = split(a:str, '\n')
    call append(line('$'), resp)
    b #
    call setpos('.', save_cursor)
    call winrestview(win_view)
  endif
endfunction

Unfortunately I don't figure out how to scroll the response window when more text comes in.

Newer vimscript has macros to do at least the current thing without having to fiddle with user's view and cursor. Latest Ubuntu LTS is still going at 8.0 though. Anyway it's time to add the window prompt into the callback function.

func! IdrisMessage(msg)
    call IAppend(printf("%s", a:msg))
endfunc

Next if we write anything into the output

[{'command': 'protocol-version'}, 1, 0]
[{'command': 'output'},
    [{'command': 'ok'},
        [{'command': 'highlight-source'},
            [[[[{'command': 'filename'}, 'Test.idr'],
                [{'command': 'start'}, 1, 8],
                [{'command': 'end'}, 1, 11]],
                [[{'command': 'namespace'}, 'Test'],
                [{'command': 'decor'}, {'command': 'module'}],
                [{'command': 'source-file'}, '/path/to/Test.idr']]]]]],
    1]
[{'command': 'set-prompt'}, '*Test', 1]
[{'command': 'return'}, [{'command': 'ok'}, []], 1]
[{'command': 'return'},
    [{'command': 'ok'}, 'test : Type', [
        [0, 4, [[{'command': 'name'}, 'Test.test'], [{'command': 'implicit'}, {'command': 'False'}],
            [{'command': 'key'}, 'AQAAAAAAAAAABHRlc3QAAAAAAAAAAQAAAAAAAAAEVGVzdA=='],
            [{'command': 'decor'}, {'command': 'function'}], [{'command': 'doc-overview'}, ''],
            [{'command': 'type'}, 'Type'], [{'command': 'namespace'}, 'Test']]],
        [7, 4, [[{'command': 'decor'}, {'command': 'type'}], [{'command': 'type'}, 'Type'],
            [{'command': 'doc-overview'}, 'The type of types'], [{'command': 'name'}, 'Type']]],
        [7, 4, [[{'command': 'tt-term'}, 'AAAAAAAAAAAHAAAAAAAAAAAKLi9UZXN0LmlkcgAAAAAAAAAW']]]]],
    2]

Aside having to track the message numbers ourselves, we can now pass in commands and see what they do.

let msg = ToSExpr([[{'command':'interpret'}, "1 + 2"], 4]) . "\n"
call Write6HexMessage(msg)

It gives something like this:

[{'command': 'return'}, [{'command': 'ok'}, '3 : Integer',
    [
        [0, 1, [[{'command': 'decor'}, {'command': 'data'}], [{'command': 'type'}, 'Integer'],
            [{'command': 'doc-overview'}, 'An arbitrary-precision integer'], [{'command': 'name'}, '3']]],
        [0, 1, [[{'command': 'tt-term'}, 'AAAAAAAAAAAEAQAAAAAD']]],
        [4, 7, [[{'command': 'decor'}, {'command': 'type'}],
            [{'command': 'type'}, 'Type'],
            [{'command': 'doc-overview'}, 'Arbitrary-precision integers'],
            [{'command': 'name'}, 'Integer']]],
        [4, 7, [[{'command': 'tt-term'}, 'AAAAAAAAAAAECg==']]]]],
    3]

Soon we can start adding existing commands from vim-idris. The system we are about to build needs to keep track of pending commands and ensure they work with the new protocol as well.

Protocol version&response tracking

Since the system courteously tells us the version in the beginning and there are two versions to support, it'd be a great idea to use this on determining which way the interface works. We are going to do that.

The first element in each command appears to be a command to do something, so we start by looking at that. If the message isn't what we care about, it can write as 'echoerr'.

let w:protocol_version = 0
let w:pending_requests = {}
func! IdrisMessage(msg)
    if !IsList(a:msg)
        echoerr printf("idris ide message that is not a list: %s", a:msg)
        return 0
    endif
    if !IsCommand(a:msg[0])
        echoerr printf("idris ide message that is not a command: %s", a:msg)
        return 0
    endif
    let name = a:msg[0]['command']
    if name == 'return' && IsNumber(a:msg[2])
        if has_key(w:pending_requests, a:msg[2])
            let req = remove(w:pending_requests, a:msg[2])
            call req.ok(req, a:msg[1])
        endif
    elseif name == 'output' && IsNumber(a:msg[2])
    elseif name == 'protocol-version' && IsNumber(a:msg[1])
        let w:protocol_version = a:msg[1]
    elseif name == 'set-prompt' && IsString(a:msg[1])
        " doing nothing on this message.
    else
        echoerr printf("unknown idris ide message: %s", a:msg)
    endif
endfunc

func! PrepareSending()
    if w:protocol_version == 0
        echoerr "protocol not initialized"
    endif
    return w:protocol_version
endfunc

let w:next_message_id = 1
func! IdrisSendMessage(command)
    let this_message_id = w:next_message_id
    let msg = ToSExpr([a:command, this_message_id]) . "\n"
    let w:next_message_id = w:next_message_id + 1
    call Write6HexMessage(msg)
    return this_message_id
endfunc

func! IdrisRequest(command, req)
    let w:pending_requests[w:next_message_id] = a:req
    call IdrisSendMessage(a:command)
endfunc

func! DefaultResponse(req, command)
    call IWrite(printf("%s", ToSExpr(a:command)))
endfunc
let w:default_response = {'ok':function("DefaultResponse")}

For now there's possibility that protocol would send malformed messages and cause our handler to fail. As long as script variables remembered across calls stay good, I guess I just accept that.

The PrepareSending is there in case that we want to start the protocol up. Also the w:protocol_version is returned in this manner because it may be temporarily down.

Additionally the protocol version need to be handled by the IdrisStart/IdrisStop so we are going to add it there later when we modify it again.

Now we can try this.

echo IdrisSendMessage([{'command':'load-file'}, "Test"])

echo IdrisRequest([{'command':'type-of'}, "test"], w:default_response)
echo IdrisRequest([{'command':'case-split'}, line, name], w:default_response)
echo IdrisRequest([{'command':'proof-search'}, line, name, hints], w:default_response)

only in version 1
echo IdrisRequest([{'command':'interpret'}, "1 + 2"], w:default_response)
echo IdrisRequest([{'command':'add-clause'}, line, name], w:default_response)
echo IdrisRequest([{'command':'add-proof-clause'}, line, name], w:default_response)
echo IdrisRequest([{'command':'add-missing'}, line, name], w:default_response)
echo IdrisRequest([{'command':'make-with'}, line, name], w:default_response)
echo IdrisRequest([{'command':'make-case'}, line, name], w:default_response)
echo IdrisRequest([{'command':'make-lemma'}, line, name], w:default_response)
echo IdrisRequest([{'command':'docs-for'}, name], w:default_response)
echo IdrisRequest([{'command':'apropos'}, name], w:default_response)
echo IdrisRequest([{'command':'metavariables'}, 80], w:default_response)
echo IdrisRequest([{'command':'who-calls'}, name], w:default_response)
echo IdrisRequest([{'command':'calls-who'}, name], w:default_response)
echo IdrisRequest([{'command':'browse-namespace'}, namespace], w:default_response)
echo IdrisRequest([{'command':'print-definition'}, name], w:default_response)
echo IdrisRequest({'command':'version'}, w:default_response)

only in version 2
echo IdrisRequest([{'command':'generate-def'}, line, name], w:default_response)

For now all the script has been sitting in the blogtext file. Things are going so well that I fork the repository in github and transfer these changes there.

Idris plugin changes

The only file I really have to change is the ftplugin/idris.vim. I write nice bundle out of everything and move it down there.

Mostly I have to replace all 'w:' with 's:' -prefixes and rewrite the protocol handling few times. It also needs somoe documentation for the connection/disconnection features that become available here.

The plugin seems to be working occassionally. Sometimes I get the message I suppose I was meant to get every time when I load a file, other times I don't get that.

I decided that it's time to show idris-hackers what I got here and go onward from there.

Similar posts

• Vulkan API Overview
• The story of a failed archival utility
• Idris review
• Return to Plan 9
• "Porting" of kapow to Plan 9