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.

@[inline, reducible]

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

Equations

• Aesop.ProfileT m = 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 α) (profile : Aesop.Profile) : m (α × Aesop.Profile)

Equations

• Aesop.ProfileT.run x profile = StateRefT'.run x profile

def Aesop.ProfileT.liftBase {m : Type → Type} {n : Type → Type} {α : Type} [MonadLiftT m n] (x : Aesop.ProfileT m α) : Aesop.ProfileT n α

Equations

• Aesop.ProfileT.liftBase x r = liftM (x r)

class Aesop.MonadProfile (m : Type → Type) extends Lean.MonadOptions , MonadStateOf : Type 1

@[always_inline]

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

Equations

• Aesop.isProfilingEnabled = do let __do_lift ← Lean.getOptions pure (Lean.KVMap.getBool __do_lift `profiler)

@[always_inline]

def Aesop.recordRuleSelectionProfile {m : Type → Type} [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} [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} [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.