"""

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

     def __init__(self):

         Operator.__init__(self, NOT)

     def __call__(self):

         pass

 class And(Operator):

     def __init__(self):

         Operator.__init__(self, AND)

 class Or(Operator):

     def __init__(self):

         Operator.__init__(self, OR)

 class Imp(Operator):

     def __init__(self):

         Operator.__init__(self, IMP)

 class Eq(Operator):

     def __init__(self):

         Operator.__init__(self, EQ)

 class Box(Operator):

     def __init__(self):

         Operator.__init__(self,BOX )

 class Diamond(Operator):

     def __init__(self):

         Operator.__init__(self, DIAMOND)

 class Variable(Operator):

     def __init__(self):

         Operator.__init__(self, VARIABLE)

 class Formula(object):

     def __init__(self, f):

         self.f = f

 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

             self.i += 1

     def reset(self, source):

         self.i = 0

         self.source = source

 S = Formula

 A = "A"

 #S: (Variable,),

 #S: (Not, S),

 #S: (LB, A, RB),

 #S: (Box, S),

 #S: (Diamond, S),

 #A: (S, And, S),

 #A: (S, Or, S),

 #A: (S, Imp, S),

 #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 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]

         out = []

         self.scanner.reset(source)

         token = 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:

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

         return (accepted and not len(stack), out)

 def main():

     args = parse_arguments()

     scanner = Scanner(TOKENS)

     parser = Parser(SYNTAX, scanner)

     print parser.parse(args.formula)

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