"""

Name: 

Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>

"""

from os import path

import os

import re

import token

def main():

    args = parse_arguments()

    scanner = Scanner(TOKENS)

    parser = Parser(SYNTAX, scanner)

    #(accepted, out, tree_nodes) = parser.parse(args.formula)

    #tree = SyntaxTree(out, tree_nodes)

    #print tree.root

    p = Variable(["p"])

    q = Variable(["q"])

    r = Variable(["r"])

    formula = Imp([Eq([p, q]), r])

    #formula = Not([Or([p, q])])

    #formula = Not([Not([p])])

    print formula

    print "reduced"

    print reduce(formula)

def reduce(formula):  

    map = {IMP: lambda (a, b): Or([Not([a]), b]),

           EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])]),

           NOT: lambda (a,): not isinstance(a, Not) 

           and not isinstance(a.values[0], Not) 

           and a.__class__([Not([v]) for v in a.values]) or a.values[0],

           AND: lambda (a, b): And([a, b]), 

           OR: lambda (a, b): Or([a, b])}

    def values():       

        return [reduce(v) for v in formula.values] 

    if not isinstance(formula, Operator) or formula.id not in map:       

        return formula

    return map[formula.id](values())    

NOT = "~"

AND = "&"

OR = "|"

IMP = "->"

EQ = "<->"

BOX = "[]"

DIAMOND = "<>"

VARIABLE = "p"

LB = "("

RB = ")"

class Operator(object):

    def __init__(self, id, arity, values):

        self.id = id         

        self.arity = arity

        self.values = values

    def __str__(self):

        out = self.id

        if self.arity == 0:

            out = str(self.values[0])

        if self.arity == 1:

            out = self.id + str(self.values[0])

        elif self.arity  == 2:

            #print self.id

            #print self.values

            out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"

        return out

class Not(Operator):

    arity = 1

    def __init__(self, values):

        Operator.__init__(self, NOT, Not.arity, values)       

    def __call__(self):

        pass

class And(Operator):

    arity = 2

    def __init__(self, values):

        Operator.__init__(self, AND, And.arity, values)

class Or(Operator):

    arity = 2

    def __init__(self, values):

        Operator.__init__(self, OR, Or.arity, values)       

class Imp(Operator):

    arity = 2

    def __init__(self, values):

        Operator.__init__(self, IMP, Imp.arity, values)

class Eq(Operator):

    arity = 2

    def __init__(self, values):

        Operator.__init__(self, EQ, Eq.arity, values)

class Box(Operator):

    arity = 1

    def __init__(self, values):

        Operator.__init__(self, BOX, Box.arity, values)

class Diamond(Operator):

    arity = 1

    def __init__(self, values):

        Operator.__init__(self, DIAMOND, Diamond.arity, values)

class Variable(Operator):

    arity = 0

    def __init__(self, values):

        Operator.__init__(self, VARIABLE, Variable.arity, values)   

class Lb(Operator):

    arity = -1

    def __init__(self, values):

        Operator.__init__(self, LB, Lb.arity, values)

class Rb(Operator):

    arity = -1

    def __init__(self, values):

        Operator.__init__(self, RB, Rb.arity, values)

class Formula(object):

    def __init__(self):

        pass 

TOKENS = {re.compile("\("): Lb,

          re.compile("\)"): Rb,

          re.compile("~"): Not,

          re.compile("&"): And,

          re.compile("\|"): Or,

          re.compile("->"): Imp,

          re.compile("<->"): Eq,

          re.compile("\[\]"): Box,

          re.compile("<>"): Diamond,

          re.compile("[a-z]+"): Variable}

class Scanner(object):

    def __init__(self, tokens, source=None):

        self.tokens = tokens

        self.reset(source)

    def next(self):         

        while self.i < len(self.source):

            re.purge()

            for p, token in self.tokens.iteritems():

                m = p.match(self.source[self.i:])               

                if m:                  

                    self.i += m.end(0)

                    value = m.group(0)  

                    return (token, value)

            self.i += 1

        return (None, None)

    def reset(self, source):

        self.i = 0

        self.source = source

S = Formula

A = "A"

#0 S: (Variable,),

#1 S: (Not, S),

#2 S: (Lb, A, Rb),

#3 S: (Box, S),

#4 S: (Diamond, S),

#5 A: (S, And, S),

#6 A: (S, Or, S),

#7 A: (S, Imp, S),

#8 A: (S, Eq, S)

SYNTAX = ((Variable,),

          (Not, S),

          (Lb, A, Rb),

          (Box, S),

          (Diamond, S),

          (S, And, S),

          (S, Or, S),

          (S, Imp, S),

          (S, Eq, S))

class Node(object):

    def __init__(self, parent, value):

        self.parent = parent

        self.value = value

        self.children = []

    def addChild(self, value):

        self.children.append(self, node)

class Parser(object):

    def __init__(self, syntax, scanner):

        self.syntax = syntax

        self.scanner = scanner

    def parse(self, source):

        table = {(S, Variable): 0,

                 (S, Not): 1,

                 (S, Lb): 2,

                 (S, Box): 3,

                 (S, Diamond): 4,

                 (A, S, And): 5,

                 (A, S, Or): 6,

                 (A, S, Imp): 7,

                 (A, S, Eq): 8,

                 (A, Variable, And): 5,

                 (A, Variable, Or): 6,

                 (A, Variable, Imp): 7,

                 (A, Variable, Eq): 8,

                 (A, Not, Variable, And): 5,

                 (A, Not, Variable, Or): 6,

                 (A, Not, Variable, Imp): 7,

                 (A, Not, Variable, Eq): 8}

        stack = [S]

        tree_nodes = []

        tree = None

        out = []

        self.scanner.reset(source)

        (token, value) = self.scanner.next()

        (lookahead, la_value) = self.scanner.next()

        (lookahead2, la2_value) = self.scanner.next()

        accepted = True 

        while token and len(stack): 

            top = stack[-1]               

            if top == token:

                tree_nodes.append((token, value))

                stack.pop()

                #tree_nodes.append((stack.pop(), value))

                (token, value) = (lookahead, la_value)

                (lookahead, la_value) = (lookahead2, la2_value)

                #(lookahead, _) = self.scanner.next()

                (lookahead2, la2_value) = self.scanner.next()

            else:

                action = None

                if (top, token) in table:

                    action = table[(top, token)]

                elif (top, token, lookahead) in table:

                    action = table[(top, token, lookahead)]  

                elif (top, token, lookahead, lookahead2) in table:

                    action = table[(top, token, lookahead, lookahead2)]    

                if action is None:

                    accepted = False

                    break

                out.append(action)

                stack.pop()

                stack.extend(reversed(self.syntax[action]))

        accepted = accepted and not len(stack)

        return (accepted, out, tree_nodes) 

class SyntaxTree(object):

    def __init__(self, seq, tree_nodes):

        seq.reverse()

        tree_nodes.reverse()

        print tree_nodes

        print seq

        self.root = self.compile(seq, tree_nodes)[0]

        print self.root

    def compile(self, seq, tree_nodes):

        stack = []

        waiting = []  

        print seq

        while len(seq):           

            s = seq.pop()

            if s == 0:

                c, v = tree_nodes.pop()

                while c != Variable:

                    c, v = tree_nodes.pop()

                stack.append(Variable(v))

            elif s == 1:

                stack.append(Not(self.compile(seq, tree_nodes)))

            elif s == 2:

                stack.extend(self.compile(seq, tree_nodes))

            elif s == 3:

                stack.append(Box(self.compile(seq, tree_nodes)))

            elif s == 4:

                stack.append(Diamond(self.compile(seq, tree_nodes)))

            elif s == 5:

                stack.append(And(self.compile(seq, tree_nodes)))

            elif s == 6:

                stack.append(Or(self.compile(seq, tree_nodes)))

            elif s == 7:

                stack.append(Imp(self.compile(seq, tree_nodes)))

            elif s == 8:

                stack.append(Eq(self.compile(seq, tree_nodes)))

        print stack

        return stack

    def compile_(self, tree_nodes):

        table = []

        unfinished = []

        node = None

        print tree_nodes

        for n, v in (tree_nodes): 

            print

            print n

            if n.arity >= 0:              

                if len(table) < n.arity:

                    print "appending unfinished ", n

                    unfinished.append(n)

                else:

                    args = table[:n.arity]

                    if n.arity == 0:

                        args = [v]

                    table = table[n.arity:]            

                    node = n(args)                                  

                    table.append(node)

                if len(unfinished) and unfinished[-1].arity <= len(table):                   

                    n = unfinished[-1] 

                    print "finishing ", n

                    args = table[:n.arity]                   

                    table = table[n.arity:]

                    node = n(args)                                          

                    table.append(node)

                    unfinished.pop()            

        return table[0]

from argparse import ArgumentParser

def parse_arguments():

    parser = ArgumentParser(description="Parses simple modal logic syntax.")

    parser.add_argument("formula", help="your formula") 

    return parser.parse_args()

if __name__ == "__main__":

    main()