inductive Lake.Verbosity : Type

• quiet : Verbosity
• normal : Verbosity
• verbose : Verbosity

instance Lake.instReprVerbosity : Repr Verbosity

Equations

• Lake.instReprVerbosity = { reprPrec := Lake.instReprVerbosity.repr }

def Lake.instReprVerbosity.repr : Verbosity → Nat → Std.Format

Equations

• Lake.instReprVerbosity.repr Lake.Verbosity.quiet prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.Verbosity.quiet")).group prec✝
• Lake.instReprVerbosity.repr Lake.Verbosity.normal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.Verbosity.normal")).group prec✝
• Lake.instReprVerbosity.repr Lake.Verbosity.verbose prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.Verbosity.verbose")).group prec✝

instance Lake.instDecidableEqVerbosity : DecidableEq Verbosity

Equations

• Lake.instDecidableEqVerbosity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Lake.instOrdVerbosity : Ord Verbosity

Equations

• Lake.instOrdVerbosity = { compare := Lake.instOrdVerbosity.ord }

def Lake.instOrdVerbosity.ord : Verbosity → Verbosity → Ordering

Equations

• Lake.instOrdVerbosity.ord Lake.Verbosity.quiet Lake.Verbosity.quiet = Ordering.eq
• Lake.instOrdVerbosity.ord Lake.Verbosity.quiet x✝ = Ordering.lt
• Lake.instOrdVerbosity.ord x Lake.Verbosity.quiet = Ordering.gt
• Lake.instOrdVerbosity.ord Lake.Verbosity.normal Lake.Verbosity.normal = Ordering.eq
• Lake.instOrdVerbosity.ord Lake.Verbosity.normal x✝ = Ordering.lt
• Lake.instOrdVerbosity.ord x Lake.Verbosity.normal = Ordering.gt
• Lake.instOrdVerbosity.ord Lake.Verbosity.verbose Lake.Verbosity.verbose = Ordering.eq

instance Lake.instLTVerbosity : LT Verbosity

Equations

• Lake.instLTVerbosity = ltOfOrd

instance Lake.instLEVerbosity : LE Verbosity

Equations

• Lake.instLEVerbosity = leOfOrd

instance Lake.instMinVerbosity : Min Verbosity

Equations

• Lake.instMinVerbosity = minOfLe

instance Lake.instMaxVerbosity : Max Verbosity

Equations

• Lake.instMaxVerbosity = maxOfLe

instance Lake.instInhabitedVerbosity : Inhabited Verbosity

Equations

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

inductive Lake.AnsiMode : Type

Whether to ANSI escape codes.

• auto : AnsiMode

  Automatically determine whether to use ANSI escape codes based on whether the stream written to is a terminal.

• ansi : AnsiMode

  Use ANSI escape codes.

• noAnsi : AnsiMode

  Do not use ANSI escape codes.

instance Lake.instReprAnsiMode : Repr AnsiMode

Equations

• Lake.instReprAnsiMode = { reprPrec := Lake.instReprAnsiMode.repr }

def Lake.instReprAnsiMode.repr : AnsiMode → Nat → Std.Format

Equations

• Lake.instReprAnsiMode.repr Lake.AnsiMode.auto prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.AnsiMode.auto")).group prec✝
• Lake.instReprAnsiMode.repr Lake.AnsiMode.ansi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.AnsiMode.ansi")).group prec✝
• Lake.instReprAnsiMode.repr Lake.AnsiMode.noAnsi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.AnsiMode.noAnsi")).group prec✝

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

Returns whether to ANSI escape codes with the stream out.

Equations

• Lake.AnsiMode.isEnabled out Lake.AnsiMode.auto = out.isTty
• Lake.AnsiMode.isEnabled out Lake.AnsiMode.ansi = pure true
• Lake.AnsiMode.isEnabled out Lake.AnsiMode.noAnsi = pure false

def Lake.Ansi.chalk (colorCode 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"

inductive Lake.OutStream : Type

A pure representation of output stream.

• stdout : OutStream
• stderr : OutStream
• stream (s : IO.FS.Stream) : OutStream

def Lake.OutStream.get : OutStream → BaseIO IO.FS.Stream

Returns the real output stream associated with OutStream.

Equations

• Lake.OutStream.stdout.get = IO.getStdout
• Lake.OutStream.stderr.get = IO.getStderr
• (Lake.OutStream.stream s).get = pure s

instance Lake.instCoeStreamOutStream : Coe IO.FS.Stream OutStream

Equations

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

instance Lake.instCoeHandleOutStream : Coe IO.FS.Handle OutStream

Equations

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

inductive Lake.LogLevel : Type

• trace : LogLevel
• info : LogLevel
• warning : LogLevel
• error : LogLevel

instance Lake.instInhabitedLogLevel : Inhabited LogLevel

Equations

• Lake.instInhabitedLogLevel = { default := Lake.instInhabitedLogLevel.default }

def Lake.instInhabitedLogLevel.default : LogLevel

Equations

• Lake.instInhabitedLogLevel.default = Lake.LogLevel.trace

instance Lake.instReprLogLevel : Repr LogLevel

Equations

• Lake.instReprLogLevel = { reprPrec := Lake.instReprLogLevel.repr }

def Lake.instReprLogLevel.repr : LogLevel → Nat → Std.Format

Equations

• Lake.instReprLogLevel.repr Lake.LogLevel.trace prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.LogLevel.trace")).group prec✝
• Lake.instReprLogLevel.repr Lake.LogLevel.info prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.LogLevel.info")).group prec✝
• Lake.instReprLogLevel.repr Lake.LogLevel.warning prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.LogLevel.warning")).group prec✝
• Lake.instReprLogLevel.repr Lake.LogLevel.error prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.LogLevel.error")).group prec✝

instance Lake.instDecidableEqLogLevel : DecidableEq LogLevel

Equations

• Lake.instDecidableEqLogLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Lake.instOrdLogLevel : Ord LogLevel

Equations

• Lake.instOrdLogLevel = { compare := Lake.instOrdLogLevel.ord }

def Lake.instOrdLogLevel.ord : LogLevel → LogLevel → Ordering

Equations

• Lake.instOrdLogLevel.ord Lake.LogLevel.trace Lake.LogLevel.trace = Ordering.eq
• Lake.instOrdLogLevel.ord Lake.LogLevel.trace x✝ = Ordering.lt
• Lake.instOrdLogLevel.ord x Lake.LogLevel.trace = Ordering.gt
• Lake.instOrdLogLevel.ord Lake.LogLevel.info Lake.LogLevel.info = Ordering.eq
• Lake.instOrdLogLevel.ord Lake.LogLevel.info x✝ = Ordering.lt
• Lake.instOrdLogLevel.ord x Lake.LogLevel.info = Ordering.gt
• Lake.instOrdLogLevel.ord Lake.LogLevel.warning Lake.LogLevel.warning = Ordering.eq
• Lake.instOrdLogLevel.ord Lake.LogLevel.warning x✝ = Ordering.lt
• Lake.instOrdLogLevel.ord x Lake.LogLevel.warning = Ordering.gt
• Lake.instOrdLogLevel.ord Lake.LogLevel.error Lake.LogLevel.error = Ordering.eq

instance Lake.instToJsonLogLevel : Lean.ToJson LogLevel

Equations

• Lake.instToJsonLogLevel = { toJson := Lake.instToJsonLogLevel.toJson }

def Lake.instToJsonLogLevel.toJson : LogLevel → Lean.Json

Equations

• Lake.instToJsonLogLevel.toJson Lake.LogLevel.trace = Lean.toJson "trace"
• Lake.instToJsonLogLevel.toJson Lake.LogLevel.info = Lean.toJson "info"
• Lake.instToJsonLogLevel.toJson Lake.LogLevel.warning = Lean.toJson "warning"
• Lake.instToJsonLogLevel.toJson Lake.LogLevel.error = Lean.toJson "error"

def Lake.instFromJsonLogLevel.fromJson : Lean.Json → Except String LogLevel

Equations

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

instance Lake.instFromJsonLogLevel : Lean.FromJson LogLevel

Equations

• Lake.instFromJsonLogLevel = { fromJson? := Lake.instFromJsonLogLevel.fromJson }

instance Lake.instLTLogLevel : LT LogLevel

Equations

• Lake.instLTLogLevel = ltOfOrd

instance Lake.instLELogLevel : LE LogLevel

Equations

• Lake.instLELogLevel = leOfOrd

instance Lake.instMinLogLevel : Min LogLevel

Equations

• Lake.instMinLogLevel = minOfLe

instance Lake.instMaxLogLevel : Max LogLevel

Equations

• Lake.instMaxLogLevel = maxOfLe

def Lake.LogLevel.icon : LogLevel → Char

Unicode icon for representing the log level.

Equations

• Lake.LogLevel.trace.icon = 'ℹ'
• Lake.LogLevel.info.icon = 'ℹ'
• Lake.LogLevel.warning.icon = '⚠'
• Lake.LogLevel.error.icon = '✖'

def Lake.LogLevel.ansiColor : LogLevel → String

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

Equations

• Lake.LogLevel.trace.ansiColor = "34"
• Lake.LogLevel.info.ansiColor = "34"
• Lake.LogLevel.warning.ansiColor = "33"
• Lake.LogLevel.error.ansiColor = "31"

def Lake.LogLevel.ofString? (s : String) : Option LogLevel

Equations

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

def Lake.LogLevel.toString : LogLevel → String

Equations

• Lake.LogLevel.trace.toString = "trace"
• Lake.LogLevel.info.toString = "info"
• Lake.LogLevel.warning.toString = "warning"
• Lake.LogLevel.error.toString = "error"

def Lake.LogLevel.ofMessageSeverity : Lean.MessageSeverity → LogLevel

Equations

• Lake.LogLevel.ofMessageSeverity Lean.MessageSeverity.information = Lake.LogLevel.info
• Lake.LogLevel.ofMessageSeverity Lean.MessageSeverity.warning = Lake.LogLevel.warning
• Lake.LogLevel.ofMessageSeverity Lean.MessageSeverity.error = Lake.LogLevel.error

def Lake.LogLevel.toMessageSeverity : LogLevel → Lean.MessageSeverity

Equations

• Lake.LogLevel.info.toMessageSeverity = Lean.MessageSeverity.information
• Lake.LogLevel.trace.toMessageSeverity = Lean.MessageSeverity.information
• Lake.LogLevel.warning.toMessageSeverity = Lean.MessageSeverity.warning
• Lake.LogLevel.error.toMessageSeverity = Lean.MessageSeverity.error

def Lake.Verbosity.minLogLv : Verbosity → LogLevel

Equations

• Lake.Verbosity.quiet.minLogLv = Lake.LogLevel.warning
• Lake.Verbosity.normal.minLogLv = Lake.LogLevel.info
• Lake.Verbosity.verbose.minLogLv = Lake.LogLevel.trace

structure Lake.LogEntry : Type

• level : LogLevel
• message : String

instance Lake.instInhabitedLogEntry : Inhabited LogEntry

Equations

• Lake.instInhabitedLogEntry = { default := Lake.instInhabitedLogEntry.default }

def Lake.instInhabitedLogEntry.default : LogEntry

Equations

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

def Lake.instToJsonLogEntry.toJson : LogEntry → Lean.Json

Equations

• Lake.instToJsonLogEntry.toJson x✝ = Lean.Json.mkObj [[("level", Lean.toJson x✝.level)], [("message", Lean.toJson x✝.message)]].flatten

instance Lake.instToJsonLogEntry : Lean.ToJson LogEntry

Equations

• Lake.instToJsonLogEntry = { toJson := Lake.instToJsonLogEntry.toJson }

def Lake.instFromJsonLogEntry.fromJson : Lean.Json → Except String LogEntry

Equations

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

instance Lake.instFromJsonLogEntry : Lean.FromJson LogEntry

Equations

• Lake.instFromJsonLogEntry = { fromJson? := Lake.instFromJsonLogEntry.fromJson }

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

Equations

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

instance Lake.instToStringLogEntry : ToString LogEntry

Equations

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

@[inline]

def Lake.LogEntry.trace (message : String) : LogEntry

Equations

• Lake.LogEntry.trace message = { level := Lake.LogLevel.trace, message := message }

@[inline]

def Lake.LogEntry.info (message : String) : LogEntry

Equations

• Lake.LogEntry.info message = { level := Lake.LogLevel.info, message := message }

@[inline]

def Lake.LogEntry.warning (message : String) : LogEntry

Equations

• Lake.LogEntry.warning message = { level := Lake.LogLevel.warning, message := message }

@[inline]

def Lake.LogEntry.error (message : String) : LogEntry

Equations

• Lake.LogEntry.error message = { level := Lake.LogLevel.error, message := message }

def Lake.LogEntry.ofSerialMessage (msg : Lean.SerialMessage) : LogEntry

Equations

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

def Lake.LogEntry.ofMessage (msg : Lean.Message) : BaseIO LogEntry

Equations

• Lake.LogEntry.ofMessage msg = do let __do_lift ← msg.serialize pure (inline (Lake.LogEntry.ofSerialMessage __do_lift))

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

• logEntry (e : LogEntry) : m PUnit

@[inline]

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

Equations

• Lake.logVerbose message = Lake.logEntry (Lake.LogEntry.trace message)

@[inline]

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

Equations

• Lake.logInfo message = Lake.logEntry (Lake.LogEntry.info message)

@[inline]

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

Equations

• Lake.logWarning message = Lake.logEntry (Lake.LogEntry.warning message)

@[inline]

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

Equations

• Lake.logError message = Lake.logEntry (Lake.LogEntry.error message)

@[inline]

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

Equations

• Lake.logSerialMessage msg = if msg.isSilent = true then pure PUnit.unit else Lake.logEntry (Lake.LogEntry.ofSerialMessage msg)

@[inline]

def Lake.logMessage {m : Type → Type u_1} (msg : Lean.Message) [Monad m] [MonadLog m] [MonadLiftT BaseIO m] : m PUnit

Equations

• Lake.logMessage msg = if msg.isSilent = true then pure PUnit.unit else do let __do_lift ← liftM (Lake.LogEntry.ofMessage msg) Lake.logEntry __do_lift

def Lake.logToStream (e : LogEntry) (out : IO.FS.Stream) (minLv : 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

@[reducible, inline]

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

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

• Lake.MonadLog.instOfMonadLift = methods.lift

@[reducible, inline]

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

Equations

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

@[inline]

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

Equations

• Lake.MonadLog.error msg = Lake.logError msg *> failure

def Lake.OutStream.logEntry (self : OutStream) (e : LogEntry) (minLv : LogLevel := LogLevel.info) (ansiMode : AnsiMode := 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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[inline]

def Lake.OutStream.getLogger {m : Type → Type} [MonadLiftT BaseIO m] (out : OutStream) (minLv : LogLevel := LogLevel.info) (ansiMode : AnsiMode := AnsiMode.auto) : BaseIO (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)

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

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 (MonadLogT m n α)

Equations

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

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

Equations

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

@[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 : MonadLog m → MonadLog m') (self : MonadLogT m' n α) : 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 : MonadLogT m n α) : n α

Equations

• self.ignoreLog = self Lake.MonadLog.nop

structure Lake.Log : Type

• entries : Array LogEntry

instance Lake.instInhabitedLog : Inhabited Log

Equations

• Lake.instInhabitedLog = { default := Lake.instInhabitedLog.default }

def Lake.instInhabitedLog.default : Log

Equations

• Lake.instInhabitedLog.default = { entries := default }

instance Lake.instToJsonLog : Lean.ToJson Log

Equations

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

instance Lake.instFromJsonLog : Lean.FromJson Log

Equations

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

structure Lake.Log.Pos : Type

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

• val : Nat

instance Lake.Log.instInhabitedPos : Inhabited Pos

Equations

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

def Lake.Log.instInhabitedPos.default : Pos

Equations

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

instance Lake.Log.instDecidableEqPos : DecidableEq Pos

Equations

• Lake.Log.instDecidableEqPos = Lake.Log.instDecidableEqPos.decEq

def Lake.Log.instDecidableEqPos.decEq (x✝ x✝¹ : Pos) : Decidable (x✝ = x✝¹)

Equations

• Lake.Log.instDecidableEqPos.decEq { val := a } { val := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Lake.instOfNatPos : OfNat Log.Pos 0

Equations

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

instance Lake.instOrdPos : Ord Log.Pos

Equations

• Lake.instOrdPos = { compare := fun (x1 x2 : Lake.Log.Pos) => compare x1.val x2.val }

instance Lake.instLTPos : LT Log.Pos

Equations

• Lake.instLTPos = { lt := fun (x1 x2 : Lake.Log.Pos) => x1.val < x2.val }

instance Lake.instDecidableRelPosLt : DecidableRel LT.lt

Equations

• Lake.instDecidableRelPosLt = inferInstanceAs (DecidableRel fun (x1 x2 : Lake.Log.Pos) => x1.val < x2.val)

instance Lake.instLEPos : LE Log.Pos

Equations

• Lake.instLEPos = { le := fun (x1 x2 : Lake.Log.Pos) => x1.val ≤ x2.val }

instance Lake.instDecidableRelPosLe : DecidableRel LE.le

Equations

• Lake.instDecidableRelPosLe = inferInstanceAs (DecidableRel fun (x1 x2 : Lake.Log.Pos) => x1.val ≤ x2.val)

instance Lake.instMinPos : Min Log.Pos

Equations

• Lake.instMinPos = minOfLe

instance Lake.instMaxPos : Max Log.Pos

Equations

• Lake.instMaxPos = maxOfLe

@[inline]

def Lake.Log.empty : Log

Equations

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

instance Lake.Log.instEmptyCollection : EmptyCollection Log

Equations

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

@[inline]

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

Equations

• log.size = log.entries.size

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

instance Lake.Log.instAppend : Append Log

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

Removes log entries after pos (inclusive).

Equations

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

@[inline]

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

Takes log entries before pos (exclusive).

Equations

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

@[inline]

def Lake.Log.split (log : Log) (pos : Pos) : Log × 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)

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

Equations

• log.toString = Array.foldl (fun (x1 : String) (x2 : Lake.LogEntry) => x1 ++ x2.toString ++ "\n") "" log.entries

instance Lake.Log.instToString : ToString Log

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

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

Equations

• log.maxLv = Array.foldl (fun (x1 : Lake.LogLevel) (x2 : Lake.LogEntry) => max x1 x2.level) Lake.LogLevel.trace log.entries

@[inline]

def Lake.pushLogEntry {m : Type → Type u_1} [MonadStateOf Log m] (e : 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

@[reducible, inline]

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

Equations

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

@[inline]

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

Returns the monad's log.

Equations

• Lake.getLog = get

@[inline]

def Lake.getLogPos {m : Type → Type u_1} [Functor m] [MonadStateOf Log m] : m 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

@[inline]

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

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

Equations

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

@[inline]

def Lake.takeLogFrom {m : Type → Type u_1} [MonadStateOf Log m] (pos : Log.Pos) : m 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)

@[inline]

def Lake.dropLogFrom {m : Type → Type u_1} [MonadStateOf Log m] (pos : 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

@[inline]

def Lake.extractLog {m : Type → Type u_1} [Monad m] [MonadStateOf Log m] (x : m PUnit) : m 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)

@[inline]

def Lake.withExtractLog {m : Type → Type u_1} {α : Type} [Monad m] [MonadStateOf Log m] (x : m α) : m (α × 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)

@[inline]

def Lake.withLogErrorPos {m : Type → Type u_1} {α : Type} [Monad m] [MonadStateOf Log m] [MonadExceptOf 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

@[inline]

def Lake.errorWithLog {m : Type → Type u_1} {β : Type} [Monad m] [MonadStateOf Log m] [MonadExceptOf 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

@[inline]

def Lake.withLoggedIO {m : Type → Type u_1} {α : Type} [Monad m] [MonadLiftT BaseIO m] [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.

@[inline]

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

Throw with the logged error message.

Equations

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

@[reducible, inline]

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

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

Equations

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

@[inline]

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

Fail without logging anything.

Equations

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

@[inline]

def Lake.ELog.orElse {m : Type → Type u_1} {α : Type} [Monad m] [MonadStateOf Log m] [MonadExceptOf 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 ()

@[reducible, inline]

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

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

Equations

• Lake.ELog.alternative = { toApplicative := inst✝².toApplicative, failure := fun {α : Type} => Lake.ELog.failure, orElse := fun {α : Type} => Lake.ELog.orElse }

@[reducible, inline]

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

A monad equipped with a log.

Equations

• Lake.LogT m = StateT Lake.Log m

instance Lake.instMonadLogLogTOfMonad {m : Type → Type} [Monad m] : MonadLog (LogT m)

Equations

• Lake.instMonadLogLogTOfMonad = Lake.MonadLog.ofMonadState

@[reducible, inline]

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

Equations

• self.run log = StateT.run self log

@[reducible, inline]

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

Equations

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

@[inline]

def Lake.LogT.takeAndRun {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [MonadStateOf Log n] [MonadLiftT m n] [MonadFinally n] (self : 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

@[inline]

def Lake.LogT.replayLog {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [logger : MonadLog n] [MonadLiftT m n] (self : 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

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

@[reducible, inline]

abbrev Lake.ELogResult (α : Type u_1) : Type u_1

Equations

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

instance Lake.instMonadLogELogTOfMonad {m : Type → Type} [Monad m] : MonadLog (ELogT m)

Equations

• Lake.instMonadLogELogTOfMonad = Lake.MonadLog.ofMonadState

instance Lake.instMonadErrorELogTOfMonad {m : Type → Type} [Monad m] : MonadError (ELogT m)

Equations

• Lake.instMonadErrorELogTOfMonad = Lake.ELog.monadError

instance Lake.instAlternativeELogTOfMonad {m : Type → Type} [Monad m] : Alternative (ELogT m)

Equations

• Lake.instAlternativeELogTOfMonad = Lake.ELog.alternative

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• self.toLogT = Lake.EStateT.toStateT self

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[inline]

def Lake.ELogT.catchLog {m : Type → Type} {α : Type} [Monad m] (f : Log → LogT m α) (self : ELogT m α) : 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

@[inline]

def Lake.ELogT.takeAndRun {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [MonadStateOf Log n] [MonadExceptOf Log.Pos n] [MonadLiftT m n] (self : 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. This 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.

@[inline]

def Lake.ELogT.replayLog? {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [logger : MonadLog n] [MonadLiftT m n] (self : 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

• self.replayLog? = do let __do_lift ← liftM self.run match __do_lift with | Lake.EResult.ok a log => log.replay *> pure (some a) | Lake.EResult.error a log => log.replay *> pure none

@[inline]

def Lake.ELogT.replayLog {n : Type → Type u_1} {m : Type → Type} {α : Type} [Alternative n] [Monad n] [logger : MonadLog n] [MonadLiftT m n] (self : 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

• self.replayLog = do let __do_lift ← liftM self.run match __do_lift with | Lake.EResult.ok a log => log.replay *> pure a | Lake.EResult.error a log => log.replay *> failure

@[reducible, inline]

abbrev Lake.LogIO (α : Type) : Type

A monad equipped with a log, a log error position, and the ability to perform I/O.

Equations

• Lake.LogIO = Lake.ELogT BaseIO

instance Lake.instMonadLiftIOLogIO : MonadLift IO LogIO

Equations

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

@[inline]

def Lake.LogIO.toBaseIO {α : Type} (self : LogIO α) (minLv : LogLevel := LogLevel.info) (ansiMode : AnsiMode := AnsiMode.auto) (out : OutStream := OutStream.stderr) : BaseIO (Option α)

Runs a LogIO action in BaseIO. Prints log entries of at least minLv to out.

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Lake.LoggerIO (α : Type) : Type

A monad equipped with a log function and the ability to perform I/O. Unlike LogIO, log entries are not retained by the monad but instead eagerly passed to the log function.

Equations

• Lake.LoggerIO = Lake.MonadLogT BaseIO (EIO PUnit)

instance Lake.instMonadErrorLoggerIO : MonadError LoggerIO

Equations

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

instance Lake.instMonadLiftIOLoggerIO : MonadLift IO LoggerIO

Equations

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

instance Lake.instMonadLiftLogIOLoggerIO : MonadLift LogIO LoggerIO

Equations

• Lake.instMonadLiftLogIOLoggerIO = { monadLift := fun {α : Type} => Lake.ELogT.replayLog }

@[inline]

def Lake.LoggerIO.toBaseIO {α : Type} (self : LoggerIO α) (minLv : LogLevel := LogLevel.info) (ansiMode : AnsiMode := AnsiMode.auto) (out : OutStream := OutStream.stderr) : BaseIO (Option α)

Runs a LoggerIO action in BaseIO. Prints log entries of at least minLv to out.

Equations

• self.toBaseIO minLv ansiMode out = do let __do_lift ← out.getLogger minLv ansiMode (fun (x : Except PUnit α) => x.toOption) <$> (ReaderT.run self __do_lift).toBaseIO

def Lake.LoggerIO.captureLog {α : Type} (self : LoggerIO α) : BaseIO (Option α × Log)

Equations

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

@[reducible, inline]

abbrev Lake.LoggerIO.run? {α : Type} (self : LoggerIO α) : BaseIO (Option α × Log)

Equations

• @Lake.LoggerIO.run? = @Lake.LoggerIO.captureLog

@[inline]

def Lake.LoggerIO.run?' {α : Type} (self : LoggerIO α) (logger : LogEntry → BaseIO PUnit := fun (x : LogEntry) => pure ()) : BaseIO (Option α)

Equations

• self.run?' logger = (fun (x : Except PUnit α) => x.toOption) <$> (ReaderT.run self { logEntry := logger }).toBaseIO