logik2021/code/aussagenlogik/schema.py

130 lines
4.3 KiB
Python

#!/usr/bin/env python3
# -*- coding: utf-8 -*-
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# IMPORTS
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
from __future__ import annotations;
# install: lark; lark-parser; lark-parser[regex].
# https://lark-parser.readthedocs.io/en/latest/grammar.html
from lark import Lark;
from lark import Tree;
from typing import List;
from typing import Union;
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# GLOBALE KONSTANTEN
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
## lexer
with open('aussagenlogik/grammar.lark', 'r') as fp:
grammar = ''.join(fp.readlines());
lexerAussagenlogik = Lark(grammar, start='expr', regex=True);
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# KLASSE: Syntaxbaum
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
class SyntaxBaum(object):
expr: str;
kind: str;
children: List[SyntaxBaum];
tree: Tree;
def __init__(self, fml: Tree):
self.kind = fml.data;
if len(fml.children) == 1 and isinstance(fml.children[0], str):
self.expr = fml.children[0];
self.children = [];
self.tree = Tree(self.kind, fml.children);
else:
self.children = [ SyntaxBaum(child) for child in fml.children if isinstance(child, Tree) and child.data != 'symb' ];
self.tree = Tree(self.kind, [child.tree for child in self.children]);
signature_parts = [];
i = 0;
for teilfml in fml.children:
if isinstance(teilfml, str):
signature_parts.append(teilfml);
elif teilfml.data == 'symb':
signature_parts.append(getText(teilfml));
else:
signature_parts.append('{{{}}}'.format(i));
i += 1;
signature = ' '.join(signature_parts);
self.expr = signature.format(*self.children);
if self.kind in [ 'konj', 'konj_lang', 'disj', 'disj_lang', 'impl' ]:
self.expr = ('(' if self.expr.startswith('(') else '( ') + self.expr;
self.expr += (')' if self.expr.endswith(')') else ' )');
return;
def __str__(self):
return self.expr;
def pretty(self):
return self.tree.pretty(indent_str='- ');
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# METHODE: string -> Syntaxbaum
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
def stringToSyntaxbaum(u: str) -> SyntaxBaum:
try:
return SyntaxBaum(lexerAussagenlogik.parse(u));
except:
raise Exception('Ausdruck \033[1m{}\033[0m konnte nicht erkannt werden!'.format(u));
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# METHODEN: Erkennung von Formeltypen
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
def isAtom(fml: SyntaxBaum) -> bool:
return fml.kind == 'atom';
def isBeliebig(fml: SyntaxBaum) -> bool:
return fml.kind == 'beliebig';
def isTrueSymbol(fml: SyntaxBaum) -> bool:
return fml.kind == 'taut';
def isFalseSymbol(fml: SyntaxBaum) -> bool:
return fml.kind == 'kontr';
def isNegation(fml: SyntaxBaum) -> bool:
return fml.kind == 'neg';
def isConjunction(fml: SyntaxBaum) -> bool:
return fml.kind == 'konj';
def isLongConjunction(fml: SyntaxBaum) -> bool:
return fml.kind == 'konj_lang';
def isDisjunction(fml: SyntaxBaum) -> bool:
return fml.kind == 'disj';
def isLongDisjunction(fml: SyntaxBaum) -> bool:
return fml.kind == 'disj_lang';
def isImplication(fml: SyntaxBaum) -> bool:
return fml.kind == 'impl';
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# METHODEN: Formel -> Textinhalt
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
def getText(fml: Tree) -> str:
text = fml.children[0];
if isinstance(text, str):
return text;
raise Exception('Konnte Textinhalt nicht ablesen!');
def getName(fml: SyntaxBaum) -> str:
return fml.expr;
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# METHODEN: Formel -> Textinhalt
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
def prettifyTree(fml: Union[Tree, SyntaxBaum]) -> str:
return fml.pretty();