ziman / lightyear

Parser combinators for Idris
Other
238 stars 43 forks source link

getPosition is invalidating the parser state? #61

Closed BartAdv closed 7 years ago

BartAdv commented 7 years ago

Given parser:

pFrob : Parser String
pFrob = do
  pos <- getPosition
  string "frob"
  pure "frob!"

following test code

parse (pFrob <|> string "w00t") "w00t"

should fail on left branch and succeed on second. However, this happens:

Left "At 1:1:\n\tstring \"frob\"\nAt 1:1:\n\tcharacter 'f'\nAt 1:1:\n\ta different token" : Either String
                                                                                                   String

Now, if I remove the getPosition action:

pFrob : Parser String
pFrob = do
  string "frob"
  pure "frob!"

it succeeds:

Right "w00t" : Either String String
ziman commented 7 years ago

Thank you!

I suspect the problem has something to do with cs being used here: https://github.com/ziman/lightyear/blob/master/Lightyear/Core.idr#L225

while pure uses just the uncommitted us: https://github.com/ziman/lightyear/blob/master/Lightyear/Core.idr#L79

This means that as soon as you run getState, the parser will commit for no reason.

I propose changing getState to use us. @jfdm, how does that sound?