Skip to content

Instantly share code, notes, and snippets.

@dhilst
Created February 20, 2024 00:13
Show Gist options
  • Save dhilst/b6499057b9f4388bdb8574e451560b78 to your computer and use it in GitHub Desktop.
Save dhilst/b6499057b9f4388bdb8574e451560b78 to your computer and use it in GitHub Desktop.
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment