"""

 Name: 

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

 """

 from os import path

 import os

 import re

 import token

 def main():

     p = Variable(["p"])

     q = Variable(["q"])

     r = Variable(["r"])

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

     formula2 = Not([Or([p, q])])

     formula3 = Not([Not([p])])

     use = formula1

     args = parse_arguments()

     if (args.formula):

         scanner = Scanner(TOKENS)

         parser = Parser(SYNTAX, scanner)

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

         if not accepted:

             print EXCUSE 

             return

         tree = SyntaxTree(out, tree_nodes) 

         formula = tree.root

     print formula

     print "reduced"

     print reduce(formula)

     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:          

             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()      

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

     def compile(self, seq, tree_nodes):

         stack = []     

         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)))       

         return stack   

 from argparse import ArgumentParser

 def parse_arguments():

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

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

     return parser.parse_args()

 EXCUSE = """The formula was not accepted by the parser, because the parser doesn't like you or the rest of the world. It seems to have some real issues with formulae with inner nesting and generally suffers from its hasty implementation. The parser would like to thank you for your coorporation by providing the formula within the code file itself. Thank you."""

 if __name__ == "__main__":

     main()