sawine@0
|
1 |
"""
|
sawine@0
|
2 |
Name:
|
sawine@0
|
3 |
|
sawine@0
|
4 |
Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>
|
sawine@0
|
5 |
"""
|
sawine@0
|
6 |
from os import path
|
sawine@0
|
7 |
import os
|
sawine@0
|
8 |
import re
|
sawine@0
|
9 |
import token
|
sawine@0
|
10 |
|
sawine@0
|
11 |
NOT = "~"
|
sawine@0
|
12 |
AND = "&"
|
sawine@0
|
13 |
OR = "|"
|
sawine@0
|
14 |
IMP = "->"
|
sawine@0
|
15 |
EQ = "<->"
|
sawine@0
|
16 |
BOX = "[]"
|
sawine@0
|
17 |
DIAMOND = "<>"
|
sawine@1
|
18 |
VARIABLE = "p"
|
sawine@1
|
19 |
LB = "("
|
sawine@1
|
20 |
RB = ")"
|
sawine@0
|
21 |
|
sawine@1
|
22 |
class Operator(object):
|
sawine@6
|
23 |
def __init__(self, id, arity, values):
|
sawine@6
|
24 |
self.id = id
|
sawine@6
|
25 |
self.arity = arity
|
sawine@4
|
26 |
self.values = values
|
sawine@1
|
27 |
def __str__(self):
|
sawine@6
|
28 |
out = self.id
|
sawine@6
|
29 |
if self.arity == 0:
|
sawine@6
|
30 |
out = str(self.values[0])
|
sawine@6
|
31 |
if self.arity == 1:
|
sawine@6
|
32 |
out = self.id + str(self.values[0])
|
sawine@6
|
33 |
elif self.arity == 2:
|
sawine@6
|
34 |
#print self.id
|
sawine@6
|
35 |
#print self.values
|
sawine@6
|
36 |
out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"
|
sawine@6
|
37 |
return out
|
sawine@1
|
38 |
|
sawine@1
|
39 |
class Not(Operator):
|
sawine@2
|
40 |
arity = 1
|
sawine@2
|
41 |
def __init__(self, values):
|
sawine@6
|
42 |
Operator.__init__(self, NOT, Not.arity, values)
|
sawine@1
|
43 |
def __call__(self):
|
sawine@1
|
44 |
pass
|
sawine@1
|
45 |
|
sawine@1
|
46 |
class And(Operator):
|
sawine@2
|
47 |
arity = 2
|
sawine@2
|
48 |
def __init__(self, values):
|
sawine@6
|
49 |
Operator.__init__(self, AND, And.arity, values)
|
sawine@4
|
50 |
|
sawine@1
|
51 |
class Or(Operator):
|
sawine@2
|
52 |
arity = 2
|
sawine@2
|
53 |
def __init__(self, values):
|
sawine@6
|
54 |
Operator.__init__(self, OR, Or.arity, values)
|
sawine@2
|
55 |
|
sawine@1
|
56 |
class Imp(Operator):
|
sawine@2
|
57 |
arity = 2
|
sawine@5
|
58 |
def __init__(self, values):
|
sawine@6
|
59 |
Operator.__init__(self, IMP, Imp.arity, values)
|
sawine@1
|
60 |
|
sawine@1
|
61 |
class Eq(Operator):
|
sawine@2
|
62 |
arity = 2
|
sawine@5
|
63 |
def __init__(self, values):
|
sawine@6
|
64 |
Operator.__init__(self, EQ, Eq.arity, values)
|
sawine@1
|
65 |
|
sawine@1
|
66 |
class Box(Operator):
|
sawine@2
|
67 |
arity = 1
|
sawine@2
|
68 |
def __init__(self, values):
|
sawine@6
|
69 |
Operator.__init__(self, BOX, Box.arity, values)
|
sawine@2
|
70 |
|
sawine@1
|
71 |
class Diamond(Operator):
|
sawine@2
|
72 |
arity = 1
|
sawine@5
|
73 |
def __init__(self, values):
|
sawine@6
|
74 |
Operator.__init__(self, DIAMOND, Diamond.arity, values)
|
sawine@1
|
75 |
|
sawine@1
|
76 |
class Variable(Operator):
|
sawine@2
|
77 |
arity = 0
|
sawine@2
|
78 |
def __init__(self, values):
|
sawine@6
|
79 |
Operator.__init__(self, VARIABLE, Variable.arity, values)
|
sawine@6
|
80 |
|
sawine@2
|
81 |
class Lb(Operator):
|
sawine@2
|
82 |
arity = -1
|
sawine@2
|
83 |
def __init__(self, values):
|
sawine@6
|
84 |
Operator.__init__(self, LB, Lb.arity, values)
|
sawine@2
|
85 |
|
sawine@2
|
86 |
class Rb(Operator):
|
sawine@2
|
87 |
arity = -1
|
sawine@2
|
88 |
def __init__(self, values):
|
sawine@6
|
89 |
Operator.__init__(self, RB, Rb.arity, values)
|
sawine@2
|
90 |
|
sawine@1
|
91 |
class Formula(object):
|
sawine@2
|
92 |
def __init__(self):
|
sawine@5
|
93 |
pass
|
sawine@1
|
94 |
|
sawine@2
|
95 |
TOKENS = {re.compile("\("): Lb,
|
sawine@2
|
96 |
re.compile("\)"): Rb,
|
sawine@1
|
97 |
re.compile("~"): Not,
|
sawine@1
|
98 |
re.compile("&"): And,
|
sawine@1
|
99 |
re.compile("\|"): Or,
|
sawine@1
|
100 |
re.compile("->"): Imp,
|
sawine@1
|
101 |
re.compile("<->"): Eq,
|
sawine@1
|
102 |
re.compile("\[\]"): Box,
|
sawine@1
|
103 |
re.compile("<>"): Diamond,
|
sawine@1
|
104 |
re.compile("[a-z]+"): Variable}
|
sawine@0
|
105 |
|
sawine@0
|
106 |
class Scanner(object):
|
sawine@0
|
107 |
def __init__(self, tokens, source=None):
|
sawine@0
|
108 |
self.tokens = tokens
|
sawine@0
|
109 |
self.reset(source)
|
sawine@0
|
110 |
def next(self):
|
sawine@6
|
111 |
while self.i < len(self.source):
|
sawine@6
|
112 |
re.purge()
|
sawine@0
|
113 |
for p, token in self.tokens.iteritems():
|
sawine@0
|
114 |
m = p.match(self.source[self.i:])
|
sawine@0
|
115 |
if m:
|
sawine@0
|
116 |
self.i += m.end(0)
|
sawine@6
|
117 |
value = m.group(0)
|
sawine@2
|
118 |
return (token, value)
|
sawine@0
|
119 |
self.i += 1
|
sawine@2
|
120 |
return (None, None)
|
sawine@0
|
121 |
def reset(self, source):
|
sawine@0
|
122 |
self.i = 0
|
sawine@0
|
123 |
self.source = source
|
sawine@0
|
124 |
|
sawine@1
|
125 |
S = Formula
|
sawine@1
|
126 |
A = "A"
|
sawine@2
|
127 |
#0 S: (Variable,),
|
sawine@2
|
128 |
#1 S: (Not, S),
|
sawine@2
|
129 |
#2 S: (Lb, A, Rb),
|
sawine@2
|
130 |
#3 S: (Box, S),
|
sawine@2
|
131 |
#4 S: (Diamond, S),
|
sawine@2
|
132 |
#5 A: (S, And, S),
|
sawine@2
|
133 |
#6 A: (S, Or, S),
|
sawine@2
|
134 |
#7 A: (S, Imp, S),
|
sawine@2
|
135 |
#8 A: (S, Eq, S)
|
sawine@1
|
136 |
SYNTAX = ((Variable,),
|
sawine@1
|
137 |
(Not, S),
|
sawine@2
|
138 |
(Lb, A, Rb),
|
sawine@1
|
139 |
(Box, S),
|
sawine@1
|
140 |
(Diamond, S),
|
sawine@1
|
141 |
(S, And, S),
|
sawine@1
|
142 |
(S, Or, S),
|
sawine@1
|
143 |
(S, Imp, S),
|
sawine@1
|
144 |
(S, Eq, S))
|
sawine@1
|
145 |
|
sawine@2
|
146 |
class Node(object):
|
sawine@2
|
147 |
def __init__(self, parent, value):
|
sawine@2
|
148 |
self.parent = parent
|
sawine@2
|
149 |
self.value = value
|
sawine@2
|
150 |
self.children = []
|
sawine@2
|
151 |
def addChild(self, value):
|
sawine@2
|
152 |
self.children.append(self, node)
|
sawine@2
|
153 |
|
sawine@0
|
154 |
class Parser(object):
|
sawine@1
|
155 |
def __init__(self, syntax, scanner):
|
sawine@1
|
156 |
self.syntax = syntax
|
sawine@0
|
157 |
self.scanner = scanner
|
sawine@0
|
158 |
def parse(self, source):
|
sawine@1
|
159 |
table = {(S, Variable): 0,
|
sawine@1
|
160 |
(S, Not): 1,
|
sawine@2
|
161 |
(S, Lb): 2,
|
sawine@1
|
162 |
(S, Box): 3,
|
sawine@1
|
163 |
(S, Diamond): 4,
|
sawine@1
|
164 |
(A, S, And): 5,
|
sawine@1
|
165 |
(A, S, Or): 6,
|
sawine@1
|
166 |
(A, S, Imp): 7,
|
sawine@1
|
167 |
(A, S, Eq): 8,
|
sawine@1
|
168 |
(A, Variable, And): 5,
|
sawine@1
|
169 |
(A, Variable, Or): 6,
|
sawine@1
|
170 |
(A, Variable, Imp): 7,
|
sawine@6
|
171 |
(A, Variable, Eq): 8,
|
sawine@6
|
172 |
(A, Not, Variable, And): 5,
|
sawine@6
|
173 |
(A, Not, Variable, Or): 6,
|
sawine@6
|
174 |
(A, Not, Variable, Imp): 7,
|
sawine@6
|
175 |
(A, Not, Variable, Eq): 8}
|
sawine@1
|
176 |
stack = [S]
|
sawine@3
|
177 |
tree_nodes = []
|
sawine@6
|
178 |
tree = None
|
sawine@1
|
179 |
out = []
|
sawine@0
|
180 |
self.scanner.reset(source)
|
sawine@2
|
181 |
(token, value) = self.scanner.next()
|
sawine@6
|
182 |
(lookahead, la_value) = self.scanner.next()
|
sawine@6
|
183 |
(lookahead2, la2_value) = self.scanner.next()
|
sawine@6
|
184 |
accepted = True
|
sawine@6
|
185 |
while token and len(stack):
|
sawine@4
|
186 |
top = stack[-1]
|
sawine@1
|
187 |
if top == token:
|
sawine@6
|
188 |
tree_nodes.append((token, value))
|
sawine@6
|
189 |
stack.pop()
|
sawine@6
|
190 |
#tree_nodes.append((stack.pop(), value))
|
sawine@6
|
191 |
(token, value) = (lookahead, la_value)
|
sawine@6
|
192 |
(lookahead, la_value) = (lookahead2, la2_value)
|
sawine@6
|
193 |
#(lookahead, _) = self.scanner.next()
|
sawine@6
|
194 |
(lookahead2, la2_value) = self.scanner.next()
|
sawine@1
|
195 |
else:
|
sawine@1
|
196 |
action = None
|
sawine@1
|
197 |
if (top, token) in table:
|
sawine@1
|
198 |
action = table[(top, token)]
|
sawine@1
|
199 |
elif (top, token, lookahead) in table:
|
sawine@6
|
200 |
action = table[(top, token, lookahead)]
|
sawine@6
|
201 |
elif (top, token, lookahead, lookahead2) in table:
|
sawine@6
|
202 |
action = table[(top, token, lookahead, lookahead2)]
|
sawine@1
|
203 |
if action is None:
|
sawine@1
|
204 |
accepted = False
|
sawine@1
|
205 |
break
|
sawine@6
|
206 |
|
sawine@1
|
207 |
out.append(action)
|
sawine@1
|
208 |
stack.pop()
|
sawine@1
|
209 |
stack.extend(reversed(self.syntax[action]))
|
sawine@2
|
210 |
accepted = accepted and not len(stack)
|
sawine@3
|
211 |
return (accepted, out, tree_nodes)
|
sawine@4
|
212 |
|
sawine@3
|
213 |
class SyntaxTree(object):
|
sawine@6
|
214 |
def __init__(self, seq, tree_nodes):
|
sawine@6
|
215 |
seq.reverse()
|
sawine@6
|
216 |
tree_nodes.reverse()
|
sawine@6
|
217 |
print tree_nodes
|
sawine@6
|
218 |
print seq
|
sawine@6
|
219 |
self.root = self.compile(seq, tree_nodes)[0]
|
sawine@6
|
220 |
print self.root
|
sawine@6
|
221 |
def compile(self, seq, tree_nodes):
|
sawine@6
|
222 |
stack = []
|
sawine@6
|
223 |
waiting = []
|
sawine@6
|
224 |
print seq
|
sawine@6
|
225 |
while len(seq):
|
sawine@6
|
226 |
s = seq.pop()
|
sawine@6
|
227 |
if s == 0:
|
sawine@6
|
228 |
c, v = tree_nodes.pop()
|
sawine@6
|
229 |
while c != Variable:
|
sawine@6
|
230 |
c, v = tree_nodes.pop()
|
sawine@6
|
231 |
stack.append(Variable(v))
|
sawine@6
|
232 |
elif s == 1:
|
sawine@6
|
233 |
stack.append(Not(self.compile(seq, tree_nodes)))
|
sawine@6
|
234 |
elif s == 2:
|
sawine@6
|
235 |
stack.extend(self.compile(seq, tree_nodes))
|
sawine@6
|
236 |
elif s == 3:
|
sawine@6
|
237 |
stack.append(Box(self.compile(seq, tree_nodes)))
|
sawine@6
|
238 |
elif s == 4:
|
sawine@6
|
239 |
stack.append(Diamond(self.compile(seq, tree_nodes)))
|
sawine@6
|
240 |
elif s == 5:
|
sawine@6
|
241 |
stack.append(And(self.compile(seq, tree_nodes)))
|
sawine@6
|
242 |
elif s == 6:
|
sawine@6
|
243 |
stack.append(Or(self.compile(seq, tree_nodes)))
|
sawine@6
|
244 |
elif s == 7:
|
sawine@6
|
245 |
stack.append(Imp(self.compile(seq, tree_nodes)))
|
sawine@6
|
246 |
elif s == 8:
|
sawine@6
|
247 |
stack.append(Eq(self.compile(seq, tree_nodes)))
|
sawine@6
|
248 |
print stack
|
sawine@6
|
249 |
return stack
|
sawine@6
|
250 |
|
sawine@6
|
251 |
def compile_(self, tree_nodes):
|
sawine@3
|
252 |
table = []
|
sawine@3
|
253 |
unfinished = []
|
sawine@4
|
254 |
node = None
|
sawine@6
|
255 |
print tree_nodes
|
sawine@6
|
256 |
for n, v in (tree_nodes):
|
sawine@6
|
257 |
print
|
sawine@6
|
258 |
print n
|
sawine@4
|
259 |
if n.arity >= 0:
|
sawine@3
|
260 |
if len(table) < n.arity:
|
sawine@6
|
261 |
print "appending unfinished ", n
|
sawine@3
|
262 |
unfinished.append(n)
|
sawine@3
|
263 |
else:
|
sawine@6
|
264 |
args = table[:n.arity]
|
sawine@6
|
265 |
if n.arity == 0:
|
sawine@6
|
266 |
args = [v]
|
sawine@3
|
267 |
table = table[n.arity:]
|
sawine@4
|
268 |
node = n(args)
|
sawine@3
|
269 |
table.append(node)
|
sawine@6
|
270 |
if len(unfinished) and unfinished[-1].arity <= len(table):
|
sawine@6
|
271 |
n = unfinished[-1]
|
sawine@6
|
272 |
print "finishing ", n
|
sawine@3
|
273 |
args = table[:n.arity]
|
sawine@3
|
274 |
table = table[n.arity:]
|
sawine@4
|
275 |
node = n(args)
|
sawine@3
|
276 |
table.append(node)
|
sawine@4
|
277 |
unfinished.pop()
|
sawine@3
|
278 |
return table[0]
|
sawine@3
|
279 |
|
sawine@0
|
280 |
|
sawine@0
|
281 |
def main():
|
sawine@0
|
282 |
args = parse_arguments()
|
sawine@0
|
283 |
scanner = Scanner(TOKENS)
|
sawine@1
|
284 |
parser = Parser(SYNTAX, scanner)
|
sawine@3
|
285 |
(accepted, out, tree_nodes) = parser.parse(args.formula)
|
sawine@6
|
286 |
tree = SyntaxTree(out, tree_nodes)
|
sawine@6
|
287 |
#print tree.root
|
sawine@0
|
288 |
|
sawine@0
|
289 |
from argparse import ArgumentParser
|
sawine@0
|
290 |
|
sawine@0
|
291 |
def parse_arguments():
|
sawine@2
|
292 |
parser = ArgumentParser(description="Parses simple modal logic syntax.")
|
sawine@0
|
293 |
parser.add_argument("formula", help="your formula")
|
sawine@0
|
294 |
return parser.parse_args()
|
sawine@0
|
295 |
|
sawine@0
|
296 |
if __name__ == "__main__":
|
sawine@0
|
297 |
main()
|