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

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

import os;
import sys;
# sys.tracebacklimit = 0;
from dotenv import dotenv_values;
from lark import Tree;
from textwrap import dedent;
from typing import List;

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

from aussagenlogik.schema import stringToSyntaxbaum;
from aussagenlogik.syntaxbaum import SyntaxBaum;
from aussagenlogik.rekursion import rekursivEval;
from aussagenlogik.rekursion import rekursivAtoms;
from aussagenlogik.rekursion import rekursivDepth;
from aussagenlogik.rekursion import rekursivLength;
from aussagenlogik.rekursion import rekursivParentheses;

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

DATA_ENV = "data.env"; # Pfad zu Daten.

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

def main():
    ## Daten einlesen:
    expr, I = getData();
    ## Formel in Teilformeln zerlegen:
    tree = stringToSyntaxbaum(expr);
    ## Methoden ausführen:
    results = dict(
        eval         = rekursivEval(tree, I),
        atoms        = rekursivAtoms(tree),
        depth        = rekursivDepth(tree),
        length       = rekursivLength(tree),
        nParentheses = rekursivParentheses(tree),
    );
    ## Resultate anzeigen:
    display_results(tree, I, results);
    return;

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# SONSTIGE METHODEN
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

def getData():
    data = dotenv_values(dotenv_path=DATA_ENV);
    expr = data['expr'] or '0';
    I = eval(data['interpretation'] or '[]');
    return expr, I;

def display_results(tree: SyntaxBaum, I: List[str], results: dict):
    print(dedent(
        '''
        Syntaxbaum von
        F := \033[92;1m{expr}\033[0m:
        '''.format(expr=tree.expr)
    ));
    print(tree.pretty('    '))
    print(dedent(
        '''

        Für I = [{I}] und F wie oben gilt
        eval(F, I)      = \033[94;1m{eval}\033[0m,
        \033[2matoms(F)        = \033[94;1m{atoms}\033[0m; \033[91;1m<- *\033[0m
        \033[2mdepth(F)        = \033[94;1m{depth}\033[0m; \033[91;1m<- *\033[0m
        \033[2mlength(F)       = \033[94;1m{length}\033[0m; \033[91;1m<- *\033[0m
        \033[2m#parentheses(F) = \033[94;1m{nParentheses}\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! (siehe README.md)\033[0m
        '''.format(**results, I=', '.join(I))
    ));
    return;

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

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