Progress.hs

{-# 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           Language.Fixpoint.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 ()