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