# README for beautifHOL, a HOL prettyprinter
# Based on the paper found at http://www.cs.indiana.edu/~lepike/pub_pages/pphol.html
# Lee Pike <lee-pike-@-gma-il-.com> (remove dashes)
# Jan 5, 2009
# Copyright 2008
# This file is part of beautifHOL.
# BSD3.
This README contains the following sections:
* Program Description
* License information
* Installation information
* Usage information
* How to modify the program
* Todos (including known bugs)
==DESCRIPTION==
This is a pretty-printer for higher-order logic (HOL). It reads in a formula
and outputs it to standard out. More information about the pretty-printer can
be found in the paper, "How to Pretty-Print a Long Formula"
<http://www.cs.indiana.edu/~lepike/pubs/pike-holpp.pdf>.
==LICENSE==
BSD3 license.
==INSTALLATION==
This program is distributed as a Cabal package, a packaging system for Haskell
programs. For information on how to install a Cabal package, see
<http://www.haskell.org/haskellwiki/Cabal/How_to_install_a_Cabal_package>. The
easiest way to install a Cabal package is to use cabal-install:
<http://hackage.haskell.org/trac/hackage/wiki/CabalInstall>. Instructions for
getting cabal-install are located there.
==USAGE==
If you install this program using Cabal (describe above), then the executable,
beautifulHOL, should be in your path. Then issue
> beautifHOL
to interact with the program in a read-eval-print loop. From there, you can
enter HOL formulas. Examples of the syntax can be found in the file
formulas.txt. Be sure to terminate a formula with a semicolon. After entering
a formula, its pretty-printed rendering will be sent to standard out.
The available options to the program can be seen by issuing
> beautifHOL --help
Among others, there is an option to suppress labels (--nolabel) and an option to
read in a set of formulas from a file and print their renderings to
standard-out. For example, issuing
> beautifHOL --f formulas.txt
will render all the example formulas.
==MODIFYING THE PROGRAM==
The syntax of the current input language is documented in
<http://www.cs.indiana.edu/~lepike/pub_pages/docHOL.pdf>.
To modify the input language to use with other variants of HOL, you will need
the BNF Converter (BNFC). BNFC is an GPL-licensed that generates a
compiler-front end from a labeled Bakus Normal Form language specification. It
also generates docs, etc. BNFC is available at
<http://www.cs.chalmers.se/Cs/Research/Language-technology/BNFC/>. The latest
version can be obtained by issuing
darcs get --partial
http://www.cs.chalmers.se/Cs/Research/Language-technology/darcs/BNFC/
There are only three files you need to modify:
* HOL.cf, the BNF specification of the input grammar, read in by BNFC.
* PrintHOL.hs, the guts of the pretty-printer.
* ConfigHOL.hs,
==TODOs==
==Code Cleanups==
* Remove dead code.
* Run HPC and HLint over this.
* How spaces are handled needs to be reimplemented.
* Should be reimplemented to use SPJ/John Hughes pretty-printing library:
pretty on Hackage
<http://hackage.haskell.org/cgi-bin/hackage-scripts/package/pretty>.
==New Functionality==
* Desired new functionality is described in the accompanying paper, "How to
Pretty-Print a Long Formula" (pphol.pdf).
* Better parse-error messages.
==Bugs/Issues==
* Can't have a breakline char -- it'll break things if it's really a string (e.g., Latex).
* There are known issues with using different widths for spcStr, argSepStr, etc.
* Parsing doesn't work if there is whitespace between relation or function
identifiers and parentheses.
* In ConfigHOL.hs, "in" is defined "in " to fix a pretty-printing bug.
