117 lines
3.5 KiB
Python
117 lines
3.5 KiB
Python
#!/usr/bin/env python3
|
|
# -*- coding: utf-8 -*-
|
|
|
|
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
# IMPORTS
|
|
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
|
from __future__ import annotations;
|
|
from lark import Tree as larkTree;
|
|
from typing import Generator;
|
|
from typing import List;
|
|
|
|
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
# GLOBALE KONSTANTEN
|
|
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
|
#
|
|
|
|
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
# KLASSE: Syntaxbaum
|
|
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
|
class SyntaxBaum(object):
|
|
kind: str;
|
|
expr: str;
|
|
valence: int;
|
|
children: List[SyntaxBaum];
|
|
|
|
def __init__(self, fml: larkTree):
|
|
self.kind = fml.data;
|
|
self.children = [];
|
|
self.valence = 0;
|
|
expr_parts = []
|
|
for child in fml.children:
|
|
if isinstance(child, str):
|
|
expr_parts.append(child);
|
|
## subfml is instance larkTree:
|
|
elif child.data == 'symb':
|
|
symb = str(child.children[0]);
|
|
expr_parts.append(symb);
|
|
else:
|
|
subtree = SyntaxBaum(child);
|
|
self.children.append(subtree);
|
|
self.valence += 1;
|
|
expr_parts.append(subtree.expr);
|
|
self.expr = ' '.join(expr_parts);
|
|
if self.valence > 1:
|
|
self.expr = '(' + self.expr + ')';
|
|
return;
|
|
|
|
def __str__(self):
|
|
return self.expr;
|
|
|
|
def __iter__(self) -> Generator[SyntaxBaum, None, None]:
|
|
for child in self.children:
|
|
yield child;
|
|
|
|
@property
|
|
def child(self) -> SyntaxBaum:
|
|
return self.children[0];
|
|
|
|
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
# METHOD: Pretty
|
|
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
|
def pretty(self, preindent: str = '', tab: str = ' ', prepend: str = '', depth: int = 0) -> str:
|
|
indent = preindent + tab*depth;
|
|
if self.valence == 0 and self.kind in [ 'atom', 'generic' ]:
|
|
return indent + prepend + self.kind + ' ' + self.expr;
|
|
return '\n'.join(
|
|
[indent + prepend + self.kind] \
|
|
+ [subtree.pretty(preindent, tab, '|__ ', depth+1) for subtree in self.children]
|
|
);
|
|
|
|
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
# METHODS: Erkennung von Formeltypen
|
|
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
|
def isIrreducible(self) -> bool:
|
|
return self.valence == 0;
|
|
|
|
def isAtom(self) -> bool:
|
|
return self.kind == 'atom';
|
|
|
|
def isLiteral(self) -> bool:
|
|
return self.isAtom() or (self.isNegation() and self.child.isAtom());
|
|
|
|
def isGeneric(self) -> bool:
|
|
return self.kind == 'generic';
|
|
|
|
def isTautologySymbol(self) -> bool:
|
|
return self.kind == 'taut';
|
|
|
|
def isContradictionSymbol(self) -> bool:
|
|
return self.kind == 'contradiction';
|
|
|
|
def isConnective(self) -> bool:
|
|
return self.valence > 0;
|
|
|
|
def isNegation(self) -> bool:
|
|
return self.kind == 'not';
|
|
|
|
def isConjunction2(self) -> bool:
|
|
return self.kind == 'and2';
|
|
|
|
def isConjunction(self) -> bool:
|
|
return self.kind in ['and', 'and2'];
|
|
|
|
def isDisjunction2(self) -> bool:
|
|
return self.kind == 'or2';
|
|
|
|
def isDisjunction(self) -> bool:
|
|
return self.kind in ['or', 'or2'];
|
|
|
|
def isImplication(self) -> bool:
|
|
return self.kind == 'implies';
|