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.