#!/usr/bin/env python3
# -*- coding: utf-8 -*-

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# IMPORTS
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

from __future__ import annotations;
import os;
import sys;
sys.tracebacklimit = 0;
from itertools import product;
from lark import Tree;
from textwrap import dedent;
from typing import Dict;
from typing import Generator;
from typing import List;
from typing import Tuple;
from typing import Union;

sys.path.insert(0, os.getcwd());

from schema import string_to_parts;

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# GLOBAL CONSTANTS
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

# zeichenkette = 'A0';
# zeichenkette = '! A0';
# zeichenkette = '( A0 && A1 )';
# zeichenkette = '( A0 || A1 )';
# zeichenkette = '( A0 -> A1 )';
zeichenkette = '( A0 -> ((A0 && A3) || ! A2) )';
# zeichenkette = '(( {G} || !{G} ) -> A5)';

I = ['A0', 'A2'];

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# HAUPTVORGANG
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

def main():
    tree = string_to_parts(zeichenkette);
    print(dedent(
        '''
        Syntaxbaum von
            F := \033[92;1m{F}\033[0m:
        '''.format(
            F=zeichenkette,
        )
    ));
    print(tree.pretty());
    print(dedent(
        '''
        eval(F, I)      = \033[94;1m{eval}\033[0m;
        atoms(F)        = \033[94;1m{atoms}\033[0m; \033[91;1m<- *\033[0m
        depth(F)        = \033[94;1m{d}\033[0m; \033[91;1m<- *\033[0m
        length(F)       = \033[94;1m{l}\033[0m; \033[91;1m<- *\033[0m
        #parentheses(F) = \033[94;1m{p}\033[0m; \033[91;1m<- *\033[0m

        \033[91;1m*\033[0m \033[2mnoch nicht implementiert!\033[0m
        \033[1;2;4mChallenge:\033[0m \033[2mschreibe diese Methoden. Probiere mit Stift-und-Zettel die Methoden händisch auszuführen und vergleiche mit dem Code-Output.\033[0m
        '''.format(
            eval  = rekursiv_eval(tree, I),
            atoms = rekursiv_atoms(tree),
            d     = rekursiv_depth(tree),
            l     = rekursiv_length(tree),
            p     = rekursiv_parentheses(tree),
        )
    ));
    return;

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# SEKUNDÄRVORGÄNGE
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

def rekursiv_atoms(fml: Tree) -> List[str]:
    ## Herausforderung: schreibe diese Funktion!
    return [];

def rekursiv_depth(fml: Tree) -> int:
    ## Herausforderung: schreibe diese Funktion!
    return 0;

def rekursiv_length(fml: Tree) -> int:
    ## Herausforderung: schreibe diese Funktion!
    return 0;

def rekursiv_parentheses(fml: Tree) -> int:
    ## Herausforderung: schreibe diese Funktion!
    return 0;

def rekursiv_eval(fml: Tree, I: List[str]) -> int:
    if fml.data in ['atom', 'beliebig']:
        index = fml.children[0];
        return 1 if ('{}'.format(index) in I) else 0;
    elif fml.data == 'wahr':
        return 1;
    elif fml.data == 'falsch':
        return 0;
    elif fml.data == 'negation':
        teilformel1 = fml.children[1];
        if isinstance(teilformel1, Tree):
            val1 = rekursiv_eval(teilformel1, I);
            return 1 - val1;
    elif fml.data == 'konjunktion':
        teilformel1 = fml.children[0];
        teilformel2 = fml.children[2];
        if isinstance(teilformel1, Tree) and isinstance(teilformel2, Tree):
            val1 = rekursiv_eval(teilformel1, I);
            val2 = rekursiv_eval(teilformel2, I);
            return min(val1, val2);
    elif fml.data == 'disjunktion':
        teilformel1 = fml.children[0];
        teilformel2 = fml.children[2];
        if isinstance(teilformel1, Tree) and isinstance(teilformel2, Tree):
            val1 = rekursiv_eval(teilformel1, I);
            val2 = rekursiv_eval(teilformel2, I);
            return max(val1, val2);
    elif fml.data == 'implikation':
        teilformel1 = fml.children[0];
        teilformel2 = fml.children[2];
        if isinstance(teilformel1, Tree) and isinstance(teilformel2, Tree):
            val1 = rekursiv_eval(teilformel1, I);
            val2 = rekursiv_eval(teilformel2, I);
            return 0 if val1 == 1 and val2 == 0 else 1;
    else:
        raise Exception('Evaluation nicht möglich!');
    return True;

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# CODE AUSFÜHREN
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

if __name__ == '__main__':
    main();