logik2021/code/aussagenlogik/schema.py

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