Compare commits

..

2 Commits

Author SHA1 Message Date
bog badb08ec05 parser for formula. 2024-04-24 14:40:43 +02:00
bog 5cecb1f1ed 🎉 lexer for formula. 2024-04-24 10:56:13 +02:00
10 changed files with 469 additions and 0 deletions

1
.gitignore vendored Normal file
View File

@ -0,0 +1 @@
__pycache__

18
conftest.py Normal file
View File

@ -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

16
doc/grammar.bnf Normal file
View File

@ -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

10
fol/__init__.py Normal file
View File

@ -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

173
fol/lexer.py Normal file
View File

@ -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',
'-',
'\\',
'&',
'|',
'~',
'(',
')',
','
]

170
fol/parser.py Normal file
View File

@ -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

26
fol/tests/test_lexer.py Normal file
View File

@ -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

45
fol/tests/test_parser.py Normal file
View File

@ -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)

8
requirements.txt Normal file
View File

@ -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

2
sine_patre.py Normal file
View File

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