1.1 --- a/smm.py Mon May 16 17:10:56 2011 +0200
1.2 +++ b/smm.py Mon May 16 20:23:22 2011 +0200
1.3 @@ -15,16 +15,64 @@
1.4 EQ = "<->"
1.5 BOX = "[]"
1.6 DIAMOND = "<>"
1.7 -P = "p"
1.8 +VARIABLE = "p"
1.9 +LB = "("
1.10 +RB = ")"
1.11
1.12 -TOKENS = {re.compile("~"): NOT,
1.13 - re.compile("&"): AND,
1.14 - re.compile("\|"): OR,
1.15 - re.compile("->"): IMP,
1.16 - re.compile("<->"): EQ,
1.17 - re.compile("\[\]"): BOX,
1.18 - re.compile("<>"): DIAMOND,
1.19 - re.compile("[a-z]+"): P}
1.20 +class Operator(object):
1.21 + def __init__(self, id):
1.22 + self.id = id
1.23 + def __str__(self):
1.24 + return self.id
1.25 +
1.26 +class Not(Operator):
1.27 + def __init__(self):
1.28 + Operator.__init__(self, NOT)
1.29 + def __call__(self):
1.30 + pass
1.31 +
1.32 +class And(Operator):
1.33 + def __init__(self):
1.34 + Operator.__init__(self, AND)
1.35 +
1.36 +class Or(Operator):
1.37 + def __init__(self):
1.38 + Operator.__init__(self, OR)
1.39 +
1.40 +class Imp(Operator):
1.41 + def __init__(self):
1.42 + Operator.__init__(self, IMP)
1.43 +
1.44 +class Eq(Operator):
1.45 + def __init__(self):
1.46 + Operator.__init__(self, EQ)
1.47 +
1.48 +class Box(Operator):
1.49 + def __init__(self):
1.50 + Operator.__init__(self,BOX )
1.51 +
1.52 +class Diamond(Operator):
1.53 + def __init__(self):
1.54 + Operator.__init__(self, DIAMOND)
1.55 +
1.56 +class Variable(Operator):
1.57 + def __init__(self):
1.58 + Operator.__init__(self, VARIABLE)
1.59 +
1.60 +class Formula(object):
1.61 + def __init__(self, f):
1.62 + self.f = f
1.63 +
1.64 +TOKENS = {re.compile("\("): LB,
1.65 + re.compile("\)"): RB,
1.66 + re.compile("~"): Not,
1.67 + re.compile("&"): And,
1.68 + re.compile("\|"): Or,
1.69 + re.compile("->"): Imp,
1.70 + re.compile("<->"): Eq,
1.71 + re.compile("\[\]"): Box,
1.72 + re.compile("<>"): Diamond,
1.73 + re.compile("[a-z]+"): Variable}
1.74
1.75 class Scanner(object):
1.76 def __init__(self, tokens, source=None):
1.77 @@ -37,28 +85,89 @@
1.78 if m:
1.79 self.i += m.end(0)
1.80 value = m.group(0)
1.81 - return (token, value)
1.82 + return token
1.83 self.i += 1
1.84 def reset(self, source):
1.85 self.i = 0
1.86 self.source = source
1.87
1.88 +S = Formula
1.89 +A = "A"
1.90 +#S: (Variable,),
1.91 +#S: (Not, S),
1.92 +#S: (LB, A, RB),
1.93 +#S: (Box, S),
1.94 +#S: (Diamond, S),
1.95 +#A: (S, And, S),
1.96 +#A: (S, Or, S),
1.97 +#A: (S, Imp, S),
1.98 +#A: (S, Eq, S)
1.99 +SYNTAX = ((Variable,),
1.100 + (Not, S),
1.101 + (LB, A, RB),
1.102 + (Box, S),
1.103 + (Diamond, S),
1.104 + (S, And, S),
1.105 + (S, Or, S),
1.106 + (S, Imp, S),
1.107 + (S, Eq, S))
1.108 +
1.109 class Parser(object):
1.110 - def __init__(self, scanner):
1.111 + def __init__(self, syntax, scanner):
1.112 + self.syntax = syntax
1.113 self.scanner = scanner
1.114 def parse(self, source):
1.115 + table = {(S, Variable): 0,
1.116 + (S, Not): 1,
1.117 + (S, LB): 2,
1.118 + (S, Box): 3,
1.119 + (S, Diamond): 4,
1.120 + (A, S, And): 5,
1.121 + (A, S, Or): 6,
1.122 + (A, S, Imp): 7,
1.123 + (A, S, Eq): 8,
1.124 + (A, Variable, And): 5,
1.125 + (A, Variable, Or): 6,
1.126 + (A, Variable, Imp): 7,
1.127 + (A, Variable, Eq): 8}
1.128 + stack = [S]
1.129 + out = []
1.130 self.scanner.reset(source)
1.131 token = self.scanner.next()
1.132 - while token:
1.133 - print token
1.134 - token = self.scanner.next()
1.135 + lookahead = self.scanner.next()
1.136 + accepted = True
1.137 + while token and len(stack):
1.138 + top = stack[-1]
1.139 + #print
1.140 + #print "stack ", top
1.141 + #print "token ", token
1.142 + #print "lookahead ", lookahead
1.143 + if top == token:
1.144 + stack.pop()
1.145 + token = lookahead
1.146 + lookahead = self.scanner.next()
1.147 + else:
1.148 + action = None
1.149 + if (top, token) in table:
1.150 + action = table[(top, token)]
1.151 + elif (top, token, lookahead) in table:
1.152 + action = table[(top, token, lookahead)]
1.153 + #print "action ", action, " replace ", self.syntax[action]
1.154 + if action is None:
1.155 + accepted = False
1.156 + break
1.157 + out.append(action)
1.158 + stack.pop()
1.159 + stack.extend(reversed(self.syntax[action]))
1.160 + return (accepted and not len(stack), out)
1.161 +
1.162
1.163
1.164 def main():
1.165 args = parse_arguments()
1.166 scanner = Scanner(TOKENS)
1.167 - parser = Parser(scanner)
1.168 - parser.parse(args.formula)
1.169 + parser = Parser(SYNTAX, scanner)
1.170 + print parser.parse(args.formula)
1.171
1.172 from argparse import ArgumentParser
1.173