Haskell中如何将用户输入的逻辑命题字符串解析为自定义数据类型？

看起来你已经搞定了逻辑命题的数据类型和基础类型类实例，现在就差把用户输入的数学式字符串转成你的Prop类型了对吧？Haskell里做这类解析最顺手的工具就是Parsec库，它比手写递归下降解析器简洁，也比自定义Read实例灵活（毕竟Read的语法和Haskell代码绑定，没法直接支持¬、^这种数学符号）。

下面我一步步给你演示怎么实现：

1. 先对齐你的Prop数据类型（示例） #

先按照你给出的例子，假设你的数据类型定义是这样的（如果实际有差异，你可以对应调整解析器）：

data Prop = V String       -- 变量，比如 q、p
          | No Prop       -- 否定 ¬
          | Y Prop Prop   -- 合取 ^
          deriving (Eq, Ord, Show)

2. 安装并导入Parsec库 #

首先确保你已经安装了parsec包，用cabal install parsec或者在你的cabal文件里添加依赖。然后导入必要的模块：

import Text.Parsec
import Text.Parsec.String (Parser)  -- 我们要解析String类型的输入
import Text.Parsec.Char (letter, oneOf)
import Text.Parsec.Combinator (many1)

3. 编写基础解析组件 #

我们把解析拆成几个小部分，从最基础的开始：

3.1 解析变量 #

变量是字母组成的字符串，比如p、q、abc：

varParser :: Parser Prop
varParser = V <$> many1 letter  -- many1 letter 匹配一个或多个字母，然后用V包装

3.2 解析否定 #

否定符号支持¬或者~（方便用户输入），后面紧跟一个高优先级的命题：

negParser :: Parser Prop
negParser = do
  oneOf "¬~"  -- 匹配¬或者~
  p <- atomParser  -- 否定后面只能跟“原子命题”（变量、括号里的命题）
  return $ No p

3.3 解析括号包裹的命题 #

括号里的是完整命题，用来改变优先级：

parenParser :: Parser Prop
parenParser = do
  char '('
  p <- propParser  -- 递归解析括号里的整个命题
  char ')'
  return p

3.4 定义“原子命题” #

原子命题是优先级最高的表达式：变量、否定命题或者括号里的命题：

atomParser :: Parser Prop
atomParser = varParser <|> negParser <|> parenParser

3.5 解析合取 #

合取符号是^，支持符号前后的空格，用chainl1处理连续合取（比如p ^ q ^ r会被解析成Y (Y (V "p") (V "q")) (V "r")）：

conjParser :: Parser Prop
conjParser = chainl1 atomParser (do
  char '^'
  spaces  -- 允许符号前后有空格
  return Y)

3.6 顶层解析器 #

顶层解析器处理输入前后的空格，确保整个输入都被解析完：

propParser :: Parser Prop
propParser = do
  spaces  -- 跳过开头的空格
  p <- conjParser
  spaces  -- 跳过结尾的空格
  eof  -- 确保没有剩余未解析的内容
  return p

4. 编写对外的解析函数 #

最后写一个易用的函数，把字符串传入解析器，返回Either String Prop——成功返回Right Prop，失败返回Left错误信息：

parseProp :: String -> Either String Prop
parseProp input = case parse propParser "" input of
  Left err -> Left (show err)
  Right p -> Right p

5. 测试一下 #

在GHCi里测试你给的例子：

-- 输入你给的例子
parseProp "¬q ^ p"
-- 应该得到 Right (Y (No (V "q")) (V "p"))

-- 测试带括号的情况
parseProp "(¬p ^ q) ^ r"
-- 得到 Right (Y (Y (No (V "p")) (V "q")) (V "r"))

-- 测试连续否定
parseProp "¬¬p"
-- 得到 Right (No (No (V "p")))

补充说明 #

• 如果你的Prop类型还有其他构造器（比如析取∨、蕴含→），只需要按照同样的逻辑添加对应的解析器，并且调整优先级（比如蕴含优先级最低，析取次之，合取次之，否定最高）。
• 如果用户输入的符号和你用的不一样（比如用not代替¬），只需要修改negParser里的oneOf参数即可。
• 如果你不想用Parsec，也可以手写递归下降解析器，但Parsec已经帮你处理了错误提示、空格处理、优先级等细节，效率也不差。

内容的提问来源于stack exchange，提问作者HRDSL