
   0 | module Control.Monad.JustAMonad
   1 | 
   2 | 
   3 | import Data.List
   4 | import Data.List1
   5 | import Data.SnocList
   6 | import Data.Vect
   7 | import Data.Either
   8 | 
   9 | import Deriving.Show
  10 | 
  11 | import Language.Reflection
  12 | 
  13 | import System.File.ReadWrite
  14 | 
  15 | import Text.PrettyPrint.Prettyprinter.Render.Terminal
  16 | import Text.PrettyPrint.Prettyprinter
  17 | 
  18 | import public System.Clock
  19 | 
  20 | %language ElabReflection
  21 | 
  22 | %inline
  23 | public export
  24 | Arrow : Type -> Type -> Type
  25 | Arrow a b = a -> b
  26 | 
  27 | public export
  28 | data Channel = Timing | Debug
  29 | 
  30 | %hint
  31 | export
  32 | channelShow : Show Channel
  33 | channelShow = %runElab derive
  34 | 
  35 | public export
  36 | Eq Channel where
  37 |   Timing  == Timing  = True
  38 |   Debug   == Debug   = True
  39 |   _       == _       = False
  40 | 
  41 | %inline
  42 | public export
  43 | Subset : Type -> Type
  44 | Subset a = a -> Bool
  45 | 
  46 | ||| Failure over stateful computation wrapped in IO.
  47 | %inline
  48 | public export
  49 | M : (err : Type) -> (st : Type) -> (res : Type) -> Type
  50 | M e s = Arrow (Subset Channel, s) . IO . (Subset Channel,) . Either e . (s,)
  51 | 
  52 | namespace M
  53 |   ||| Chain computations. Main ingredient for overloaded do-notation.
  54 |   %inline
  55 |   public export
  56 |   (>>=) : M e s a -> (a -> M e s b) -> M e s b
  57 |   m >>= f = \s => Prelude.do
  58 |     case !(m s) of
  59 |       (ch, Left e) => pure (ch, Left e)
  60 |       (ch, Right (s, x)) => f x (ch, s)
  61 | 
  62 |   %inline
  63 |   public export
  64 |   (=<<) : (a -> M e s b) -> M e s a -> M e s b
  65 |   (=<<) = flip (>>=)
  66 | 
  67 |   ||| Composition of monadic functions.
  68 |   %inline
  69 |   public export
  70 |   (>=>) : (a -> M e s b) -> (b -> M e s c) -> (a -> M e s c)
  71 |   (>=>) f g x = g !(f x)
  72 | 
  73 |   %inline
  74 |   public export
  75 |   (<=<) : (b -> M e s c) -> (a -> M e s b) -> (a -> M e s c)
  76 |   (<=<) = flip (>=>)
  77 | 
  78 |   %inline
  79 |   public export
  80 |   (>>) : M e s () -> M e s b -> M e s b
  81 |   (>>) m f = (>>=) m (const f)
  82 | 
  83 |   ||| Wrap a pure result in a computation/monad.
  84 |   %inline
  85 |   public export
  86 |   return : a -> M e s a
  87 |   return x = \(ch, s) => pure (ch, Right (s, x))
  88 | 
  89 |   ||| Throw an error.
  90 |   %inline
  91 |   public export
  92 |   throw : e -> M e s a
  93 |   throw e (ch, s) = pure (ch, Left e)
  94 | 
  95 |   ||| Get the state.
  96 |   %inline
  97 |   public export
  98 |   get : M e s s
  99 |   get = \(ch, s) => pure (ch, Right (s, s))
 100 | 
 101 |   ||| Set the state.
 102 |   %inline
 103 |   public export
 104 |   set : s -> M e s ()
 105 |   set s (ch, _) = pure (ch, Right (s, ()))
 106 | 
 107 |   ||| Update the state.
 108 |   %inline
 109 |   public export
 110 |   update : (s -> s) -> M e s ()
 111 |   update f = get >>= set . f
 112 | 
 113 |   public export
 114 |   mapError : (e -> e') -> M e s a -> M e' s a
 115 |   mapError f m = \s => Prelude.do
 116 |     case !(m s) of
 117 |       (ch, Left x) => pure (ch, Left (f x))
 118 |       (ch, Right x) => pure (ch, Right x)
 119 | 
 120 |   public export
 121 |   mapState : (s -> s') -> (s' -> s) -> M e s a -> M e s' a
 122 |   mapState f f' m = \(ch, s') => Prelude.do
 123 |     case !(m (ch, f' s')) of
 124 |       (ch, Left x) => pure (ch, Left x)
 125 |       (ch, Right (st, x)) => pure (ch, Right (f st, x))
 126 | 
 127 |   public export
 128 |   mapResult : (a -> b) -> M e s a -> M e s b
 129 |   mapResult f m = \s => Prelude.do
 130 |     case !(m s) of
 131 |       (ch, Left x) => pure (ch, Left x)
 132 |       (ch, Right (st, x)) => pure (ch, Right (st, f x))
 133 | 
 134 |   public export
 135 |   (<$>) : (a -> b) -> M e s a -> M e s b
 136 |   (<$>) = mapResult
 137 | 
 138 |   public export
 139 |   (<&>) : M e s a -> (a -> b) -> M e s b
 140 |   (<&>) = flip mapResult
 141 | 
 142 |   public export
 143 |   (<*>) : M e s (a -> b) -> M e s a -> M e s b
 144 |   (<*>) f x = M.do
 145 |     f <- f
 146 |     x <- x
 147 |     return (f x)
 148 | 
 149 |   public export
 150 |   fromEither : Either e a -> M e s a
 151 |   fromEither (Left x) (ch, s) = pure (ch, Left x)
 152 |   fromEither (Right x) (ch, s) = pure (ch, Right (s, x))
 153 | 
 154 |   ||| Runs gathering output from all channels.
 155 |   public export
 156 |   run : M e s r -> s -> IO (Either e (s, r))
 157 |   run m initial = map snd (m (const True, initial))
 158 | 
 159 |   ||| Runs gathering output from all channels, throws away the resulting state.
 160 |   public export
 161 |   eval : M e s r -> s -> IO (Either e r)
 162 |   eval m initial = Prelude.do
 163 |     case !(m (const True, initial)) of
 164 |       (ch, Left x) => pure (Left x)
 165 |       (ch, Right (st, x)) => pure (Right x)
 166 | 
 167 |   ||| Run the computation and discard its result.
 168 |   public export
 169 |   discard : M e s a -> M e s ()
 170 |   discard x = x >>= const (return ())
 171 | 
 172 |   ||| Run the computation when the condition is true.
 173 |   public export
 174 |   when : Bool -> M e s () -> M e s ()
 175 |   when True x = x
 176 |   when False x = return ()
 177 | 
 178 |   ||| Check if the channel is listened.
 179 |   public export
 180 |   isListening : Channel -> M e s Bool
 181 |   isListening me = \(listen, s) => pure (listen, (Right (s, listen me)))
 182 | 
 183 |   ||| Sets whether to listen or not on that channel.
 184 |   public export
 185 |   doListen : Channel -> Bool -> M e s ()
 186 |   doListen ch switch = \(listen, s) => pure (set listen ch switch, Right (s, ()))
 187 |    where
 188 |     set : (Channel -> Bool) -> Channel -> Bool -> Channel -> Bool
 189 |     set f x switch y =
 190 |       case x == y of
 191 |        True => switch
 192 |        False => f x
 193 | 
 194 |   public export
 195 |   sequenceMaybe : Maybe (M e s a) -> M e s (Maybe a)
 196 |   sequenceMaybe Nothing = return Nothing
 197 |   sequenceMaybe (Just x) = return (Just !x)
 198 | 
 199 |   public export
 200 |   sequenceList : List (M e s a)
 201 |               -> M e s (List a)
 202 |   sequenceList [] = return []
 203 |   sequenceList (x :: xs) = return (!x :: !(sequenceList xs))
 204 | 
 205 |   public export
 206 |   sequenceVect : Vect n (M e s a)
 207 |               -> M e s (Vect n a)
 208 |   sequenceVect [] = return []
 209 |   sequenceVect (x :: xs) = return (!x :: !(sequenceVect xs))
 210 | 
 211 |   public export
 212 |   sequenceSnocList : SnocList (M e s a)
 213 |                   -> M e s (SnocList a)
 214 |   sequenceSnocList [<] = return [<]
 215 |   sequenceSnocList (xs :< x) = return (!(sequenceSnocList xs) :< !x)
 216 | 
 217 |   public export
 218 |   sequenceList1 : List1 (M e s a)
 219 |                -> M e s (List1 a)
 220 |   sequenceList1 (x ::: []) = return (singleton !x)
 221 |   sequenceList1 (x ::: y :: zs) = return (!x `cons` !(sequenceList1 (y ::: zs)))
 222 | 
 223 |   public export
 224 |   sequenceProduct : (M e s a, M e s b)
 225 |                  -> M e s (a, b)
 226 |   sequenceProduct (f, g) = return (!f, !g)
 227 | 
 228 |   public export
 229 |   sequenceEither : Either (M e s a) (M e s b)
 230 |                 -> M e s (Either a b)
 231 |   sequenceEither (Left f)  = return (Left !f)
 232 |   sequenceEither (Right g) = return (Right !g)
 233 | 
 234 |   ||| Run a computation for each element of the list and join the results.
 235 |   public export
 236 |   forList : List a -> (a -> M e s b) -> M e s (List b)
 237 |   forList xs f = sequenceList (map f xs)
 238 | 
 239 |   ||| Run a computation for each element of the pair and join the results.
 240 |   public export
 241 |   forProduct : (a, b)
 242 |             -> (a -> M e s a')
 243 |             -> (b -> M e s b')
 244 |             -> M e s (a', b')
 245 |   forProduct p f g = sequenceProduct (bimap f g p)
 246 | 
 247 |   public export
 248 |   traverseProduct : (a -> M e s a')
 249 |                  -> (b -> M e s b')
 250 |                  -> (a, b)
 251 |                  -> M e s (a', b')
 252 |   traverseProduct f g p = forProduct p f g
 253 | 
 254 |   public export
 255 |   forCatMaybes : List a
 256 |               -> (a -> M e s (Maybe b))
 257 |               -> M e s (List b)
 258 |   forCatMaybes list f =
 259 |     mapResult catMaybes (forList list f)
 260 | 
 261 |   ||| Run a computation for each element of the List1 and join the results.
 262 |   public export
 263 |   forList1 : List1 a -> (a -> M e s b) -> M e s (List1 b)
 264 |   forList1 xs f = sequenceList1 (map f xs)
 265 | 
 266 |   ||| Run a computation for each element of the SnocList and join the results.
 267 |   public export
 268 |   forSnocList : SnocList a -> (a -> M e s b) -> M e s (SnocList b)
 269 |   forSnocList xs f = sequenceSnocList (map f xs)
 270 | 
 271 |   public export
 272 |   traverseSnocList : (a -> M e s b)
 273 |                   -> SnocList a
 274 |                   -> M e s (SnocList b)
 275 |   traverseSnocList f xs = forSnocList xs f
 276 | 
 277 |   public export
 278 |   traverseList : (a -> M e s b)
 279 |               -> List a
 280 |               -> M e s (List b)
 281 |   traverseList f xs = forList xs f
 282 | 
 283 |   public export
 284 |   traverseList1 : (a -> M e s b)
 285 |                -> List1 a
 286 |                -> M e s (List1 b)
 287 |   traverseList1 f xs = forList1 xs f
 288 | 
 289 |   public export
 290 |   traverseList_ : (a -> M e s ())
 291 |                -> List a
 292 |                -> M e s ()
 293 |   traverseList_ f xs = discard $ traverseList f xs
 294 | 
 295 |   public export
 296 |   traverseList1_ : (a -> M e s ())
 297 |                 -> List1 a
 298 |                 -> M e s ()
 299 |   traverseList1_ f xs = discard $ traverseList1 f xs
 300 | 
 301 |   ||| Run a computation for each element of the Vect and join the results.
 302 |   public export
 303 |   forVect : Vect n a -> (a -> M e s b) -> M e s (Vect n b)
 304 |   forVect xs f = sequenceVect (map f xs)
 305 | 
 306 |   ||| Run a computation for each element of the Maybe and join the results.
 307 |   public export
 308 |   forMaybe : Maybe a -> (a -> M e s b) -> M e s (Maybe b)
 309 |   forMaybe mb f = sequenceMaybe (map f mb)
 310 | 
 311 |   public export
 312 |   traverseMaybe : (a -> M e s b)
 313 |                -> Maybe a
 314 |                -> M e s (Maybe b)
 315 |   traverseMaybe f m = forMaybe m f
 316 | 
 317 |   public export
 318 |   forList_ : List a -> (a -> M e s b) -> M e s ()
 319 |   forList_ xs f = discard $ forList xs f
 320 | 
 321 |   public export
 322 |   forSnocList_ : SnocList a -> (a -> M e s b) -> M e s ()
 323 |   forSnocList_ xs f = discard $ forSnocList xs f
 324 | 
 325 |   public export
 326 |   forVect_ : Vect n a -> (a -> M e s b) -> M e s ()
 327 |   forVect_ xs f = discard $ forVect xs f
 328 | 
 329 |   public export
 330 |   filterMaybeListM : List a -> (a -> M e s (Maybe b)) -> M e s (List b)
 331 |   filterMaybeListM [] f = return []
 332 |   filterMaybeListM (x :: xs) f = M.do
 333 |     rest <- filterMaybeListM xs f
 334 |     r <- f x
 335 |     case r of
 336 |       Nothing => return rest
 337 |       Just x' => return (x' :: rest)
 338 | 
 339 |   ||| Never fails.
 340 |   public export
 341 |   try : M e s a -> M e s (Either e a)
 342 |   try m = \(ch, s) => Prelude.do
 343 |     case !(m (ch, s)) of
 344 |       (ch, Left x) => pure (ch, Right (s, Left x))
 345 |       (ch, Right (s, x)) => pure (ch, Right (s, Right x))
 346 | 
 347 |   ||| Either one must work. Tries the left one first.
 348 |   public export
 349 |   one : M e s a -> M e s b -> M e s (Either a b)
 350 |   one f g = M.do
 351 |    case !(try f) of
 352 |      Right x => return (Left x)
 353 |      Left _ => g <&> Right
 354 | 
 355 |   ||| Both must work. Tries the left one first.
 356 |   public export
 357 |   both : M e s a -> M e s b -> M e s (a, b)
 358 |   both f g = (f <&> (,)) <*> g
 359 | 
 360 |   ||| First working alternative.
 361 |   public export
 362 |   (<|>) : M e s a -> M e s a -> M e s a
 363 |   (f <|> g) = one f g <&> fromEither
 364 | 
 365 |   public export
 366 |   allList : List (M e s Bool) -> M e s Bool
 367 |   allList [] = return True
 368 |   allList (x :: xs) = M.do
 369 |     x <- x
 370 |     case x of
 371 |       False => return False
 372 |       True => allList xs
 373 | 
 374 |   ||| Lazy logical disjunction.
 375 |   public export
 376 |   or : M e s Bool -> M e s Bool -> M e s Bool
 377 |   or a b = M.do
 378 |     case !a of
 379 |       True => return True
 380 |       False => b
 381 | 
 382 |   infixr 8 `and`
 383 | 
 384 |   infixr 7 `or`
 385 | 
 386 |   ||| Lazy logical conjunction.
 387 |   public export
 388 |   and : M e s Bool -> M e s Bool -> M e s Bool
 389 |   and a b = M.do
 390 |     case !a of
 391 |       True => b
 392 |       False => return False
 393 | 
 394 |   public export
 395 |   io : IO a -> M e s a
 396 |   io cmd (ch, s) = Prelude.do
 397 |     r <- cmd
 398 |     pure (ch, Right (s, r))
 399 | 
 400 |   public export
 401 |   data OutputMode = STDOUT | FILE String
 402 | 
 403 |   ||| Eagerly prints something out (using IO) on the given channel.
 404 |   public export
 405 |   print_ : Channel -> OutputMode -> String -> M e s ()
 406 |   print_ ch mode str = M.do
 407 |     when !(isListening ch) $ M.do
 408 |       case mode of
 409 |         STDOUT => io $ putStrLn str
 410 |         FILE file => discard $ io $ appendFile {io = IO} file str
 411 | 
 412 |   public export
 413 |   timestamp : M e s (Clock Process)
 414 |   timestamp = io $ clockTime Process
 415 | 
 416 |   public export
 417 |   gcTimestamp : FromString e => M e s (Clock GCCPU)
 418 |   gcTimestamp = M.do
 419 |     Just x <- io $ clockTime GCCPU
 420 |       | _ => throw ("GC CPU-time not supported")
 421 |     return x
 422 | 
 423 |   -- Whole seconds & 3 significant fractional digits
 424 |   public export
 425 |   formatted : Clock type -> String
 426 |   formatted (MkClock sec nan) =
 427 |     let mantisa = cast {to = Int} (cast {to = Double} nan / 1_000_000) in -- XXX.GARBAGE
 428 |     "\{show sec}.\{pad mantisa}s"
 429 |    where
 430 |     pad : Int -> String
 431 |     pad x =
 432 |       case x < 10 of
 433 |         True => "00" ++ show x
 434 |         False =>
 435 |           case x < 100 of
 436 |             True => "0" ++ show x
 437 |             False => show x
 438 | 
 439 |   ||| Clocks the given computation, prints out (eagerly) the time it took to run the computation.
 440 |   public export
 441 |   clock : FromString e => String -> M e s a -> M e s a
 442 |   clock msg m = M.do
 443 |     t0 <- timestamp
 444 |     t0' <- gcTimestamp
 445 |     r <- m
 446 |     t1 <- timestamp
 447 |     t1' <- gcTimestamp
 448 |     let dif = timeDifference t1 t0
 449 |     let dif' = timeDifference t1' t0'
 450 |     print_ Timing STDOUT "\{msg} took overall-time: \{formatted dif}; gc time: \{formatted dif'}"
 451 |     return r
 452 | 
 453 |   ||| Clocks the given computation when the condition is true, prints out (eagerly) the time it took to run the computation.
 454 |   public export
 455 |   clockWhen : FromString e => Bool -> String -> M e s a -> M e s a
 456 |   clockWhen False msg m = m
 457 |   clockWhen True msg m = clock msg m
 458 | 
 459 |   public export
 460 |   clockThresholdD : FromString e => (a -> M e s String) -> Integer -> M e s a -> M e s a
 461 |   clockThresholdD msg threshold m = M.do
 462 |     t0 <- timestamp
 463 |     t0' <- gcTimestamp
 464 |     r <- m
 465 |     t1 <- timestamp
 466 |     t1' <- gcTimestamp
 467 |     let dif = timeDifference t1 t0
 468 |     let dif' = timeDifference t1' t0'
 469 |     let workloadTime = toNano dif - toNano dif'
 470 |     -- It has been noticed that sometimes trivial operations are claimed to take insensible amount of time.
 471 |     -- Coincidence or not, such claims have been always accompanied by 0 nanosecond GC time.
 472 |     -- By filtering out all output that has zero GC time, we discard spurious output.
 473 |     -- That means some output is lost (never shown) but the trade-off has been worth it so far.
 474 |     when (workloadTime > threshold && toNano dif' > 0) $ M.do
 475 |       msg <- msg r
 476 |       print_ Timing STDOUT "\{msg} took overall-time: \{formatted dif}; gc time: \{formatted dif'}" -- ; workload time: \{show workloadTime}ns"
 477 |     return r
 478 | 
 479 |   ||| Clocks the given computation, prints out (eagerly) the time it took to run the computation.
 480 |   public export
 481 |   clockThreshold : FromString e => String -> Integer -> M e s a -> M e s a
 482 |   clockThreshold msg threshold m = M.do
 483 |     clockThresholdD (\x => return msg) threshold m
 484 | 
 485 |   ||| Currently, write is just an alias to print_ on *Debug* channel.
 486 |   ||| So all output of write is eagerly shown in console.
 487 |   public export
 488 |   write : String -> M e s ()
 489 |   write x = M.do
 490 |     print_ Debug STDOUT x
 491 | 
 492 |   ||| Computes the workload time (process time - GC time)
 493 |   public export
 494 |   time : FromString e => M e s a -> M e s (a, Clock Duration)
 495 |   time computation = M.do
 496 |    t0 <- timestamp
 497 |    t0' <- gcTimestamp
 498 |    x <- computation
 499 |    t1 <- timestamp
 500 |    t1' <- gcTimestamp
 501 |    let dif = timeDifference t1 t0
 502 |    let dif' = timeDifference t1' t0'
 503 |    let workloadTime = timeDifference dif dif'
 504 |    return (x, workloadTime)
 505 |