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