import astunparse
import ast
import random
import string
from plyxproto.parser import *
import pdb

BINOPS = ['|', '&', '=>']
QUANTS = ['exists', 'forall']


class PolicyException(Exception):
    pass


class AutoVariable:
    def __init__(self, base):
        self.base = base

    def __iter__(self):
        self.idx = 0
        return self

    def next(self):
        var = 'i%d' % self.idx
        self.idx += 1
        return var


def gen_random_string():
    return ''.join(random.choice(string.ascii_lowercase + string.digits) for _ in range(5))


class FOL2Python:
    def __init__(self, context_map=None):
        # This will produce i0, i1, i2 etc.
        self.loopvar = iter(AutoVariable('i'))
        self.verdictvar = iter(AutoVariable('result'))

        self.loop_variable = self.loopvar.next()
        self.verdict_variable = self.verdictvar.next()
        self.context_map = context_map

        if not self.context_map:
            self.context_map = {'user': 'self', 'obj': 'obj'}

    def loop_next(self):
        self.loop_variable = self.loopvar.next()

    def verdict_next(self):
        self.verdict_variable = self.verdictvar.next()

    def gen_enumerate(self, fol):
        pass

    def format_term_for_query(self, model, term, django=False):
        if term.startswith(model + '.'):
            term = term[len(model) + 1:]
            if django:
                term = term.replace('.', '__')
            else:
                term = '__elt' + '.' + term
        return term

    def fol_to_python_filter(self, model, e, django=False, negate=False):
        try:
            (k, v), = e.items()
        except AttributeError:
            return [self.format_term_for_query(model, e)]

        if django:
            if negate:
                # De Morgan's negation
                q_bracket = '~Q(%s)'
                or_expr = ','
                and_expr = '|'
            else:
                q_bracket = 'Q(%s)'
                or_expr = '|'
                and_expr = ','
        else:
            if negate:
                # De Morgan's negation
                q_bracket = 'not %s'
                or_expr = ' and '
                and_expr = ' or '
            else:
                q_bracket = '%s'
                or_expr = ' or '
                and_expr = ' and '

        if k == '=':
            v = [self.format_term_for_query(
                model, term, django=django) for term in v]
            if django:
                operator = ' = '
            else:
                operator = ' == '
            return [q_bracket % operator.join(v)]
        elif k == '|':
            components = [self.fol_to_python_filter(
                model, x, django=django).pop() for x in v]
            return [or_expr.join(components)]
        elif k == '&':
            components = [self.fol_to_python_filter(
                model, x, django=django).pop() for x in v]
            return [and_expr.join(components)]
        elif k == '=>':
            components = [self.fol_to_python_filter(
                model, x, django=django).pop() for x in v]
            return ['~%s | %s' % (components[0], components[1])]

    """ Convert a single leaf node from a string
        to an AST"""

    def str_to_ast(self, s):
        ast_module = ast.parse(s)
        return ast_module.body[0]

    def hoist_constants(self, fol, var=None):
        try:
            (k, v), = fol.items()
        except AttributeError:
            k = 'term'
            v = fol

        if k == 'python':
            # Tainted, don't optimize
            if var:
                return {'hoist': []}
            else:
                return fol

        if var:
            if k == 'term':
                if not v.startswith(var):
                    return {'hoist': ['const', fol], 'result': 'True'}
                else:
                    return {'hoist': [], 'result': fol}
            elif k == '=':
                lhs, rhs = v
                if not lhs.startswith(var) and not rhs.startswith(var):
                    return {'hoist': ['=', fol], 'result': 'True'}  # XXX
                else:
                    return {'hoist': [], 'result': fol}
            elif k in BINOPS:
                lhs, rhs = v
                rlhs = self.hoist_constants(lhs, var)
                rrhs = self.hoist_constants(rhs, var)

                if rlhs['hoist'] and rrhs['hoist']:
                    return {'hoist': ['=', fol], 'result': 'True'}
                elif rlhs['hoist']:
                    return {'hoist': [k, lhs], 'result': rhs}
                elif rrhs['hoist']:
                    return {'hoist': [k, rhs], 'result': lhs}
                else:
                    return {'hoist': [], 'result': fol}

            elif k in QUANTS:
                var2, expr = v
                result = self.hoist_constants(expr, var2)
                if result['hoist']:
                    if result['result'] == 'True':
                        return {'hoist': ['const'], 'result': result['hoist'][1]}
                    elif result['hoist'][0] in BINOPS:
                        return {'hoist': ['const'], 'result': {result['hoist'][0]: [result['hoist'][1], {k: [var2, result['result']]}]}}
                    else:
                        return {'hoist': ['const'], 'result': {k: [var2, result['result']]}}
                else:
                    result = self.hoist_constants(expr, var)
                    if result['result'] == 'True':
                        return {'hoist': ['&', fol], 'result': 'True'}
                    else:
                        return {'hoist': [], 'result': fol}
            else:
                return {'hoist': [], 'result': fol}
        else:
            if k in BINOPS:
                lhs, rhs = v
                rlhs = self.hoist_constants(lhs)
                rrhs = self.hoist_constants(rhs)
                return {k: [rlhs, rrhs]}
            elif k in QUANTS:
                var, expr = v
                result = self.hoist_constants(expr, var)
                if result['hoist']:
                    if result['result'] == 'True':
                        return result['hoist'][1]
                    elif result['hoist'][0] in BINOPS:
                        return {result['hoist'][0]: [result['hoist'][1], {k: [var, result['result']]}]}
                    else:
                        return {k: [var, result['result']]}
                else:
                    return fol
            else:
                return fol

    def gen_test_function(self, fol, policy_name, tag):
        if not tag:
            tag = gen_random_string()

        policy_function_name = 'policy_%(policy_name)s_%(random_string)s' % {
            'policy_name': policy_name, 'random_string': tag}
        self.verdict_next()
        function_str = """
def %(fn_name)s(obj, ctx):
    return %(vvar)s
        """ % {'fn_name': policy_function_name, 'vvar': self.verdict_variable}

        function_ast = self.str_to_ast(function_str)
        policy_code = self.gen_test(fol, self.verdict_variable)

        function_ast.body = [policy_code] + function_ast.body

        return astunparse.unparse(function_ast)

    def gen_test(self, fol, verdict_var, bindings=None):
        if isinstance(fol, str):
            return self.str_to_ast('%(verdict_var)s = %(constant)s' % {'verdict_var': verdict_var, 'constant': fol})

        (k, v), = fol.items()

        if k == '=':
            # This is the simplest case, we don't recurse further
            # To use terms that are not simple variables, use
            # the Python escape, e.g. {{ slice.creator is not None }}
            lhs, rhs = v

            assignments = []

            try:
                for t in lhs, rhs:
                    py_expr = t['python']

                    self.verdict_next()
                    vv = self.verdict_variable

                    try:
                        expr_ast = self.str_to_ast(py_expr)
                    except SyntaxError:
                        raise PolicyException('Syntax error in %s' % v)

                    if not isinstance(expr_ast, ast.Expr):
                        raise PolicyException(
                            '%s is not an expression' % expr_ast)

                    assignment_str = """
%(verdict_var)s = (%(escape_expr)s)
                    """ % {'verdict_var': vv, 'escape_expr': py_expr}

                    if t == lhs:
                        lhs = vv
                    else:
                        rhs = vv

                    assignment_ast = self.str_to_ast(assignment_str)
                    assignments.append(assignment_ast)
            except TypeError:
                pass

            comparison_str = """
%(verdict_var)s = (%(lhs)s == %(rhs)s)
            """ % {'verdict_var': verdict_var, 'lhs': lhs, 'rhs': rhs}

            comparison_ast = self.str_to_ast(comparison_str)

            combined_ast = ast.Module(body=assignments + [comparison_ast])
            return combined_ast
        elif k in BINOPS:
            lhs, rhs = v

            top_vvar = self.verdict_variable

            self.verdict_next()
            lvar = self.verdict_variable

            self.verdict_next()
            rvar = self.verdict_variable

            lblock = self.gen_test(lhs, lvar)
            rblock = self.gen_test(rhs, rvar)

            invert = ''
            if k == '&':
                binop = 'and'
            elif k == '|':
                binop = 'or'
            elif k == '=>':
                binop = 'or'
                invert = 'not'

            binop_str = """
%(verdict_var)s = %(invert)s %(lvar)s %(binop)s %(rvar)s
            """ % {'verdict_var': top_vvar, 'invert': invert, 'lvar': lvar, 'binop': binop, 'rvar': rvar}

            binop_ast = self.str_to_ast(binop_str)

            combined_ast = ast.Module(body=[lblock, rblock, binop_ast])
            return combined_ast
        elif k == 'exists':
            # If the variable starts with a capital letter,
            # we assume that it is a model. If it starts with
            # a small letter, we assume it is an enumerable
            #
            # We do not support nested exists yet. FIXME.

            var, expr = v

            if var.istitle():
                f = self.fol_to_python_filter(var, expr, django=True)
                entry = f.pop()

                python_str = """
%(verdict_var)s = %(model)s.objects.filter(%(query)s)[0]
                """ % {'verdict_var': verdict_var, 'model': var, 'query': entry}

                python_ast = ast.parse(python_str)
            else:
                f = self.fol_to_python_filter(var, expr, django=False)
                entry = f.pop()

                python_str = """
%(verdict_var)s = filter(lambda __elt:%(query)s, %(model)s)
                """ % {'verdict_var': verdict_var, 'model': var, 'query': entry}

                python_ast = ast.parse(python_str)

            return python_ast
        elif k=='forall':
            var, expr = v

            if var.istitle():
                f = self.fol_to_python_filter(var, expr, django=True, negate = True)
                entry = f.pop()

                self.verdict_next()
                vvar = self.verdict_variable

                python_str = """
%(verdict_var)s = %(model)s.objects.filter(%(query)s)[0]
                """ % {'verdict_var': vvar, 'model': var, 'query': entry}

                python_ast = ast.parse(python_str)
            else:
                f = self.fol_to_python_filter(var, expr, django=False, negate = True)
                entry = f.pop()

                python_str = """
%(verdict_var)s = next(elt for elt in %(model)s if %(query)s)
                """ % {'verdict_var': vvar, 'model': var, 'query': entry}

                python_ast = ast.parse(python_str)

            negate_str = """
%(verdict_var)s = not %(vvar)s
            """ % {'verdict_var': verdict_var, 'vvar': vvar}

            negate_ast = ast.parse(negate_str)

            return ast.Module(body=[python_ast, negate_ast])

def xproto_fol_to_python_test(fol, model, tag=None):
    f2p = FOL2Python()
    fol = f2p.hoist_constants(fol)
    a = f2p.gen_test_function(fol, 'output', tag)
    return a


def main():
    while True:
        inp = raw_input()
        fol_lexer = lex.lex(module=FOLLexer())
        fol_parser = yacc.yacc(module=FOLParser(), start='goal')

        val = fol_parser.parse(inp, lexer=fol_lexer)
        a = xproto_fol_to_python_test(val, 'output')
        print a


if __name__ == "__main__":
    main()