使用 Python Yacc\Lex 作为公式解析器

Question

目前，我正在使用 Yacc/Lex 的 python 实现来构建一个公式解析器，用于将公式字符串转换为一组类定义的操作数。到目前为止，我基本上是成功的，但由于括号的含糊性和一些移位/归约错误，我在定义解析规则时陷入了困境。

我一直在研究的公式的巴科斯诺尔形式

phi ::= p ; !p ; phi_0 & phi_1 ; phi_0 | phi_1 ; AX phi ; AF phi ; AG phi ; AU phi_0 U phi_1.

也是我一直在尝试允许任意匹配的括号，但这也是很多混乱的来源，我正在思考移位减少错误的来源。对于我将其应用到的任务来说，括号是相当必要的，它可以强制对公式进行特定的评估，所以我必须解决这个问题。

目前我的解析器是在一个类中定义的，该类构建了词法分析器，

            tokens = (
            'NEGATION',
            'FUTURE',
            'GLOBAL',
            'NEXT',
            'CONJUNCTION',
            'DISJUNCTION',
            'EQUIVALENCE',
            'IMPLICATION',
            'PROPOSITION',             
            'LPAREN',
            'RPAREN',
            'TRUE',
            'FALSE',
            )

        # regex in order of parsing precedence
        t_NEGATION    = r'[\s]*\![\s]*'
        t_FUTURE      = r'[\s]*AF[\s]*'
        t_GLOBAL      = r'[\s]*AG[\s]*'
        t_NEXT        = r'[\s]*AX[\s]*'
        t_CONJUNCTION = r'[\s]*\&[\s]*'
        t_DISJUNCTION = r'[\s]*\|[\s]*'
        t_EQUIVALENCE = r'[\s]*\<\-\>[\s]*'
        t_IMPLICATION = r'[\s]*[^<]\-\>[\s]*'
        t_LPAREN      = r'[\s]*\([\s]*'
        t_RPAREN      = r'[\s]*\)[\s]*'
        t_PROPOSITION = r'[\s]*[a-z]+[-\w\._]*[\s]*'
        t_TRUE        = r'[\s]*TRUE[\s]*'
        t_FALSE       = r'[\s]*FALSE[\s]*'

        precedence = (
        ('left', 'ASSIGNMENT'),
        ('left', 'NEGATION'),
        ('left', 'GLOBAL','NEXT','FUTURE'),
        ('left', 'CONJUNCTION'), 
        ('left', 'DISJUNCTION'), 
        ('left', 'EQUIVALENCE'),
        ('left', 'IMPLICATION'),   
        ('left', 'AUB', 'AUM'),
        ('left', 'LPAREN', 'RPAREN', 'TRUE', 'FALSE'),
        )            

        lexer = lex.lex()
        lexer.input(formula)

并且

        def p_double_neg_paren(p):
            '''formula : NEGATION LPAREN NEGATION LPAREN PROPOSITION RPAREN RPAREN
            '''
            stack.append(p[5].strip())

        def p_double_neg(p):
            '''formula : NEGATION NEGATION PROPOSITION
            '''
            stack.append(p[3].strip())

        def p_double_neg_inner_paren(p):
            '''formula : NEGATION NEGATION LPAREN PROPOSITION RPAREN
            '''
            stack.append(p[4].strip())

        def p_double_neg_mid_paren(p):
            '''formula : NEGATION LPAREN NEGATION PROPOSITION RPAREN
            '''
            stack.append(p[4].strip())

        def p_groupAssignment(p):
            '''formula : PROPOSITION ASSIGNMENT ASSIGNVAL
            '''
            stack.append(p[1].strip() + p[2].strip() + p[3].strip())

        def p_neg_paren_take_outer_token(p):
            '''formula : NEGATION LPAREN PROPOSITION RPAREN
                       | NEGATION LPAREN TRUE RPAREN
                       | NEGATION LPAREN FALSE RPAREN
            '''
            stack.append(Neg(p[3]))

        def p_neg_take_outer_token(p):
            '''formula : NEGATION PROPOSITION
                       | NEGATION TRUE
                       | NEGATION FALSE
            '''

            stack.append(Neg(p[2].strip()))

        def p_neg_take_outer_token_paren(p):
            '''formula : LPAREN NEGATION PROPOSITION RPAREN
                       | LPAREN NEGATION TRUE RPAREN
                       | LPAREN NEGATION FALSE RPAREN
            '''
            stack.append(Neg(p[3].strip()))

        def p_unary_paren_nest_take_outer_token(p):
            '''formula : GLOBAL LPAREN LPAREN NEGATION formula RPAREN RPAREN
                       | NEXT LPAREN LPAREN NEGATION formula RPAREN RPAREN
                       | FUTURE LPAREN LPAREN NEGATION formula RPAREN RPAREN
            '''
            if len(stack) >= 1:
                if p[1].strip() == 'AG':
                    stack.append(['AG', ['!', stack.pop()]])
                elif p[1].strip() == 'AF':
                    stack.append(['AF', ['!', stack.pop()]])
                elif p[1].strip() == 'AX':    
                    stack.append(['AX', ['!', stack.pop()]])


        def p_unary_paren_take_outer_token(p):
            '''formula : GLOBAL LPAREN formula RPAREN
                       | NEXT LPAREN formula RPAREN
                       | FUTURE LPAREN formula RPAREN
            '''
            if len(stack) >= 1:
                if p[1].strip() == "AG":
                    stack.append(AG(stack.pop()))
                elif p[1].strip() == "AF":
                    stack.append(AF(stack.pop()))
                elif p[1].strip() == "AX":
                    stack.append(AX(stack.pop()))

        def p_unary_take_outer_token(p):
            '''formula : GLOBAL formula
                       | NEXT formula
                       | FUTURE formula
            '''

            if len(stack) >= 1:
                if p[1].strip() == "AG":
                    stack.append(AG(stack.pop()))
                elif p[1].strip() == "AF":
                    stack.append(AF(stack.pop()))
                elif p[1].strip() == "AX":
                    stack.append(AX(stack.pop()))

        def p_unary_take_outer_token_prop(p):
            '''formula : GLOBAL PROPOSITION
                       | NEXT PROPOSITION
                       | FUTURE PROPOSITION
            '''

            if len(stack) >= 1:
                if p[1].strip() == "AG":
                    stack.append(AG(stack.pop()))
                elif p[1].strip() == "AF":
                    stack.append(AF(stack.pop()))
                elif p[1].strip() == "AX":
                    stack.append(AX(stack.pop()))

        def p_binary_take_outer_token(p):
            '''formula : formula CONJUNCTION formula 
                       | formula DISJUNCTION formula 
                       | formula EQUIVALENCE formula
                       | formula IMPLICATION formula
            '''

            if len(stack) >= 2:
                a, b = stack.pop(), stack.pop()
                if self.IMPLICATION.search(p[2].strip()) and not self.EQUIVALENCE.search(p[2].strip()):
                    stack.append(Or(a, Neg(b)))
                elif self.EQUIVALENCE.search(p[2].strip()):
                    stack.append(And(Or(Neg(a), b), Or(Neg(b), a)))
                else:
                    if p[2].strip() == "|":
                        stack.append(Or(b, a))
                    elif p[2].strip() == "&":
                        stack.append(And(b, a))

        def p_binary_paren_take_outer_token(p):
            '''formula : LPAREN formula RPAREN CONJUNCTION LPAREN formula RPAREN 
                       | LPAREN formula RPAREN DISJUNCTION LPAREN formula RPAREN
                       | LPAREN formula RPAREN EQUIVALENCE LPAREN formula RPAREN 
                       | LPAREN formula RPAREN IMPLICATION LPAREN formula RPAREN
            '''
            if len(stack) >= 2:
                a, b = stack.pop(), stack.pop()
                if self.IMPLICATION.search(p[4].strip()) and not self.EQUIVALENCE.search(p[4].strip()):
                    stack.append(Or(a, Neg(b)))
                elif self.EQUIVALENCE.search(p[4].strip()):
                    stack.append(And(Or(Neg(a), b), Or(Neg(b), a)))
                else:
                    if p[4].strip() == "|":
                        stack.append(Or(b, a))
                    elif p[4].strip() == "&":
                        stack.append(And(b, a))

        def p_binary_lparen_take_outer_token(p):
            '''formula : LPAREN formula RPAREN CONJUNCTION formula 
                       | LPAREN formula RPAREN DISJUNCTION formula
                       | LPAREN formula RPAREN EQUIVALENCE formula 
                       | LPAREN formula RPAREN IMPLICATION formula
            '''
            if len(stack) >= 2:
                a = stack.pop()
                b = stack.pop()
                if self.IMPLICATION.search(p[4].strip()) and not self.EQUIVALENCE.search(p[4].strip()):
                    stack.append(Or(a, Neg(b)))
                elif self.EQUIVALENCE.search(p[4].strip()):
                    stack.append(And(Or(Neg(a), b), Or(Neg(b), a)))
                else:
                    if p[4].strip() == "|":
                        stack.append(Or(b, a))
                    elif p[4].strip() == "&":
                        stack.append(And(b, a))

        def p_binary_rparen_take_outer_token(p):
            '''formula : formula CONJUNCTION LPAREN formula RPAREN 
                       | formula DISJUNCTION LPAREN formula RPAREN
                       | formula EQUIVALENCE LPAREN formula RPAREN 
                       | formula IMPLICATION LPAREN formula RPAREN
            '''
            if len(stack) >= 2:
                a = stack.pop()
                b = stack.pop()
                if self.IMPLICATION.search(p[4].strip()) and not self.EQUIVALENCE.search(p[4].strip()):
                    stack.append(Or(a, Neg(b)))
                elif self.EQUIVALENCE.search(p[4].strip()):
                    stack.append(And(Or(Neg(a), b), Or(Neg(b), a)))
                else:
                    if p[4].strip() == "|":
                        stack.append(Or(b, a))
                    elif p[4].strip() == "&":
                        stack.append(And(b, a))

        def p_proposition_take_token_paren(p):
            '''formula : LPAREN formula RPAREN
            '''
            stack.append(p[2].strip())

        def p_proposition_take_token_atom(p):
            '''formula : LPAREN PROPOSITION RPAREN
            '''
            stack.append(p[2].strip())

        def p_proposition_take_token(p):
            '''formula : PROPOSITION
            '''
            stack.append(p[1].strip())

        def p_true_take_token(p):
            '''formula : TRUE
                       '''
            stack.append(p[1].strip())

        def p_false_take_token(p):
            '''formula : FALSE
                       '''
            stack.append(p[1].strip())

        # Error rule for syntax errors
        def p_error(p):
            print "Syntax error in input!: " + str(p)
            os.system("pause")
            return 0

我可以看到 lex\yacc 规则的解析规则相当混乱，为了简洁和整洁，我已经删除了每个规则中的大部分调试代码，但任何人都可以看看我哪里错了？我应该将括号的处理转移到另一种方法还是可以用我现在拥有的方法来完成？是否有其他方法可以将这些公式字符串处理为预定义的类操作，而不会出现所有移位/归约错误？

很抱歉在网上公开了我所有的脏代码，但我确实需要一些帮助来解决困扰我几个月的问题。谢谢。

Answer 1

从小事做起！！！无论您最终使用什么解析器库，请尝试仅执行简单的二进制运算，例如 expr & expr，然后让它工作。然后添加对“|”的支持。现在你有两个不同的运算符，并且有足够的空间来表示运算的优先级，并且括号实际上发挥了作用。这个 BNF 看起来像这样：

atom := TRUE | FALSE | '(' expr ')'
and_op := atom '&' atom
or_op := and_op '|' and_op
expr = or_op

你明白这是如何工作的吗？没有明确的“取左括号”、“弹出右括号”之类的东西。弄清楚其他操作的优先级是什么，然后扩展这个递归中缀表示法解析器以反映它们。但在你首先让这个最小的部分工作之前，不要做任何其他事情。否则，你只是想一次解决太多问题。

Answer 2

解析器令人沮丧，而且您的符号并不简单。创建中缀表示法的解析器需要一定的心态。但如果这是您系统的核心部分，您就必须让它正常工作一段时间。我不确定您对 lepl 的困惑是什么，我相信它在概念上与 pyparsing 非常相似。本着SO的精神，也许我可以为你发布一个pyparsing starter。

您的 BNF 与您的词法分析代码并不真正匹配，因为您的代码包含对“<->”和“->”的引用运算符、赋值语句和命题（我假设基本上是小写标识符）。我在网上查找了该语言的参考资料，但没有找到。另外，您没有发布任何测试用例。所以我对你的语言 BNF 应该是什么进行了最好的猜测。

"""
phi ::= p 
        !p 
        phi_0 & phi_1 
        phi_0 | phi_1 
        AX phi 
        AF phi 
        AG phi 
        AU phi_0 U phi_1
"""

from pyparsing import *

LPAR,RPAR = map(Suppress,"()")
NOT = Literal("!")
TRUE = Keyword("TRUE")
FALSE = Keyword("FALSE")
AX, AF, AG, AU, U = map(Keyword, "AX AF AG AU U".split())
AND_OP = "&"
OR_OP = "|"
ident = Word(alphas.lower())

phi = Forward()
p = Optional(NOT) + (TRUE | FALSE | ident | Group(LPAR + phi + RPAR) )
binand = p + ZeroOrMore(AND_OP + p)
binor = binand + ZeroOrMore(OR_OP + binand)
phi << (
    Group(AX + phi) |
    Group(AF + phi) |
    Group(AG + phi) |
    Group(AU + phi + U + phi) |
    binor)

assign = ident + "=" + Group(phi)
equiv = Group(phi) + "<->" + Group(phi)
implicate = Group(phi) + "->" + Group(phi)

statement = assign | equiv | implicate

tests = """\
a=TRUE
b = FALSE
c = !TRUE
d <-> b & !c
AG b & d -> !e""".splitlines()

for t in tests:
    print statement.parseString(t).asList()

打印：

['a', '=', ['TRUE']]
['b', '=', ['FALSE']]
['c', '=', ['!', 'TRUE']]
[['d'], '<->', ['b', '&', '!', 'c']]
[[['AG', 'b', '&', 'd']], '->', ['!', 'e']]

Group 类有助于将结果构建为准 AST。 pyparsing wiki 上有许多示例可以帮助您从这里获取它。我建议查看 simpleBool.py 示例，了解如何让解析器生成求值器。