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

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

from typing import List;

from aussagenlogik.syntaxbaum import SyntaxBaum;

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# GLOBALE KONSTANTEN
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

#

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# METHODEN
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

def rekursivEval(fml: SyntaxBaum, I: List[str]) -> int:
    subfml = fml.children;
    ########
    # FÄLLE AUS DER VORLESUNG
    ########
    # Fall Atom
    if fml.isAtom():
        name = fml.expr;
        return 1 if (name in I) else 0;
    # Fall ¬F
    elif fml.isNegation():
        val0 = rekursivEval(subfml[0], I);
        return 1 - val0;
    # Fall F1 ⋀ F2
    elif fml.isConjunction2():
        val0 = rekursivEval(subfml[0], I);
        val1 = rekursivEval(subfml[1], I);
        return min(val0, val1);
    # Fall F1 ⋁ F2
    elif fml.isDisjunction2():
        val0 = rekursivEval(subfml[0], I);
        val1 = rekursivEval(subfml[1], I);
        return max(val0, val1);
    ########
    # WEITERE FÄLLE NICHT IN VORLESUNG
    ########
    # Sonderfall: generische Formel als Variable
    if fml.isGeneric():
        name = fml.expr;
        return 1 if (name in I) else 0;
    # Sonderfall: Tautologiesymbol
    elif fml.isTautologySymbol():
        return 1;
    # Sonderfall: Kontradiktionssymbol
    elif fml.isContradictionSymbol():
        return 0;
    # Fall Implikation: F1 ⟶ F2
    elif fml.isImplication():
        val0 = rekursivEval(subfml[0], I);
        val1 = rekursivEval(subfml[1], I);
        return 0 if val0 == 1 and val1 == 0 else 1;
    # Fall F1 ⋀ F2 ⋀ ... ⋀ Fn
    elif fml.isConjunction():
        values = [rekursivEval(t, I) for t in subfml];
        return min(values);
    # Fall F1 ⋁ F2 ⋁ ... ⋁ Fn
    elif fml.isDisjunction():
        values = [rekursivEval(t, I) for t in subfml];
        return max(values);
    raise Exception('Evaluation nicht möglich!');

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

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

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

def rekursivParentheses(fml: SyntaxBaum) -> int:
    ## Herausforderung: schreibe diese Funktion!
    return 0