✨ parser for formula.

.gitignore

@@ -0,0 +1 @@
+__pycache__

conftest.py

@@ -0,0 +1,18 @@
+import pytest
+from fol.lexer import Lexer
+from fol.parser import Parser
+
+
+@pytest.fixture
+def lexer():
+    return Lexer()
+
+
+@pytest.fixture
+def parser():
+    def inner(text):
+        lexer = Lexer()
+        lexer.scan(text)
+        parser = Parser(lexer)
+        return parser
+    return inner

doc/grammar.bnf

@@ -0,0 +1,16 @@
+F ::= EXISTS
+EXISTS ::= exists var FORALL | FORALL
+FORALL ::= forall var IMP | IMP
+IMP ::= OR imp OR
+OR ::= AND (or AND)*
+AND ::= NOT (and NOT)*
+NOT ::= not? GROUP
+GROUP ::= NOT | opar F cpar
+PRED ::= pred opar TERM (comma TERM)* cpar
+
+TERM ::=
+| var
+| const
+| FUN
+
+FUN ::= var opar TERM (comma TERM)* cpar

fol/__init__.py

@@ -0,0 +1,10 @@
+from fol import lexer
+from fol import parser
+
+
+def parse(text):
+    lex = lexer.Lexer()
+    lex.scan(text)
+    p = parser.Parser(lex)
+    root = p.parse()
+    return root

fol/lexer.py

@@ -0,0 +1,173 @@
+class Token:
+    def __init__(self, name, value=None):
+        self.name = name
+        self.value = value
+
+    def is_a(self, name):
+        return self.name == name
+
+    def __str__(self):
+        if self.value is not None:
+            return f'{self.name}[{self.value}]'
+        return f'{self.name}'
+
+
+class Lexer:
+    def __init__(self):
+        self.text = ''
+        self.cursor = 0
+
+    def scan(self, text):
+        self.text = text
+        self.cursor = 0
+
+    def next(self):
+        self.scan_spaces()
+
+        scanners = [
+            self.scan_text('AND', '&'),
+            self.scan_text('OR', '|'),
+            self.scan_text('IMP', '->'),
+            self.scan_text('NOT', '~'),
+            self.scan_text('OPAR', '('),
+            self.scan_text('CPAR', ')'),
+            self.scan_text('COMMA', ','),
+            self.scan_keyword('exists'),
+            self.scan_keyword('forall'),
+            self.scan_var,
+            self.scan_const,
+            self.scan_pred,
+        ]
+
+        for scanner in scanners:
+            tok = scanner()
+            if tok is not None:
+                return tok
+
+        return None
+
+    def peek(self, lookahead=0):
+        tok = None
+        cursor = self.cursor
+
+        for i in range(lookahead + 1):
+            tok = self.next()
+
+        self.cursor = cursor
+
+        return tok
+
+    def scan_spaces(self):
+        while self.cursor < len(self.text) \
+              and self.text[self.cursor].isspace():
+            self.cursor += 1
+
+    def scan_var(self):
+        cursor = self.cursor
+        value = ''
+
+        while cursor < len(self.text) and self.text[cursor].islower():
+            value += self.text[cursor]
+            cursor += 1
+
+        if value != '':
+            self.cursor = cursor
+            return Token('VAR', value)
+
+        return None
+
+    def scan_const(self):
+        cursor = self.cursor
+        value = ''
+
+        while cursor < len(self.text) and self.text[cursor].isupper():
+            value += self.text[cursor]
+            cursor += 1
+
+        if value != '' and self.is_sep(cursor):
+            self.cursor = cursor
+            return Token('CONST', value)
+
+        return None
+
+    def scan_pred(self):
+        cursor = self.cursor
+        value = ''
+
+        while cursor < len(self.text) and not self.is_sep(cursor):
+            value += self.text[cursor]
+            cursor += 1
+
+        format = len(value) > 1 and value[0].isupper() \
+            and value[1:].islower()
+
+        if len(value) > 0 and format:
+            self.cursor = cursor
+            return Token('PRED', value)
+
+        return None
+
+    def scan_keyword(self, name):
+        def scanner():
+            cursor = self.cursor
+            value = ''
+
+            if cursor >= len(self.text) or self.text[cursor] != '\\':
+                return None
+
+            cursor += 1
+            i = 0
+
+            while cursor < len(self.text) and i < len(name) \
+                    and self.text[cursor] == name[i]:
+                cursor += 1
+                value += name[i]
+                i += 1
+
+            if not self.is_sep(cursor):
+                return None
+
+            if value == name:
+                self.cursor = cursor
+                return Token(f'{name.upper()}')
+
+            return None
+        return scanner
+
+    def scan_text(self, name, text, tok_value=None):
+        def scanner():
+            cursor = self.cursor
+            value = ''
+
+            i = 0
+
+            while cursor < len(self.text) and i < len(text) \
+                    and self.text[cursor] == text[i]:
+                cursor += 1
+                value += text[i]
+                i += 1
+
+            if value == text:
+                self.cursor = cursor
+                return Token(name, tok_value)
+
+            return None
+        return scanner
+
+    def is_sep(self, idx):
+        if idx < 0 or idx >= len(self.text):
+            return True
+
+        return self.text[idx] in [
+            ' ',
+            '\n',
+            '\t',
+            '-',
+            '\\',
+            '&',
+            '|',
+            '~',
+            '(',
+            ')',
+            ','
+        ]

fol/parser.py

@@ -0,0 +1,170 @@
+class Node:
+    def __init__(self, name, value=None):
+        self.name = name
+        self.value = value
+        self.children = []
+
+    def add_child(self, child):
+        self.children.append(child)
+
+    def __str__(self):
+        res = self.name
+        if self.value is not None:
+            res += f'[{self.value}]'
+
+        if len(self.children) > 0:
+            res += '('
+            sep = ''
+
+            for child in self.children:
+                res += sep + str(child)
+                sep = ','
+            res += ')'
+        return res
+
+
+class Parser:
+    def __init__(self, lexer):
+        self.lexer = lexer
+
+    def consume(self, name):
+        tok = self.lexer.peek()
+
+        if tok and tok.is_a(name):
+            self.lexer.next()
+            return tok
+
+        return None
+
+    def ensure(self, name):
+        tok = self.consume(name)
+
+        if tok is None:
+            raise Exception(f'invalid {name}')
+
+        if tok and not tok.is_a(name):
+            raise Exception(f'expected {name}, got {tok.name}')
+
+        return tok
+
+    def parse(self):
+        return self.parse_f()
+
+    def parse_f(self):
+        return self.parse_exists()
+
+    def parse_exists(self):
+        if self.consume('EXISTS'):
+            tok_var = self.ensure('VAR')
+            rhs = self.parse_forall()
+            node = Node('EXISTS')
+            node.add_child(Node('VAR', tok_var.value))
+            node.add_child(rhs)
+            return node
+
+        return self.parse_forall()
+
+    def parse_forall(self):
+        if self.consume('FORALL'):
+            tok_var = self.ensure('VAR')
+            rhs = self.parse_imp()
+            node = Node('FORALL')
+            node.add_child(Node('VAR', tok_var.value))
+            node.add_child(rhs)
+            return node
+
+        return self.parse_imp()
+
+    def parse_imp(self):
+        lhs = self.parse_or()
+
+        if self.consume('IMP'):
+            rhs = self.parse_or()
+            node = Node('IMP')
+            node.add_child(lhs)
+            node.add_child(rhs)
+            lhs = node
+
+        return lhs
+
+    def parse_or(self):
+        lhs = self.parse_and()
+
+        while self.consume('OR'):
+            rhs = self.parse_and()
+            node = Node('OR')
+            node.add_child(lhs)
+            node.add_child(rhs)
+            lhs = node
+
+        return lhs
+
+    def parse_and(self):
+        lhs = self.parse_not()
+
+        while self.consume('AND'):
+            rhs = self.parse_not()
+            node = Node('AND')
+            node.add_child(lhs)
+            node.add_child(rhs)
+            lhs = node
+
+        return lhs
+
+    def parse_not(self):
+        if self.consume('NOT'):
+            node = Node('NOT')
+            node.add_child(self.parse_pred())
+            return node
+
+        return self.parse_group()
+
+    def parse_group(self):
+        if self.consume('OPAR'):
+            node = self.parse_f()
+            self.ensure('CPAR')
+            return node
+        return self.parse_pred()
+
+    def parse_pred(self):
+        tok = self.ensure('PRED')
+        self.ensure('OPAR')
+
+        node = Node('PRED', tok.value)
+        node.add_child(self.parse_term())
+
+        while self.consume('COMMA'):
+            node.add_child(self.parse_term())
+
+        self.ensure('CPAR')
+        return node
+
+    def parse_term(self):
+        maybe_var = self.lexer.peek(0)
+        maybe_opar = self.lexer.peek(1)
+
+        if maybe_var and maybe_opar and maybe_var.is_a('VAR') \
+           and maybe_opar.is_a('OPAR'):
+            return self.parse_function()
+
+        tok = self.lexer.next()
+        if tok is None:
+            raise Exception('unexpected end')
+
+        if tok.name in ['VAR', 'CONST']:
+            return Node(tok.name, tok.value)
+
+        raise Exception(f'unknown term {tok.value}')
+
+    def parse_function(self):
+        tok = self.ensure('VAR')
+        self.ensure('OPAR')
+
+        node = Node('FUN', tok.value)
+        node.add_child(self.parse_term())
+
+        while self.consume('COMMA'):
+            node.add_child(self.parse_term())
+
+        self.ensure('CPAR')
+        return node

fol/tests/test_lexer.py

@@ -0,0 +1,26 @@
+import pytest
+
+
+@pytest.mark.parametrize(['text', 'oracles'], [
+    ('hello world', ['VAR[hello]', 'VAR[world]']),
+    ('HELLO WORLD', ['CONST[HELLO]', 'CONST[WORLD]']),
+    ('\\exists \\forall', ['EXISTS', 'FORALL']),
+    ('\\existsX', [None]),
+    ('\\exists X', ['EXISTS', 'CONST[X]']),
+    (' A->B ', ['CONST[A]', 'IMP', 'CONST[B]']),
+    (' x&y ', ['VAR[x]', 'AND', 'VAR[y]']),
+    (' a|b ', ['VAR[a]', 'OR', 'VAR[b]']),
+    (' ~s ', ['NOT', 'VAR[s]']),
+    (' (k) ', ['OPAR', 'VAR[k]', 'CPAR']),
+    (' a,b ', ['VAR[a]', 'COMMA', 'VAR[b]']),
+    (' Pr(x) ', ['PRED[Pr]', 'OPAR', 'VAR[x]', 'CPAR']),
+])
+def test_token(lexer, text, oracles):
+    lexer.scan(text)
+
+    for oracle in oracles:
+        tok = lexer.next()
+        if tok is None:
+            assert oracle is None
+        else:
+            assert str(tok) == oracle

fol/tests/test_parser.py

@@ -0,0 +1,45 @@
+import pytest
+
+
+@pytest.mark.parametrize(['oracle', 'text'], [
+    ('PRED[Happy](VAR[x])', 'Happy(x)'),
+    ('PRED[Sad](VAR[y],VAR[z])', 'Sad(y, z)'),
+    # EXISTS
+    ('EXISTS(VAR[x],PRED[Happy](VAR[x]))', '\\exists x Happy(x)'),
+    # FORALL
+    ('FORALL(VAR[z],PRED[Sad](VAR[z]))', '\\forall z Sad(z)'),
+    # IMP
+    ('IMP(PRED[Rich](VAR[x]),PRED[Happy](VAR[x]))',
+     'Rich(x) -> Happy(x)'),
+    # OR
+    ('OR(OR(PRED[Rich](VAR[x]),PRED[Happy](VAR[x])),'
+     'PRED[Smart](VAR[x]))',
+     'Rich(x) | Happy(x) | Smart(x)'),
+    # AND
+    ('AND(AND(PRED[Rich](VAR[x]),PRED[Happy](VAR[x])),'
+     'PRED[Smart](VAR[x]))',
+     'Rich(x) & Happy(x) & Smart(x)'),
+
+    ('OR(AND(PRED[Rich](VAR[x]),'
+     'PRED[Happy](VAR[x])),PRED[Smart](VAR[x]))',
+     'Rich(x) & Happy(x) | Smart(x)'),
+
+    ('AND(PRED[Rich](VAR[x]),OR(PRED[Happy](VAR[x]),'
+     'PRED[Smart](VAR[x])))',
+     'Rich(x) & (Happy(x) | Smart(x))'),
+
+    # NOT
+    ('FORALL(VAR[x],NOT(PRED[Happy](VAR[x])))',
+     '\\forall x ~Happy(x)'),
+    # PRED
+    ('PRED[Rich](CONST[BOB])',
+     'Rich(BOB)'),
+    ('PRED[Rich](FUN[father](CONST[BOB]))',
+     'Rich(father(BOB))'),
+])
+def test_parser(parser, oracle, text):
+
+    p = parser(text)
+    root = p.parse()
+
+    assert oracle == str(root)

requirements.txt

@@ -0,0 +1,8 @@
+flake8==7.0.0
+iniconfig==2.0.0
+mccabe==0.7.0
+packaging==24.0
+pluggy==1.5.0
+pycodestyle==2.11.1
+pyflakes==3.2.0
+pytest==8.1.1

sine_patre.py

@@ -0,0 +1,2 @@
+if __name__ == '__main__':
+    print('Sine Patre')