Experimentally support some syntactic sugar for logic notation.
Chris Pressey
8 years ago
| 4 | 4 |
|
| 5 | 5 |
sys.path.insert(0, join(dirname(realpath(sys.argv[0])), '..', 'src'))
|
| 6 | 6 |
|
| 7 | |
from maxixe.parser import Parser
|
|
7 |
from maxixe.parser import Parser, SugaredParser
|
| 8 | 8 |
from maxixe.checker import Checker
|
| 9 | 9 |
|
| 10 | 10 |
|
| 11 | |
if __name__ == '__main__':
|
| 12 | |
filename = sys.argv[1]
|
|
11 |
def main(args):
|
|
12 |
parser_cls = Parser
|
|
13 |
while args and args[0].startswith('--'):
|
|
14 |
option = args.pop(0)
|
|
15 |
if option == '--sugar':
|
|
16 |
parser_cls = SugaredParser
|
|
17 |
else:
|
|
18 |
raise NotImplementedError(option)
|
|
19 |
filename = args.pop(0)
|
| 13 | 20 |
with open(filename, 'r') as f:
|
| 14 | |
p = Parser(f.read())
|
|
21 |
p = parser_cls(f.read().decode('utf-8'))
|
| 15 | 22 |
proof = p.proof()
|
| 16 | 23 |
c = Checker(proof)
|
| 17 | 24 |
c.check()
|
|
25 |
|
|
26 |
|
|
27 |
if __name__ == '__main__':
|
|
28 |
main(sys.argv[1:])
|
| 18 | 29 |
print 'ok'
|
| 19 | 30 |
sys.exit(0)
|
|
0 |
given
|
|
1 |
Modus_Ponens = impl(P, Q) ; P |- Q
|
|
2 |
Modus_Tollens = impl(P, Q) ; not(Q) |- not(P)
|
|
3 |
Hypothetical_Syllogism = impl(P, Q) ; impl(Q, R) |- impl(P, R)
|
|
4 |
Disjunctive_Syllogism = or(P, Q) ; not(P) |- Q
|
|
5 |
Addition = P |- or(P, Q)
|
|
6 |
Simplification = P ∧ Q |- Q
|
|
7 |
Conjunction = P ; Q |- P ∧ Q
|
|
8 |
Resolution = or(not(P, R)) ; or(P, Q) |- or(Q, R)
|
|
9 |
|
|
10 |
Commutativity_of_Conjunction = P ∧ Q |- Q ∧ P
|
|
11 |
|
|
12 |
Premise = |- p ∧ impl(p, q)
|
|
13 |
show
|
|
14 |
q
|
|
15 |
proof
|
|
16 |
Step_1 = p ∧ impl(p, q) by Premise
|
|
17 |
Step_2 = impl(p, q) ∧ p by Commutativity_of_Conjunction with Step_1
|
|
18 |
Step_3 = impl(p, q) by Simplification with Step_1
|
|
19 |
Step_4 = p by Simplification with Step_2
|
|
20 |
Step_5 = q by Modus_Ponens with Step_3, Step_4
|
|
21 |
qed
|
| 154 | 154 |
return step
|
| 155 | 155 |
|
| 156 | 156 |
def term(self):
|
|
157 |
return self.basic_term()
|
|
158 |
|
|
159 |
def basic_term(self):
|
| 157 | 160 |
if self.scanner.on_type('variable'):
|
| 158 | 161 |
return self.var()
|
| 159 | 162 |
self.scanner.check_type('atom')
|
|
| 192 | 195 |
self.scanner.expect('->')
|
| 193 | 196 |
rhs = self.term()
|
| 194 | 197 |
return (lhs, rhs)
|
|
198 |
|
|
199 |
|
|
200 |
# Term ::= Term0 {"∨" Term0}.
|
|
201 |
# Term0 ::= Term1 {"∧" Term1}.
|
|
202 |
# Term1 ::= BasicTerm.
|
|
203 |
|
|
204 |
|
|
205 |
class SugaredParser(Parser):
|
|
206 |
|
|
207 |
def term(self):
|
|
208 |
term_a = self.term0()
|
|
209 |
while self.scanner.consume(u'∨'):
|
|
210 |
term_b = self.term0()
|
|
211 |
term_a = Term('or', [term_a, term_b])
|
|
212 |
return term_a
|
|
213 |
|
|
214 |
def term0(self):
|
|
215 |
term_a = self.term1()
|
|
216 |
while self.scanner.consume(u'∧'):
|
|
217 |
term_b = self.term1()
|
|
218 |
term_a = Term('and', [term_a, term_b])
|
|
219 |
return term_a
|
|
220 |
|
|
221 |
def term1(self):
|
|
222 |
return self.basic_term()
|