"""

 Name: sml - Simple Modal Logic Lib.

 Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax.

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

 """

 import re

 def main():

     # edit your formulae here

     p = Variable(["p"])

     q = Variable(["q"])

     r = Variable(["r"])

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

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

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

     formula =  formula1 # choose your formula here

     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: \t\t", formula

     print "expanded -> and <->: \t", expand_imp_eq(formula)

     print "reduced ~: \t\t", reduce_not(expand_imp_eq(formula))

 def expand_imp_eq(formula):  

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

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

     def values():       

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

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

         return formula

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

 def reduce_not(formula):  

     negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),

               OR: lambda (a, b): And([negate(a), negate(b)]),

               VARIABLE: lambda (a,): Not([a]),

               NOT: lambda (a,): a}

     def values():

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

     def negate(f):

          return negmap[f.id](f.values)

     if not isinstance(formula, Operator):

         return formula   

     if formula.id == NOT:

         return negate(formula.values[0])

     return formula.__class__(values())

 NOT = "~"

 AND = "&"

 OR = "|"

 IMP = "->"

 EQ = "<->"

 BOX = "[]"

 DIAMOND = "<>"

 VARIABLE = "VAR"

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