Correctly pass ranges to Agda when operating over IPs

[isovector]

The Agda interface needs a lot of love here:

1. [x] Mangle Ranges into the right representation for over the wire
2. [ ] Attach buffer offsets to the ranges. I think we can get these via:

function! FileOffset()
    return line2byte(line('.')) + col('.') - 1
endfunction

3. [x] More correctly track IPs. These currently have an interval attached to them, but a better way would be to track them in extmarks.

[isovector]

To do the extmarks stuff, we'll need a map from interaction points to their extmarks. And then check whether nvim_buf_get_extmark_by_id with the details option correctly gives back the ending of its extmark after editing.

[isovector]

This might now be fixed by @Lysxia's new patch.

[Lysxia]

Right, the "attach buffer offsets" task seems to be subsumed by the new ability to convert between the two kinds of offsets at will.