{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Crux.Log (
  -- * Output Configuration
  Logs,
  OutputConfig(..)
  , outputHandle
  , quiet
  -- * Standard output API functions
  , CruxLogMessage(..)
  , LogDoc(..)
  , LogProofObligation(..)
  , SayWhat(..)
  , SayLevel(..)
  , SupportsCruxLogMessage
  , cruxLogMessageToSayWhat
  , cruxLogTag
  , logException
  , logGoal
  , logSimResult
  , say
  , sayCrux
  , withCruxLogMessage
  -- * Low-level output API functions
  , output
  , outputLn
  -- * Converting and emitting output
  , logToStd
  ) where

import           Control.Exception ( SomeException, bracket_,  )
import           Control.Lens ( Getter, view )
import qualified Data.Aeson as JSON
import           Data.Aeson.TH ( deriveToJSON )
import qualified Data.Text as T
import           Data.Text.IO as TIO ( hPutStr, hPutStrLn )
import           Data.Version ( Version, showVersion )
import           Data.Word ( Word64 )
import           GHC.Generics ( Generic )
import qualified Lumberjack as LJ
import           Prettyprinter ( SimpleDocStream )
import           Prettyprinter.Render.Text ( renderStrict )
import           System.Console.ANSI
    ( Color(..), ColorIntensity(..), ConsoleIntensity(..), ConsoleLayer(..)
    , SGR(..), hSetSGR )
import           System.IO ( Handle, hPutStr, hPutStrLn )

import           Crux.Types
    ( CruxSimulationResult, ProvedGoals, SayLevel(..), SayWhat(..) )
import           Crux.Version ( version )
import           Lang.Crucible.Backend ( ProofGoal(..), ProofObligation )
import           What4.Expr.Builder ( ExprBuilder )
import           What4.LabeledPred ( labeledPred, labeledPredMsg )

----------------------------------------------------------------------
-- Various functions used by the main code to generate logging output

newtype LogDoc = LogDoc (SimpleDocStream ())

instance JSON.ToJSON LogDoc where
  toJSON :: LogDoc -> Value
toJSON (LogDoc SimpleDocStream ()
doc) = Text -> Value
JSON.String (SimpleDocStream () -> Text
forall ann. SimpleDocStream ann -> Text
renderStrict SimpleDocStream ()
doc)

-- | A version of 'ProofObligation' that supports a 'ToJSON' instance.
data LogProofObligation =
  forall t st fs.
  LogProofObligation (ProofObligation (ExprBuilder t st fs))

instance JSON.ToJSON LogProofObligation where
  -- for now, we only need the goal in the IDE
  toJSON :: LogProofObligation -> Value
toJSON (LogProofObligation ProofObligation (ExprBuilder t st fs)
g) =
    let
      goal :: LabeledPred (Expr t BaseBoolType) SimError
goal = ProofGoal
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError)
-> LabeledPred (Expr t BaseBoolType) SimError
forall asmp goal. ProofGoal asmp goal -> goal
proofGoal ProofObligation (ExprBuilder t st fs)
ProofGoal
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError)
g
    in
    [Pair] -> Value
JSON.object [ Key
"labeledPred" Key -> String -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
JSON..= Expr t BaseBoolType -> String
forall a. Show a => a -> String
show (Getting
  (Expr t BaseBoolType)
  (LabeledPred (Expr t BaseBoolType) SimError)
  (Expr t BaseBoolType)
-> LabeledPred (Expr t BaseBoolType) SimError
-> Expr t BaseBoolType
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Expr t BaseBoolType)
  (LabeledPred (Expr t BaseBoolType) SimError)
  (Expr t BaseBoolType)
forall pred msg pred' (f :: * -> *).
Functor f =>
(pred -> f pred')
-> LabeledPred pred msg -> f (LabeledPred pred' msg)
labeledPred LabeledPred (Expr t BaseBoolType) SimError
goal)
                , Key
"labeledPredMsg" Key -> String -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
JSON..= SimError -> String
forall a. Show a => a -> String
show (Getting
  SimError (LabeledPred (Expr t BaseBoolType) SimError) SimError
-> LabeledPred (Expr t BaseBoolType) SimError -> SimError
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  SimError (LabeledPred (Expr t BaseBoolType) SimError) SimError
forall pred msg msg' (f :: * -> *).
Functor f =>
(msg -> f msg')
-> LabeledPred pred msg -> f (LabeledPred pred msg')
labeledPredMsg LabeledPred (Expr t BaseBoolType) SimError
goal)
                ]

-- | All messages that Crux wants to output should be listed here.
--
-- Messages ought to be serializable to JSON so that they have a somewhat
-- portable machine-readable representation.  Some tools may rely on the
-- serialization format, so be sure to check with consumers before changing the
-- 'ToJSON' instance.
--
-- Other crux-based tools are encouraged to create their own:
--
-- * log message datatype '<Tool>LogMessage', similar to 'CruxLogMessage' below,
--
-- * constraint synonym 'Supports<Tool>LogMessage' similar to
-- 'SupportsCruxLogMessage' below,
--
-- * constraint dispatcher 'with<Tool>LogMessage' similar to
-- 'withCruxLogMessage' below,
--
-- * logger method 'say<Tool>' similar to 'sayCrux' below,
--
-- * default log message converter '<Tool>LogMessageToSayWhat' similar to
-- 'cruxLogMessageToSayWhat'.
--
-- The default log message converter can be used to decide how messages are
-- displayed to the standard output for a human consumer.  Automated tools may
-- prefer to filter and encode log messages in some machine-readable format and
-- exchange it over a separate channel.
data CruxLogMessage
  = AttemptingProvingVCs
  | Checking [FilePath]
  | DisablingBranchCoverageRequiresPathSatisfiability
  | DisablingProfilingIncompatibleWithPathSplitting
  | EndedGoal Integer
  | FoundCounterExample
  | Help LogDoc
  | PathsUnexplored Int
  | ProofObligations [LogProofObligation]
  | SimulationComplete
  | SimulationTimedOut
  | SkippingUnsatCoresBecauseMCSatEnabled
  | StartedGoal Integer
  | TotalPathsExplored Word64
  | UnsupportedTimeoutFor String -- ^ name of the backend
  | Version T.Text Version
  deriving ((forall x. CruxLogMessage -> Rep CruxLogMessage x)
-> (forall x. Rep CruxLogMessage x -> CruxLogMessage)
-> Generic CruxLogMessage
forall x. Rep CruxLogMessage x -> CruxLogMessage
forall x. CruxLogMessage -> Rep CruxLogMessage x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CruxLogMessage -> Rep CruxLogMessage x
from :: forall x. CruxLogMessage -> Rep CruxLogMessage x
$cto :: forall x. Rep CruxLogMessage x -> CruxLogMessage
to :: forall x. Rep CruxLogMessage x -> CruxLogMessage
Generic)

$(deriveToJSON JSON.defaultOptions ''CruxLogMessage)


type SupportsCruxLogMessage msgs =
  ( ?injectCruxLogMessage :: CruxLogMessage -> msgs )

withCruxLogMessage ::
  (SupportsCruxLogMessage CruxLogMessage => a) -> a
withCruxLogMessage :: forall a. (SupportsCruxLogMessage CruxLogMessage => a) -> a
withCruxLogMessage SupportsCruxLogMessage CruxLogMessage => a
a =
  let ?injectCruxLogMessage = SupportsCruxLogMessage CruxLogMessage
CruxLogMessage -> CruxLogMessage
forall a. a -> a
id in a
SupportsCruxLogMessage CruxLogMessage => a
a


cruxLogTag :: T.Text
cruxLogTag :: Text
cruxLogTag = Text
"Crux"


cruxNoisily :: T.Text -> SayWhat
cruxNoisily :: Text -> SayWhat
cruxNoisily = SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Noisily Text
cruxLogTag

cruxOK :: T.Text -> SayWhat
cruxOK :: Text -> SayWhat
cruxOK = SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
OK Text
cruxLogTag

cruxSimply :: T.Text -> SayWhat
cruxSimply :: Text -> SayWhat
cruxSimply = SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Simply Text
cruxLogTag

cruxWarn :: T.Text -> SayWhat
cruxWarn :: Text -> SayWhat
cruxWarn = SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Warn Text
cruxLogTag


cruxLogMessageToSayWhat :: CruxLogMessage -> SayWhat

cruxLogMessageToSayWhat :: CruxLogMessage -> SayWhat
cruxLogMessageToSayWhat CruxLogMessage
AttemptingProvingVCs =
  Text -> SayWhat
cruxSimply Text
"Attempting to prove verification conditions."

cruxLogMessageToSayWhat (Checking [String]
files) =
  Text -> SayWhat
cruxNoisily (Text
"Checking " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
", " (String -> Text
T.pack (String -> Text) -> [String] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
files))

cruxLogMessageToSayWhat CruxLogMessage
DisablingBranchCoverageRequiresPathSatisfiability =
  Text -> SayWhat
cruxWarn
    Text
"Branch coverage requires enabling path satisfiability checking.  Coverage measurement is disabled!"

cruxLogMessageToSayWhat CruxLogMessage
DisablingProfilingIncompatibleWithPathSplitting =
  Text -> SayWhat
cruxWarn
    Text
"Path splitting strategies are incompatible with Crucible profiling. Profiling is disabled!"

-- for now, this message is only for IDE consumers
cruxLogMessageToSayWhat (EndedGoal {}) = SayWhat
SayNothing

cruxLogMessageToSayWhat CruxLogMessage
FoundCounterExample =
  Text -> SayWhat
cruxOK Text
"Counterexample found, skipping remaining goals"

cruxLogMessageToSayWhat (Help (LogDoc SimpleDocStream ()
doc)) =
  Text -> SayWhat
cruxOK (SimpleDocStream () -> Text
forall ann. SimpleDocStream ann -> Text
renderStrict SimpleDocStream ()
doc)

cruxLogMessageToSayWhat (PathsUnexplored Int
numberOfPaths) =
  Text -> SayWhat
cruxWarn
    ( [Text] -> Text
T.unwords
        [ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
numberOfPaths,
          Text
"paths remaining not explored: program might not be fully verified"
        ]
    )

-- for now, this message is only for IDE consumers
cruxLogMessageToSayWhat (ProofObligations {}) = SayWhat
SayNothing

cruxLogMessageToSayWhat CruxLogMessage
SimulationComplete =
  Text -> SayWhat
cruxNoisily Text
"Simulation complete."

cruxLogMessageToSayWhat CruxLogMessage
SimulationTimedOut =
  Text -> SayWhat
cruxWarn
    Text
"Simulation timed out! Program might not be fully verified!"

cruxLogMessageToSayWhat CruxLogMessage
SkippingUnsatCoresBecauseMCSatEnabled =
  Text -> SayWhat
cruxWarn Text
"Warning: skipping unsat cores because MC-SAT is enabled."

-- for now, this message is only for IDE consumers
cruxLogMessageToSayWhat (StartedGoal {}) = SayWhat
SayNothing

cruxLogMessageToSayWhat (TotalPathsExplored Word64
i) =
  Text -> SayWhat
cruxSimply (Text
"Total paths explored: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Word64 -> String
forall a. Show a => a -> String
show Word64
i))

cruxLogMessageToSayWhat (UnsupportedTimeoutFor String
backend) =
  Text -> SayWhat
cruxWarn
    (String -> Text
T.pack (String
"Goal timeout requested but not supported by " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
backend))

cruxLogMessageToSayWhat (Version Text
nm Version
ver) =
  Text -> SayWhat
cruxOK
    ( String -> Text
T.pack
        ( [String] -> String
unwords
            [ String
"version: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
version String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
",",
              Text -> String
T.unpack Text
nm,
              String
"version: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> (Version -> String
showVersion Version
ver)
            ]
        )
    )

-- | Main function used to log/output a general text message of some kind
say ::
  Logs msgs =>
  ( ?injectMessage :: msg -> msgs ) =>
  msg -> IO ()
say :: forall msgs msg.
(Logs msgs, ?injectMessage::msg -> msgs) =>
msg -> IO ()
say = LogAction IO msgs -> msgs -> IO ()
forall (m :: * -> *) msg. LogAction m msg -> msg -> m ()
LJ.writeLog (Getting (LogAction IO msgs) (OutputConfig msgs) (LogAction IO msgs)
-> OutputConfig msgs -> LogAction IO msgs
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (LogAction IO msgs) (OutputConfig msgs) (LogAction IO msgs)
forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(LogAction IO msgs -> f (LogAction IO msgs))
-> OutputConfig msgs -> f (OutputConfig msgs)
logMsg Logs msgs
OutputConfig msgs
?outputConfig) (msgs -> IO ()) -> (msg -> msgs) -> msg -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ?injectMessage::msg -> msgs
msg -> msgs
?injectMessage

sayCrux ::
  Logs msgs =>
  SupportsCruxLogMessage msgs =>
  CruxLogMessage -> IO ()
sayCrux :: forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux CruxLogMessage
msg =
  let ?injectMessage = SupportsCruxLogMessage msgs
?injectMessage::CruxLogMessage -> msgs
CruxLogMessage -> msgs
?injectCruxLogMessage in
  CruxLogMessage -> IO ()
forall msgs msg.
(Logs msgs, ?injectMessage::msg -> msgs) =>
msg -> IO ()
say CruxLogMessage
msg

-- | Function used to log/output exception information
logException :: Logs msgs => SomeException -> IO ()
logException :: forall msgs. Logs msgs => SomeException -> IO ()
logException = LogAction IO SomeException -> SomeException -> IO ()
forall (m :: * -> *) msg. LogAction m msg -> msg -> m ()
LJ.writeLog (OutputConfig msgs -> LogAction IO SomeException
forall msgs. OutputConfig msgs -> LogAction IO SomeException
_logExc Logs msgs
OutputConfig msgs
?outputConfig)

-- | Function used to output the summary result for a completed
-- simulation.  If the flag is true, show the details of each failed
-- goal before showing the summary.
logSimResult :: Logs msgs => Bool -> CruxSimulationResult -> IO ()
logSimResult :: forall msgs. Logs msgs => Bool -> CruxSimulationResult -> IO ()
logSimResult Bool
showFailedGoals = LogAction IO CruxSimulationResult -> CruxSimulationResult -> IO ()
forall (m :: * -> *) msg. LogAction m msg -> msg -> m ()
LJ.writeLog (OutputConfig msgs -> Bool -> LogAction IO CruxSimulationResult
forall msgs.
OutputConfig msgs -> Bool -> LogAction IO CruxSimulationResult
_logSimResult Logs msgs
OutputConfig msgs
?outputConfig Bool
showFailedGoals)

-- | Function used to output any individual goal proof failures from a simulation
logGoal :: Logs msgs => ProvedGoals -> IO ()
logGoal :: forall msgs. Logs msgs => ProvedGoals -> IO ()
logGoal = LogAction IO ProvedGoals -> ProvedGoals -> IO ()
forall (m :: * -> *) msg. LogAction m msg -> msg -> m ()
LJ.writeLog (OutputConfig msgs -> LogAction IO ProvedGoals
forall msgs. OutputConfig msgs -> LogAction IO ProvedGoals
_logGoal Logs msgs
OutputConfig msgs
?outputConfig)


----------------------------------------------------------------------
-- Logging types and constraints

-- | The Logs constraint should be applied for any function that will
-- use the main logging functions: says, logException, logSimResult,
-- or logGoal.
type Logs msgs = ( ?outputConfig :: OutputConfig msgs )

-- | Global options for Crux's main. These are not CruxOptions because
-- they are expected to be set directly by main, rather than by a
-- user's command-line options. They exist primarily to improve the
-- testability of the code.
--
-- The Crux mkOutputConfig is recommended as a helper function for
-- creating this object, although it can be initialized directly if
-- needed.
data OutputConfig msgs =
  OutputConfig { forall msgs. OutputConfig msgs -> Handle
_outputHandle :: Handle
               , forall msgs. OutputConfig msgs -> Bool
_quiet :: Bool
               , forall msgs. OutputConfig msgs -> LogAction IO msgs
_logMsg :: LJ.LogAction IO msgs
               , forall msgs. OutputConfig msgs -> LogAction IO SomeException
_logExc :: LJ.LogAction IO SomeException
               , forall msgs.
OutputConfig msgs -> Bool -> LogAction IO CruxSimulationResult
_logSimResult :: Bool -> LJ.LogAction IO CruxSimulationResult
                 -- ^ True to show individual goals, false for summary only
               , forall msgs. OutputConfig msgs -> LogAction IO ProvedGoals
_logGoal :: LJ.LogAction IO ProvedGoals
               }

-- | Some client code will want to output to the main output stream
-- directly instead of using the logging/output functions above.  It
-- can either get the _outputHandle directly or it can use the
-- output/outputLn functions below.
outputHandle :: Getter (OutputConfig msgs) Handle
outputHandle :: forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(Handle -> f Handle) -> OutputConfig msgs -> f (OutputConfig msgs)
outputHandle Handle -> f Handle
f OutputConfig msgs
o = OutputConfig msgs
o OutputConfig msgs -> f Handle -> f (OutputConfig msgs)
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Handle -> f Handle
f (OutputConfig msgs -> Handle
forall msgs. OutputConfig msgs -> Handle
_outputHandle OutputConfig msgs
o)

-- | Lens to allow client code to determine if running in quiet mode.
quiet :: Getter (OutputConfig msgs) Bool
quiet :: forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(Bool -> f Bool) -> OutputConfig msgs -> f (OutputConfig msgs)
quiet Bool -> f Bool
f OutputConfig msgs
o = OutputConfig msgs
o OutputConfig msgs -> f Bool -> f (OutputConfig msgs)
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> f Bool
f (OutputConfig msgs -> Bool
forall msgs. OutputConfig msgs -> Bool
_quiet OutputConfig msgs
o)

logMsg :: Getter (OutputConfig msgs) (LJ.LogAction IO msgs)
logMsg :: forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(LogAction IO msgs -> f (LogAction IO msgs))
-> OutputConfig msgs -> f (OutputConfig msgs)
logMsg LogAction IO msgs -> f (LogAction IO msgs)
f OutputConfig msgs
o = OutputConfig msgs
o OutputConfig msgs -> f (LogAction IO msgs) -> f (OutputConfig msgs)
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ LogAction IO msgs -> f (LogAction IO msgs)
f (OutputConfig msgs -> LogAction IO msgs
forall msgs. OutputConfig msgs -> LogAction IO msgs
_logMsg OutputConfig msgs
o)


----------------------------------------------------------------------
-- Logging default implementations (can be over-ridden by different
-- front end configurations).

-- | This is the default logging output function for a SayWhat
-- message.  It will emit the information with possible coloring (if
-- enabled via the first argument) to the proper handle (normal output
-- goes to the first handle, error output goes to the second handle,
-- and the same handle may be used for both).
--
-- Front-ends that don't have specific output needs can simply use
-- this function.  Alternative output functions can be used where
-- useful (e.g. JSON output).
logToStd :: (Handle, Bool) -> (Handle, Bool) -> SayWhat -> IO ()
logToStd :: (Handle, Bool) -> (Handle, Bool) -> SayWhat -> IO ()
logToStd (Handle, Bool)
outSpec (Handle, Bool)
errSpec = \case
  SayWhat SayLevel
lvl Text
frm Text
msg ->
    let sayer :: Text -> IO ()
sayer = case SayLevel
lvl of
                  SayLevel
OK -> Color -> (Handle, Bool) -> Text -> IO ()
colOut Color
Green (Handle, Bool)
outSpec
                  SayLevel
Warn -> Color -> (Handle, Bool) -> Text -> IO ()
colOut Color
Yellow (Handle, Bool)
errSpec
                  SayLevel
Fail -> Color -> (Handle, Bool) -> Text -> IO ()
colOut Color
Red (Handle, Bool)
errSpec
                  SayLevel
Simply -> (Handle, Bool) -> Text -> IO ()
straightOut (Handle, Bool)
outSpec
                  SayLevel
Noisily -> (Handle, Bool) -> Text -> IO ()
straightOut (Handle, Bool)
outSpec
        colOut :: Color -> (Handle, Bool) -> Text -> IO ()
colOut Color
clr (Handle
hndl, Bool
True) Text
l =
           do IO () -> IO () -> IO () -> IO ()
forall a b c. IO a -> IO b -> IO c -> IO c
bracket_
                (Handle -> [SGR] -> IO ()
hSetSGR Handle
hndl [ ConsoleIntensity -> SGR
SetConsoleIntensity ConsoleIntensity
BoldIntensity
                              , ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Vivid Color
clr])
                (Handle -> [SGR] -> IO ()
hSetSGR Handle
hndl [SGR
Reset])
                (Handle -> Text -> IO ()
TIO.hPutStr Handle
hndl (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Text
"[" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
frm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"] ")
              Handle -> Text -> IO ()
TIO.hPutStrLn Handle
hndl Text
l
        colOut Color
_ hSpec :: (Handle, Bool)
hSpec@(Handle
_, Bool
False) Text
l = (Handle, Bool) -> Text -> IO ()
straightOut (Handle, Bool)
hSpec Text
l
        straightOut :: (Handle, Bool) -> Text -> IO ()
straightOut (Handle
hndl, Bool
_) Text
l = do Handle -> Text -> IO ()
TIO.hPutStr Handle
hndl (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Text
"[" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
frm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"] "
                                     Handle -> Text -> IO ()
TIO.hPutStrLn Handle
hndl Text
l
    in (Text -> IO ()) -> [Text] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Text -> IO ()
sayer ([Text] -> IO ()) -> [Text] -> IO ()
forall a b. (a -> b) -> a -> b
$ Text -> [Text]
T.lines Text
msg
  SayMore SayWhat
s1 SayWhat
s2 -> do (Handle, Bool) -> (Handle, Bool) -> SayWhat -> IO ()
logToStd (Handle, Bool)
outSpec (Handle, Bool)
errSpec SayWhat
s1
                      (Handle, Bool) -> (Handle, Bool) -> SayWhat -> IO ()
logToStd (Handle, Bool)
outSpec (Handle, Bool)
errSpec SayWhat
s2
  SayWhat
SayNothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()


----------------------------------------------------------------------
-- Direct Output

-- | This function emits output to the normal output handle (specified
-- at initialization time).  This function is not recommended for
-- general use (the 'says', 'logException', 'logSimResult', 'logGoal',
-- etc. are preferred), but can be used by code needing more control
-- over the output formatting.
--
-- This function does _not_ emit a newline at the end of the output.

output :: Logs msgs => String -> IO ()
output :: forall msgs. Logs msgs => String -> IO ()
output String
str = Handle -> String -> IO ()
System.IO.hPutStr (Getting Handle (OutputConfig msgs) Handle
-> OutputConfig msgs -> Handle
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Handle (OutputConfig msgs) Handle
forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(Handle -> f Handle) -> OutputConfig msgs -> f (OutputConfig msgs)
outputHandle Logs msgs
OutputConfig msgs
?outputConfig) String
str

-- | This function emits output to the normal output handle (specified
-- at initialization time).  This function is not recommended for
-- general use (the 'says', 'logException', 'logSimResult', 'logGoal',
-- etc. are preferred), but can be used by code needing more control
-- over the output formatting.
--
-- This function emits a newline at the end of the output.

outputLn :: Logs msgs => String -> IO ()
outputLn :: forall msgs. Logs msgs => String -> IO ()
outputLn String
str = Handle -> String -> IO ()
System.IO.hPutStrLn (Getting Handle (OutputConfig msgs) Handle
-> OutputConfig msgs -> Handle
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Handle (OutputConfig msgs) Handle
forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(Handle -> f Handle) -> OutputConfig msgs -> f (OutputConfig msgs)
outputHandle Logs msgs
OutputConfig msgs
?outputConfig) String
str