search

ziman / lightyear

Parser combinators for Idris
Other
238 stars 43 forks source link

Infinite loop #62

Closed BartAdv closed 7 years ago

BartAdv commented 7 years ago

I haven't managed to prepare smaller repro, this is what I found out so far.

Given following code: http://lpaste.net/2559959787278172160 (with test cases in comments), one of the test cases causes infinite loop.

Removing one of those fixes it (that's why I haven't been able to nail it down, since it might be tad more complicated interplay between two parsers):

1) Removing many from here (throwing entire sepBy, as it uses many indirectly):

pKey : Parser (List String)
pKey = sepBy1 (pack <$> many alphaNum) (char '.')

2) Removing getPosition from here (I run the branch with latest getState fix):

pPartial : (Position -> Maybe Position) -> Parser Node
pPartial f = do
  pos <- f <$> getPosition
  key <- pTag ">" <?> "partial tag"
  pure (Partial key pos)
BartAdv commented 7 years ago

Quite possibly, it might be some Idris bug (although in my above repro, I didn't use :x):

λΠ> parse (pack <$> many alphaNum) "frob"
Right "frob" : Either String String
λΠ> :x parse (pack <$> many alphaNum) "frob"
<<hangs>>

EDIT:

And the previous repro is fine when run as executable! Will raise the ticket for Idris, if nothing like that is already reported.

BartAdv commented 7 years ago

Opened Idris ticket: https://github.com/idris-lang/Idris-dev/issues/4060, closing this one - it doesn't look like Lightyear issue.