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.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1, 0.10, 0.11
Dependencies array, base, haskell98, mtl [details]
License LicenseRef-GPL
Author Lee Pike <leepike@gmail.com>
Maintainer Lee Pike <leepike@gmail.com>
Category Text
Home page http://www.cs.indiana.edu/~lepike/pub_pages/holpp.html
Uploaded by LeePike at 2009-01-21T05:53:49Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Executables beautifHOL
Downloads 2725 total (10 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-10-27 [all 10 reports]

Readme for beautifHOL-0.11

[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
# 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==

==
MODIFYING THE INPUT LANGUAGE
==

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/

BNFC will generate new files for you based on your new input language.  The
current input language is defined in HOL.cf as a labeled BNF grammar.  Edit this
file.  *BE SURE* to move or rename PrintHOL.hs, ConfigHOL.hs, and TestHOL.hs
when generating new files as BNFC will overwrite these files (which have been
modified in beautifHOL).  After generation from BNFC, overwrite the generated
files and compile as usual.  If you have added new language constructs, you will
have to add corresponding cases to PrintHOL.hs.

==
MODIFYING ANYTHING ELSE
==
If you want to modify only the output syntax or the pretty-printing style, you
need only to modify one or more of the following files:
  * PrintHOL.hs, the guts of the pretty-printer.
  * ConfigHOL.hs, where user-defined constants are (e.g., the output syntax for
    conjunction, the maximum length of a formula on a line, etc.).
  * TestHOL.hs, where main is defined.

You do *NOT* need BNFC to make these modifications.  Simply rebuild the program
by issuing 
  > ghc --make TestHOL.hs -o beautifHOL
or
  > runhaskell Setup.lhs configure
  > runhaskell Setup.lhs build
  > runhaskell Setup.lhs install

BE SURE TO SEND ME ANY PATCHES!

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