
   0 | module Pack.Core.Logging
   1 | 
   2 | import Control.Monad.Either
   3 | import Control.Monad.Trans
   4 | import Pack.Core.Types
   5 | 
   6 | import System
   7 | 
   8 | %default total
   9 | 
  10 | --------------------------------------------------------------------------------
  11 | --          Support
  12 | --------------------------------------------------------------------------------
  13 | 
  14 | public export
  15 | data ConfirmResult = Yes | No | Unknown
  16 | 
  17 | ||| Converts a string into a `ConfirmResult`, ignoring case.
  18 | ||| Recognises `"y"` or `"yes"` as `Yes`, `"n"` or `"no"` as `No`.
  19 | ||| An empty string defaults to `No`. Any other input is treated as `Unknown`.
  20 | parseConfirmResult : String -> ConfirmResult
  21 | parseConfirmResult x = case toLower x of
  22 |   "y"   => Yes
  23 |   "yes" => Yes
  24 |   "n"   => No
  25 |   "no"  => No
  26 |   ""    => No -- Default
  27 |   _     => Unknown
  28 | 
  29 | ||| Constructs a prompt message for a confirmation dialog.
  30 | confirmMessage : String -> String
  31 | confirmMessage msg =
  32 |   if isLong
  33 |      then "\{msg}\n\n\{continueMessage}"
  34 |      else "\{msg} \{continueMessage}"
  35 |   where
  36 |     isLong : Bool
  37 |     isLong = length msg > 80 || isInfixOf "\n\n" msg
  38 | 
  39 |     continueMessage : String
  40 |     continueMessage = "Continue (yes/*no)?"
  41 | 
  42 | ||| Executes an action that returns a `ConfirmResult` and ensures
  43 | ||| that it is confirmed by the user. If not, throws `SafetyAbort`.
  44 | mustConfirm :
  45 |      HasIO io
  46 |   => io ConfirmResult
  47 |   -> EitherT PackErr io ()
  48 | mustConfirm action = case !(lift action) of
  49 |   Yes => pure ()
  50 |   _   => throwE SafetyAbort
  51 | 
  52 | --------------------------------------------------------------------------------
  53 | --          Logging
  54 | --------------------------------------------------------------------------------
  55 | 
  56 | printLogMessage :
  57 |      {auto _ : HasIO io}
  58 |   -> {auto _ : Interpolation logLevel}
  59 |   -> (lvl : logLevel)
  60 |   -> (msg : String)
  61 |   -> (msgs : List String)
  62 |   -> io ()
  63 | printLogMessage lvl msg msgs = do
  64 |   let prefx := "[ \{lvl} ] "
  65 |   let baseIndent := replicate (length prefx) ' '
  66 |   printMultilineIndented prefx baseIndent msg
  67 |   for_ msgs $ printMultilineIndented "\{baseIndent}- " "\{baseIndent}  "
  68 | 
  69 |   where
  70 |     printMultilineIndented :
  71 |          (fstPrefix, restPrefix : String)
  72 |       -> (msg : String)
  73 |       -> io ()
  74 |     printMultilineIndented fstPrefix restPrefix msg = do
  75 |       let (s::ss) = lines msg
  76 |         | [] => putStrLn "\{fstPrefix}"
  77 |       putStrLn "\{fstPrefix}\{s}"
  78 |       for_ ss $ \s => putStrLn "\{restPrefix}\{s}"
  79 | 
  80 | ||| Logs a message to stdout if the log level is greater than or equal
  81 | ||| than the reference level `ref`.
  82 | ||| If the given string contains newlines, all lines are printed indented
  83 | ||| to the beginning of the first one.
  84 | export
  85 | log :
  86 |      {auto _ : HasIO io}
  87 |   -> (ref : LogRef)
  88 |   -> (lvl : LogLevel)
  89 |   -> (msg : Lazy String)
  90 |   -> io ()
  91 | log ref lvl msg =
  92 |   when (lvl >= ref.level) $ printLogMessage lvl msg []
  93 | 
  94 | ||| Logs a message to stdout and reads an reply from stdin.
  95 | ||| This uses the given log level but makes sure the message is always
  96 | ||| printed no matter the current log level preferences.
  97 | export %inline
  98 | prompt : HasIO io => (lvl : LogLevel) -> (msg : String) -> io String
  99 | prompt lvl msg = log (MkLogRef lvl) lvl msg >> map trim getLine
 100 | 
 101 | ||| Requests confirmation from the user with the specified message and
 102 | ||| parses a reply from stdin as `Yes` or `No`.
 103 | |||
 104 | ||| This uses the given log level but makes sure the message is always
 105 | ||| printed no matter the current log level preferences.
 106 | export %inline
 107 | confirm : HasIO io => (lvl : LogLevel) -> (msg : String) -> io ConfirmResult
 108 | confirm lvl msg =
 109 |   map parseConfirmResult $ prompt lvl $ confirmMessage msg
 110 | 
 111 | ||| Requests confirmation from the user with the specified message and
 112 | ||| If the reply is not `Yes`, aborts with `SafetyAbort`.
 113 | |||
 114 | ||| This uses the given log level but makes sure the message is always
 115 | ||| printed no matter the current log level preferences.
 116 | export %inline
 117 | confirmOrAbort :
 118 |      HasIO io
 119 |   => (lvl : LogLevel)
 120 |   -> (msg : String)
 121 |   -> EitherT PackErr io ()
 122 | confirmOrAbort = mustConfirm .: confirm
 123 | 
 124 | ||| Logs an idented list of values to stdout if the given log level
 125 | ||| is greater than or equal than the (auto-implicit) reference level `ref`.
 126 | ||| If messages list is empty, no log message is printed.
 127 | |||
 128 | ||| `inlineSingle` parameter being set to `True` makes a single element of
 129 | ||| the given list to be printed at the same line as the main message.
 130 | |||
 131 | ||| Note: Most of the time `ref` is automatically being extracted from
 132 | ||| a value of type `Pack.Config.Types.Config` in scope.
 133 | export
 134 | logMany :
 135 |      {auto _ : HasIO io}
 136 |   -> {auto ref  : LogRef}
 137 |   -> {default False inlineSingle : Bool}
 138 |   -> (lvl  : LogLevel)
 139 |   -> (msg  : Lazy String)
 140 |   -> (msgs : Lazy (List String))
 141 |   -> io ()
 142 | logMany lvl msg msgs =
 143 |   when (lvl >= ref.level && not (null msgs)) $
 144 |     case (inlineSingle, force msgs) of
 145 |       (True, [x] ) => printLogMessage lvl "\{msg} \{x}" []
 146 |       (_   , msgs) => printLogMessage lvl msg msgs
 147 | 
 148 | ||| Logs an indented list of values to stdout and reads a reply from stdin.
 149 | |||
 150 | ||| This uses the given log level but makes sure the message is always
 151 | ||| printed no matter the current log level preferences.
 152 | export %inline
 153 | promptMany :
 154 |      {auto _ : HasIO io}
 155 |   -> (lvl : LogLevel)
 156 |   -> (msg : String)
 157 |   -> (msgs : List String)
 158 |   -> io String
 159 | promptMany lvl msg msgs =
 160 |   let ref := MkLogRef lvl
 161 |    in logMany lvl msg msgs >> map trim getLine
 162 | 
 163 | ||| Logs an indented list of values to stdout and requests confirmation
 164 | ||| from the user and parses a reply from stdin as `Yes` or `No`.
 165 | |||
 166 | ||| This uses the given log level but makes sure the message is always
 167 | ||| printed no matter the current log level preferences.
 168 | export %inline
 169 | confirmMany :
 170 |      {auto _ : HasIO io}
 171 |   -> (lvl : LogLevel)
 172 |   -> (msg : String)
 173 |   -> (msgs : List String)
 174 |   -> io ConfirmResult
 175 | confirmMany lvl msg msgs =
 176 |   map parseConfirmResult $ promptMany lvl (confirmMessage msg) msgs
 177 | 
 178 | ||| Logs an indented list of values to stdout and requests confirmation
 179 | ||| from the user. If the reply is not `Yes`, aborts with `SafetyAbort`.
 180 | |||
 181 | ||| This uses the given log level but makes sure the message is always
 182 | ||| printed no matter the current log level preferences.
 183 | export %inline
 184 | confirmManyOrAbort :
 185 |      {auto _ : HasIO io}
 186 |   -> (lvl : LogLevel)
 187 |   -> (msg : String)
 188 |   -> (msgs : List String)
 189 |   -> EitherT PackErr io ()
 190 | confirmManyOrAbort lvl = mustConfirm .: confirmMany lvl
 191 | 
 192 | ||| Alias for `log ref Debug`.
 193 | |||
 194 | ||| Note: Most of the time `ref` is automatically being extracted from
 195 | ||| a value of type `Pack.Config.Types.Config` in scope.
 196 | export %inline
 197 | debug : HasIO io => (ref : LogRef) => (msg  : Lazy String) -> io ()
 198 | debug = log ref Debug
 199 | 
 200 | ||| Alias for `log ref Info`.
 201 | |||
 202 | ||| Note: Most of the time `ref` is automatically being extracted from
 203 | ||| a value of type `Pack.Config.Types.Config` in scope.
 204 | export %inline
 205 | info : HasIO io => (ref : LogRef) => (msg  : Lazy String) -> io ()
 206 | info = log ref Info
 207 | 
 208 | ||| Alias for `log ref Cache`.
 209 | |||
 210 | ||| Note: Most of the time `ref` is automatically being extracted from
 211 | ||| a value of type `Pack.Config.Types.Config` in scope.
 212 | export %inline
 213 | cache : HasIO io => (ref : LogRef) => (msg  : Lazy String) -> io ()
 214 | cache = log ref Cache
 215 | 
 216 | ||| Alias for `log ref Warning`.
 217 | |||
 218 | ||| Note: Most of the time `ref` is automatically being extracted from
 219 | ||| a value of type `Pack.Config.Types.Config` in scope.
 220 | export %inline
 221 | warn : HasIO io => (ref : LogRef) => (msg  : Lazy String) -> io ()
 222 | warn = log ref Warning
 223 | 
 224 | ||| Fail fatally with error message logged.
 225 | ||| This is like `System.die` but with error printer like a log message.
 226 | export
 227 | fatal : HasIO io => (err : PackErr) -> io a
 228 | fatal err = do
 229 |   printLogMessage "fatal" (printErr err) []
 230 |   exitFailure
 231 |