1.1 --- a/smm.py Mon May 16 21:51:29 2011 +0200
1.2 +++ b/smm.py Mon May 16 22:12:54 2011 +0200
1.3 @@ -20,71 +20,72 @@
1.4 RB = ")"
1.5
1.6 class Operator(object):
1.7 - def __init__(self, id):
1.8 - self.id = id
1.9 + def __init__(self, id, values):
1.10 + self.id = id
1.11 + self.values = values
1.12 def __str__(self):
1.13 - return self.id
1.14 + values = ""
1.15 + if len(self.values):
1.16 + values = "(" + "".join([str(v) for v in self.values]) + ")"
1.17 + return self.id + values
1.18
1.19 class Not(Operator):
1.20 arity = 1
1.21 def __init__(self, values):
1.22 - Operator.__init__(self, NOT)
1.23 - self.value = values[0]
1.24 + Operator.__init__(self, NOT, values)
1.25 def __call__(self):
1.26 pass
1.27
1.28 class And(Operator):
1.29 arity = 2
1.30 def __init__(self, values):
1.31 - Operator.__init__(self, AND)
1.32 - self.value = values
1.33 -
1.34 + Operator.__init__(self, AND, values)
1.35 +
1.36 class Or(Operator):
1.37 arity = 2
1.38 def __init__(self, values):
1.39 - Operator.__init__(self, OR)
1.40 - self.value = values
1.41 + Operator.__init__(self, OR, values)
1.42 +
1.43
1.44 class Imp(Operator):
1.45 arity = 2
1.46 def __init__(self):
1.47 - Operator.__init__(self, IMP)
1.48 + Operator.__init__(self, IMP, values)
1.49
1.50 class Eq(Operator):
1.51 arity = 2
1.52 def __init__(self):
1.53 - Operator.__init__(self, EQ)
1.54 + Operator.__init__(self, EQ, values)
1.55
1.56 class Box(Operator):
1.57 arity = 1
1.58 def __init__(self, values):
1.59 - Operator.__init__(self, BOX)
1.60 - self.value = values[0]
1.61 + Operator.__init__(self, BOX, values)
1.62
1.63 class Diamond(Operator):
1.64 arity = 1
1.65 def __init__(self):
1.66 - Operator.__init__(self, DIAMOND)
1.67 + Operator.__init__(self, DIAMOND, values)
1.68
1.69 class Variable(Operator):
1.70 arity = 0
1.71 def __init__(self, values):
1.72 - Operator.__init__(self, VARIABLE)
1.73 -
1.74 + Operator.__init__(self, VARIABLE, values)
1.75 +
1.76 class Lb(Operator):
1.77 arity = -1
1.78 def __init__(self, values):
1.79 - Operator.__init__(self, LB)
1.80 + Operator.__init__(self, LB, values)
1.81
1.82 class Rb(Operator):
1.83 arity = -1
1.84 def __init__(self, values):
1.85 - Operator.__init__(self, RB)
1.86 + Operator.__init__(self, RB, values)
1.87
1.88 class Formula(object):
1.89 def __init__(self):
1.90 pass
1.91 -
1.92 +
1.93
1.94 TOKENS = {re.compile("\("): Lb,
1.95 re.compile("\)"): Rb,
1.96 @@ -170,11 +171,7 @@
1.97 (lookahead, _) = self.scanner.next()
1.98 accepted = True
1.99 while token and len(stack):
1.100 - top = stack[-1]
1.101 - #print
1.102 - #print "stack ", top
1.103 - #print "token ", token
1.104 - #print "lookahead ", lookahead
1.105 + top = stack[-1]
1.106 if top == token:
1.107 tree_nodes.append(stack.pop())
1.108 token = lookahead
1.109 @@ -184,8 +181,7 @@
1.110 if (top, token) in table:
1.111 action = table[(top, token)]
1.112 elif (top, token, lookahead) in table:
1.113 - action = table[(top, token, lookahead)]
1.114 - #print "action ", action, " replace ", self.syntax[action]
1.115 + action = table[(top, token, lookahead)]
1.116 if action is None:
1.117 accepted = False
1.118 break
1.119 @@ -194,73 +190,40 @@
1.120 stack.extend(reversed(self.syntax[action]))
1.121 accepted = accepted and not len(stack)
1.122 return (accepted, out, tree_nodes)
1.123 +
1.124 class SyntaxTree(object):
1.125 def __init__(self, tree_nodes):
1.126 - self.root = compile(tree_nodes)
1.127 + self.root = self.compile(tree_nodes)
1.128 def compile(self, tree_nodes):
1.129 table = []
1.130 unfinished = []
1.131 - for n in reversed(tree_nodes):
1.132 - if n.arity >= 0:
1.133 - print "\nt ", n
1.134 - print "arity ", n.arity
1.135 - print "table ", table
1.136 + node = None
1.137 + for n in reversed(tree_nodes):
1.138 + if n.arity >= 0:
1.139 if len(table) < n.arity:
1.140 unfinished.append(n)
1.141 else:
1.142 - args = table[:n.arity]
1.143 - print "args ", args
1.144 + args = table[:n.arity]
1.145 table = table[n.arity:]
1.146 - node = n(args)
1.147 - print "node ", node
1.148 + node = n(args)
1.149 table.append(node)
1.150 if len(unfinished) and unfinished[-1].arity <= len(table):
1.151 n = unfinished[-1]
1.152 args = table[:n.arity]
1.153 table = table[n.arity:]
1.154 - node = n(args)
1.155 + node = n(args)
1.156 table.append(node)
1.157 - unfinished.pop()
1.158 + unfinished.pop()
1.159 return table[0]
1.160
1.161 -
1.162
1.163 def main():
1.164 args = parse_arguments()
1.165 scanner = Scanner(TOKENS)
1.166 parser = Parser(SYNTAX, scanner)
1.167 (accepted, out, tree_nodes) = parser.parse(args.formula)
1.168 - print (accepted, out, tree_nodes)
1.169 - SyntaxTree tree(tree_nodes)
1.170 - print tree.root
1.171 - return
1.172 - table = []
1.173 - unfinished = []
1.174 - for t in reversed(trash):
1.175 - if t.arity >= 0:
1.176 - print "\nt ", t
1.177 - print "arity ", t.arity
1.178 - print "table ", table
1.179 - if len(table) < t.arity:
1.180 - unfinished.append(t)
1.181 - else:
1.182 - args = table[:t.arity]
1.183 - print "args ", args
1.184 - table = table[t.arity:]
1.185 -
1.186 - node = t(args)
1.187 - print "node ", node
1.188 - table.append(node)
1.189 - if len(unfinished) and unfinished[-1].arity <= len(table):
1.190 - args = table[:unfinished[-1].arity]
1.191 - print "unfinished args ", args
1.192 - table = table[unfinished[-1].arity:]
1.193 - node = unfinished[-1](args)
1.194 - print "unfinished node ", node
1.195 - table.append(node)
1.196 - unfinished.pop()
1.197 -
1.198 - print "\n", table
1.199 + tree = SyntaxTree(tree_nodes)
1.200 + print tree.root
1.201
1.202 from argparse import ArgumentParser
1.203