Lightyear 解析器以意想不到的方式运行

Question

我正在尝试使用 Lightyear 为 Idris 构建格式化程序。到目前为止的整个程序在这里：

https://github.com/hejfelix/IdrisFMT/blob/501a4a9e8b1b4154ed0d7836676c24d98de8b76a/IdrisFmt.idr

目前，目的是标记文件本身然后漂亮地打印它，即作为输入的文件应该是一个固定点。

问题出现在每个字符串文字之后，我的解析器似乎用完了空格。如果我在字符串文字后立即放置除空格之外的任何其他内容，它将解析该字符以及所有后续空格。

此示例程序将显示错误：

main2 : IO ()
main2 = putStrLn $ str
    where
      str = case parse tokenParser "\"IdrisFMT.idr\" \n" of
                 (Left l) => "failed" ++ show l
                 (Right r) => show $ map (show @{default}) r

打印出来：

*IdrisFMT> :exec main2
["StringLiteral(\"IdrisFMT.idr\")"]

如果我将要解析的字符串更改为 "\"IdrisFMT.idr\"c \n"，我会得到：

*IdrisFMT> :exec main2
["StringLiteral(\"IdrisFMT.idr\")", "Identifier(c)", "' '", "'\n'"]

这是我所期望的。

我认为错误是由于我解析字符串文字的方式引起的，但我无法理解我的错误，而且我找不到调试 lightyear 解析器的好方法。我的字符串文字解析器的实现如下：

escape : Parser String
escape = do
  d <- char '\'
  c <- oneOf "\\"0nrvtbf"
  pure $ pack $ (the $ List Char) [d,c]

nonEscape : Parser String
nonEscape = map (\x => pack $ (the $ List _) [x]) $ noneOf "\\"[=13=]\n\r\v\t\b\f"

character : Parser String
character = nonEscape <|>| escape

stringLiteralToken : Parser Token
stringLiteralToken = map (StringLiteral . concat) $ dquote (many character)

如何防止我的字符串文字解析器耗尽文字后的空格？

Answer 1

在#idris 频道聊天后，我了解到大多数内置的高阶解析器（例如dquote）会在末尾跳过空格。就我而言，这不是我想要的。相反，我使用了 between 函数，它接受 3 个参数，一个解析器用于何时开始，另一个用于何时停止，第三个用于介于两者之间的任何内容。

为了解析字符串文字，我现在这样做：

escape : Parser String
escape = do
  d <- char '\'
  c <- oneOf "\\"0nrvtbf'"
  pure $ pack $ (the $ List Char) [d,c]

nonEscape : Parser String
nonEscape = map (\x => pack $ (the $ List _) [x]) $ noneOf "\\"[=10=]\n\r\v\t\b\f"

character : Parser String
character = nonEscape <|>| escape

stringLiteralToken : Parser Token
stringLiteralToken = map (StringLiteral . concat) $ (between (char '"') (char '"')) (many character)

这解决了我的问题。

Lightyear 解析器以意想不到的方式运行

Lightyear parser behaves in unexpected way

whitespace

idris

parser-combinators

lightyear