# beautifHOL: A pretty-printer for higher-order logic

[ program, text ] [ Propose Tags ]

This is a pretty-printer for higher-order logic (HOL). It reads in a formula and outputs it to standard out. A paper describes its design and motivation at the project website. The approach expands upon Leslie Lamport's paper, "How to Write a Long Formula," available at http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#lamport-howtowrite.

Versions 0.1, 0.10, 0.11 array, base, haskell98, mtl [details] LicenseRef-GPL Lee Pike Lee Pike Text http://www.cs.indiana.edu/~lepike/pub_pages/holpp.html by LeePike at Tue Jan 20 03:42:19 UTC 2009 NixOS:0.11 beautifHOL 1291 total (12 in the last 30 days) (no votes yet) [estimated by rule of succession] λ λ λ Docs not available All reported builds failed as of 2017-01-02 Hackage Matrix CI

#### Maintainer's Corner

For package maintainers and hackage trustees

[back to package description]
# 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

#  This file is part of beautifHOL.
# BSD3.

This README contains the following sections:

* Program Description
* 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
be found in the paper, "How to Pretty-Print a Long Formula"
<http://www.cs.indiana.edu/~lepike/pubs/pike-holpp.pdf>.

==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
easiest way to install a Cabal package is to use cabal-install:
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==
* 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

==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.