beautifHOL (empty) → 0.1
raw patch · 5 files changed
+268/−0 lines, 5 filesdep +arraydep +basedep +haskell98setup-changed
Dependencies added: array, base, haskell98, mtl
Files
- LICENSE +26/−0
- README +106/−0
- Setup.lhs +4/−0
- TestHOL.hs +109/−0
- beautifHOL.cabal +23/−0
+ LICENSE view
@@ -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.
+ README view
@@ -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 <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.+++
+ Setup.lhs view
@@ -0,0 +1,4 @@+#! /usr/bin/env runhaskell++> import Distribution.Simple+> main = defaultMain
+ TestHOL.hs view
@@ -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 <lee-pike-@-gma-il-.com> (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."+ ]++
+ beautifHOL.cabal view
@@ -0,0 +1,23 @@+Name: beautifHOL+Version: 0.1+Cabal-Version: >= 1.2+License: GPL+License-file: LICENSE+Author: Lee Pike <leepike@gmail.com>+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 + <http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#lamport-howtowrite>.+Maintainer: Lee Pike <leepike@gmail.com>+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++