structure Aesop.RuleProfile : Type

• rule : Aesop.DisplayRuleName
• elapsed : Aesop.Nanos
• successful : Bool

instance Aesop.instInhabitedRuleProfile : Inhabited Aesop.RuleProfile

Equations

• Aesop.instInhabitedRuleProfile = { default := { rule := default, elapsed := default, successful := default } }

instance Aesop.RuleProfile.instToStringRuleProfile : ToString Aesop.RuleProfile

Equations

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

structure Aesop.Profile : Type

• total : Aesop.Nanos
• configParsing : Aesop.Nanos
• ruleSetConstruction : Aesop.Nanos
• search : Aesop.Nanos
• ruleSelection : Aesop.Nanos
• ruleApplications : Array Aesop.RuleProfile

instance Aesop.instInhabitedProfile : Inhabited Aesop.Profile

Equations

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

def Aesop.Profile.empty : Aesop.Profile

Equations

• Aesop.Profile.empty = { total := 0, configParsing := 0, ruleSetConstruction := 0, search := 0, ruleSelection := 0, ruleApplications := #[] }

instance Aesop.Profile.instEmptyCollectionProfile : EmptyCollection Aesop.Profile

Equations

• Aesop.Profile.instEmptyCollectionProfile = { emptyCollection := Aesop.Profile.empty }

def Aesop.Profile.ruleApplicationTotals (p : Aesop.Profile) : Lean.HashMap Aesop.DisplayRuleName (Aesop.Nanos × Aesop.Nanos)

Equations

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

def Aesop.Profile.trace (p : Aesop.Profile) (opt : Aesop.TraceOption) : Lean.CoreM Unit

Equations

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

def Aesop.Profile.trace.compareTimings (x : Aesop.DisplayRuleName × Aesop.Nanos × Aesop.Nanos) (y : Aesop.DisplayRuleName × Aesop.Nanos × Aesop.Nanos) : Ordering

Equations

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

structure Aesop.ProfileT.Context : Type

• isProfilingEnabled : Bool

@[inline, reducible]

abbrev Aesop.ProfileT (m : Type → Type) (α : Type) : Type

Equations

• Aesop.ProfileT m = ReaderT Aesop.ProfileT.Context (StateRefT' IO.RealWorld Aesop.Profile m)

def Aesop.ProfileT.run {m : Type → Type} {α : Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (x : Aesop.ProfileT m α) (isProfilingEnabled : Bool) (profile : Aesop.Profile) : m (α × Aesop.Profile)

Equations

• Aesop.ProfileT.run x isProfilingEnabled profile = StateRefT'.run (ReaderT.run x { isProfilingEnabled := isProfilingEnabled }) profile

class Aesop.MonadProfile (m : Type → Type u_1) extends MonadReaderOf , MonadStateOf : Type (max 1 u_1)

@[always_inline]

def Aesop.isProfilingEnabled {m : Type → Type u_1} [Monad m] [Aesop.MonadProfile m] : m Bool

Equations

• Aesop.isProfilingEnabled = do let __do_lift ← read pure __do_lift.isProfilingEnabled

@[always_inline]

def Aesop.recordRuleSelectionProfile {m : Type → Type u_1} [Aesop.MonadProfile m] (elapsed : Aesop.Nanos) : m Unit

Equations

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

@[always_inline]

def Aesop.recordRuleProfile {m : Type → Type u_1} [Aesop.MonadProfile m] (rp : Aesop.RuleProfile) : m Unit

Equations

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

@[always_inline]

def Aesop.profiling {m : Type → Type u_1} [Monad m] [Aesop.MonadProfile m] {α : Type} [MonadLiftT BaseIO m] (x : m α) (recordProfile : α → Aesop.Nanos → m Unit) : m α

Equations

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