advent/src/Util/Eff.md

# Effects utilities

Contains utility functions extending the functionality of the `eff` package.

```idris
module Util.Eff

import Control.Eff
import Data.Subset
import Text.ANSI

import System
import System.File

%default total
```

## Logging

### Log Levels

Basic enumeration describing log levels, we define some (hidden) utility
functions for working with these.

The `Other n` log level is restricted to `n` greater than 4, to prevent
ambiguity between custom log levels and predefined log levels.

```idris
public export
data Level : Type where
  Err : Level
  Warn : Level
  Info : Level
  Debug : Level
  Trace : Level
  Other : (n : Nat) -> {auto _ : n `GT` 4} -> Level
```

```idris hide
export
levelToNat : Level -> Nat
levelToNat Err = 0
levelToNat Warn = 1
levelToNat Info = 2
levelToNat Debug = 3
levelToNat Trace = 4
levelToNat (Other k) = k

export
natToLevel : Nat -> Level
natToLevel 0 = Err
natToLevel 1 = Warn
natToLevel 2 = Info
natToLevel 3 = Debug
natToLevel 4 = Trace
natToLevel (S (S (S (S (S k))))) = Other (5 + k)

export
Eq Level where
  x == y = levelToNat x == levelToNat y

export
Ord Level where
  compare x y = compare (levelToNat x) (levelToNat y)

export infixl 8 >+
export
(>+) : Level -> Nat -> Level
(>+) x k = natToLevel (k + levelToNat x)
```

Convert a `Level` into a colorized tag

```idris
export
levelToTag : Level -> String
levelToTag Err =
    show . bolden . show . colored BrightRed $ "[Error]"
levelToTag Warn =
    show . bolden . show . colored BrightYellow $ "[Warning]"
levelToTag Info =
    show . bolden . show . colored Green $ "[Info]"
levelToTag Debug =
    show . bolden . show . colored Magenta $ "[Debug]"
levelToTag Trace =
    show . bolden . show . colored Cyan $ "[Trace]"
levelToTag (Other k) =
    show . bolden . show . colored BrightWhite $ "[\{show k}]"
```

### Logger effect

This is a basic data structure that captures a lazy log message (so we don't
have to pay any of the costs associated with generating the log message when it
is filtered)

```idris
public export
data Logger : Type -> Type where
  Log : (level : Level) -> (msg : Lazy String) -> Logger ()
```

We'll also provide some basic accessors, and an `ignore` function useful for
writing handlers.

```idris
export  
(.level) : Logger t -> Level
(.level) (Log level msg) = level

export
(.msg) : Logger t -> Lazy String
(.msg) (Log level msg) = msg

export
ignore : Logger t -> t
ignore (Log level msg) = ()
```

#### Handler

Because we know that we will only be using `logger` in an `IO` context, we
aren't currently going to provide a `runLogger` or the like, instead we'll
define a function, suitable for use as a `runEff` handler, that filters log
messages and prints them to `stderr` over `IO`.

In the event a log message is filtered out, it's inner message is never
inspected, avoiding evaluation.

```idris
export
handleLoggerIO : 
  (max_level : Level) -> Logger t -> IO t
handleLoggerIO max_level x = 
  if x.level <= max_level 
    then do
      _ <- fPutStrLn stderr "\{levelToTag x.level}: \{x.msg}"
      pure . ignore $ x
    else pure . ignore $ x
```

Provide a family of effectful actions that emit log messages at the different
log levels.

```idris
export
error : Has Logger fs => Lazy String -> Eff fs ()
error x = send $ Log Err x

export
warn : Has Logger fs => Lazy String -> Eff fs ()
warn x = send $ Log Warn x

export
info : Has Logger fs => Lazy String -> Eff fs ()
info x = send $ Log Info x

export
debug : Has Logger fs => Lazy String -> Eff fs ()
debug x = send $ Log Debug x

export
trace : Has Logger fs => Lazy String -> Eff fs ()
trace x = send $ Log Trace x

export
logAt : Has Logger fs => Level -> Lazy String -> Eff fs ()
logAt level x = send $ Log level x
```

## Choose

Lifts any foldable data structure into the Choose effect, enabling the style of
nondeterministic programming from the list monad

```idris
export
oneOf : Has (Choose) fs => Foldable f =>
    f a -> Eff fs a
oneOf x = foldl oneOf' empty x
  where
  oneOf' : Eff fs a -> a -> Eff fs a
  oneOf' acc val = pure val `alt` acc
```

Lifts any foldable of effectful computations into the Choose effect much the
same as `oneOf`

```idris
export
oneOfM : Has (Choose) fs => Foldable f =>
    f (Eff fs a) -> Eff fs a
oneOfM x = foldl alt empty x
```

## Subset

Reorder the first two elements of the first argument of a subset

```idris
public export
subsetReorderLeft : Subset (x :: g :: xs) ys -> Subset (g :: x :: xs) ys
subsetReorderLeft (e :: (e' :: subset)) = e' :: e :: subset
```

Add the same element to both arguments of a subset

```idris
public export
subsetConsBoth : {0 xs, ys : List a} -> {0 g : a} -> Subset xs ys 
  -> Subset (g :: xs) (g :: ys)
subsetConsBoth {xs = []} {ys = ys} [] = [Z]
subsetConsBoth {xs = (x :: xs)} {ys} (e :: subset) = 
  let rest = S e :: subsetConsBoth subset {g}
  in subsetReorderLeft rest
```

A list is always a subset of itself

```idris
public export
subsetReflexive : {xs : List a} -> Subset xs xs
subsetReflexive {xs = []} = []
subsetReflexive {xs = (x :: xs)} = 
  let rest = subsetReflexive {xs} 
  in subsetConsBoth rest
```

If `xs` is a subset of `ys`, then it is also a subset of `ys + g`

```idris
public export
subsetConsRight : {0 g: _} -> {0 xs, ys: _} -> Subset xs ys -> Subset xs (g :: ys)
subsetConsRight {xs = []} {ys = ys} [] = []
subsetConsRight {xs = (x :: xs)} {ys} (e :: subset) = 
  S e :: subsetConsRight subset {g}
```

`xs` is always a subset of `xs + g`

```idris
public export
trivialSubset : {0 g : a} -> {xs : List a} -> Subset xs (g :: xs)
trivialSubset = subsetConsRight subsetReflexive
```

`fs - f` is always a subset of `f`

```idris
public export
minusLemma : {fs : List a} -> {0 x : a} -> {auto prf : Has x fs} 
  -> Subset (fs - x) fs
minusLemma {fs = (_ :: vs)} {prf = Z} = trivialSubset
minusLemma {fs = (w :: vs)} {prf = (S y)} = 
  let rest = minusLemma {fs = vs} {prf = y}
  in subsetConsBoth rest
```