ziman / lightyear

Parser combinators for Idris
Other
238 stars 43 forks source link

Alternative backtracks, but the transformer does not #64

Open BartAdv opened 7 years ago

BartAdv commented 7 years ago

Steps to reproduce

import Control.Monad.State
import Lightyear
import Lightyear.Char
import Lightyear.Combinators
import Lightyear.Strings

-- hide the one from Lightyear.Strings
%hide Parser

Parser : Type -> Type
Parser = ParserT String (State Integer)

pModify : Parser ()
pModify = do
  token "+"
  modify (+ 1)

pTextBlock : Parser String
pTextBlock = pack <$> many anyChar

parser : Parser (List String)
parser = manyTill (choice alts) eof
  where
    alts : List (Parser String)
    alts = [ pure "" <* ((pModify <* string "can'thappen") <|> pModify)
           , pTextBlock
           ]

testParse : Parser a -> String -> Either String (a, Integer)
testParse p src =
  let initialVal = 0
      Id (r,s) = flip runStateT initialVal $ execParserT p (initialState Nothing src 8)
  in case r of
    MkReply _ (Success x)  => Right (x,s)
    MkReply _ (Failure es) => Left $ concat $ intersperse "\n" $ map display es

Running

λΠ> :exec testParse parser "+ho ho"

gives

Right (["", "ho ho"], 2)

Observed behaviour

The returned value means that our state had been modified two times. And this is because of the alternative:

((pModify <* string "can'thappen") <|> pModify)

which first enters the left branch (which won't succeed due to dummy string parse at the end), and then the right branch kicks in, and succeeds.

Expected behavior

If the default behavior is to backtrack, then the result of the transformer needs to be discarded as well.

BartAdv commented 7 years ago

Hmm...looking at the lift implementation I don't even see how it could possibly work like I want. So I guess it's by design. I'll try StateT s (ParserT String Identity)