#!/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
lexerAussagenlogik = Lark(
    '''
    %import common.WS
    %import common.NUMBER
    %import common.WORD
    %ignore WS

    ?start: expr | open

    ?expr:     atomic | not | closed
    ?open:     and | and_long | or | or_long | impl
    ?closed:   "(" open ")"

    // atomische Ausdrücke
    ?atomic:    false | true | atom | generic
    ?false:     "0"                     -> kontr
    ?true:      "1"                     -> taut
    ?atom:      /A[0-9]+/               -> atom
    ?generic:   "{" /((?!({|})).)+/ "}" -> beliebig

    // Symbole
    ?symb_not:  /!/     -> symb
    ?symb_and:  /&+/    -> symb
    ?symb_or:   /\\|+/  -> symb
    ?symb_impl: /->|=>/ -> symb

    // Junktoren
    ?not:               symb_not   expr      -> neg
    ?and:        expr   symb_and   expr      -> konj
    ?and_long: [ expr ( symb_and   expr )+ ] -> konj_lang
    ?or:         expr   symb_or    expr      -> disj
    ?or_long:  [ expr ( symb_or    expr )+ ] -> disj_lang
    ?impl:       expr   symb_impl  expr      -> impl
    ''',
    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 = '( {} )'.format(self.expr);
        return;

    def __str__(self):
        return self.expr;

    def pretty(self):
        return self.tree.pretty();

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# 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();