logik2021/code/aussagenlogik/schema.py

70 lines
2.1 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 aussagenlogik.syntaxbaum import SyntaxBaum;
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# GLOBALE KONSTANTEN
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
## lexer
with open('aussagenlogik/grammar.lark', 'r') as fp:
grammar = ''.join(fp.readlines());
lexerAussagenlogik = Lark(grammar, start='expr', regex=True);
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# METHODE: string -> Syntaxbaum
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
def stringToSyntaxbaum(expr: str) -> SyntaxBaum:
try:
return SyntaxBaum(lexerAussagenlogik.parse(expr));
except:
raise Exception('Ausdruck \033[1m{}\033[0m konnte nicht erkannt werden!'.format(expr));
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# METHODEN: Erkennung von Formeltypen
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
def isAtom(fml: SyntaxBaum) -> bool:
return fml.kind == 'atom';
def isLiteral(fml: SyntaxBaum) -> bool:
return isAtom(fml) or (isNegation(fml) and isAtom(fml.child));
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 in ['konj', 'konj_lang'];
def isDisjunction(fml: SyntaxBaum) -> bool:
return fml.kind == 'disj';
def isLongDisjunction(fml: SyntaxBaum) -> bool:
return fml.kind in ['disj', 'disj_lang'];
def isImplication(fml: SyntaxBaum) -> bool:
return fml.kind == 'impl';