#!/usr/bin/env python2.3
# ----------------------------------
#
# example_parser.py
#
# Simple example of a parser for parsing propositional formulae
#
# Copyright 2005 Stephan Schulz, schulz@eprover.org
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program ; if not, write to the Free Software
# Foundation, Inc., 59 Temple Place, Suite 330, Boston,
# MA 02111-1307 USA
#
# The original copyright holder can be contacted as
#
# Stephan Schulz
# Helene-Mayer-Ring 10/907
# 80809 Muenchen
# Germany
# Email: schulz@eprover.org
"""
Usage: parser_example.py ...
Read any number of files and parse the formulae in it. Print internal
representation and rebuild formula back.
"""
from pylib_lexer import *
def parse_formula(lex):
"""
Parse a propositional formula into nested lists (i.e. s-expression
form).
"""
lex.check_token([OpenBracket, Proposition])
if lex.test_token(Proposition):
# It is a single proposition - we store it as a string
res = lex.look_token().literal
lex.accept_token(Proposition)
else:
# It's a composite formula!
res = []
lex.accept_token(OpenBracket)
if lex.test_token(LogicalNot):
# It is of the form (~F) - so store the ~
res.append(lex.look_token().literal) # Lazy!
lex.accept_token(LogicalNot)
res.append(parse_formula(lex)) # Recursive descent to parse F
else:
# It is of the form (F1 * F2), so we parse F1
arg1 = parse_formula(lex) # Recursive descent
# Next has to come the binary operator!
res.append(lex.look_token().literal) # Lazy and optimistic!
lex.accept_token([LogicalAnd, LogicalOr, LogicalEquiv, LogicalImpl])
# Now we parse F2
arg2 = parse_formula(lex) # Recursive descent
res.append(arg1)
res.append(arg2)
lex.accept_token(CloseBracket)
return res
def pretty_list_formula(form):
"""
Given one of the list-style formulas generated by parse_formula(),
convert it back to a nice, syntactically corret WFPF.
This is one example for traversing a recursive structure. It
works on nested lists of a special format, but the principle works
for other structures as well.
"""
if type(form) == type (""):
# It is a string, and hence a proposition and it's own
# representation.
return form
else:
if len(form) == 2:
# It's ~ F
return "(~"+pretty_list_formula(form[1])+")"
else:
assert len(form) == 3; # It has to be F1 op F2
# Note that this is represented as [op F1 F2]!
return "("+pretty_list_formula(form[1])+\
form[0]+\
pretty_list_formula(form[2])+")"
for name in sys.argv[1:]:
if name == "-h":
print __doc__
sys.exit(0)
else:
fp = open(name, "r")
source = fp.read()
fp.close()
lex = lexer(source, name)
while not lex.test_token(EOFToken):
form = parse_formula(lex)
print form
print pretty_list_formula(form)