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

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

import unittest;
from unittest import TestCase;

from aussagenlogik.schema import stringToSyntaxbaum;
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
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

#

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# TESTFALL eval(·, ·)
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

# @unittest.skip('Methode noch nicht implementiert')
class TestRekursivEval(TestCase):
    def test_literale(self):
        fml = stringToSyntaxbaum('A0');
        val = rekursivEval(fml, [ 'A0' ]);
        assert val == 1;
        fml = stringToSyntaxbaum('A0');
        val = rekursivEval(fml, []);
        assert val == 0;
        fml = stringToSyntaxbaum('! A0');
        val = rekursivEval(fml, [ 'A0' ]);
        assert val == 0;
        fml = stringToSyntaxbaum('! A0');
        val = rekursivEval(fml, []);
        assert val == 1;

    def test_complex1(self):
        fml = stringToSyntaxbaum('( ! A0 || (( A0 && A3 ) || A2 ))');
        val = rekursivEval(fml, [ 'A0', 'A2' ]);
        assert val == 1;
        val = rekursivEval(fml, [ 'A0', 'A3' ]);
        assert val == 1;
        val = rekursivEval(fml, [ 'A0' ]);
        assert val == 0;
        val = rekursivEval(fml, [ 'A4', 'A8' ]);
        assert val == 1;

    def test_complex2(self):
        fml = stringToSyntaxbaum('( ! A0 || (( A0 && A3 ) || ! A2 ))');
        val = rekursivEval(fml, [ 'A0', 'A2' ]);
        assert val == 0;
        val = rekursivEval(fml, [ 'A0', 'A3' ]);
        assert val == 1;
    pass;

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# TESTFALL Atome(·)
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

@unittest.skip('Methode noch nicht implementiert')
class TestRekursivAtoms(TestCase):
    def test_noduplicates(self):
        fml = stringToSyntaxbaum('( A4 && ( A4 || A4 ))');
        val = sorted(rekursivAtoms(fml));
        assert len([_ for _ in val if _ == 'A4']) == 1, 'Atome dürfen nicht mehrfach vorkommen!';

    def test_nononatoms(self):
        fml = stringToSyntaxbaum('( {F} || A3 )');
        val = sorted(rekursivAtoms(fml));
        assert 'F' not in val, 'Nichtatomare Formeln dürfen nicht vorkommen!';

    def test_calc1(self):
        fml = stringToSyntaxbaum('A0');
        val = sorted(rekursivAtoms(fml));
        assert val == ['A0'], 'computed {}'.format(val);

    def test_calc2(self):
        fml = stringToSyntaxbaum('((( ! A0 && A3 ) || A4 ) && A8 )');
        val = sorted(rekursivAtoms(fml));
        assert val == ['A0', 'A3', 'A4', 'A8'], 'computed {}'.format(val);
    pass;

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# TESTFALL Depth(·)
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

@unittest.skip('Methode noch nicht implementiert')
class TestRekursivDepth(TestCase):
    def test_calc1(self):
        fml = stringToSyntaxbaum('A0');
        val = rekursivDepth(fml);
        assert val == 0, 'computed {}'.format(val);

    def test_calc2(self):
        fml = stringToSyntaxbaum('!! A8');
        val = rekursivDepth(fml);
        assert val == 2, 'computed {}'.format(val);

    def test_calc3(self):
        fml = stringToSyntaxbaum('( ! A0 && A3 )');
        val = rekursivDepth(fml);
        assert val == 2, 'computed {}'.format(val);

    def test_calc4(self):
        fml = stringToSyntaxbaum('((( ! A0 && A3 ) || A4 ) && A8 )');
        val = rekursivDepth(fml);
        assert val == 4, 'computed {}'.format(val);

    def test_calc5(self):
        fml = stringToSyntaxbaum('! ((( ! A0 && A3 ) || A4 ) && A8 )');
        val = rekursivDepth(fml);
        assert val == 5, 'computed {}'.format(val);
    pass;

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# TESTFALL Länge(·)
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

@unittest.skip('Methode noch nicht implementiert')
class TestRekursivLength(TestCase):
    def test_calc1(self):
        fml = stringToSyntaxbaum('A0');
        val = rekursivLength(fml);
        assert val == 1, 'computed {}'.format(val);

    def test_calc2(self):
        fml = stringToSyntaxbaum('!! A8');
        val = rekursivLength(fml);
        assert val == 3, 'computed {}'.format(val);

    def test_calc3(self):
        fml = stringToSyntaxbaum('( ! A0 && A3 )');
        val = rekursivLength(fml);
        assert val == 4, 'computed {}'.format(val);

    def test_calc4(self):
        fml = stringToSyntaxbaum('((( ! A0 && A3 ) || A4 ) && A8 )');
        val = rekursivLength(fml);
        assert val == 8, 'computed {}'.format(val);

    def test_calc5(self):
        fml = stringToSyntaxbaum('! ((( ! A0 && A3 ) || A4 ) && A8 )');
        val = rekursivLength(fml);
        assert val == 9, 'computed {}'.format(val);
    pass;

# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# TESTFALL Anzahl Klammern(·)
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

@unittest.skip('Methode noch nicht implementiert')
class TestRekursivParentheses(TestCase):
    def test_calc1(self):
        fml = stringToSyntaxbaum('A0');
        val = rekursivParentheses(fml);
        assert val == 0, 'computed {}'.format(val);

    def test_calc2(self):
        fml = stringToSyntaxbaum('!! A8');
        val = rekursivParentheses(fml);
        assert val == 0, 'computed {}'.format(val);

    def test_calc3(self):
        fml = stringToSyntaxbaum('( ! A0 && A3 )');
        val = rekursivParentheses(fml);
        assert val == 2, 'computed {}'.format(val);

    def test_calc4(self):
        fml = stringToSyntaxbaum('((( ! A0 && A3 ) || A4 ) && A8 )');
        val = rekursivParentheses(fml);
        assert val == 6, 'computed {}'.format(val);

    def test_calc5(self):
        fml = stringToSyntaxbaum('! ((( ! A0 && A3 ) || A4 ) && A8 )');
        val = rekursivParentheses(fml);
        assert val == 6, 'computed {}'.format(val);
    pass;