1.1 --- a/smm.py Mon May 16 20:23:22 2011 +0200
1.2 +++ b/smm.py Mon May 16 21:43:50 2011 +0200
1.3 @@ -21,50 +21,73 @@
1.4
1.5 class Operator(object):
1.6 def __init__(self, id):
1.7 - self.id = id
1.8 + self.id = id
1.9 def __str__(self):
1.10 return self.id
1.11
1.12 class Not(Operator):
1.13 - def __init__(self):
1.14 + arity = 1
1.15 + def __init__(self, values):
1.16 Operator.__init__(self, NOT)
1.17 + self.value = values[0]
1.18 def __call__(self):
1.19 pass
1.20
1.21 class And(Operator):
1.22 - def __init__(self):
1.23 + arity = 2
1.24 + def __init__(self, values):
1.25 Operator.__init__(self, AND)
1.26 -
1.27 + self.value = values
1.28 +
1.29 class Or(Operator):
1.30 - def __init__(self):
1.31 + arity = 2
1.32 + def __init__(self, values):
1.33 Operator.__init__(self, OR)
1.34 -
1.35 + self.value = values
1.36 +
1.37 class Imp(Operator):
1.38 + arity = 2
1.39 def __init__(self):
1.40 Operator.__init__(self, IMP)
1.41
1.42 class Eq(Operator):
1.43 + arity = 2
1.44 def __init__(self):
1.45 Operator.__init__(self, EQ)
1.46
1.47 class Box(Operator):
1.48 - def __init__(self):
1.49 - Operator.__init__(self,BOX )
1.50 -
1.51 + arity = 1
1.52 + def __init__(self, values):
1.53 + Operator.__init__(self, BOX)
1.54 + self.value = values[0]
1.55 +
1.56 class Diamond(Operator):
1.57 + arity = 1
1.58 def __init__(self):
1.59 Operator.__init__(self, DIAMOND)
1.60
1.61 class Variable(Operator):
1.62 - def __init__(self):
1.63 + arity = 0
1.64 + def __init__(self, values):
1.65 Operator.__init__(self, VARIABLE)
1.66
1.67 +class Lb(Operator):
1.68 + arity = -1
1.69 + def __init__(self, values):
1.70 + Operator.__init__(self, LB)
1.71 +
1.72 +class Rb(Operator):
1.73 + arity = -1
1.74 + def __init__(self, values):
1.75 + Operator.__init__(self, RB)
1.76 +
1.77 class Formula(object):
1.78 - def __init__(self, f):
1.79 - self.f = f
1.80 + def __init__(self):
1.81 + pass
1.82 +
1.83
1.84 -TOKENS = {re.compile("\("): LB,
1.85 - re.compile("\)"): RB,
1.86 +TOKENS = {re.compile("\("): Lb,
1.87 + re.compile("\)"): Rb,
1.88 re.compile("~"): Not,
1.89 re.compile("&"): And,
1.90 re.compile("\|"): Or,
1.91 @@ -85,26 +108,27 @@
1.92 if m:
1.93 self.i += m.end(0)
1.94 value = m.group(0)
1.95 - return token
1.96 + return (token, value)
1.97 self.i += 1
1.98 + return (None, None)
1.99 def reset(self, source):
1.100 self.i = 0
1.101 self.source = source
1.102
1.103 S = Formula
1.104 A = "A"
1.105 -#S: (Variable,),
1.106 -#S: (Not, S),
1.107 -#S: (LB, A, RB),
1.108 -#S: (Box, S),
1.109 -#S: (Diamond, S),
1.110 -#A: (S, And, S),
1.111 -#A: (S, Or, S),
1.112 -#A: (S, Imp, S),
1.113 -#A: (S, Eq, S)
1.114 +#0 S: (Variable,),
1.115 +#1 S: (Not, S),
1.116 +#2 S: (Lb, A, Rb),
1.117 +#3 S: (Box, S),
1.118 +#4 S: (Diamond, S),
1.119 +#5 A: (S, And, S),
1.120 +#6 A: (S, Or, S),
1.121 +#7 A: (S, Imp, S),
1.122 +#8 A: (S, Eq, S)
1.123 SYNTAX = ((Variable,),
1.124 (Not, S),
1.125 - (LB, A, RB),
1.126 + (Lb, A, Rb),
1.127 (Box, S),
1.128 (Diamond, S),
1.129 (S, And, S),
1.130 @@ -112,6 +136,14 @@
1.131 (S, Imp, S),
1.132 (S, Eq, S))
1.133
1.134 +class Node(object):
1.135 + def __init__(self, parent, value):
1.136 + self.parent = parent
1.137 + self.value = value
1.138 + self.children = []
1.139 + def addChild(self, value):
1.140 + self.children.append(self, node)
1.141 +
1.142 class Parser(object):
1.143 def __init__(self, syntax, scanner):
1.144 self.syntax = syntax
1.145 @@ -119,7 +151,7 @@
1.146 def parse(self, source):
1.147 table = {(S, Variable): 0,
1.148 (S, Not): 1,
1.149 - (S, LB): 2,
1.150 + (S, Lb): 2,
1.151 (S, Box): 3,
1.152 (S, Diamond): 4,
1.153 (A, S, And): 5,
1.154 @@ -131,11 +163,12 @@
1.155 (A, Variable, Imp): 7,
1.156 (A, Variable, Eq): 8}
1.157 stack = [S]
1.158 + trash = []
1.159 out = []
1.160 self.scanner.reset(source)
1.161 - token = self.scanner.next()
1.162 - lookahead = self.scanner.next()
1.163 - accepted = True
1.164 + (token, value) = self.scanner.next()
1.165 + (lookahead, _) = self.scanner.next()
1.166 + accepted = True
1.167 while token and len(stack):
1.168 top = stack[-1]
1.169 #print
1.170 @@ -143,9 +176,9 @@
1.171 #print "token ", token
1.172 #print "lookahead ", lookahead
1.173 if top == token:
1.174 - stack.pop()
1.175 + trash.append(stack.pop())
1.176 token = lookahead
1.177 - lookahead = self.scanner.next()
1.178 + (lookahead, _) = self.scanner.next()
1.179 else:
1.180 action = None
1.181 if (top, token) in table:
1.182 @@ -159,20 +192,48 @@
1.183 out.append(action)
1.184 stack.pop()
1.185 stack.extend(reversed(self.syntax[action]))
1.186 - return (accepted and not len(stack), out)
1.187 -
1.188 + accepted = accepted and not len(stack)
1.189 + return (accepted, out, trash)
1.190
1.191
1.192 def main():
1.193 args = parse_arguments()
1.194 scanner = Scanner(TOKENS)
1.195 parser = Parser(SYNTAX, scanner)
1.196 - print parser.parse(args.formula)
1.197 + (accepted, out, trash) = parser.parse(args.formula)
1.198 + print (accepted, out, trash)
1.199 + table = []
1.200 + unfinished = []
1.201 + for t in reversed(trash):
1.202 + if t.arity >= 0:
1.203 + print "\nt ", t
1.204 + print "arity ", t.arity
1.205 + print "table ", table
1.206 + if len(table) < t.arity:
1.207 + unfinished.append(t)
1.208 + else:
1.209 + args = table[:t.arity]
1.210 + print "args ", args
1.211 + table = table[t.arity:]
1.212 +
1.213 + node = t(args)
1.214 + print "node ", node
1.215 + table.append(node)
1.216 + if len(unfinished) and unfinished[-1].arity <= len(table):
1.217 + args = table[:unfinished[-1].arity]
1.218 + print "unfinished args ", args
1.219 + table = table[unfinished[-1].arity:]
1.220 + node = unfinished[-1](args)
1.221 + print "unfinished node ", node
1.222 + table.append(node)
1.223 + unfinished.pop()
1.224 +
1.225 + print "\n", table
1.226
1.227 from argparse import ArgumentParser
1.228
1.229 def parse_arguments():
1.230 - parser = ArgumentParser(description="Parses Simple Modal Logic syntax.")
1.231 + parser = ArgumentParser(description="Parses simple modal logic syntax.")
1.232 parser.add_argument("formula", help="your formula")
1.233 return parser.parse_args()
1.234