search

idris-hackers / idris-vim

Idris mode for vim
221 stars 52 forks source link

<Leader>p over hole generates code that should not be #54

Open mbbx6spp opened 8 years ago

mbbx6spp commented 8 years ago

I upgraded to Idris 0.12.2 recently from 0.9.x (on a brand new machine) and had to rewrite a few things due to the interface and related changes between those versions. I do not believe my version of this vim plugin changed (which is likely the problem). I am not much of a vim plugin developer (though I have dabbled in the black arts), so if you provide pointers to me, I might be able to provide a PR if it is still a problem on the master HEAD.

I have detailed out my environment's versions here: https://gist.github.com/mbbx6spp/6fe833d300b1492f9373864be3cae396#file-versions-txt

module Predicates

import Data.Vect

isElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
isElem value [] = ?bug -- with cursor over ?bug hole if you <Leader>p it will complete with `Yes ?bug1`
isElem value (x :: xs) = ?irrelevant

Now put cursor over the ?bug hole above and then do <Leader>p in vim. This will complete with the code Yes ?bug1. See below.

module Predicates

import Data.Vect

isElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
isElem value [] = Yes ?bug1
isElem value (x :: xs) = Yes (There ?isElem_rhs_5)

In another pane I have idris REPL running.

I am sure I have done something incredibly silly but it wasn't behavior I noticed on my old laptop with Idris v0.9.x.

I assume this is perhaps searching for the case in the line below where the hole actually is?

LeifW commented 8 years ago

Sorry, I think https://github.com/idris-lang/Idris-dev would be a more appropriate place to report this, as that answer is just coming from the Idris repl and there's nothing the vim code that talks to it can do about it. To reproduce this seperate from vim: Load your file in the repl, and then run :proofsearch 6 bug (assuming that ?bug is on line 6 of the file), which is the command <Leader>p is running - https://github.com/idris-hackers/idris-vim/blob/master/ftplugin/idris.vim#L137 Reports back Yes ?bug1