sndordlogic.py

from lark import Lark, Transformer, v_args

# 1. Define the grammar for second order logic using ASCII characters
grammar = """
    start: formula
    
    ?expr: arith_expr
         | bool_expr

    ?arith_expr: term
              | arith_expr "+" term        -> add
              | arith_expr "-" term        -> sub

    ?term: factor
         | term "*" factor               -> mul
         | term "/" factor               -> div

    ?factor: "(" arith_expr ")"          -> arith_expr_paren
           | NUMBER
           | VAR

    bool_expr: arith_expr "==" arith_expr        -> eq
             | arith_expr "!=" arith_expr        -> ne
             | arith_expr ">=" arith_expr        -> ge
             | arith_expr ">" arith_expr         -> gt
             | arith_expr "<=" arith_expr        -> le
             | arith_expr "<" arith_expr         -> lt

    formula: predicate | forall | exists
    
    predicate: VAR "(" VAR ("," VAR)* ")" | expr

    
    forall: "forall" "(" VAR ":" predicate ")"
    
    exists: "exists" "(" VAR ":" predicate ")"
    
    NUMBER: /-?\d+(\.\d+)?/
    VAR: /[a-zA-Z_]\w*/
    %import common.WS
    %ignore WS
"""

# 2. Create the parser using LALR mode
parser = Lark(grammar, parser="lalr")


# 3. Define the visitor class with v_args decorator
@v_args(inline=True)
class SecondOrderLogicVisitor(Transformer):
    def start(self, formula):
        return formula

    def formula(self, f):
        return f

    def predicate(self, pred, *args):
        if not args:
            return pred
        return f'{pred}({", ".join(args)})'

    def forall(self, name, predicate):
        return f"forall ({name} : {predicate})"

    def exists(self, *items):
        name, predicate = items
        return f"exists {name} : {predicate}"

    def add(self, lhs, rhs):
        return f"({lhs} + {rhs})"

    def sub(self, lhs, rhs):
        return f"({lhs} - {rhs})"

    def mul(self, lhs, rhs):
        return f"({lhs} * {rhs})"

    def div(self, lhs, rhs):
        return f"({lhs} / {rhs})"

    def eq(self, lhs, rhs):
        return f"({lhs} == {rhs})"

    def ne(self, lhs, rhs):
        return f"({lhs} != {rhs})"

    def ge(self, lhs, rhs):
        return f"({lhs} >= {rhs})"

    def gt(self, lhs, rhs):
        return f"({lhs} > {rhs})"

    def le(self, lhs, rhs):
        return f"({lhs} <= {rhs})"

    def lt(self, lhs, rhs):
        return f"({lhs} < {rhs})"

    def NUMBER(self, number):
        return number[0]

    def VAR(self, var):
        return var[0]


# 4. Write a visitor class with lark, add functions for all the production rules in the grammar
parser_visitor = SecondOrderLogicVisitor()

# 5. Write a requirements.txt with the dependencies
# File: requirements.txt
# lark-parser==0.12.0


def parse_second_order_logic(expression):
    tree = parser.parse(expression)
    return parser_visitor.transform(tree)


# Example usage:
parsed_expression = parse_second_order_logic(expression)
print(parsed_expression)