"""

 Name: 

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

 """

 from os import path

 import os

 import re

 import token

 NOT = "~"

 AND = "&"

 OR = "|"

 IMP = "->"

 EQ = "<->"

 BOX = "[]"

 DIAMOND = "<>"

 VARIABLE = "p"

 LB = "("

 RB = ")"

 class Operator(object):

     def __init__(self, id):

         self.id = id  

     def __str__(self):

         return self.id

 class Not(Operator):

     arity = 1

     def __init__(self, values):

         Operator.__init__(self, NOT)

         self.value = values[0]

     def __call__(self):

         pass

 class And(Operator):

     arity = 2

     def __init__(self, values):

         Operator.__init__(self, AND)

         self.value = values

 class Or(Operator):

     arity = 2

     def __init__(self, values):

         Operator.__init__(self, OR)

         self.value = values

 class Imp(Operator):

     arity = 2

     def __init__(self):

         Operator.__init__(self, IMP)

 class Eq(Operator):

     arity = 2

     def __init__(self):

         Operator.__init__(self, EQ)

 class Box(Operator):

     arity = 1

     def __init__(self, values):

         Operator.__init__(self, BOX)

         self.value = values[0]

 class Diamond(Operator):

     arity = 1

     def __init__(self):

         Operator.__init__(self, DIAMOND)

 class Variable(Operator):

     arity = 0

     def __init__(self, values):

         Operator.__init__(self, VARIABLE)

 class Lb(Operator):

     arity = -1

     def __init__(self, values):

         Operator.__init__(self, LB)

 class Rb(Operator):

     arity = -1

     def __init__(self, values):

         Operator.__init__(self, RB)

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

             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}

         stack = [S]

         trash = []

         out = []

         self.scanner.reset(source)

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

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

         accepted = True      

         while token and len(stack):

             top = stack[-1]  

             #print

             #print "stack ", top

             #print "token ", token

             #print "lookahead ", lookahead            

             if top == token:

                 trash.append(stack.pop())

                 token = lookahead

                 (lookahead, _) = 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)]

                 #print "action ", action, " replace ", self.syntax[action] 

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

 def main():

     args = parse_arguments()

     scanner = Scanner(TOKENS)

     parser = Parser(SYNTAX, scanner)

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

     print (accepted, out, trash)

     table = []

     unfinished = []

     for t in reversed(trash):

         if t.arity >= 0:

             print "\nt ", t

             print "arity ", t.arity

             print "table ", table

             if len(table) < t.arity:

                 unfinished.append(t)

             else:

                 args = table[:t.arity]

                 print "args ", args

                 table = table[t.arity:]

                 node = t(args)

                 print "node ", node

                 table.append(node)

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

                 args = table[:unfinished[-1].arity]

                 print "unfinished args ", args

                 table = table[unfinished[-1].arity:]

                 node = unfinished[-1](args)

                 print "unfinished node ", node

                 table.append(node)

                 unfinished.pop()

     print "\n", table

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