diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,26 @@ +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +Redistributions of source code must retain the above copyright +notice, this list of conditions and the following disclaimer. + +Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer in the +documentation and/or other materials provided with the distribution. + +Neither the name of Lee Pike; nor the names of its contributors +may be used to endorse or promote products derived from this software +without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,106 @@ +# README for beautifHOL, a HOL prettyprinter +# Based on the paper found at http://www.cs.indiana.edu/~lepike/pub_pages/pphol.html +# Lee Pike (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" +. + +==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 +. The +easiest way to install a Cabal package is to use cabal-install: +. 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 +. + +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 +. 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 + . + + ==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. + + + diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,4 @@ +#! /usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain diff --git a/TestHOL.hs b/TestHOL.hs new file mode 100644 --- /dev/null +++ b/TestHOL.hs @@ -0,0 +1,109 @@ +{- +# Main for beautifHOL, a HOL prettyprinter +# Based on the paper found at http://www.cs.indiana.edu/~lepike/pub_pages/pphol.html +# Lee Pike (remove dashes) +# Jan 5, 2009 +# Copyright 2008 + +# This file is part of beautifHOL. +# BSD3. +-} + +module Main where + +import IO ( stdin, hGetContents ) +import System ( getArgs ) + +import LexHOL +import ParHOL +--import SkelHOL +import PrintHOL +--import AbsHOL +import ErrM +import Data.List + +type ParseFun a = [Token] -> Err a + +myLLexer = myLexer + +runFile :: (Print a, Show a) => Flags -> ParseFun a -> FilePath -> IO () +runFile flags p f = putStrLn f >> readFile f >>= run flags p + +run :: (Print a, Show a) => Flags -> ParseFun a -> String -> IO () +run flags p s = if s == ":q" then putStrLn "Bye." + else let ts = myLLexer s + in case p ts of + Bad s -> do putStrLn "\nParse Failed...\n" + putStrLn "Tokens:" + putStrLn $ show ts + putStrLn s + Ok tree -> do putStrLn "\nParse Successful!" + (if elem silentArg flags + then return () + else showTree flags tree s) + putStrLn "" + putStrLn "" + (if elem fileArg flags + then return () + else do interactMsg + getLine >>= run flags pPROGRAM) + +showTree :: (Show a, Print a) => Flags -> a -> String -> IO () +showTree flags tree s = + do putStrFlg notree ast + putStrFlg notree formulas + putStrLn $ printTree tree flags + where ast = "\n[Abstract Syntax]\n" ++ show tree + formulas = if elem showinputArg flags + then "\n[Input formulas]\n" ++ s + else "" + notree = not $ elem notreeArg flags + putStrFlg b s = if b then putStrLn s else return () + + +interactMsg :: IO () +interactMsg = putStrLn "Reading from standard in. Enter a formula or :q to quit." + +main :: IO () +main = do args <- getArgs + case args of + _ | "-help" `elem` args -> printHelp + | "--help" `elem` args -> printHelp + -- all args (except a possible file handle) recognizable? + | not $ null $ (args \\ (getFile args)) \\ arglst -> printHelp + -- no file given + | (null $ getFile args) && (not $ fileArg `elem` args) + -> do interactMsg + getLine >>= run flags pPROGRAM + -- -f given but no file or non-file + | null (getFile args) && fileArg `elem` args -> printHelp + -- file given + | otherwise -> runFile flags pPROGRAM $ head (getFile args) + where flags = intersect args arglst + getFile a = case (elemIndex fileArg a) of + Nothing -> [] + -- argsLst too short to have file? + Just k -> if length a < k+2 + then [] + -- get file + else [a !! (k+1)] + + +printHelp :: IO () +printHelp = + mapM_ + putStrLn + [ "Usage: TestHOL [--silent] [--notree] [--showinput] " ++ + "[--nolabels] [--help] [--f filename]" + , "where" + , "--silent : Output nothing but whether parsing was successful." + , "--notree : Do not output the parse tree." + , "--showinput : Ouput the input formula(s)." + , "--nolabels : Do not label formulas." + , "--help : Ouput this usage guide." + , "--f filename : the optional text file containing the formulas to be pretty-printed. Otherwise, start the program, and then enter formlas from standard-in." + , "" + , "All options not recognized are ignored." + ] + + diff --git a/beautifHOL.cabal b/beautifHOL.cabal new file mode 100644 --- /dev/null +++ b/beautifHOL.cabal @@ -0,0 +1,23 @@ +Name: beautifHOL +Version: 0.1 +Cabal-Version: >= 1.2 +License: GPL +License-file: LICENSE +Author: Lee Pike +Synopsis: A pretty-printer for higher-order logic +Build-Type: Simple +Description: + 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 + . +Maintainer: Lee Pike +Category: Text +Homepage: http://www.cs.indiana.edu/~lepike/pub_pages/holpp.html +extra-source-files: README +Executable beautifHOL + Main-is: TestHOL.hs + Build-Depends: haskell98, mtl, array, base + +