{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NondecreasingIndentation #-}
-- | Description: Log msgs via a synchronized channel
--
-- Log msgs via a synchronized channel.
--
-- With inspiration from the @monad-logger@ package.
--
-- See examples in 'SemMC.Log.Tests'.
--
-- WARNING: loggers that automatically infer the call stack (via
-- `Ghc.HasCallStack`) are not composable, in that they infer a call
-- stack at their call site. So, if you use one to build up another
-- log function, then that derived log function will infer bogus call
-- sites! Of course, it's pretty easy to write
--
--     writeLogEvent logCfg level msg
--
-- when defining a new logger, so not a big deal, just something to
-- watch out for.
module What4.Serialize.Log (
  -- * Misc
  LogLevel(..),
  LogEvent(..),
  LogMsg,
  Ghc.HasCallStack,
  -- * Implicit param logger interface
  HasLogCfg,
  logIO,
  logTrace,
  withLogCfg,
  getLogCfg,
  -- * Explicit parameter logger interface
  logIOWith,
  logEndWith,
  writeLogEvent,
  -- * Monadic logger interface
  MonadHasLogCfg(..),
  logM,
  -- * Configuration
  LogCfg,
  mkLogCfg,
  mkNonLogCfg,
  withLogging,
  -- * Log consumers
  stdErrLogEventConsumer,
  fileLogEventConsumer,
  tmpFileLogEventConsumer,
  -- * Log formatting and consumption (useful for 3rd-party consumers)
  prettyLogEvent,
  consumeUntilEnd,
  -- * Named threads
  named,
  namedIO,
  namedM
  ) where

import qualified GHC.Stack as Ghc

import qualified Control.Concurrent as Cc
import qualified Control.Exception as Cc
import           Control.Monad (when)

import qualified Data.Time.Clock as T
import qualified Data.Time.Format as T

import qualified System.IO as IO
import qualified System.IO.Unsafe as IO

import qualified UnliftIO as U

import qualified Control.Concurrent.STM as Stm
import qualified Control.Concurrent.BoundedChan as BC
import           Control.Monad.IO.Class ( MonadIO, liftIO )
import           Data.Map.Strict ( Map )
import qualified Data.Map.Strict as Map
import           System.Directory ( createDirectoryIfMissing, getTemporaryDirectory )
import           Text.Printf ( printf )

import Debug.Trace

----------------------------------------------------------------
-- * API

-- | Log levels, in increasing severity/precedence order.
data LogLevel = Debug -- ^ Fine details
              | Info  -- ^ Tracking progress
              | Warn  -- ^ Something notable or suspicious
              | Error -- ^ Something bad
              deriving (Show, Eq, Ord, Read)

type LogMsg = String

----------------------------------------------------------------
-- ** Implicit param logger interface

-- | Access to the log config.
--
-- Users should prefer 'withLogCfg' to binding the implicit param. The
-- implicit param is an implementation detail, and we could change the
-- implementation later, e.g. to use the @reflection@ package.
--
-- We use an implicit param to avoid having to change all code in 'IO'
-- that wants to log to be in 'MonadHasLogCfg' and 'MonadIO' classes.
--
-- An even more convenient but more \"unsafe\" implementation would
-- store the 'LogCfg' in a global, 'unsafePerformIO'd 'IORef'
-- (cf. @uniqueSource@ in 'Data.Unique').
type HasLogCfg = (?logCfg :: LogCfg)

-- | Satisfy a 'HasLogCfg' constraint.
--
-- Users can call this function instead of using @ImplicitParams@
-- themselves.
withLogCfg :: LogCfg -> (HasLogCfg => a) -> a
withLogCfg logCfg x = let ?logCfg = logCfg in x

-- | Recover the log config.
--
-- Useful for going between implicit and monadic interfaces. E.g.
--
-- > flip runReaderT getLogCfg ...
getLogCfg :: HasLogCfg => LogCfg
getLogCfg = ?logCfg

-- | Log in a 'MonadIO'.
--
-- If you want the name of function that called 'log' to be included
-- in the output, then you need to add a 'Ghc.HasCallStack' constraint
-- to it as well (see 'LogC'). Otherwise, one of two things will happen:
--
-- - if no enclosing function has a 'Ghc.HasCallStack' constraint,
--   then '???' will be used for the enclosing function name.
--
-- - if at least one enclosing function has a 'Ghc.HasCallStack'
--   constraint, then the name of the *closest* enclosing function
--   with that constraint will be used for the enclosing function
--   name. So, for example, if you define @outer@ by
--
--   > outer :: (MonadHasLogCfg m, Ghc.HasCallStack) => m Int
--   > outer = inner
--   >   where
--   >     inner = do
--   >       log Debug "Inside 'inner' ..."
--   >       return 42
--
--   then the call to 'log' in @inner@ will have \"outer\" as the
--   enclosing function name.
logIO :: (HasLogCfg, Ghc.HasCallStack, MonadIO m)
      => LogLevel -> LogMsg -> m ()
logIO level msg = do
  liftIO $ writeLogEvent ?logCfg Ghc.callStack level msg

-- | 'logIO' with an explicit config
logIOWith :: (Ghc.HasCallStack, MonadIO m) => LogCfg -> LogLevel -> LogMsg -> m ()
logIOWith cfg level msg =
  liftIO $ writeLogEvent cfg Ghc.callStack level msg

-- | Log in pure code using 'unsafePerformIO', like 'Debug.Trace'.
--
-- See 'logIO'.
logTrace :: (HasLogCfg, Ghc.HasCallStack) => LogLevel -> LogMsg -> a -> a
logTrace level msg x = IO.unsafePerformIO $ do
  writeLogEvent ?logCfg Ghc.callStack level msg
  return x
{-# NOINLINE logTrace #-}

----------------------------------------------------------------
-- ** Monadic logger interface

-- | Monads with logger configuration.
class MonadHasLogCfg m where
  getLogCfgM :: m LogCfg

-- | Log in a 'MonadHasLogCfg'.
--
-- See 'logIO'.
logM :: (MonadHasLogCfg m, Ghc.HasCallStack, MonadIO m)
     => LogLevel -> LogMsg -> m ()
logM level msg = do
  logCfg <- getLogCfgM
  liftIO $ writeLogEvent logCfg Ghc.callStack level msg

-- | Signal to the log consumer that there are no more log messages and
-- terminate the log consumer.  This is useful for cases where the logger is
-- running in a separate thread and the parent thread wants to wait until the
-- logger has finished logging and has successfully flushed all log messages
-- before terminating it.
logEndWith :: LogCfg -> IO ()
logEndWith cfg = case lcChan cfg of
                   Just c -> BC.writeChan c Nothing
                   Nothing -> return ()

----------------------------------------------------------------
-- ** Initialization

-- | Initialize a 'LogCfg'.
--
-- The first argument is the human friendly name to assign to the
-- current thread. Since logging should be configured as soon as
-- possible on startup, \"main\" is probably the right name.
--
-- See 'asyncNamed' for naming other threads.
--
-- Need to start a log event consumer in another thread,
-- e.g. 'stdErrLogEventConsumer', if you want anything to happen with
-- the log events.
mkLogCfg :: String -> IO LogCfg
mkLogCfg threadName = do
  chan <- BC.newBoundedChan 100
  threadMap <- do
    tid <- show <$> Cc.myThreadId
    return $ Map.fromList [ (tid, threadName) ]
  threadMapVar <- Stm.newTVarIO threadMap
  return $ LogCfg { lcChan = Just chan
                  , lcThreadMap = threadMapVar }


-- | Initialize a 'LogCfg' that does no logging.
--
-- This can be used as a LogCfg when no logging is to be performed.
-- Runtime overhead is smaller when this configuration is specified at
-- compile time.
mkNonLogCfg :: IO LogCfg
mkNonLogCfg = do tmVar <- Stm.newTVarIO Map.empty
                 return LogCfg { lcChan = Nothing
                               , lcThreadMap = tmVar
                               }


-- | Run an action with the given log event consumer.
--
-- In particular this provides an easy way to run one-off computations
-- that assume logging, e.g. in GHCi. Spawns the log even consumer
-- before running the action and cleans up the log event consumer
-- afterwards.
withLogging :: (U.MonadUnliftIO m, MonadIO m)
            => String -> (LogCfg -> IO ()) -> (HasLogCfg => m a) -> m a
withLogging threadName logEventConsumer action = do
  cfg <- liftIO $ mkLogCfg threadName
  U.withAsync (liftIO $ logEventConsumer cfg) $ \a -> do
  x <- withLogCfg cfg action
  liftIO $ logEndWith cfg
  U.wait a
  return x

----------------------------------------------------------------
-- ** Log event consumers

-- | Consume a log channel until it receives a shutdown message
-- (i.e. a 'Nothing').
--
-- Only messages that satisfy the predicate will be passed to the
-- continuation. For example, using @const True@ will process all log
-- messages, and using @(>= Info) . leLevel@ will only process
-- messsages with 'LogLevel' equal to 'Info' or higher, ignoring
-- 'Debug' level messages.
consumeUntilEnd ::
  (LogEvent -> Bool) -> (LogEvent -> IO ()) -> LogCfg -> IO ()
consumeUntilEnd keepEvent k cfg =
  case lcChan cfg of
    Nothing -> return ()
    Just c -> do
      mevent <- BC.readChan c
      case mevent of
        Just event -> do when (keepEvent event) $ k event
                         consumeUntilEnd keepEvent k cfg
        _ -> return ()

-- | A log event consumer that prints formatted log events to stderr.
stdErrLogEventConsumer :: (LogEvent -> Bool) -> LogCfg -> IO ()
stdErrLogEventConsumer keepEvent =
  consumeUntilEnd keepEvent $ \e -> do
    -- Use 'traceIO' because it seems to be atomic in practice,
    -- avoiding problems with interleaving output from other sources.
    traceIO (prettyLogEvent e)
    IO.hFlush IO.stderr -- Probably unnecessary.

-- | A logger that writes to a user-specified file
--
-- Note that logs are opened in the 'w' mode (i.e., overwrite).  Callers should
-- preserve old log files if they really want.
fileLogEventConsumer :: FilePath -> (LogEvent -> Bool) -> LogCfg -> IO ()
fileLogEventConsumer fp keepEvent cfg = IO.withFile fp IO.WriteMode $ \h -> do
  let k e = IO.hPutStrLn h (prettyLogEvent e) >> IO.hFlush h
  consumeUntilEnd keepEvent k cfg

-- | A log event consumer that writes formatted log events to a tmp
-- file.
tmpFileLogEventConsumer :: (LogEvent -> Bool) -> LogCfg -> IO ()
tmpFileLogEventConsumer keepEvent cfg = do
  tmpdir <- (++ "/brittle") <$> getTemporaryDirectory
  createDirectoryIfMissing True tmpdir
  (tmpFilePath, tmpFile) <- IO.openTempFile tmpdir "log.txt"
  printf "\n\nWriting logs to %s\n\n" tmpFilePath
  let k e = IO.hPutStrLn tmpFile (prettyLogEvent e) >> IO.hFlush tmpFile
  consumeUntilEnd keepEvent k cfg

----------------------------------------------------------------
-- ** Named threads

-- | Run an IO action with a human friendly thread name.
--
-- Any existing thread name will be restored when the action finishes.
named :: (U.MonadUnliftIO m, MonadIO m) => LogCfg -> String -> m a -> m a
named cfg threadName action = do
  actionIO <- U.toIO action
  liftIO $ do
    tid <- show <$> Cc.myThreadId
    mOldName <- Map.lookup tid <$> Stm.readTVarIO (lcThreadMap cfg)
    Cc.bracket_ (insert tid) (remove tid mOldName) actionIO
  where
    modify = Stm.atomically . Stm.modifyTVar' (lcThreadMap cfg)

    insert tid = modify $ Map.insert tid threadName

    remove tid Nothing        = modify $ Map.delete tid
    remove tid (Just oldName) = modify $ Map.insert tid oldName

-- | Version of 'named' for implicit log cfg.
namedIO :: (HasLogCfg, U.MonadUnliftIO m, MonadIO m)
        => String -> m a -> m a
namedIO threadName action = named ?logCfg threadName action

-- | Version of 'named' for 'MonadHasLogCfg' monads.
namedM :: (MonadHasLogCfg m, U.MonadUnliftIO m, MonadIO m)
       => String -> m a -> m a
namedM threadName action = do
  cfg <- getLogCfgM
  named cfg threadName action

----------------------------------------------------------------
-- * Internals

-- | Stored as 'String' because 'Control.Concurrent.ThreadId' docs say
-- a thread can't be GC'd as long as someone maintains a reference to
-- its 'ThreadId'!!!
type ThreadId = String

-- | A log event.
--
-- Can be converted to a string later, or thrown away.
data LogEvent = LogEvent
  { leCallSite :: (Maybe String, Ghc.SrcLoc)
    -- ^ The @Maybe String@ is the name of the enclosing function in
    -- which the logging function was called. Not always available,
    -- since it depends on the enclosing function having a
    -- 'Ghc.HasCallStack' constraint.
  , leLevel    :: LogLevel
  , leMsg      :: LogMsg
  , leThreadId :: ThreadId
    -- ^ ID of thread that generated the event.
  , leTime     :: T.UTCTime
  }

-- | Logging configuration.
data LogCfg = LogCfg
  { lcChan :: Maybe (BC.BoundedChan (Maybe LogEvent))
  , lcThreadMap :: Stm.TVar (Map ThreadId String)
    -- ^ User friendly names for threads. See 'asyncNamed'.

  -- Idea: add a predicate on log events that is used to discard log
  -- events that e.g. aren't of a high enough precedence
  -- level. E.g. only keep events of level 'Warn' or above:
  --
  -- > lcPred le = leLevel le >= Warn
  --
  -- , lcPred :: LogEvent -> Bool
  }

-- | Format a log event.
prettyLogEvent :: LogEvent -> String
prettyLogEvent le =
  printf "[%s][%s][%s][%s]\n%s"
    (show $ leLevel le) time location (leThreadId le) (leMsg le)
  where
    time :: String
    time = T.formatTime T.defaultTimeLocale "%T" (leTime le)
    location :: String
    location = printf "%s:%s"
      (prettyFun maybeFun) (Ghc.prettySrcLoc srcLoc)
    (maybeFun, srcLoc) = leCallSite le
    prettyFun Nothing = "???"
    prettyFun (Just fun) = fun

prettyThreadId :: LogCfg -> ThreadId -> IO ThreadId
prettyThreadId cfg tid = do
  mThreadName <- Map.lookup tid <$> Stm.readTVarIO (lcThreadMap cfg)
  return $ printf "%s (%s)" (maybe "???" id mThreadName) tid

-- | Write a 'LogEvent' to the underlying channel.
--
-- This is a low-level function. See 'logIO', 'logM', and 'logTrace'
-- for a high-level interface that supplies the 'LogCfg' and
-- 'Ghc.CallStack' parameters automatically.
--
-- However, those functions can't be used to build up custom loggers,
-- since they infer call stack information automatically. If you want
-- to define a custom logger (even something simple like
--
-- > debug msg = logM Debug msg
--
-- ) then use 'writeLogEvent'.
writeLogEvent :: LogCfg -> Ghc.CallStack -> LogLevel -> LogMsg -> IO ()
writeLogEvent cfg cs level msg = do
  tid <- show <$> Cc.myThreadId
  ptid <- prettyThreadId cfg tid
  time <- T.getCurrentTime
  case lcChan cfg of
    Nothing -> return ()
    Just c -> BC.writeChan c (Just (event ptid time))
  where
    event tid time = LogEvent
      { leCallSite = callSite
      , leLevel = level
      , leMsg = msg
      , leThreadId = tid
      , leTime = time
      }
    -- | The call stack has the most recent call first. Assuming
    -- 'writeLogEvent' is always called in a logging function with a
    -- 'Ghc.HasCallStack' constraint, the call stack will be non-empty
    -- -- i.e. @topSrcLoc@ will be defined -- but there may not be a
    -- lower frame corresponding to the context in which the logging
    -- function was called. To get a lower frame, some enclosing
    -- function needs a 'Ghc.HasCallStack' constraint itself.
    --
    -- And only functions with 'Ghc.HasCallStack' will get frames. See
    -- discussion at 'log'.
    callSite = case Ghc.getCallStack cs of
                 (_,topSrcLoc):rest -> case rest of
                   []                 -> (Nothing,           topSrcLoc)
                   (enclosingFun,_):_ -> (Just enclosingFun, topSrcLoc)
                 [] -> error "Do we ever not have a call site?"