inductive Lake.LogLevel : Type

• info: Lake.LogLevel
• warning: Lake.LogLevel
• error: Lake.LogLevel

inductive Lake.Verbosity : Type u

• quiet: Lake.Verbosity
• normal: Lake.Verbosity
• verbose: Lake.Verbosity

instance Lake.instBEqVerbosity : BEq Lake.Verbosity

Equations

• Lake.instBEqVerbosity = { beq := Lake.beqVerbosity✝ }

instance Lake.instInhabitedVerbosity : Inhabited Lake.Verbosity

Equations

• Lake.instInhabitedVerbosity = { default := Lake.Verbosity.normal }

Class

class Lake.MonadLog (m : Type u → Type v) : Type v

• getVerbosity : m Lake.Verbosity
• log : String → Lake.LogLevel → m PUnit

@[inline]

def Lake.getIsVerbose {m : Type → Type u_1} [Functor m] [Lake.MonadLog m] : m Bool

Equations

• Lake.getIsVerbose = Lake.getVerbosity <&> fun (x : Lake.Verbosity) => x == Lake.Verbosity.verbose

@[inline]

def Lake.getIsQuiet {m : Type → Type u_1} [Functor m] [Lake.MonadLog m] : m Bool

Equations

• Lake.getIsQuiet = Lake.getVerbosity <&> fun (x : Lake.Verbosity) => x == Lake.Verbosity.quiet

@[inline]

def Lake.logVerbose {m : Type → Type u_1} [Monad m] [Lake.MonadLog m] (message : String) : m PUnit

Equations

• Lake.logVerbose message = do let __do_lift ← Lake.getIsVerbose if __do_lift = true then Lake.log message Lake.LogLevel.info else pure PUnit.unit

@[inline]

def Lake.logInfo {m : Type → Type u_1} [Monad m] [Lake.MonadLog m] (message : String) : m PUnit

Equations

• Lake.logInfo message = do let __do_lift ← Lake.getIsQuiet if (!__do_lift) = true then Lake.log message Lake.LogLevel.info else pure PUnit.unit

@[inline]

def Lake.logWarning {m : Type u_1 → Type u_2} [Lake.MonadLog m] (message : String) : m PUnit

Equations

• Lake.logWarning message = Lake.log message Lake.LogLevel.warning

@[inline]

def Lake.logError {m : Type u_1 → Type u_2} [Lake.MonadLog m] (message : String) : m PUnit

Equations

• Lake.logError message = Lake.log message Lake.LogLevel.error

@[specialize #[]]

def Lake.MonadLog.nop {m : Type → Type u_1} [Pure m] : Lake.MonadLog m

Equations

• Lake.MonadLog.nop = { getVerbosity := pure Lake.Verbosity.normal, log := fun (x : String) (x : Lake.LogLevel) => pure () }

instance Lake.MonadLog.instInhabitedMonadLog {m : Type → Type u_1} [Pure m] : Inhabited (Lake.MonadLog m)

Equations

• Lake.MonadLog.instInhabitedMonadLog = { default := Lake.MonadLog.nop }

@[specialize #[]]

def Lake.MonadLog.io {m : Type → Type u_1} [MonadLiftT BaseIO m] (verbosity : optParam Lake.Verbosity Lake.Verbosity.normal) : Lake.MonadLog m

Equations

• One or more equations did not get rendered due to their size.

@[specialize #[]]

def Lake.MonadLog.eio {m : Type → Type u_1} [MonadLiftT BaseIO m] (verbosity : optParam Lake.Verbosity Lake.Verbosity.normal) : Lake.MonadLog m

Equations

• One or more equations did not get rendered due to their size.

@[specialize #[]]

def Lake.MonadLog.lift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLiftT m n] (self : Lake.MonadLog m) : Lake.MonadLog n

Equations

• Lake.MonadLog.lift self = { getVerbosity := liftM Lake.getVerbosity, log := fun (msg : String) (lv : Lake.LogLevel) => liftM (Lake.log msg lv) }

instance Lake.MonadLog.instMonadLog {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLift m n] [methods : Lake.MonadLog m] : Lake.MonadLog n

Equations

• Lake.MonadLog.instMonadLog = Lake.MonadLog.lift methods

@[inline]

def Lake.MonadLog.error {m : Type u_1 → Type u_2} {α : Type u_1} [Alternative m] [Lake.MonadLog m] (msg : String) : m α

Log the given error message and then fail.

Equations

• Lake.MonadLog.error msg = SeqRight.seqRight (Lake.logError msg) fun (x : Unit) => failure

Transformers

@[inline, reducible]

abbrev Lake.MonadLogT (m : Type u → Type v) (n : Type v → Type w) (α : Type v) : Type (max v w)

Equations

• Lake.MonadLogT m n = ReaderT (Lake.MonadLog m) n

instance Lake.instInhabitedMonadLogT {n : Type u_1 → Type u_2} {α : Type u_1} {m : Type u_3 → Type u_1} [Pure n] [Inhabited α] : Inhabited (Lake.MonadLogT m n α)

Equations

• Lake.instInhabitedMonadLogT = { default := fun (x : Lake.MonadLog m) => pure default }

instance Lake.instMonadLogMonadLogT {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_1} [Monad n] [MonadLiftT m n] : Lake.MonadLog (Lake.MonadLogT m n)

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.MonadLogT.adaptMethods {n : Type u_1 → Type u_2} {m : Type u_3 → Type u_1} {m' : Type u_4 → Type u_1} {α : Type u_1} [Monad n] (f : Lake.MonadLog m → Lake.MonadLog m') (self : Lake.MonadLogT m' n α) : Lake.MonadLogT m n α

Equations

• Lake.MonadLogT.adaptMethods f self = ReaderT.adapt f self

@[inline]

def Lake.MonadLogT.ignoreLog {m : Type → Type u_1} {n : Type u_1 → Type u_2} {α : Type u_1} [Pure m] (self : Lake.MonadLogT m n α) : n α

Equations

• Lake.MonadLogT.ignoreLog self = self Lake.MonadLog.nop

@[inline, reducible]

abbrev Lake.LogIO (α : Type) : Type

Equations

• Lake.LogIO = Lake.MonadLogT BaseIO Lake.OptionIO

instance Lake.instMonadErrorLogIO : Lake.MonadError Lake.LogIO

Equations

• Lake.instMonadErrorLogIO = { error := fun {α : Type} => Lake.MonadLog.error }

instance Lake.instMonadLiftIOLogIO : MonadLift IO Lake.LogIO

Equations

• Lake.instMonadLiftIOLogIO = { monadLift := fun {α : Type} => Lake.MonadError.runIO }

def Lake.LogIO.captureLog {α : Type} (self : Lake.LogIO α) (verbosity : optParam Lake.Verbosity Lake.Verbosity.normal) : BaseIO (String × Option α)

Equations

• Lake.LogIO.captureLog self verbosity = IO.FS.withIsolatedStreams (Lake.OptionIO.toBaseIO (self (Lake.MonadLog.eio verbosity))) true

@[inline, reducible]

abbrev Lake.LogT (m : Type → Type) (α : Type) : Type

Equations

• Lake.LogT m = Lake.MonadLogT m m