{-# LANGUAGE ForeignFunctionInterface #-} -- | Progress Bar API module Language.Fixpoint.Utils.Progress ( withProgress , withProgressM , progressInit , progressTick , progressClose ) where import Control.Monad (when) import System.IO.Unsafe (unsafePerformIO) import System.Console.CmdArgs.Verbosity (isNormal, getVerbosity, Verbosity(..)) import Data.IORef import System.Console.AsciiProgress -- import Language.Fixpoint.Misc (traceShow) foreign import ccall unsafe "unistd.h isatty" c_isatty :: Int -> IO Int {-# NOINLINE pbRef #-} pbRef :: IORef (Maybe ProgressBar) pbRef = unsafePerformIO (newIORef Nothing) withProgress :: Int -> IO a -> IO a withProgress = withProgressM id withProgressM :: (m a -> IO b) -> Int -> m a -> IO b withProgressM mToIO n act = do showBar <- (Quiet /=) <$> getVerbosity -- We don't show the progress bar if the output is not a terminal. -- Besides improving the output, this also avoids a concurrency -- issue: -- https://github.com/ucsd-progsys/liquid-fixpoint/issues/782 isTTY <- (== 1) <$> c_isatty 1 if showBar && isTTY then displayConsoleRegions $ do -- putStrLn $ "withProgress: " ++ show n progressInit n r <- mToIO act progressClose return r else mToIO act progressInit :: Int -> IO () progressInit n = do normal <- isNormal when normal $ do pr <- mkPB n writeIORef pbRef (Just pr) mkPB :: Int -> IO ProgressBar mkPB n = newProgressBar def { pgWidth = 80 , pgTotal = {- traceShow "MAKE-PROGRESS" -} toInteger n , pgFormat = "Working :percent [:bar]" , pgPendingChar = '.' , pgOnCompletion = Nothing } progressTick :: IO () progressTick = go =<< readIORef pbRef where go (Just pr) = incTick pr go _ = return () incTick :: ProgressBar -> IO () incTick pb = do st <- getProgressStats pb when (incomplete st) (tick pb) -- then tick pb -- putStrLn (show (stPercent st, stTotal st, stCompleted st)) >> (tick pb) -- else return () incomplete :: Stats -> Bool incomplete st = {- traceShow "INCOMPLETE" -} stRemaining st > 0 -- incomplete st = stPercent st < 100 progressClose :: IO () progressClose = go =<< readIORef pbRef where go (Just p) = complete p go _ = return ()