import unittest
from xosgenx.jinja2_extensions.fol2 import FOL2Python
import vimpdb

class XProtoOptimizeTest(unittest.TestCase):
    def setUp(self):
        self.f2p = FOL2Python()
        self.maxDiff=None

    def test_constant(self):
        input = 'True'
        output = self.f2p.hoist_outer(input)
        self.assertEqual(output, input)

    def test_exists(self):
        input = {'exists': ['X',{'|':['X.foo','y']}]}

        output = self.f2p.hoist_outer(input)
        expected = {'|': ['y', {'&': [{'not': 'y'}, {'exists': ['X', 'X.foo']}]}]}
        self.assertEqual(output, expected)
        
    def test_exists_implies(self):
        input = {'exists': ['Foo', {'&': [{'=': ('Foo.a', '1')}, {'->': ['write_access', {'=': ('Foo.b', '1')}]}]}]}

        output = self.f2p.hoist_outer(input)
        expected = {'|': [{'&': ['write_access', {'exists': ['Foo', {'&': [{'=': ['Foo.a', '1']}, {'=': ['Foo.b', '1']}]}]}]}, {'&': [{'not': 'write_access'}, {'exists': ['Foo', {'=': ['Foo.a', '1']}]}]}]}
        self.assertEqual(output, expected)

    def test_forall(self):
        input = {'forall': ['X',{'|':['X.foo','y']}]}

        output = self.f2p.hoist_outer(input)
        expected = {'|': ['y', {'&': [{'not': 'y'}, {'forall': ['X', 'X.foo']}]}]}
        self.assertEqual(output, expected)

    def test_exists_embedded(self):
        input = {'&':['True',{'exists': ['X',{'|':['X.foo','y']}]}]}

        output = self.f2p.hoist_outer(input)
        expected = {'|': ['y', {'&': [{'not': 'y'}, {'exists': ['X', 'X.foo']}]}]}
        self.assertEqual(output, expected)
    
    def test_exists_equals(self):
        input = {'&':['True',{'exists': ['X',{'|':['X.foo',{'=':['y','z']}]}]}]}

        output = self.f2p.hoist_outer(input)
        expected = {'|': [{'=': ['y', 'z']}, {'&': [{'not': {'=': ['y', 'z']}}, {'exists': ['X', 'X.foo']}]}]}
        self.assertEqual(output, expected)

    def test_exists_nested_constant(self):
        input = {'&':['True',{'exists': ['X',{'|':['y',{'=':['y','X.foo']}]}]}]}

        output = self.f2p.hoist_outer(input)
        expected = {'|': ['y', {'&': [{'not': 'y'}, {'exists': ['X', {'=': ['False', 'X.foo']}]}]}]}
        self.assertEqual(output, expected)

    def test_exists_nested(self):
        input = {'exists': ['X',{'exists':['Y',{'=':['Y.foo','X.foo']}]}]}

        output = self.f2p.hoist_outer(input)
        expected = input
        self.assertEqual(input, output)

    def test_exists_nested2(self):
        input = {'exists': ['X',{'exists':['Y',{'=':['Z','Y']}]}]}

        output = self.f2p.hoist_outer(input)
        expected = {'exists': ['Y', {'=': ['Z', 'Y']}]}
        self.assertEqual(output, expected)

    def test_exists_nested3(self):
        input = {'exists': ['X',{'exists':['Y',{'=':['Z','X']}]}]}

        output = self.f2p.hoist_outer(input)
        expected = {'exists': ['X', {'=': ['Z', 'X']}]}
        self.assertEqual(output, expected)


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