ziman / lightyear

Parser combinators for Idris
Other
238 stars 43 forks source link

requireFailure consumes an input (does not do backtracking) #66

Closed stop-cran closed 6 years ago

stop-cran commented 6 years ago

The documentation claims that requireFailure is called notFollowedBy in parsec and that it doesn't consume any input. However, I see it does.

For example, I want to parse a series of any 4 chars. However, these chars shouldn't form a specific string ("bb" in an example below). So "aaaa" and "abcd" should math, but neither "bbcd" nor "abbc" should not.

I composed a following parser:

ntimes 4 (requireFailure (string "bb") *> anyChar)

However, I noticed, that it "eats" single b chars. E.g.

parse (ntimes 4 (requireFailure (string "bb") *> anyChar)) "abcde"

results in ['a', 'c', 'd', 'e'] (it fails, however, on "bbcd" and "abbc" as expected).

If following implementation of requireFailure is used:

requireFailure' : ParserT str m tok -> ParserT str m ()
requireFailure' (PT f) = PT requireFailureHelper where
    requireFailureHelper r us cs ue ce ss@(ST i pos tw) =
        f r
            (\t, s => ue [Err pos "argument parser to fail"] s)
            (\t, s => ce [Err pos "argument parser to fail"] s)
            (\errs, _ => us () ss)
            (\errs, _ => cs () ss)
            ss
parse (ntimes 4 (requireFailure' (string "bb") *> anyToken)) "abcde"

gives ['a', 'b', 'c', 'd'] as I expect.

Asked previously on StackOverflow.

ziman commented 6 years ago

Oh, thank you (and Guillaume), well spotted! I also like that you gave the @-bound variable a name different from s, it's easier to spot what's going on.

I'll push the update.

ziman commented 6 years ago

Fix pushed, thank you!