sawine@12: """
sawine@12: Name: 
sawine@12: 
sawine@12: Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>
sawine@12: """
sawine@12: from os import path
sawine@12: import os
sawine@12: import re
sawine@12: import token
sawine@12: 
sawine@12: def main():
sawine@12:     p = Variable(["p"])
sawine@12:     q = Variable(["q"])
sawine@12:     r = Variable(["r"])
sawine@12:     formula1 = Imp([Eq([p, q]), r])
sawine@12:     formula2 = Not([Or([p, q])])
sawine@12:     formula3 = Not([Not([p])])
sawine@12:     use = formula1
sawine@12: 
sawine@12:     args = parse_arguments()
sawine@12:     if (args.formula):
sawine@12:         scanner = Scanner(TOKENS)
sawine@12:         parser = Parser(SYNTAX, scanner)
sawine@12:         (accepted, out, tree_nodes) = parser.parse(args.formula)
sawine@12:         if not accepted:
sawine@12:             print EXCUSE 
sawine@12:             return
sawine@12:         tree = SyntaxTree(out, tree_nodes) 
sawine@12:         formula = tree.root
sawine@12:    
sawine@12:     print formula
sawine@12:     print "reduced"
sawine@12:     print reduce(formula)
sawine@12:     print reduce(formula)
sawine@12: 
sawine@12: def reduce(formula):  
sawine@12:     map = {IMP: lambda (a, b): Or([Not([a]), b]),
sawine@12:            EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])]),
sawine@12:            NOT: lambda (a,): not isinstance(a, Not) 
sawine@12:            and not isinstance(a.values[0], Not) 
sawine@12:            and a.__class__([Not([v]) for v in a.values]) or a.values[0],
sawine@12:            AND: lambda (a, b): And([a, b]), 
sawine@12:            OR: lambda (a, b): Or([a, b])}
sawine@12:     def values():       
sawine@12:         return [reduce(v) for v in formula.values] 
sawine@12: 
sawine@12:     if not isinstance(formula, Operator) or formula.id not in map:       
sawine@12:         return formula
sawine@12:     return map[formula.id](values())    
sawine@12:  
sawine@12: NOT = "~"
sawine@12: AND = "&"
sawine@12: OR = "|"
sawine@12: IMP = "->"
sawine@12: EQ = "<->"
sawine@12: BOX = "[]"
sawine@12: DIAMOND = "<>"
sawine@12: VARIABLE = "p"
sawine@12: LB = "("
sawine@12: RB = ")"
sawine@12: 
sawine@12: class Operator(object):
sawine@12:     def __init__(self, id, arity, values):
sawine@12:         self.id = id         
sawine@12:         self.arity = arity
sawine@12:         self.values = values
sawine@12:     def __str__(self):
sawine@12:         out = self.id
sawine@12:         if self.arity == 0:
sawine@12:             out = str(self.values[0])
sawine@12:         if self.arity == 1:
sawine@12:             out = self.id + str(self.values[0])
sawine@12:         elif self.arity  == 2:          
sawine@12:             out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"
sawine@12:         return out
sawine@12: 
sawine@12: class Not(Operator):
sawine@12:     arity = 1
sawine@12:     def __init__(self, values):
sawine@12:         Operator.__init__(self, NOT, Not.arity, values)       
sawine@12:     def __call__(self):
sawine@12:         pass
sawine@12: 
sawine@12: class And(Operator):
sawine@12:     arity = 2
sawine@12:     def __init__(self, values):
sawine@12:         Operator.__init__(self, AND, And.arity, values)
sawine@12:        
sawine@12: class Or(Operator):
sawine@12:     arity = 2
sawine@12:     def __init__(self, values):
sawine@12:         Operator.__init__(self, OR, Or.arity, values)       
sawine@12: 
sawine@12: class Imp(Operator):
sawine@12:     arity = 2
sawine@12:     def __init__(self, values):
sawine@12:         Operator.__init__(self, IMP, Imp.arity, values)
sawine@12:     
sawine@12: class Eq(Operator):
sawine@12:     arity = 2
sawine@12:     def __init__(self, values):
sawine@12:         Operator.__init__(self, EQ, Eq.arity, values)
sawine@12:     
sawine@12: class Box(Operator):
sawine@12:     arity = 1
sawine@12:     def __init__(self, values):
sawine@12:         Operator.__init__(self, BOX, Box.arity, values)
sawine@12: 
sawine@12: class Diamond(Operator):
sawine@12:     arity = 1
sawine@12:     def __init__(self, values):
sawine@12:         Operator.__init__(self, DIAMOND, Diamond.arity, values)
sawine@12:     
sawine@12: class Variable(Operator):
sawine@12:     arity = 0
sawine@12:     def __init__(self, values):
sawine@12:         Operator.__init__(self, VARIABLE, Variable.arity, values)   
sawine@12: 
sawine@12: class Lb(Operator):
sawine@12:     arity = -1
sawine@12:     def __init__(self, values):
sawine@12:         Operator.__init__(self, LB, Lb.arity, values)
sawine@12: 
sawine@12: class Rb(Operator):
sawine@12:     arity = -1
sawine@12:     def __init__(self, values):
sawine@12:         Operator.__init__(self, RB, Rb.arity, values)
sawine@12: 
sawine@12: class Formula(object):
sawine@12:     def __init__(self):
sawine@12:         pass 
sawine@12: 
sawine@12: TOKENS = {re.compile("\("): Lb,
sawine@12:           re.compile("\)"): Rb,
sawine@12:           re.compile("~"): Not,
sawine@12:           re.compile("&"): And,
sawine@12:           re.compile("\|"): Or,
sawine@12:           re.compile("->"): Imp,
sawine@12:           re.compile("<->"): Eq,
sawine@12:           re.compile("\[\]"): Box,
sawine@12:           re.compile("<>"): Diamond,
sawine@12:           re.compile("[a-z]+"): Variable}
sawine@12:          
sawine@12: class Scanner(object):
sawine@12:     def __init__(self, tokens, source=None):
sawine@12:         self.tokens = tokens
sawine@12:         self.reset(source)
sawine@12:     def next(self):         
sawine@12:         while self.i < len(self.source):
sawine@12:             re.purge()
sawine@12:             for p, token in self.tokens.iteritems():
sawine@12:                 m = p.match(self.source[self.i:])               
sawine@12:                 if m:                  
sawine@12:                     self.i += m.end(0)
sawine@12:                     value = m.group(0)  
sawine@12:                     return (token, value)
sawine@12:             self.i += 1
sawine@12:         return (None, None)
sawine@12:     def reset(self, source):
sawine@12:         self.i = 0
sawine@12:         self.source = source
sawine@12: 
sawine@12: S = Formula
sawine@12: A = "A"
sawine@12: #0 S: (Variable,),
sawine@12: #1 S: (Not, S),
sawine@12: #2 S: (Lb, A, Rb),
sawine@12: #3 S: (Box, S),
sawine@12: #4 S: (Diamond, S),
sawine@12: #5 A: (S, And, S),
sawine@12: #6 A: (S, Or, S),
sawine@12: #7 A: (S, Imp, S),
sawine@12: #8 A: (S, Eq, S)
sawine@12: SYNTAX = ((Variable,),
sawine@12:           (Not, S),
sawine@12:           (Lb, A, Rb),
sawine@12:           (Box, S),
sawine@12:           (Diamond, S),
sawine@12:           (S, And, S),
sawine@12:           (S, Or, S),
sawine@12:           (S, Imp, S),
sawine@12:           (S, Eq, S))
sawine@12: 
sawine@12: class Node(object):
sawine@12:     def __init__(self, parent, value):
sawine@12:         self.parent = parent
sawine@12:         self.value = value
sawine@12:         self.children = []
sawine@12:     def addChild(self, value):
sawine@12:         self.children.append(self, node)
sawine@12: 
sawine@12: class Parser(object):
sawine@12:     def __init__(self, syntax, scanner):
sawine@12:         self.syntax = syntax
sawine@12:         self.scanner = scanner
sawine@12:     def parse(self, source):
sawine@12:         table = {(S, Variable): 0,
sawine@12:                  (S, Not): 1,
sawine@12:                  (S, Lb): 2,
sawine@12:                  (S, Box): 3,
sawine@12:                  (S, Diamond): 4,
sawine@12:                  (A, S, And): 5,
sawine@12:                  (A, S, Or): 6,
sawine@12:                  (A, S, Imp): 7,
sawine@12:                  (A, S, Eq): 8,
sawine@12:                  (A, Variable, And): 5,
sawine@12:                  (A, Variable, Or): 6,
sawine@12:                  (A, Variable, Imp): 7,
sawine@12:                  (A, Variable, Eq): 8,
sawine@12:                  (A, Not, Variable, And): 5,
sawine@12:                  (A, Not, Variable, Or): 6,
sawine@12:                  (A, Not, Variable, Imp): 7,
sawine@12:                  (A, Not, Variable, Eq): 8}
sawine@12:         stack = [S]
sawine@12:         tree_nodes = []
sawine@12:         tree = None
sawine@12:         out = []
sawine@12:         self.scanner.reset(source)
sawine@12:         (token, value) = self.scanner.next()
sawine@12:         (lookahead, la_value) = self.scanner.next()
sawine@12:         (lookahead2, la2_value) = self.scanner.next()
sawine@12:         accepted = True 
sawine@12:         while token and len(stack): 
sawine@12:             top = stack[-1]               
sawine@12:             if top == token:
sawine@12:                 tree_nodes.append((token, value))
sawine@12:                 stack.pop()
sawine@12:                 #tree_nodes.append((stack.pop(), value))
sawine@12:                 (token, value) = (lookahead, la_value)
sawine@12:                 (lookahead, la_value) = (lookahead2, la2_value)
sawine@12:                 #(lookahead, _) = self.scanner.next()
sawine@12:                 (lookahead2, la2_value) = self.scanner.next()
sawine@12:             else:
sawine@12:                 action = None
sawine@12:                 if (top, token) in table:
sawine@12:                     action = table[(top, token)]
sawine@12:                 elif (top, token, lookahead) in table:
sawine@12:                     action = table[(top, token, lookahead)]  
sawine@12:                 elif (top, token, lookahead, lookahead2) in table:
sawine@12:                     action = table[(top, token, lookahead, lookahead2)]    
sawine@12:                 if action is None:
sawine@12:                     accepted = False
sawine@12:                     break
sawine@12:                 
sawine@12:                 out.append(action)
sawine@12:                 stack.pop()
sawine@12:                 stack.extend(reversed(self.syntax[action]))
sawine@12:         accepted = accepted and not len(stack)
sawine@12:         return (accepted, out, tree_nodes) 
sawine@12: 
sawine@12: class SyntaxTree(object):
sawine@12:     def __init__(self, seq, tree_nodes):
sawine@12:         seq.reverse()
sawine@12:         tree_nodes.reverse()      
sawine@12:         self.root = self.compile(seq, tree_nodes)[0]       
sawine@12:     def compile(self, seq, tree_nodes):
sawine@12:         stack = []     
sawine@12:         while len(seq):           
sawine@12:             s = seq.pop()
sawine@12:             if s == 0:
sawine@12:                 c, v = tree_nodes.pop()
sawine@12:                 while c != Variable:
sawine@12:                     c, v = tree_nodes.pop()
sawine@12:                 stack.append(Variable(v))
sawine@12:             elif s == 1:
sawine@12:                 stack.append(Not(self.compile(seq, tree_nodes)))
sawine@12:             elif s == 2:
sawine@12:                 stack.extend(self.compile(seq, tree_nodes))
sawine@12:             elif s == 3:
sawine@12:                 stack.append(Box(self.compile(seq, tree_nodes)))
sawine@12:             elif s == 4:
sawine@12:                 stack.append(Diamond(self.compile(seq, tree_nodes)))
sawine@12:             elif s == 5:
sawine@12:                 stack.append(And(self.compile(seq, tree_nodes)))
sawine@12:             elif s == 6:
sawine@12:                 stack.append(Or(self.compile(seq, tree_nodes)))
sawine@12:             elif s == 7:
sawine@12:                 stack.append(Imp(self.compile(seq, tree_nodes)))
sawine@12:             elif s == 8:
sawine@12:                 stack.append(Eq(self.compile(seq, tree_nodes)))       
sawine@12:         return stack   
sawine@12: 
sawine@12: from argparse import ArgumentParser
sawine@12: 
sawine@12: def parse_arguments():
sawine@12:     parser = ArgumentParser(description="Parses simple modal logic syntax.")
sawine@12:     parser.add_argument("-f", "--formula", help="your formula") 
sawine@12:     return parser.parse_args()
sawine@12:  
sawine@12: 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."""
sawine@12: 
sawine@12: if __name__ == "__main__":
sawine@12:     main()