import unittest

from logics.classes.propositional import Inference, Formula
from logics.classes.propositional.proof_theories import NaturalDeductionStep, NaturalDeductionRule
from logics.utils.parsers import classical_parser
from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system


class TestClassicalNaturalDeductionSystem(unittest.TestCase):
    def test_natural_deduction_rule(self):
        """Test overriding of index and len methods in NaturalDeductionRule"""
        rule = NaturalDeductionRule([
            '(...)',
            NaturalDeductionStep(Formula(['→', ['A'], ['B']])),
            '(...)',
            NaturalDeductionStep(Formula(['B']), 'E→', [0, 1])
        ])
        self.assertEqual(rule.index(NaturalDeductionStep(Formula(['B']), 'E→', [0, 1])), 1)
        self.assertEqual(len(rule), 2)

    def test_nd_system(self):
        """Test the method that tells if a step is a correct application of a rule"""

        # A correct derivation
        deriv = classical_parser.parse_derivation(
            """p; premise
            (p → q); premise
            q; E→; [1, 0]; []
            p ∧ q; I∧; [0, 2]; []""",
            natural_deduction=True)

        # Check is application of the correct rule, and a different rule
        self.assertTrue(nd_system.is_correct_application(deriv, 2, nd_system.rules['E→']))
        self.assertFalse(nd_system.is_correct_application(deriv, 2, nd_system.rules['E∧2']))
        self.assertTrue(nd_system.is_correct_application(deriv, 3, nd_system.rules['I∧']))
        self.assertFalse(nd_system.is_correct_application(deriv, 3, nd_system.rules['E→']))

        # Check is correct derivation of the correct and an incorrect inference
        i = Inference([Formula(['p']), Formula(['→', ['p'], ['q']])],
                      [Formula(['∧', ['p'], ['q']])])
        self.assertTrue(nd_system.is_correct_derivation(deriv, i))
        i2 = Inference([Formula(['p']), Formula(['→', ['p'], ['q']])],
                      [Formula(['∧', ['q'], ['p']])])
        self.assertFalse(nd_system.is_correct_derivation(deriv, i2))

        # Repeating steps should not alter the outcome (should print a warning)
        # deriv2_0 = classical_parser.parse_derivation(
        #     """p; supposition; []; [0]
        #     p; repetition; [0, 0]; [0]""",
        #     natural_deduction=True)
        # self.assertTrue(nd_system.is_correct_application(deriv2_0, 1, nd_system.rules['repetition']))

        # Test step in the future
        deriv2_1 = classical_parser.parse_derivation(
            """p; supposition; []; [0]
            p; repetition; [1]; [0]""",
            natural_deduction=True)
        deriv2_2 = classical_parser.parse_derivation(
            """p; supposition; []; [0]
            p; repetition; [2]; [0]""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_application(deriv2_1, 1, nd_system.rules['repetition']))
        self.assertFalse(nd_system.is_correct_application(deriv2_2, 1, nd_system.rules['repetition']))

        # -------------------------------------------------
        # Test incorrect use of suppositions

        # Using a step in a closed supposition
        deriv3_1 = classical_parser.parse_derivation(
            """p; supposition; []; [0]
            p; repetition; [0]; [0]
            (p → p); I→; [0, 1]; []
            p; E→; [2, 0]; []""",
            natural_deduction=True)
        # Check correct application of rep and I→
        self.assertTrue(nd_system.is_correct_application(deriv3_1, 1, nd_system.rules['repetition']))
        self.assertTrue(nd_system.is_correct_application(deriv3_1, 2, nd_system.rules['I→']))
        self.assertFalse(nd_system.is_correct_application(deriv3_1, 3, nd_system.rules['E→']))

        # Closing a supposition with a rule that does not close
        deriv3_2 = classical_parser.parse_derivation('''
            p; premise
            p; supposition; []; [1]
            p; repetition; [0]; [1]
            (p ∨ q); I∨1; [0]; []''',
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_application(deriv3_2, 3, nd_system.rules['I∨1']))

        # Closing two suppositions at once
        deriv3_3 = classical_parser.parse_derivation(
            """p; supposition; []; [0]
            p; supposition; [0]; [0, 1]
            (p → p); I→; [0, 1]; []""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_application(deriv3_3, 2, nd_system.rules['I→']))

        # Not closing a supposition with a rule that does close
        deriv3_4 = classical_parser.parse_derivation(
            """p; supposition; []; [0]
            p; repetition; [0]; [0]
            (p → p); I→; [0, 1]; [0]""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_application(deriv3_4, 2, nd_system.rules['I→']))

        # Incorrect opening of suppositions
        deriv3_5 = classical_parser.parse_derivation(
            """p; supposition; []; []""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_derivation(deriv3_5, None))
        deriv3_6 = classical_parser.parse_derivation(
            """p; premise; []; []
            q; supposition; []; [0]""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_derivation(deriv3_6, None))

        # -------------------------------------------------
        # A correct derivation using all the rules

        deriv4 = classical_parser.parse_derivation(
            """q; premise; []; []
            ~q; supposition; []; [1]
            ~q; repetition; [1]; [1]
            (q ∧ ~q); I∧; [0, 2]; [1]
            q; E∧1; [3]; [1]
            ⊥; E~; [1, 4]; [1]
            p; EFSQ; [5]; [1]
            ⊥; repetition; [5]; [1]
            ~~q; I~; [1, 7]; []
            q; ~~; [8]; []
            q; supposition; []; [10]
            q; repetition; [10]; [10]
            (q → q); I→; [10, 11]; []
            q; E→; [12, 9]; []
            (q ∨ p); I∨1; [13]; []
            (p → q); premise; []; []
            q; E∨; [14, 12, 15]; []
            """, natural_deduction=True)
        i3 = Inference([Formula(['q']), Formula(['→', ['p'], ['q']])],
                       [Formula(['q'])])
        self.assertTrue(nd_system.is_correct_derivation(deriv4, i3))

    def test_rule_order(self):
        # i1 is conjunction introduction
        i1 = Inference([Formula(['p']), Formula(['q'])],
                      [Formula(['∧', ['p'], ['q']])])

        # First derivation: standard one
        deriv1_1 = classical_parser.parse_derivation(
            """p; premise; []; []
            q; premise; []; []
            (p ∧ q); I∧; [0, 1]; []""",
            natural_deduction=True)
        self.assertTrue(nd_system.is_correct_derivation(deriv1_1, i1))

        # Second derivation: reverse on_steps order
        deriv1_2 = classical_parser.parse_derivation(
            """p; premise; []; []
            q; premise; []; []
            (p ∧ q); I∧; [1, 0]; []""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_derivation(deriv1_2, i1))

        i2 = Inference([Formula(['p']), Formula(['q'])],
                       [Formula(['∧', ['q'], ['p']])])

        # Third derivation: reverse the conjuncts
        deriv2_1 = classical_parser.parse_derivation(
            """p; premise; []; []
            q; premise; []; []
            (q ∧ p); I∧; [1, 0]; []""",
            natural_deduction=True)
        self.assertTrue(nd_system.is_correct_derivation(deriv2_1, i2))

        # Fourth derivation: reverse the conjuncts and the on_steps
        deriv2_2 = classical_parser.parse_derivation(
            """p; premise; []; []
            q; premise; []; []
            (q ∧ p); I∧; [0, 1]; []""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_derivation(deriv2_2, i2))


if __name__ == '__main__':
    unittest.main()

[((184, 4, 184, 19), 'unittest.main', 'unittest.main', ({}, {}), '()', False, 'import unittest\n'), ((25, 16, 30, 35), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((54, 19, 57, 35), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((58, 19, 61, 35), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((69, 19, 74, 35), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((81, 19, 86, 35), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((90, 19, 94, 35), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((98, 19, 102, 35), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((106, 19, 108, 35), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((110, 19, 113, 35), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((119, 17, 137, 40), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((148, 19, 152, 35), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((156, 19, 160, 35), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((167, 19, 171, 35), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((175, 19, 179, 35), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (), '', False, 'from logics.utils.parsers import classical_parser\n'), ((33, 24, 33, 91), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', ({(33, 57, 33, 62): 'deriv', (33, 64, 33, 65): '(2)', (33, 67, 33, 90): "nd_system.rules['E→']"}, {}), "(deriv, 2, nd_system.rules['E→'])", True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((34, 25, 34, 93), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', ({(34, 58, 34, 63): 'deriv', (34, 65, 34, 66): '(2)', (34, 68, 34, 92): "nd_system.rules['E∧2']"}, {}), "(deriv, 2, nd_system.rules['E∧2'])", True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((35, 24, 35, 91), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', ({(35, 57, 35, 62): 'deriv', (35, 64, 35, 65): '(3)', (35, 67, 35, 90): "nd_system.rules['I∧']"}, {}), "(deriv, 3, nd_system.rules['I∧'])", True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((36, 25, 36, 92), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', ({(36, 58, 36, 63): 'deriv', (36, 65, 36, 66): '(3)', (36, 68, 36, 91): "nd_system.rules['E→']"}, {}), "(deriv, 3, nd_system.rules['E→'])", True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((41, 24, 41, 65), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', ({(41, 56, 41, 61): 'deriv', (41, 63, 41, 64): 'i'}, {}), '(deriv, i)', True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((44, 25, 44, 67), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', ({(44, 57, 44, 62): 'deriv', (44, 64, 44, 66): 'i2'}, {}), '(deriv, i2)', True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((62, 25, 62, 101), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', ({(62, 58, 62, 66): 'deriv2_1', (62, 68, 62, 69): '(1)', (62, 71, 62, 100): "nd_system.rules['repetition']"}, {}), "(deriv2_1, 1, nd_system.rules['repetition'])", True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((63, 25, 63, 101), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', ({(63, 58, 63, 66): 'deriv2_2', (63, 68, 63, 69): '(1)', (63, 71, 63, 100): "nd_system.rules['repetition']"}, {}), "(deriv2_2, 1, nd_system.rules['repetition'])", True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((76, 24, 76, 100), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', ({(76, 57, 76, 65): 'deriv3_1', (76, 67, 76, 68): '(1)', (76, 70, 76, 99): "nd_system.rules['repetition']"}, {}), "(deriv3_1, 1, nd_system.rules['repetition'])", True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((77, 24, 77, 94), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', ({(77, 57, 77, 65): 'deriv3_1', (77, 67, 77, 68): '(2)', (77, 70, 77, 93): "nd_system.rules['I→']"}, {}), "(deriv3_1, 2, nd_system.rules['I→'])", True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((78, 25, 78, 95), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', ({(78, 58, 78, 66): 'deriv3_1', (78, 68, 78, 69): '(3)', (78, 71, 78, 94): "nd_system.rules['E→']"}, {}), "(deriv3_1, 3, nd_system.rules['E→'])", True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((87, 25, 87, 96), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', ({(87, 58, 87, 66): 'deriv3_2', (87, 68, 87, 69): '(3)', (87, 71, 87, 95): "nd_system.rules['I∨1']"}, {}), "(deriv3_2, 3, nd_system.rules['I∨1'])", True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((95, 25, 95, 95), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', ({(95, 58, 95, 66): 'deriv3_3', (95, 68, 95, 69): '(2)', (95, 71, 95, 94): "nd_system.rules['I→']"}, {}), "(deriv3_3, 2, nd_system.rules['I→'])", True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((103, 25, 103, 95), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', ({(103, 58, 103, 66): 'deriv3_4', (103, 68, 103, 69): '(2)', (103, 71, 103, 94): "nd_system.rules['I→']"}, {}), "(deriv3_4, 2, nd_system.rules['I→'])", True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((109, 25, 109, 72), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', ({(109, 57, 109, 65): 'deriv3_5', (109, 67, 109, 71): 'None'}, {}), '(deriv3_5, None)', True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((114, 25, 114, 72), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', ({(114, 57, 114, 65): 'deriv3_6', (114, 67, 114, 71): 'None'}, {}), '(deriv3_6, None)', True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((140, 24, 140, 67), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', ({(140, 56, 140, 62): 'deriv4', (140, 64, 140, 66): 'i3'}, {}), '(deriv4, i3)', True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((153, 24, 153, 69), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', ({(153, 56, 153, 64): 'deriv1_1', (153, 66, 153, 68): 'i1'}, {}), '(deriv1_1, i1)', True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((161, 25, 161, 70), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', ({(161, 57, 161, 65): 'deriv1_2', (161, 67, 161, 69): 'i1'}, {}), '(deriv1_2, i1)', True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((172, 24, 172, 69), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', ({(172, 56, 172, 64): 'deriv2_1', (172, 66, 172, 68): 'i2'}, {}), '(deriv2_1, i2)', True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((180, 25, 180, 70), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', ({(180, 57, 180, 65): 'deriv2_2', (180, 67, 180, 69): 'i2'}, {}), '(deriv2_2, i2)', True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((39, 23, 39, 37), 'logics.classes.propositional.Formula', 'Formula', ({(39, 31, 39, 36): "['p']"}, {}), "(['p'])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((39, 39, 39, 69), 'logics.classes.propositional.Formula', 'Formula', ({(39, 47, 39, 68): "['→', ['p'], ['q']]"}, {}), "(['→', ['p'], ['q']])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((40, 23, 40, 53), 'logics.classes.propositional.Formula', 'Formula', ({(40, 31, 40, 52): "['∧', ['p'], ['q']]"}, {}), "(['∧', ['p'], ['q']])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((42, 24, 42, 38), 'logics.classes.propositional.Formula', 'Formula', ({(42, 32, 42, 37): "['p']"}, {}), "(['p'])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((42, 40, 42, 70), 'logics.classes.propositional.Formula', 'Formula', ({(42, 48, 42, 69): "['→', ['p'], ['q']]"}, {}), "(['→', ['p'], ['q']])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((43, 23, 43, 53), 'logics.classes.propositional.Formula', 'Formula', ({(43, 31, 43, 52): "['∧', ['q'], ['p']]"}, {}), "(['∧', ['q'], ['p']])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((138, 24, 138, 38), 'logics.classes.propositional.Formula', 'Formula', ({(138, 32, 138, 37): "['q']"}, {}), "(['q'])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((138, 40, 138, 70), 'logics.classes.propositional.Formula', 'Formula', ({(138, 48, 138, 69): "['→', ['p'], ['q']]"}, {}), "(['→', ['p'], ['q']])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((139, 24, 139, 38), 'logics.classes.propositional.Formula', 'Formula', ({(139, 32, 139, 37): "['q']"}, {}), "(['q'])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((144, 24, 144, 38), 'logics.classes.propositional.Formula', 'Formula', ({(144, 32, 144, 37): "['p']"}, {}), "(['p'])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((144, 40, 144, 54), 'logics.classes.propositional.Formula', 'Formula', ({(144, 48, 144, 53): "['q']"}, {}), "(['q'])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((145, 23, 145, 53), 'logics.classes.propositional.Formula', 'Formula', ({(145, 31, 145, 52): "['∧', ['p'], ['q']]"}, {}), "(['∧', ['p'], ['q']])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((163, 24, 163, 38), 'logics.classes.propositional.Formula', 'Formula', ({(163, 32, 163, 37): "['p']"}, {}), "(['p'])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((163, 40, 163, 54), 'logics.classes.propositional.Formula', 'Formula', ({(163, 48, 163, 53): "['q']"}, {}), "(['q'])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((164, 24, 164, 54), 'logics.classes.propositional.Formula', 'Formula', ({(164, 32, 164, 53): "['∧', ['q'], ['p']]"}, {}), "(['∧', ['q'], ['p']])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((14, 33, 14, 63), 'logics.classes.propositional.Formula', 'Formula', ({(14, 41, 14, 62): "['→', ['A'], ['B']]"}, {}), "(['→', ['A'], ['B']])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((16, 33, 16, 47), 'logics.classes.propositional.Formula', 'Formula', ({(16, 41, 16, 46): "['B']"}, {}), "(['B'])", False, 'from logics.classes.propositional import Inference, Formula\n'), ((18, 57, 18, 71), 'logics.classes.propositional.Formula', 'Formula', ({(18, 65, 18, 70): "['B']"}, {}), "(['B'])", False, 'from logics.classes.propositional import Inference, Formula\n')]