Clash Royale CLAN TAG#URR8PPP

Idris Lightyear requireFailure does not do backtracking

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" are okay, but neither "bbcd" nor "abbc" should not match.

"bb"

"aaaa"

"abcd"

"bbcd"

"abbc"

I composed a following parser:

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


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

b

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


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

['a', 'c', 'd', 'e']

"bbcd"

"abbc"

As a workaround I used my own implementation of requireFailure:

requireFailure

requireFailure' : Parser a -> Parser ()
requireFailure' p = do
isP <- p *> pure True <|> pure False
if isP then fail "argument parser to fail"
else pure ()


So

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


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

['a', 'b', 'c', 'd']

Apparently lightyear parsers are backtrack-by-default, unless one calls commitTo.

commitTo

So my question is why library implementation of requireFailure does not do backtracking in case it's argument fails and is it an expected behavior?

requireFailure

1 Answer
1

If you look at the implementation of requireFailure you can see that it calls the "success" continuation us with the state s it gets after running its argument rather than the one ST i pos tw it got before.

requireFailure

us

s

ST i pos tw

requireFailure : ParserT str m tok -> ParserT str m ()
requireFailure (PT f) = PT $ r, us, cs, ue, ce, (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, s => us () s)
(errs, s => cs () s)
(ST i pos tw)


The documentation claims that requireFailure is called notFollowedBy in parsec and that doesn't consume any input so you could argue it's a bug on LightYear's side.

requireFailure

notFollowedBy

You could open a bug report suggesting to replace the current code with something like (I don't know whether Idris supports @ patterns):

@

requireFailure : ParserT str m tok -> ParserT str m ()
requireFailure (PT f) = PT $ r, us, cs, ue, ce, s@(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 () s)
(errs, _ => cs () s)
s


By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.