{-
# 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."
]