sawine@12
|
1 |
"""
|
sawine@13
|
2 |
Name: sml - Simple Modal Logic Lib.
|
sawine@17
|
3 |
Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax.
|
sawine@12
|
4 |
Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>
|
sawine@12
|
5 |
"""
|
sawine@12
|
6 |
import re
|
sawine@12
|
7 |
|
sawine@12
|
8 |
def main():
|
sawine@15
|
9 |
# edit your formulae here
|
sawine@12
|
10 |
p = Variable(["p"])
|
sawine@12
|
11 |
q = Variable(["q"])
|
sawine@12
|
12 |
r = Variable(["r"])
|
sawine@12
|
13 |
formula1 = Imp([Eq([p, q]), r])
|
sawine@12
|
14 |
formula2 = Not([Or([p, q])])
|
sawine@12
|
15 |
formula3 = Not([Not([p])])
|
sawine@18
|
16 |
formula = formula1 # choose your formula here
|
sawine@12
|
17 |
|
sawine@12
|
18 |
args = parse_arguments()
|
sawine@12
|
19 |
if (args.formula):
|
sawine@12
|
20 |
scanner = Scanner(TOKENS)
|
sawine@12
|
21 |
parser = Parser(SYNTAX, scanner)
|
sawine@12
|
22 |
(accepted, out, tree_nodes) = parser.parse(args.formula)
|
sawine@12
|
23 |
if not accepted:
|
sawine@12
|
24 |
print EXCUSE
|
sawine@12
|
25 |
return
|
sawine@12
|
26 |
tree = SyntaxTree(out, tree_nodes)
|
sawine@12
|
27 |
formula = tree.root
|
sawine@12
|
28 |
|
sawine@18
|
29 |
print "formula: \t\t\t", formula
|
sawine@18
|
30 |
print "expanded -> and <->: \t\t", expand_imp_eq(formula)
|
sawine@18
|
31 |
print "reduced ~: \t\t\t", de_morgan(expand_imp_eq(formula))
|
sawine@18
|
32 |
print "reduced iterated modalities: \t", reduce_iter(de_morgan(expand_imp_eq(formula)))
|
sawine@19
|
33 |
print "distributed modalities+: \t", reduce_iter(dist(reduce_iter(de_morgan(expand_imp_eq(formula)))))
|
sawine@19
|
34 |
|
sawine@19
|
35 |
def values(fun, f):
|
sawine@19
|
36 |
return [fun(v) for v in f.values]
|
sawine@12
|
37 |
|
sawine@14
|
38 |
def expand_imp_eq(formula):
|
sawine@12
|
39 |
map = {IMP: lambda (a, b): Or([Not([a]), b]),
|
sawine@19
|
40 |
EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}
|
sawine@12
|
41 |
if not isinstance(formula, Operator) or formula.id not in map:
|
sawine@12
|
42 |
return formula
|
sawine@19
|
43 |
return map[formula.id](values(expand_imp_eq, formula))
|
sawine@14
|
44 |
|
sawine@18
|
45 |
def de_morgan(formula):
|
sawine@14
|
46 |
negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),
|
sawine@14
|
47 |
OR: lambda (a, b): And([negate(a), negate(b)]),
|
sawine@18
|
48 |
BOX: lambda (a,): Diamond([negate(a)]),
|
sawine@18
|
49 |
DIAMOND: lambda (a,): Box([negate(a)]),
|
sawine@14
|
50 |
VARIABLE: lambda (a,): Not([a]),
|
sawine@19
|
51 |
NOT: lambda (a,): a}
|
sawine@14
|
52 |
def negate(f):
|
sawine@14
|
53 |
return negmap[f.id](f.values)
|
sawine@14
|
54 |
if not isinstance(formula, Operator):
|
sawine@18
|
55 |
return formula
|
sawine@14
|
56 |
if formula.id == NOT:
|
sawine@14
|
57 |
return negate(formula.values[0])
|
sawine@19
|
58 |
return formula.__class__(values(de_morgan, formula))
|
sawine@18
|
59 |
|
sawine@18
|
60 |
def reduce_iter(formula):
|
sawine@18
|
61 |
redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))
|
sawine@18
|
62 |
if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
|
sawine@18
|
63 |
return formula
|
sawine@18
|
64 |
ids = (formula.id, formula.values[0].id)
|
sawine@18
|
65 |
if ids in redset:
|
sawine@18
|
66 |
return reduce_iter(formula.values[0])
|
sawine@19
|
67 |
return formula.__class__(values(reduce_iter, formula))
|
sawine@19
|
68 |
|
sawine@19
|
69 |
def dist(formula):
|
sawine@19
|
70 |
distmap = {(BOX, AND): lambda (a, b): And([Box([a]), Box([b])]),
|
sawine@19
|
71 |
(DIAMOND, OR): lambda (a, b): Or([Diamond([a]), Diamond([b])]),
|
sawine@19
|
72 |
(BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))
|
sawine@19
|
73 |
and Or([Box([a]), Box([b])]) or Box([Or([a, b])]),
|
sawine@19
|
74 |
(DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond))
|
sawine@19
|
75 |
and And([Diamond([a]), Diamond([b])]) or Diamond([And([a, b])])}
|
sawine@19
|
76 |
if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
|
sawine@19
|
77 |
return formula
|
sawine@19
|
78 |
ids = (formula.id, formula.values[0].id)
|
sawine@19
|
79 |
if ids in distmap:
|
sawine@19
|
80 |
return distmap[ids](formula.values[0].values)
|
sawine@19
|
81 |
return formula.__class__(values(dist, formula))
|
sawine@12
|
82 |
|
sawine@12
|
83 |
NOT = "~"
|
sawine@12
|
84 |
AND = "&"
|
sawine@12
|
85 |
OR = "|"
|
sawine@12
|
86 |
IMP = "->"
|
sawine@12
|
87 |
EQ = "<->"
|
sawine@12
|
88 |
BOX = "[]"
|
sawine@12
|
89 |
DIAMOND = "<>"
|
sawine@14
|
90 |
VARIABLE = "VAR"
|
sawine@12
|
91 |
LB = "("
|
sawine@12
|
92 |
RB = ")"
|
sawine@12
|
93 |
|
sawine@12
|
94 |
class Operator(object):
|
sawine@12
|
95 |
def __init__(self, id, arity, values):
|
sawine@12
|
96 |
self.id = id
|
sawine@12
|
97 |
self.arity = arity
|
sawine@12
|
98 |
self.values = values
|
sawine@12
|
99 |
def __str__(self):
|
sawine@12
|
100 |
out = self.id
|
sawine@12
|
101 |
if self.arity == 0:
|
sawine@12
|
102 |
out = str(self.values[0])
|
sawine@12
|
103 |
if self.arity == 1:
|
sawine@12
|
104 |
out = self.id + str(self.values[0])
|
sawine@12
|
105 |
elif self.arity == 2:
|
sawine@12
|
106 |
out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"
|
sawine@12
|
107 |
return out
|
sawine@12
|
108 |
|
sawine@12
|
109 |
class Not(Operator):
|
sawine@12
|
110 |
arity = 1
|
sawine@12
|
111 |
def __init__(self, values):
|
sawine@12
|
112 |
Operator.__init__(self, NOT, Not.arity, values)
|
sawine@12
|
113 |
def __call__(self):
|
sawine@12
|
114 |
pass
|
sawine@12
|
115 |
|
sawine@12
|
116 |
class And(Operator):
|
sawine@12
|
117 |
arity = 2
|
sawine@12
|
118 |
def __init__(self, values):
|
sawine@12
|
119 |
Operator.__init__(self, AND, And.arity, values)
|
sawine@12
|
120 |
|
sawine@12
|
121 |
class Or(Operator):
|
sawine@12
|
122 |
arity = 2
|
sawine@12
|
123 |
def __init__(self, values):
|
sawine@12
|
124 |
Operator.__init__(self, OR, Or.arity, values)
|
sawine@12
|
125 |
|
sawine@12
|
126 |
class Imp(Operator):
|
sawine@12
|
127 |
arity = 2
|
sawine@12
|
128 |
def __init__(self, values):
|
sawine@12
|
129 |
Operator.__init__(self, IMP, Imp.arity, values)
|
sawine@12
|
130 |
|
sawine@12
|
131 |
class Eq(Operator):
|
sawine@12
|
132 |
arity = 2
|
sawine@12
|
133 |
def __init__(self, values):
|
sawine@12
|
134 |
Operator.__init__(self, EQ, Eq.arity, values)
|
sawine@12
|
135 |
|
sawine@12
|
136 |
class Box(Operator):
|
sawine@12
|
137 |
arity = 1
|
sawine@12
|
138 |
def __init__(self, values):
|
sawine@12
|
139 |
Operator.__init__(self, BOX, Box.arity, values)
|
sawine@12
|
140 |
|
sawine@12
|
141 |
class Diamond(Operator):
|
sawine@12
|
142 |
arity = 1
|
sawine@12
|
143 |
def __init__(self, values):
|
sawine@12
|
144 |
Operator.__init__(self, DIAMOND, Diamond.arity, values)
|
sawine@12
|
145 |
|
sawine@12
|
146 |
class Variable(Operator):
|
sawine@12
|
147 |
arity = 0
|
sawine@12
|
148 |
def __init__(self, values):
|
sawine@12
|
149 |
Operator.__init__(self, VARIABLE, Variable.arity, values)
|
sawine@12
|
150 |
|
sawine@12
|
151 |
class Lb(Operator):
|
sawine@12
|
152 |
arity = -1
|
sawine@12
|
153 |
def __init__(self, values):
|
sawine@12
|
154 |
Operator.__init__(self, LB, Lb.arity, values)
|
sawine@12
|
155 |
|
sawine@12
|
156 |
class Rb(Operator):
|
sawine@12
|
157 |
arity = -1
|
sawine@12
|
158 |
def __init__(self, values):
|
sawine@12
|
159 |
Operator.__init__(self, RB, Rb.arity, values)
|
sawine@12
|
160 |
|
sawine@12
|
161 |
class Formula(object):
|
sawine@12
|
162 |
def __init__(self):
|
sawine@12
|
163 |
pass
|
sawine@12
|
164 |
|
sawine@12
|
165 |
TOKENS = {re.compile("\("): Lb,
|
sawine@12
|
166 |
re.compile("\)"): Rb,
|
sawine@12
|
167 |
re.compile("~"): Not,
|
sawine@12
|
168 |
re.compile("&"): And,
|
sawine@12
|
169 |
re.compile("\|"): Or,
|
sawine@12
|
170 |
re.compile("->"): Imp,
|
sawine@12
|
171 |
re.compile("<->"): Eq,
|
sawine@12
|
172 |
re.compile("\[\]"): Box,
|
sawine@12
|
173 |
re.compile("<>"): Diamond,
|
sawine@12
|
174 |
re.compile("[a-z]+"): Variable}
|
sawine@12
|
175 |
|
sawine@12
|
176 |
class Scanner(object):
|
sawine@12
|
177 |
def __init__(self, tokens, source=None):
|
sawine@12
|
178 |
self.tokens = tokens
|
sawine@12
|
179 |
self.reset(source)
|
sawine@12
|
180 |
def next(self):
|
sawine@12
|
181 |
while self.i < len(self.source):
|
sawine@12
|
182 |
re.purge()
|
sawine@12
|
183 |
for p, token in self.tokens.iteritems():
|
sawine@12
|
184 |
m = p.match(self.source[self.i:])
|
sawine@12
|
185 |
if m:
|
sawine@12
|
186 |
self.i += m.end(0)
|
sawine@12
|
187 |
value = m.group(0)
|
sawine@12
|
188 |
return (token, value)
|
sawine@12
|
189 |
self.i += 1
|
sawine@12
|
190 |
return (None, None)
|
sawine@12
|
191 |
def reset(self, source):
|
sawine@12
|
192 |
self.i = 0
|
sawine@12
|
193 |
self.source = source
|
sawine@12
|
194 |
|
sawine@12
|
195 |
S = Formula
|
sawine@12
|
196 |
A = "A"
|
sawine@12
|
197 |
#0 S: (Variable,),
|
sawine@12
|
198 |
#1 S: (Not, S),
|
sawine@12
|
199 |
#2 S: (Lb, A, Rb),
|
sawine@12
|
200 |
#3 S: (Box, S),
|
sawine@12
|
201 |
#4 S: (Diamond, S),
|
sawine@12
|
202 |
#5 A: (S, And, S),
|
sawine@12
|
203 |
#6 A: (S, Or, S),
|
sawine@12
|
204 |
#7 A: (S, Imp, S),
|
sawine@12
|
205 |
#8 A: (S, Eq, S)
|
sawine@12
|
206 |
SYNTAX = ((Variable,),
|
sawine@12
|
207 |
(Not, S),
|
sawine@12
|
208 |
(Lb, A, Rb),
|
sawine@12
|
209 |
(Box, S),
|
sawine@12
|
210 |
(Diamond, S),
|
sawine@12
|
211 |
(S, And, S),
|
sawine@12
|
212 |
(S, Or, S),
|
sawine@12
|
213 |
(S, Imp, S),
|
sawine@12
|
214 |
(S, Eq, S))
|
sawine@12
|
215 |
|
sawine@12
|
216 |
class Node(object):
|
sawine@12
|
217 |
def __init__(self, parent, value):
|
sawine@12
|
218 |
self.parent = parent
|
sawine@12
|
219 |
self.value = value
|
sawine@12
|
220 |
self.children = []
|
sawine@12
|
221 |
def addChild(self, value):
|
sawine@12
|
222 |
self.children.append(self, node)
|
sawine@12
|
223 |
|
sawine@12
|
224 |
class Parser(object):
|
sawine@12
|
225 |
def __init__(self, syntax, scanner):
|
sawine@12
|
226 |
self.syntax = syntax
|
sawine@12
|
227 |
self.scanner = scanner
|
sawine@12
|
228 |
def parse(self, source):
|
sawine@12
|
229 |
table = {(S, Variable): 0,
|
sawine@12
|
230 |
(S, Not): 1,
|
sawine@12
|
231 |
(S, Lb): 2,
|
sawine@12
|
232 |
(S, Box): 3,
|
sawine@12
|
233 |
(S, Diamond): 4,
|
sawine@12
|
234 |
(A, S, And): 5,
|
sawine@12
|
235 |
(A, S, Or): 6,
|
sawine@12
|
236 |
(A, S, Imp): 7,
|
sawine@12
|
237 |
(A, S, Eq): 8,
|
sawine@12
|
238 |
(A, Variable, And): 5,
|
sawine@12
|
239 |
(A, Variable, Or): 6,
|
sawine@12
|
240 |
(A, Variable, Imp): 7,
|
sawine@12
|
241 |
(A, Variable, Eq): 8,
|
sawine@12
|
242 |
(A, Not, Variable, And): 5,
|
sawine@12
|
243 |
(A, Not, Variable, Or): 6,
|
sawine@12
|
244 |
(A, Not, Variable, Imp): 7,
|
sawine@12
|
245 |
(A, Not, Variable, Eq): 8}
|
sawine@12
|
246 |
stack = [S]
|
sawine@12
|
247 |
tree_nodes = []
|
sawine@12
|
248 |
tree = None
|
sawine@12
|
249 |
out = []
|
sawine@12
|
250 |
self.scanner.reset(source)
|
sawine@12
|
251 |
(token, value) = self.scanner.next()
|
sawine@12
|
252 |
(lookahead, la_value) = self.scanner.next()
|
sawine@12
|
253 |
(lookahead2, la2_value) = self.scanner.next()
|
sawine@12
|
254 |
accepted = True
|
sawine@12
|
255 |
while token and len(stack):
|
sawine@12
|
256 |
top = stack[-1]
|
sawine@12
|
257 |
if top == token:
|
sawine@12
|
258 |
tree_nodes.append((token, value))
|
sawine@12
|
259 |
stack.pop()
|
sawine@12
|
260 |
#tree_nodes.append((stack.pop(), value))
|
sawine@12
|
261 |
(token, value) = (lookahead, la_value)
|
sawine@12
|
262 |
(lookahead, la_value) = (lookahead2, la2_value)
|
sawine@12
|
263 |
#(lookahead, _) = self.scanner.next()
|
sawine@12
|
264 |
(lookahead2, la2_value) = self.scanner.next()
|
sawine@12
|
265 |
else:
|
sawine@12
|
266 |
action = None
|
sawine@12
|
267 |
if (top, token) in table:
|
sawine@12
|
268 |
action = table[(top, token)]
|
sawine@12
|
269 |
elif (top, token, lookahead) in table:
|
sawine@12
|
270 |
action = table[(top, token, lookahead)]
|
sawine@12
|
271 |
elif (top, token, lookahead, lookahead2) in table:
|
sawine@12
|
272 |
action = table[(top, token, lookahead, lookahead2)]
|
sawine@12
|
273 |
if action is None:
|
sawine@12
|
274 |
accepted = False
|
sawine@12
|
275 |
break
|
sawine@12
|
276 |
|
sawine@12
|
277 |
out.append(action)
|
sawine@12
|
278 |
stack.pop()
|
sawine@12
|
279 |
stack.extend(reversed(self.syntax[action]))
|
sawine@12
|
280 |
accepted = accepted and not len(stack)
|
sawine@12
|
281 |
return (accepted, out, tree_nodes)
|
sawine@12
|
282 |
|
sawine@12
|
283 |
class SyntaxTree(object):
|
sawine@12
|
284 |
def __init__(self, seq, tree_nodes):
|
sawine@12
|
285 |
seq.reverse()
|
sawine@12
|
286 |
tree_nodes.reverse()
|
sawine@12
|
287 |
self.root = self.compile(seq, tree_nodes)[0]
|
sawine@12
|
288 |
def compile(self, seq, tree_nodes):
|
sawine@12
|
289 |
stack = []
|
sawine@12
|
290 |
while len(seq):
|
sawine@12
|
291 |
s = seq.pop()
|
sawine@12
|
292 |
if s == 0:
|
sawine@12
|
293 |
c, v = tree_nodes.pop()
|
sawine@12
|
294 |
while c != Variable:
|
sawine@12
|
295 |
c, v = tree_nodes.pop()
|
sawine@12
|
296 |
stack.append(Variable(v))
|
sawine@12
|
297 |
elif s == 1:
|
sawine@12
|
298 |
stack.append(Not(self.compile(seq, tree_nodes)))
|
sawine@12
|
299 |
elif s == 2:
|
sawine@12
|
300 |
stack.extend(self.compile(seq, tree_nodes))
|
sawine@12
|
301 |
elif s == 3:
|
sawine@12
|
302 |
stack.append(Box(self.compile(seq, tree_nodes)))
|
sawine@12
|
303 |
elif s == 4:
|
sawine@12
|
304 |
stack.append(Diamond(self.compile(seq, tree_nodes)))
|
sawine@12
|
305 |
elif s == 5:
|
sawine@12
|
306 |
stack.append(And(self.compile(seq, tree_nodes)))
|
sawine@12
|
307 |
elif s == 6:
|
sawine@12
|
308 |
stack.append(Or(self.compile(seq, tree_nodes)))
|
sawine@12
|
309 |
elif s == 7:
|
sawine@12
|
310 |
stack.append(Imp(self.compile(seq, tree_nodes)))
|
sawine@12
|
311 |
elif s == 8:
|
sawine@12
|
312 |
stack.append(Eq(self.compile(seq, tree_nodes)))
|
sawine@12
|
313 |
return stack
|
sawine@12
|
314 |
|
sawine@12
|
315 |
from argparse import ArgumentParser
|
sawine@12
|
316 |
|
sawine@12
|
317 |
def parse_arguments():
|
sawine@12
|
318 |
parser = ArgumentParser(description="Parses simple modal logic syntax.")
|
sawine@12
|
319 |
parser.add_argument("-f", "--formula", help="your formula")
|
sawine@12
|
320 |
return parser.parse_args()
|
sawine@12
|
321 |
|
sawine@19
|
322 |
EXCUSE = """The formula was not accepted by me, because I don't like you and the rest of the world. I seem to have some issues with formulae with inner nesting and I generally suffer from my hasty implementation. I would like to thank you for your coorporation by providing the formula within the code file itself. Thank you. ~The Parser"""
|
sawine@12
|
323 |
|
sawine@12
|
324 |
if __name__ == "__main__":
|
sawine@12
|
325 |
main()
|