logik2021/code/aussagenlogik/syntaxbaum.py

117 lines
3.5 KiB
Python
Raw Normal View History

#!/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';