ziman / lightyear

Parser combinators for Idris
Other
238 stars 43 forks source link

Issue translating megaparsec example #68

Open locallycompact opened 5 years ago

locallycompact commented 5 years ago

Hi, I'm trying to translate the last megaparsec example on this page.

http://akashagrawal.me/beginners-guide-to-megaparsec/

I ended up with this, which typechecks.

boldP : Parser (List Char)
boldP = do
  _ <- ntimes 2 (char '*')
  txt <- some (alphaNum <|> char ' ')
  _ <- ntimes 2 (char '*')
  pure $ unpack "<strong>" ++ txt ++ unpack "</strong>"

foo : Either String (List Char)
foo = parse boldP "**idris is cool**"

But it seems to fail to do anything.

Expression: foo = case case uncons "idris is cool**" of
       Nothing => ue [Err pos "a token, not EOF"] (ST i pos tw)
       Just (t, rest) => case f t of
                           Nothing => ue [Err pos "a different token"] (ST i pos tw)
                           Just res => case updatePos tw pos t of
                                         (newPos, b) => us res (ST rest newPos tw) of
  Id r => case r of
            MkReply _ (Success x) => Right x
            MkReply _ (Failure es) => Left (concat (intersperse "\n" (map display es))) : Either String (List Char)