Lake.Util.Log

auto: Lake.AnsiMode
Automatically determine whether to use ANSI escape codes based on whether the stream written to is a terminal.
ansi: Lake.AnsiMode
Use ANSI escape codes.
noAnsi: Lake.AnsiMode
Do not use ANSI escape codes.

source

def Lake.AnsiMode.isEnabled (out : IO.FS.Stream) :

Lake.AnsiMode → BaseIO Bool

Returns whether to ANSI escape codes with the stream out.

Equations

Lake.AnsiMode.isEnabled out x = match x with | Lake.AnsiMode.auto => out.isTty | Lake.AnsiMode.ansi => pure true | Lake.AnsiMode.noAnsi => pure false

source

def Lake.Ansi.chalk (colorCode : String) (text : String) :

String

Wrap text in ANSI escape sequences to make it bold and color it the ANSI colorCode. Resets all terminal font attributes at the end of the text.

Equations

Lake.Ansi.chalk colorCode text = toString "\x1b[1;" ++ toString colorCode ++ toString "m" ++ toString text ++ toString "\x1b[m"

source

inductive Lake.OutStream :

Type

A pure representation of output stream.

Instances For

source

def Lake.OutStream.get :

Lake.OutStream → BaseIO IO.FS.Stream

Returns the real output stream associated with OutStream.

Equations

x.get = match x with | Lake.OutStream.stdout => IO.getStdout | Lake.OutStream.stderr => IO.getStderr | Lake.OutStream.stream s => pure s

source

instance Lake.instCoeStreamOutStream :

Coe IO.FS.Stream Lake.OutStream

Equations

Lake.instCoeStreamOutStream = { coe := Lake.OutStream.stream }

source

instance Lake.instCoeHandleOutStream :

Coe IO.FS.Handle Lake.OutStream

Equations

Lake.instCoeHandleOutStream = { coe := fun (h : IO.FS.Handle) => Lake.OutStream.stream (IO.FS.Stream.ofHandle h) }

source

inductive Lake.LogLevel :

Type

Instances For

source

instance Lake.instInhabitedLogLevel :

Inhabited Lake.LogLevel

Equations

Lake.instInhabitedLogLevel = { default := Lake.LogLevel.trace }

source

instance Lake.instReprLogLevel :

Repr Lake.LogLevel

Equations

Lake.instReprLogLevel = { reprPrec := Lake.reprLogLevel✝ }

source

instance Lake.instDecidableEqLogLevel :

DecidableEq Lake.LogLevel

Equations

Lake.instDecidableEqLogLevel x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

source

instance Lake.instOrdLogLevel :

Ord Lake.LogLevel

Equations

Lake.instOrdLogLevel = { compare := Lake.ordLogLevel✝ }

source

instance Lake.instToJsonLogLevel :

Lean.ToJson Lake.LogLevel

Equations

Lake.instToJsonLogLevel = { toJson := Lake.toJsonLogLevel✝ }

source

instance Lake.instFromJsonLogLevel :

Lean.FromJson Lake.LogLevel

Equations

Lake.instFromJsonLogLevel = { fromJson? := Lake.fromJsonLogLevel✝ }

source

instance Lake.instLTLogLevel :

LT Lake.LogLevel

Equations

Lake.instLTLogLevel = ltOfOrd

source

instance Lake.instLELogLevel :

LE Lake.LogLevel

Equations

Lake.instLELogLevel = leOfOrd

source

instance Lake.instMinLogLevel :

Min Lake.LogLevel

Equations

Lake.instMinLogLevel = minOfLe

source

instance Lake.instMaxLogLevel :

Max Lake.LogLevel

Equations

Lake.instMaxLogLevel = maxOfLe

source

def Lake.LogLevel.icon :

Lake.LogLevel → Char

Unicode icon for representing the log level.

Equations

x.icon = match x with | Lake.LogLevel.trace => 'ℹ' | Lake.LogLevel.info => 'ℹ' | Lake.LogLevel.warning => '⚠' | Lake.LogLevel.error => '✖'

source

def Lake.LogLevel.ansiColor :

Lake.LogLevel → String

ANSI escape code for coloring text of at the log level.

Equations

x.ansiColor = match x with | Lake.LogLevel.trace => "34" | Lake.LogLevel.info => "34" | Lake.LogLevel.warning => "33" | Lake.LogLevel.error => "31"

source

def Lake.LogLevel.toString :

Lake.LogLevel → String

Equations

x.toString = match x with | Lake.LogLevel.trace => "trace" | Lake.LogLevel.info => "info" | Lake.LogLevel.warning => "warning" | Lake.LogLevel.error => "error"

source

def Lake.LogLevel.ofMessageSeverity :

Lean.MessageSeverity → Lake.LogLevel

Equations

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

source

instance Lake.instToStringLogLevel :

ToString Lake.LogLevel

Equations

Lake.instToStringLogLevel = { toString := Lake.LogLevel.toString }

source

def Lake.Verbosity.minLogLv :

Lake.Verbosity → Lake.LogLevel

Equations

x.minLogLv = match x with | Lake.Verbosity.quiet => Lake.LogLevel.warning | Lake.Verbosity.normal => Lake.LogLevel.info | Lake.Verbosity.verbose => Lake.LogLevel.trace

source

structure Lake.LogEntry :

Type

level : Lake.LogLevel
message : String

Instances For

source

instance Lake.instInhabitedLogEntry :

Inhabited Lake.LogEntry

Equations

Lake.instInhabitedLogEntry = { default := { level := default, message := default } }

source

instance Lake.instToJsonLogEntry :

Lean.ToJson Lake.LogEntry

Equations

Lake.instToJsonLogEntry = { toJson := Lake.toJsonLogEntry✝ }

source

instance Lake.instFromJsonLogEntry :

Lean.FromJson Lake.LogEntry

Equations

Lake.instFromJsonLogEntry = { fromJson? := Lake.fromJsonLogEntry✝ }

source

def Lake.LogEntry.toString (self : Lake.LogEntry) (useAnsi : optParam Bool false) :

String

Equations

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

source

instance Lake.instToStringLogEntry :

ToString Lake.LogEntry

Equations

Lake.instToStringLogEntry = { toString := fun (self : Lake.LogEntry) => self.toString }

source

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

Type v

logEntry : Lake.LogEntry → m PUnit

Instances

source

@[inline]

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

m PUnit

Equations

Lake.logVerbose message = Lake.logEntry { level := Lake.LogLevel.trace, message := message }

source

@[inline]

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

m PUnit

Equations

Lake.logInfo message = Lake.logEntry { level := Lake.LogLevel.info, message := message }

source

@[inline]

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

m PUnit

Equations

Lake.logWarning message = Lake.logEntry { level := Lake.LogLevel.warning, message := message }

source

@[inline]

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

m PUnit

Equations

Lake.logError message = Lake.logEntry { level := Lake.LogLevel.error, message := message }

source

@[specialize #[]]

def Lake.logSerialMessage {m : Type u_1 → Type u_2} (msg : Lean.SerialMessage) [Lake.MonadLog m] :

m PUnit

Equations

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

source

@[deprecated]

def Lake.logToIO (e : Lake.LogEntry) (minLv : Lake.LogLevel) :

BaseIO PUnit

Equations

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

source

def Lake.logToStream (e : Lake.LogEntry) (out : IO.FS.Stream) (minLv : Lake.LogLevel) (useAnsi : Bool) :

BaseIO PUnit

Equations

Lake.logToStream e out minLv useAnsi = if e.level ≥ minLv then EIO.catchExceptions (out.putStrLn (e.toString useAnsi)) fun (x : IO.Error) => pure () else pure PUnit.unit

source

@[reducible, inline]

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

Lake.MonadLog m

Equations

Lake.MonadLog.nop = { logEntry := fun (x : Lake.LogEntry) => pure () }

source

instance Lake.MonadLog.instInhabitedOfPure {m : Type → Type u_1} [Pure m] :

Inhabited (Lake.MonadLog m)

Equations

Lake.MonadLog.instInhabitedOfPure = { default := Lake.MonadLog.nop }

source

@[reducible, inline]

abbrev 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

self.lift = { logEntry := fun (e : Lake.LogEntry) => liftM (Lake.logEntry e) }

source

instance Lake.MonadLog.instOfMonadLift {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.instOfMonadLift = methods.lift

source

@[reducible, inline, deprecated]

abbrev Lake.MonadLog.io {m : Type → Type u_1} [MonadLiftT BaseIO m] (minLv : optParam Lake.LogLevel Lake.LogLevel.info) :

Lake.MonadLog m

Equations

Lake.MonadLog.io minLv = { logEntry := fun (e : Lake.LogEntry) => liftM (Lake.logToIO e minLv) }

source

@[reducible, inline]

abbrev Lake.MonadLog.stream {m : Type → Type u_1} [MonadLiftT BaseIO m] (out : IO.FS.Stream) (minLv : optParam Lake.LogLevel Lake.LogLevel.info) (useAnsi : optParam Bool false) :

Lake.MonadLog m

Equations

Lake.MonadLog.stream out minLv useAnsi = { logEntry := fun (e : Lake.LogEntry) => liftM (Lake.logToStream e out minLv useAnsi) }

source

def Lake.OutStream.logEntry (self : Lake.OutStream) (e : Lake.LogEntry) (minLv : optParam Lake.LogLevel Lake.LogLevel.info) (ansiMode : optParam Lake.AnsiMode Lake.AnsiMode.auto) :

BaseIO PUnit

Equations

self.logEntry e minLv ansiMode = do let out ← self.get let useAnsi ← Lake.AnsiMode.isEnabled out ansiMode Lake.logToStream e out minLv useAnsi

source

@[reducible, inline]

abbrev Lake.OutStream.logger {m : Type → Type u_1} [MonadLiftT BaseIO m] (out : Lake.OutStream) (minLv : optParam Lake.LogLevel Lake.LogLevel.info) (ansiMode : optParam Lake.AnsiMode Lake.AnsiMode.auto) :

Lake.MonadLog m

Equations

out.logger minLv ansiMode = { logEntry := fun (e : Lake.LogEntry) => liftM (out.logEntry e minLv ansiMode) }

source

@[reducible, inline]

abbrev Lake.MonadLog.stdout {m : Type → Type u_1} [MonadLiftT BaseIO m] (minLv : optParam Lake.LogLevel Lake.LogLevel.info) (ansiMode : optParam Lake.AnsiMode Lake.AnsiMode.auto) :

Lake.MonadLog m

Equations

Lake.MonadLog.stdout minLv ansiMode = Lake.OutStream.stdout.logger minLv ansiMode

source

@[reducible, inline]

abbrev Lake.MonadLog.stderr {m : Type → Type u_1} [MonadLiftT BaseIO m] (minLv : optParam Lake.LogLevel Lake.LogLevel.info) (ansiMode : optParam Lake.AnsiMode Lake.AnsiMode.auto) :

Lake.MonadLog m

Equations

Lake.MonadLog.stderr minLv ansiMode = Lake.OutStream.stderr.logger minLv ansiMode

source

@[inline]

def Lake.OutStream.getLogger {m : Type → Type} [MonadLiftT BaseIO m] (out : Lake.OutStream) (minLv : optParam Lake.LogLevel Lake.LogLevel.info) (ansiMode : optParam Lake.AnsiMode Lake.AnsiMode.auto) :

BaseIO (Lake.MonadLog m)

Equations

out.getLogger minLv ansiMode = do let out ← out.get let useAnsi ← Lake.AnsiMode.isEnabled out ansiMode pure (Lake.MonadLog.stream out minLv useAnsi)

source

@[reducible, inline]

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

Type (max v w)

A monad equipped with a MonadLog instance

Equations

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

Instances For

source

instance Lake.MonadLogT.instInhabitedOfPure {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.MonadLogT.instInhabitedOfPure = { default := fun (x : Lake.MonadLog m) => pure default }

source

instance Lake.MonadLogT.instMonadLogOfMonadOfMonadLiftT {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

Lake.MonadLogT.instMonadLogOfMonadOfMonadLiftT = { logEntry := fun (e : Lake.LogEntry) => do let __do_lift ← read liftM (Lake.logEntry e) }

source

@[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

source

@[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

self.ignoreLog = self Lake.MonadLog.nop

source

structure Lake.Log :

Type

entries : Array Lake.LogEntry

Instances For

source

instance Lake.instToJsonLog :

Lean.ToJson Lake.Log

Equations

Lake.instToJsonLog = { toJson := fun (x : Lake.Log) => Lean.toJson x.entries }

source

instance Lake.instFromJsonLog :

Lean.FromJson Lake.Log

Equations

Lake.instFromJsonLog = { fromJson? := fun (x : Lean.Json) => Lake.Log.mk <$> Lean.fromJson? x }

source

structure Lake.Log.Pos :

Type

A position in a Log (i.e., an array index). Can be past the log's end.

val : Nat

Instances For

source

instance Lake.Log.instInhabitedPos :

Inhabited Lake.Log.Pos

Equations

Lake.Log.instInhabitedPos = { default := { val := default } }

source

instance Lake.instOfNatPos :

OfNat Lake.Log.Pos 0

Equations

Lake.instOfNatPos = { ofNat := { val := 0 } }

source

@[inline]

def Lake.Log.empty :

Lake.Log

Equations

Lake.Log.empty = { entries := #[] }

source

instance Lake.Log.instEmptyCollection :

EmptyCollection Lake.Log

Equations

Lake.Log.instEmptyCollection = { emptyCollection := Lake.Log.empty }

source

@[inline]

def Lake.Log.size (log : Lake.Log) :

Nat

Equations

log.size = log.entries.size

source

@[inline]

def Lake.Log.isEmpty (log : Lake.Log) :

Bool

Equations

log.isEmpty = decide (log.size = 0)

source

@[inline]

def Lake.Log.hasEntries (log : Lake.Log) :

Bool

Equations

log.hasEntries = decide (log.size ≠ 0)

source

@[inline]

def Lake.Log.endPos (log : Lake.Log) :

Lake.Log.Pos

Equations

log.endPos = { val := log.entries.size }

source

@[inline]

def Lake.Log.push (log : Lake.Log) (e : Lake.LogEntry) :

Lake.Log

Equations

log.push e = { entries := log.entries.push e }

source

@[inline]

def Lake.Log.append (log : Lake.Log) (o : Lake.Log) :

Lake.Log

Equations

log.append o = { entries := log.entries.append o.entries }

source

instance Lake.Log.instAppend :

Append Lake.Log

Equations

Lake.Log.instAppend = { append := Lake.Log.append }

source

@[inline]

def Lake.Log.extract (log : Lake.Log) (start : Lake.Log.Pos) (stop : Lake.Log.Pos) :

Lake.Log

Takes log entries between start (inclusive) and stop (exclusive).

Equations

log.extract start stop = { entries := log.entries.extract start.val stop.val }

source

@[inline]

def Lake.Log.dropFrom (log : Lake.Log) (pos : Lake.Log.Pos) :

Lake.Log

Removes log entries after pos (inclusive).

Equations

log.dropFrom pos = { entries := log.entries.shrink pos.val }

source

@[inline]

def Lake.Log.takeFrom (log : Lake.Log) (pos : Lake.Log.Pos) :

Lake.Log

Takes log entries before pos (exclusive).

Equations

log.takeFrom pos = log.extract pos log.endPos

source

@[inline]

def Lake.Log.split (log : Lake.Log) (pos : Lake.Log.Pos) :

Lake.Log × Lake.Log

Splits the log into two from pos. The first log is from the start to pos (exclusive), and the second log is from pos (inclusive) to the end.

Equations

log.split pos = (log.dropFrom pos, log.takeFrom pos)

source

def Lake.Log.toString (log : Lake.Log) :

String

Equations

log.toString = Array.foldl (fun (x : String) (x_1 : Lake.LogEntry) => x ++ x_1.toString ++ "\n") "" log.entries 0

source

instance Lake.Log.instToString :

ToString Lake.Log

Equations

Lake.Log.instToString = { toString := Lake.Log.toString }

source

@[inline]

def Lake.Log.replay {m : Type u_1 → Type u_2} [Monad m] [logger : Lake.MonadLog m] (log : Lake.Log) :

m PUnit

Equations

log.replay = Array.forM (fun (e : Lake.LogEntry) => Lake.logEntry e) log.entries 0

source

@[inline]

def Lake.Log.filter (f : Lake.LogEntry → Bool) (log : Lake.Log) :

Lake.Log

Equations

Lake.Log.filter f log = { entries := Array.filter f log.entries 0 }

source

@[inline]

def Lake.Log.any (f : Lake.LogEntry → Bool) (log : Lake.Log) :

Bool

Equations

Lake.Log.any f log = log.entries.any f 0

source

def Lake.Log.maxLv (log : Lake.Log) :

Lake.LogLevel

The max log level of entries in this log. If empty, returns trace.

Equations

log.maxLv = Array.foldl (fun (x : Lake.LogLevel) (x_1 : Lake.LogEntry) => max x x_1.level) Lake.LogLevel.trace log.entries 0

source

@[inline]

def Lake.pushLogEntry {m : Type → Type u_1} [MonadStateOf Lake.Log m] (e : Lake.LogEntry) :

m PUnit

Add a LogEntry to the end of the monad's Log.

Equations

Lake.pushLogEntry e = modify fun (x : Lake.Log) => x.push e

source

@[reducible, inline]

abbrev Lake.MonadLog.ofMonadState {m : Type → Type u_1} [MonadStateOf Lake.Log m] :

Lake.MonadLog m

Equations

Lake.MonadLog.ofMonadState = { logEntry := Lake.pushLogEntry }

source

@[inline]

def Lake.getLog {m : Type → Type u_1} [MonadStateOf Lake.Log m] :

m Lake.Log

Returns the monad's log.

Equations

Lake.getLog = get

source

@[inline]

def Lake.getLogPos {m : Type → Type u_1} [Functor m] [MonadStateOf Lake.Log m] :

m Lake.Log.Pos

Returns the current end position of the monad's log (i.e., its size).

Equations

Lake.getLogPos = (fun (x : Lake.Log) => x.endPos) <$> Lake.getLog

source

@[inline]

def Lake.takeLog {m : Type → Type u_1} [MonadStateOf Lake.Log m] :

m Lake.Log

Removes the section monad's log starting and returns it.

Equations

Lake.takeLog = modifyGet fun (log : Lake.Log) => (log, ∅)

source

@[inline]

def Lake.takeLogFrom {m : Type → Type u_1} [MonadStateOf Lake.Log m] (pos : Lake.Log.Pos) :

m Lake.Log

Removes the monad's log starting at pos and returns it. Useful for extracting logged errors after catching an error position from an ELogT (e.g., LogIO).

Equations

Lake.takeLogFrom pos = modifyGet fun (log : Lake.Log) => (log.takeFrom pos, log.dropFrom pos)

source

@[inline]

def Lake.dropLogFrom {m : Type → Type u_1} [MonadStateOf Lake.Log m] (pos : Lake.Log.Pos) :

m PUnit

Backtracks the monad's log to pos. Useful for discarding logged errors after catching an error position from an ELogT (e.g., LogIO).

Equations

Lake.dropLogFrom pos = modify fun (x : Lake.Log) => x.dropFrom pos

source

@[inline]

def Lake.extractLog {m : Type → Type u_1} [Monad m] [MonadStateOf Lake.Log m] (x : m PUnit) :

m Lake.Log

Returns the log from x while leaving it intact in the monad.

Equations

Lake.extractLog x = do let iniPos ← Lake.getLogPos x let log ← Lake.getLog pure (log.takeFrom iniPos)

source

@[inline]

def Lake.withExtractLog {m : Type → Type u_1} {α : Type} [Monad m] [MonadStateOf Lake.Log m] (x : m α) :

m (α × Lake.Log)

Returns the log from x and its result while leaving it intact in the monad.

Equations

Lake.withExtractLog x = do let iniPos ← Lake.getLogPos let a ← x let log ← Lake.getLog pure (a, log.takeFrom iniPos)

source

@[inline]

def Lake.withLogErrorPos {m : Type → Type u_1} {α : Type} [Monad m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] (self : m α) :

m α

Performs x and backtracks any error to the log position before x.

Equations

Lake.withLogErrorPos self = do let iniPos ← Lake.getLogPos tryCatch self fun (x : Lake.Log.Pos) => throw iniPos

source

@[inline]

def Lake.errorWithLog {m : Type → Type u_1} {β : Type} [Monad m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] (self : m PUnit) :

m β

Performs x and groups all logs generated into an error block.

Equations

Lake.errorWithLog self = do let iniPos ← Lake.getLogPos tryCatch self fun (x : Lake.Log.Pos) => pure () throw iniPos

source

@[inline]

def Lake.withLoggedIO {m : Type → Type u_1} {α : Type} [Monad m] [MonadLiftT BaseIO m] [Lake.MonadLog m] [MonadFinally m] (x : m α) :

m α

Captures IO in x into an informational log entry.

Equations

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

source

@[inline]

def Lake.ELog.error {m : Type → Type u_1} {α : Type} [Monad m] [Lake.MonadLog m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] (msg : String) :

m α

Throw with the logged error message.

Equations

Lake.ELog.error msg = Lake.errorWithLog (Lake.logError msg)

source

@[reducible, inline]

abbrev Lake.ELog.monadError {m : Type → Type u_1} [Monad m] [Lake.MonadLog m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] :

Lake.MonadError m

Alternative instance for monads with Log state and Log.Pos errors.

Equations

Lake.ELog.monadError = { error := fun {α : Type} => Lake.ELog.error }

source

@[inline]

def Lake.ELog.failure {m : Type → Type u_1} {α : Type} [Monad m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] :

m α

Fail without logging anything.

Equations

Lake.ELog.failure = do let __do_lift ← Lake.getLogPos throw __do_lift

source

@[inline]

def Lake.ELog.orElse {m : Type → Type u_1} {α : Type} [Monad m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] (x : m α) (y : Unit → m α) :

m α

Performs x. If it fails, drop its log and perform y.

Equations

Lake.ELog.orElse x y = tryCatch x fun (errPos : Lake.Log.Pos) => do Lake.dropLogFrom errPos y ()

source

@[reducible, inline]

abbrev Lake.ELog.alternative {m : Type → Type u_1} [Monad m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] :

Alternative m

Alternative instance for monads with Log state and Log.Pos errors.

Equations

Lake.ELog.alternative = Alternative.mk (fun {α : Type} => Lake.ELog.failure) fun {α : Type} => Lake.ELog.orElse

source

@[reducible, inline]

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

Type

A monad equipped with a log.

Equations

Lake.LogT m = StateT Lake.Log m

Instances For

Lake.instMonadLogLogTOfMonad

source

instance Lake.instMonadLogLogTOfMonad {m : Type → Type} [Monad m] :

Lake.MonadLog (Lake.LogT m)

Equations

Lake.instMonadLogLogTOfMonad = Lake.MonadLog.ofMonadState

source

@[reducible, inline]

abbrev Lake.LogT.run {m : Type → Type} {α : Type} [Functor m] (self : Lake.LogT m α) (log : optParam Lake.Log ∅) :

m (α × Lake.Log)

Equations

self.run log = StateT.run self log

source

@[reducible, inline]

abbrev Lake.LogT.run' {m : Type → Type} {α : Type} [Functor m] (self : Lake.LogT m α) (log : optParam Lake.Log ∅) :

m α

Equations

self.run' log = StateT.run' self log

source

@[inline]

def Lake.LogT.takeAndRun {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [MonadStateOf Lake.Log n] [MonadLiftT m n] [MonadFinally n] (self : Lake.LogT m α) :

n α

Run self with the log taken from the state of the monad n.

Warning: If lifting self from m to n fails, the log will be lost. Thus, this is best used when the lift cannot fail.

Equations

self.takeAndRun = do let __do_lift ← Lake.takeLog let __discr ← liftM (self __do_lift) match __discr with | (a, log) => do set log pure a

source

@[inline]

def Lake.LogT.replayLog {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [logger : Lake.MonadLog n] [MonadLiftT m n] (self : Lake.LogT m α) :

n α

Runs self in n and then replays the entries of the resulting log using the new monad's logger.

Equations

self.replayLog = do let __discr ← liftM (self ∅) match __discr with | (a, log) => do log.replay pure a

source

@[reducible, inline]

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

Type

A monad equipped with a log and the ability to error at some log position.

Equations

Lake.ELogT m = Lake.EStateT Lake.Log.Pos Lake.Log m

Instances For

source

@[reducible, inline]

abbrev Lake.ELogResult (α : Type u_1) :

Type u_1

Equations

Lake.ELogResult α = Lake.EResult Lake.Log.Pos Lake.Log α

source

instance Lake.instMonadLogELogTOfMonad {m : Type → Type} [Monad m] :

Lake.MonadLog (Lake.ELogT m)

Equations

Lake.instMonadLogELogTOfMonad = Lake.MonadLog.ofMonadState

source

instance Lake.instMonadErrorELogTOfMonad {m : Type → Type} [Monad m] :

Lake.MonadError (Lake.ELogT m)

Equations

Lake.instMonadErrorELogTOfMonad = Lake.ELog.monadError

source

instance Lake.instAlternativeELogTOfMonad {m : Type → Type} [Monad m] :

Alternative (Lake.ELogT m)

Equations

Lake.instAlternativeELogTOfMonad = Lake.ELog.alternative

source

@[reducible, inline]

abbrev Lake.ELogT.run {m : Type → Type} {α : Type} (self : Lake.ELogT m α) (log : optParam Lake.Log ∅) :

m (Lake.ELogResult α)

Equations

self.run log = Lake.EStateT.run log self

source

@[reducible, inline]

abbrev Lake.ELogT.run' {m : Type → Type} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : optParam Lake.Log ∅) :

m (Except Lake.Log.Pos α)

Equations

self.run' log = Lake.EStateT.run' log self

source

@[reducible, inline]

abbrev Lake.ELogT.toLogT {m : Type → Type} {α : Type} [Functor m] (self : Lake.ELogT m α) :

Lake.LogT m (Except Lake.Log.Pos α)

Equations

self.toLogT = Lake.EStateT.toStateT self

source

@[reducible, inline]

abbrev Lake.ELogT.toLogT? {m : Type → Type} {α : Type} [Functor m] (self : Lake.ELogT m α) :

Lake.LogT m (Option α)

Equations

self.toLogT? = Lake.EStateT.toStateT? self

source

@[reducible, inline]

abbrev Lake.ELogT.run? {m : Type → Type} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : optParam Lake.Log ∅) :

m (Option α × Lake.Log)

Equations

self.run? log = Lake.EStateT.run? log self

source

@[reducible, inline]

abbrev Lake.ELogT.run?' {m : Type → Type} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : optParam Lake.Log ∅) :

m (Option α)

Equations

self.run?' log = Lake.EStateT.run?' log self

source

@[inline]

def Lake.ELogT.catchLog {m : Type → Type} {α : Type} [Monad m] (f : Lake.Log → Lake.LogT m α) (self : Lake.ELogT m α) :

Lake.LogT m α

Equations

Lake.ELogT.catchLog f self = Lake.EStateT.catchExceptions self fun (errPos : Lake.Log.Pos) => do let __do_lift ← Lake.takeLogFrom errPos f __do_lift

source

@[reducible, inline, deprecated Lake.ELogT.run?]

abbrev Lake.ELogT.captureLog {m : Type → Type} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : optParam Lake.Log ∅) :

m (Option α × Lake.Log)

Equations

@Lake.ELogT.captureLog = @Lake.ELogT.run?

source

@[inline]

def Lake.ELogT.takeAndRun {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [MonadStateOf Lake.Log n] [MonadExceptOf Lake.Log.Pos n] [MonadLiftT m n] (self : Lake.ELogT m α) :

n α

Run self with the log taken from the state of the monad n,

Warning: If lifting self from m to n fails, the log will be lost. Thus, this is best used when the lift cannot fail. Note excludes the native log position failure of ELogT, which are lifted safely.

Equations

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

source

@[inline]

def Lake.ELogT.replayLog? {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [logger : Lake.MonadLog n] [MonadLiftT m n] (self : Lake.ELogT m α) :

n (Option α)

Runs self in n and then replays the entries of the resulting log using the new monad's logger. Translates an exception in this monad to a none result.

Equations

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

source

@[inline]

def Lake.ELogT.replayLog {n : Type → Type u_1} {m : Type → Type} {α : Type} [Alternative n] [Monad n] [logger : Lake.MonadLog n] [MonadLiftT m n] (self : Lake.ELogT m α) :

n α

Runs self in n and then replays the entries of the resulting log using the new monad's logger. Translates an exception in this monad to a failure in the new monad.

Equations