1.1 --- a/smm.py Tue May 17 16:08:04 2011 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,293 +0,0 @@
1.4 -"""
1.5 -Name:
1.6 -
1.7 -Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>
1.8 -"""
1.9 -from os import path
1.10 -import os
1.11 -import re
1.12 -import token
1.13 -
1.14 -def main():
1.15 - p = Variable(["p"])
1.16 - q = Variable(["q"])
1.17 - r = Variable(["r"])
1.18 - formula1 = Imp([Eq([p, q]), r])
1.19 - formula2 = Not([Or([p, q])])
1.20 - formula3 = Not([Not([p])])
1.21 - use = formula1
1.22 -
1.23 - args = parse_arguments()
1.24 - if (args.formula):
1.25 - scanner = Scanner(TOKENS)
1.26 - parser = Parser(SYNTAX, scanner)
1.27 - (accepted, out, tree_nodes) = parser.parse(args.formula)
1.28 - if not accepted:
1.29 - print EXCUSE
1.30 - return
1.31 - tree = SyntaxTree(out, tree_nodes)
1.32 - formula = tree.root
1.33 -
1.34 - print formula
1.35 - print "reduced"
1.36 - print reduce(formula)
1.37 - print reduce(formula)
1.38 -
1.39 -def reduce(formula):
1.40 - map = {IMP: lambda (a, b): Or([Not([a]), b]),
1.41 - EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])]),
1.42 - NOT: lambda (a,): not isinstance(a, Not)
1.43 - and not isinstance(a.values[0], Not)
1.44 - and a.__class__([Not([v]) for v in a.values]) or a.values[0],
1.45 - AND: lambda (a, b): And([a, b]),
1.46 - OR: lambda (a, b): Or([a, b])}
1.47 - def values():
1.48 - return [reduce(v) for v in formula.values]
1.49 -
1.50 - if not isinstance(formula, Operator) or formula.id not in map:
1.51 - return formula
1.52 - return map[formula.id](values())
1.53 -
1.54 -NOT = "~"
1.55 -AND = "&"
1.56 -OR = "|"
1.57 -IMP = "->"
1.58 -EQ = "<->"
1.59 -BOX = "[]"
1.60 -DIAMOND = "<>"
1.61 -VARIABLE = "p"
1.62 -LB = "("
1.63 -RB = ")"
1.64 -
1.65 -class Operator(object):
1.66 - def __init__(self, id, arity, values):
1.67 - self.id = id
1.68 - self.arity = arity
1.69 - self.values = values
1.70 - def __str__(self):
1.71 - out = self.id
1.72 - if self.arity == 0:
1.73 - out = str(self.values[0])
1.74 - if self.arity == 1:
1.75 - out = self.id + str(self.values[0])
1.76 - elif self.arity == 2:
1.77 - out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"
1.78 - return out
1.79 -
1.80 -class Not(Operator):
1.81 - arity = 1
1.82 - def __init__(self, values):
1.83 - Operator.__init__(self, NOT, Not.arity, values)
1.84 - def __call__(self):
1.85 - pass
1.86 -
1.87 -class And(Operator):
1.88 - arity = 2
1.89 - def __init__(self, values):
1.90 - Operator.__init__(self, AND, And.arity, values)
1.91 -
1.92 -class Or(Operator):
1.93 - arity = 2
1.94 - def __init__(self, values):
1.95 - Operator.__init__(self, OR, Or.arity, values)
1.96 -
1.97 -class Imp(Operator):
1.98 - arity = 2
1.99 - def __init__(self, values):
1.100 - Operator.__init__(self, IMP, Imp.arity, values)
1.101 -
1.102 -class Eq(Operator):
1.103 - arity = 2
1.104 - def __init__(self, values):
1.105 - Operator.__init__(self, EQ, Eq.arity, values)
1.106 -
1.107 -class Box(Operator):
1.108 - arity = 1
1.109 - def __init__(self, values):
1.110 - Operator.__init__(self, BOX, Box.arity, values)
1.111 -
1.112 -class Diamond(Operator):
1.113 - arity = 1
1.114 - def __init__(self, values):
1.115 - Operator.__init__(self, DIAMOND, Diamond.arity, values)
1.116 -
1.117 -class Variable(Operator):
1.118 - arity = 0
1.119 - def __init__(self, values):
1.120 - Operator.__init__(self, VARIABLE, Variable.arity, values)
1.121 -
1.122 -class Lb(Operator):
1.123 - arity = -1
1.124 - def __init__(self, values):
1.125 - Operator.__init__(self, LB, Lb.arity, values)
1.126 -
1.127 -class Rb(Operator):
1.128 - arity = -1
1.129 - def __init__(self, values):
1.130 - Operator.__init__(self, RB, Rb.arity, values)
1.131 -
1.132 -class Formula(object):
1.133 - def __init__(self):
1.134 - pass
1.135 -
1.136 -TOKENS = {re.compile("\("): Lb,
1.137 - re.compile("\)"): Rb,
1.138 - re.compile("~"): Not,
1.139 - re.compile("&"): And,
1.140 - re.compile("\|"): Or,
1.141 - re.compile("->"): Imp,
1.142 - re.compile("<->"): Eq,
1.143 - re.compile("\[\]"): Box,
1.144 - re.compile("<>"): Diamond,
1.145 - re.compile("[a-z]+"): Variable}
1.146 -
1.147 -class Scanner(object):
1.148 - def __init__(self, tokens, source=None):
1.149 - self.tokens = tokens
1.150 - self.reset(source)
1.151 - def next(self):
1.152 - while self.i < len(self.source):
1.153 - re.purge()
1.154 - for p, token in self.tokens.iteritems():
1.155 - m = p.match(self.source[self.i:])
1.156 - if m:
1.157 - self.i += m.end(0)
1.158 - value = m.group(0)
1.159 - return (token, value)
1.160 - self.i += 1
1.161 - return (None, None)
1.162 - def reset(self, source):
1.163 - self.i = 0
1.164 - self.source = source
1.165 -
1.166 -S = Formula
1.167 -A = "A"
1.168 -#0 S: (Variable,),
1.169 -#1 S: (Not, S),
1.170 -#2 S: (Lb, A, Rb),
1.171 -#3 S: (Box, S),
1.172 -#4 S: (Diamond, S),
1.173 -#5 A: (S, And, S),
1.174 -#6 A: (S, Or, S),
1.175 -#7 A: (S, Imp, S),
1.176 -#8 A: (S, Eq, S)
1.177 -SYNTAX = ((Variable,),
1.178 - (Not, S),
1.179 - (Lb, A, Rb),
1.180 - (Box, S),
1.181 - (Diamond, S),
1.182 - (S, And, S),
1.183 - (S, Or, S),
1.184 - (S, Imp, S),
1.185 - (S, Eq, S))
1.186 -
1.187 -class Node(object):
1.188 - def __init__(self, parent, value):
1.189 - self.parent = parent
1.190 - self.value = value
1.191 - self.children = []
1.192 - def addChild(self, value):
1.193 - self.children.append(self, node)
1.194 -
1.195 -class Parser(object):
1.196 - def __init__(self, syntax, scanner):
1.197 - self.syntax = syntax
1.198 - self.scanner = scanner
1.199 - def parse(self, source):
1.200 - table = {(S, Variable): 0,
1.201 - (S, Not): 1,
1.202 - (S, Lb): 2,
1.203 - (S, Box): 3,
1.204 - (S, Diamond): 4,
1.205 - (A, S, And): 5,
1.206 - (A, S, Or): 6,
1.207 - (A, S, Imp): 7,
1.208 - (A, S, Eq): 8,
1.209 - (A, Variable, And): 5,
1.210 - (A, Variable, Or): 6,
1.211 - (A, Variable, Imp): 7,
1.212 - (A, Variable, Eq): 8,
1.213 - (A, Not, Variable, And): 5,
1.214 - (A, Not, Variable, Or): 6,
1.215 - (A, Not, Variable, Imp): 7,
1.216 - (A, Not, Variable, Eq): 8}
1.217 - stack = [S]
1.218 - tree_nodes = []
1.219 - tree = None
1.220 - out = []
1.221 - self.scanner.reset(source)
1.222 - (token, value) = self.scanner.next()
1.223 - (lookahead, la_value) = self.scanner.next()
1.224 - (lookahead2, la2_value) = self.scanner.next()
1.225 - accepted = True
1.226 - while token and len(stack):
1.227 - top = stack[-1]
1.228 - if top == token:
1.229 - tree_nodes.append((token, value))
1.230 - stack.pop()
1.231 - #tree_nodes.append((stack.pop(), value))
1.232 - (token, value) = (lookahead, la_value)
1.233 - (lookahead, la_value) = (lookahead2, la2_value)
1.234 - #(lookahead, _) = self.scanner.next()
1.235 - (lookahead2, la2_value) = self.scanner.next()
1.236 - else:
1.237 - action = None
1.238 - if (top, token) in table:
1.239 - action = table[(top, token)]
1.240 - elif (top, token, lookahead) in table:
1.241 - action = table[(top, token, lookahead)]
1.242 - elif (top, token, lookahead, lookahead2) in table:
1.243 - action = table[(top, token, lookahead, lookahead2)]
1.244 - if action is None:
1.245 - accepted = False
1.246 - break
1.247 -
1.248 - out.append(action)
1.249 - stack.pop()
1.250 - stack.extend(reversed(self.syntax[action]))
1.251 - accepted = accepted and not len(stack)
1.252 - return (accepted, out, tree_nodes)
1.253 -
1.254 -class SyntaxTree(object):
1.255 - def __init__(self, seq, tree_nodes):
1.256 - seq.reverse()
1.257 - tree_nodes.reverse()
1.258 - self.root = self.compile(seq, tree_nodes)[0]
1.259 - def compile(self, seq, tree_nodes):
1.260 - stack = []
1.261 - while len(seq):
1.262 - s = seq.pop()
1.263 - if s == 0:
1.264 - c, v = tree_nodes.pop()
1.265 - while c != Variable:
1.266 - c, v = tree_nodes.pop()
1.267 - stack.append(Variable(v))
1.268 - elif s == 1:
1.269 - stack.append(Not(self.compile(seq, tree_nodes)))
1.270 - elif s == 2:
1.271 - stack.extend(self.compile(seq, tree_nodes))
1.272 - elif s == 3:
1.273 - stack.append(Box(self.compile(seq, tree_nodes)))
1.274 - elif s == 4:
1.275 - stack.append(Diamond(self.compile(seq, tree_nodes)))
1.276 - elif s == 5:
1.277 - stack.append(And(self.compile(seq, tree_nodes)))
1.278 - elif s == 6:
1.279 - stack.append(Or(self.compile(seq, tree_nodes)))
1.280 - elif s == 7:
1.281 - stack.append(Imp(self.compile(seq, tree_nodes)))
1.282 - elif s == 8:
1.283 - stack.append(Eq(self.compile(seq, tree_nodes)))
1.284 - return stack
1.285 -
1.286 -from argparse import ArgumentParser
1.287 -
1.288 -def parse_arguments():
1.289 - parser = ArgumentParser(description="Parses simple modal logic syntax.")
1.290 - parser.add_argument("-f", "--formula", help="your formula")
1.291 - return parser.parse_args()
1.292 -
1.293 -EXCUSE = """The formula was not accepted by the parser, because the parser doesn't like you or the rest of the world. It seems to have some real issues with formulae with inner nesting and generally suffers from its hasty implementation. The parser would like to thank you for your coorporation by providing the formula within the code file itself. Thank you."""
1.294 -
1.295 -if __name__ == "__main__":
1.296 - main()