Lightyear requireFailure не выполняет откат

Я хочу разобрать серию любых 4 символов. Однако эти символы не должны формировать определенную строку ( "bb" в примере ниже). Итак, "aaaa" и "abcd" в порядке, но ни "bbcd", ни "abbc" не должны совпадать.

Я составил следующий парсер:

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

Однако я заметил, что он "съедает" одиночные b символов. Например.

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

приводит к ['a', 'c', 'd', 'e'] (однако он терпит неудачу на "bbcd" и "abbc", как и ожидалось).

В качестве обходного пути я использовал собственную реализацию 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"

дает ['a', 'b', 'c', 'd'], как я и ожидал.

По-видимому, синтаксические анализаторы Lightyear откатываются по умолчанию, если только не вызывается commitTo.

Итак, мой вопрос: почему библиотечная реализация requireFailure не выполняет откат в случае сбоя аргумента и является ли это ожидаемым поведением?


parser-combinators idris lightyear
person stop-cran    schedule 08.08.2018    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Если вы посмотрите на реализация 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)

В документации утверждается, что requireFailure называется notFollowedBy в парсеке и не требует никаких входных данных, так что вы можете утверждать, что это ошибка на стороне LightYear.

Вы можете открыть отчет об ошибке, предлагающий заменить текущий код чем-то вроде (я не знаю, поддерживает ли Idris шаблоны @):

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
person gallais    schedule 08.08.2018
comment
Имеет смысл. Я создал отчет об ошибке — github.com/ziman/lightyear/issues/66. - person stop-cran; 08.08.2018