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

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

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

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('Syntaxbaum von \033[1m{}\033[0m:\n'.format(zeichenkette));
    print(tree.pretty());
    val = rekursiv_eval(tree, I)
    print('eval(Formel, I) = \033[1m{}\033[0m'.format(val));
    return;

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

def rekursiv_eval(fml: Tree, I: List[str]) -> bool:
    if fml.data == 'atom':
        index = fml.children[0];
        return 'A{}'.format(index) in I;
    elif fml.data == 'beliebig':
        name = fml.children[0];
        return '{}'.format(name) in I;
    elif fml.data == 'wahr':
        return True;
    elif fml.data == 'falsch':
        return False;
    elif fml.data == 'negation':
        teilformel1 = fml.children[1];
        if isinstance(teilformel1, Tree):
            val1 = rekursiv_eval(teilformel1, I);
            return not 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 (val1 <= val2);
    else:
        raise Exception('Evaluation nicht möglich!');
    return True;

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

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