1.1 --- a/smm.py Mon May 16 22:35:49 2011 +0200
1.2 +++ b/smm.py Tue May 17 02:19:11 2011 +0200
1.3 @@ -20,66 +20,73 @@
1.4 RB = ")"
1.5
1.6 class Operator(object):
1.7 - def __init__(self, id, values):
1.8 - self.id = id
1.9 + def __init__(self, id, arity, values):
1.10 + self.id = id
1.11 + self.arity = arity
1.12 self.values = values
1.13 def __str__(self):
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 + out = self.id
1.19 + if self.arity == 0:
1.20 + out = str(self.values[0])
1.21 + if self.arity == 1:
1.22 + out = self.id + str(self.values[0])
1.23 + elif self.arity == 2:
1.24 + #print self.id
1.25 + #print self.values
1.26 + out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"
1.27 + return out
1.28
1.29 class Not(Operator):
1.30 arity = 1
1.31 def __init__(self, values):
1.32 - Operator.__init__(self, NOT, values)
1.33 + Operator.__init__(self, NOT, Not.arity, values)
1.34 def __call__(self):
1.35 pass
1.36
1.37 class And(Operator):
1.38 arity = 2
1.39 def __init__(self, values):
1.40 - Operator.__init__(self, AND, values)
1.41 + Operator.__init__(self, AND, And.arity, values)
1.42
1.43 class Or(Operator):
1.44 arity = 2
1.45 def __init__(self, values):
1.46 - Operator.__init__(self, OR, values)
1.47 + Operator.__init__(self, OR, Or.arity, values)
1.48
1.49 class Imp(Operator):
1.50 arity = 2
1.51 def __init__(self, values):
1.52 - Operator.__init__(self, IMP, values)
1.53 + Operator.__init__(self, IMP, Imp.arity, values)
1.54
1.55 class Eq(Operator):
1.56 arity = 2
1.57 def __init__(self, values):
1.58 - Operator.__init__(self, EQ, values)
1.59 + Operator.__init__(self, EQ, Eq.arity, values)
1.60
1.61 class Box(Operator):
1.62 arity = 1
1.63 def __init__(self, values):
1.64 - Operator.__init__(self, BOX, values)
1.65 + Operator.__init__(self, BOX, Box.arity, values)
1.66
1.67 class Diamond(Operator):
1.68 arity = 1
1.69 def __init__(self, values):
1.70 - Operator.__init__(self, DIAMOND, values)
1.71 + Operator.__init__(self, DIAMOND, Diamond.arity, values)
1.72
1.73 class Variable(Operator):
1.74 arity = 0
1.75 def __init__(self, values):
1.76 - Operator.__init__(self, VARIABLE, values)
1.77 -
1.78 + Operator.__init__(self, VARIABLE, Variable.arity, values)
1.79 +
1.80 class Lb(Operator):
1.81 arity = -1
1.82 def __init__(self, values):
1.83 - Operator.__init__(self, LB, values)
1.84 + Operator.__init__(self, LB, Lb.arity, values)
1.85
1.86 class Rb(Operator):
1.87 arity = -1
1.88 def __init__(self, values):
1.89 - Operator.__init__(self, RB, values)
1.90 + Operator.__init__(self, RB, Rb.arity, values)
1.91
1.92 class Formula(object):
1.93 def __init__(self):
1.94 @@ -101,12 +108,13 @@
1.95 self.tokens = tokens
1.96 self.reset(source)
1.97 def next(self):
1.98 - while self.i < len(self.source):
1.99 + while self.i < len(self.source):
1.100 + re.purge()
1.101 for p, token in self.tokens.iteritems():
1.102 m = p.match(self.source[self.i:])
1.103 if m:
1.104 self.i += m.end(0)
1.105 - value = m.group(0)
1.106 + value = m.group(0)
1.107 return (token, value)
1.108 self.i += 1
1.109 return (None, None)
1.110 @@ -160,29 +168,42 @@
1.111 (A, Variable, And): 5,
1.112 (A, Variable, Or): 6,
1.113 (A, Variable, Imp): 7,
1.114 - (A, Variable, Eq): 8}
1.115 + (A, Variable, Eq): 8,
1.116 + (A, Not, Variable, And): 5,
1.117 + (A, Not, Variable, Or): 6,
1.118 + (A, Not, Variable, Imp): 7,
1.119 + (A, Not, Variable, Eq): 8}
1.120 stack = [S]
1.121 tree_nodes = []
1.122 + tree = None
1.123 out = []
1.124 self.scanner.reset(source)
1.125 (token, value) = self.scanner.next()
1.126 - (lookahead, _) = self.scanner.next()
1.127 - accepted = True
1.128 - while token and len(stack):
1.129 + (lookahead, la_value) = self.scanner.next()
1.130 + (lookahead2, la2_value) = self.scanner.next()
1.131 + accepted = True
1.132 + while token and len(stack):
1.133 top = stack[-1]
1.134 if top == token:
1.135 - tree_nodes.append(stack.pop())
1.136 - token = lookahead
1.137 - (lookahead, _) = self.scanner.next()
1.138 + tree_nodes.append((token, value))
1.139 + stack.pop()
1.140 + #tree_nodes.append((stack.pop(), value))
1.141 + (token, value) = (lookahead, la_value)
1.142 + (lookahead, la_value) = (lookahead2, la2_value)
1.143 + #(lookahead, _) = self.scanner.next()
1.144 + (lookahead2, la2_value) = self.scanner.next()
1.145 else:
1.146 action = None
1.147 if (top, token) in table:
1.148 action = table[(top, token)]
1.149 elif (top, token, lookahead) in table:
1.150 - action = table[(top, token, lookahead)]
1.151 + action = table[(top, token, lookahead)]
1.152 + elif (top, token, lookahead, lookahead2) in table:
1.153 + action = table[(top, token, lookahead, lookahead2)]
1.154 if action is None:
1.155 accepted = False
1.156 break
1.157 +
1.158 out.append(action)
1.159 stack.pop()
1.160 stack.extend(reversed(self.syntax[action]))
1.161 @@ -190,23 +211,65 @@
1.162 return (accepted, out, tree_nodes)
1.163
1.164 class SyntaxTree(object):
1.165 - def __init__(self, tree_nodes):
1.166 - self.root = self.compile(tree_nodes)
1.167 - def compile(self, tree_nodes):
1.168 + def __init__(self, seq, tree_nodes):
1.169 + seq.reverse()
1.170 + tree_nodes.reverse()
1.171 + print tree_nodes
1.172 + print seq
1.173 + self.root = self.compile(seq, tree_nodes)[0]
1.174 + print self.root
1.175 + def compile(self, seq, tree_nodes):
1.176 + stack = []
1.177 + waiting = []
1.178 + print seq
1.179 + while len(seq):
1.180 + s = seq.pop()
1.181 + if s == 0:
1.182 + c, v = tree_nodes.pop()
1.183 + while c != Variable:
1.184 + c, v = tree_nodes.pop()
1.185 + stack.append(Variable(v))
1.186 + elif s == 1:
1.187 + stack.append(Not(self.compile(seq, tree_nodes)))
1.188 + elif s == 2:
1.189 + stack.extend(self.compile(seq, tree_nodes))
1.190 + elif s == 3:
1.191 + stack.append(Box(self.compile(seq, tree_nodes)))
1.192 + elif s == 4:
1.193 + stack.append(Diamond(self.compile(seq, tree_nodes)))
1.194 + elif s == 5:
1.195 + stack.append(And(self.compile(seq, tree_nodes)))
1.196 + elif s == 6:
1.197 + stack.append(Or(self.compile(seq, tree_nodes)))
1.198 + elif s == 7:
1.199 + stack.append(Imp(self.compile(seq, tree_nodes)))
1.200 + elif s == 8:
1.201 + stack.append(Eq(self.compile(seq, tree_nodes)))
1.202 + print stack
1.203 + return stack
1.204 +
1.205 + def compile_(self, tree_nodes):
1.206 table = []
1.207 unfinished = []
1.208 node = None
1.209 - for n in reversed(tree_nodes):
1.210 + print tree_nodes
1.211 + for n, v in (tree_nodes):
1.212 + print
1.213 + print n
1.214 if n.arity >= 0:
1.215 if len(table) < n.arity:
1.216 + print "appending unfinished ", n
1.217 unfinished.append(n)
1.218 else:
1.219 - args = table[:n.arity]
1.220 + args = table[:n.arity]
1.221 + if n.arity == 0:
1.222 + args = [v]
1.223 table = table[n.arity:]
1.224 node = n(args)
1.225 table.append(node)
1.226 - if len(unfinished) and unfinished[-1].arity <= len(table):
1.227 - n = unfinished[-1]
1.228 + if len(unfinished) and unfinished[-1].arity <= len(table):
1.229 + n = unfinished[-1]
1.230 + print "finishing ", n
1.231 args = table[:n.arity]
1.232 table = table[n.arity:]
1.233 node = n(args)
1.234 @@ -220,8 +283,8 @@
1.235 scanner = Scanner(TOKENS)
1.236 parser = Parser(SYNTAX, scanner)
1.237 (accepted, out, tree_nodes) = parser.parse(args.formula)
1.238 - tree = SyntaxTree(tree_nodes)
1.239 - print tree.root
1.240 + tree = SyntaxTree(out, tree_nodes)
1.241 + #print tree.root
1.242
1.243 from argparse import ArgumentParser
1.244