opaque Aesop.collectStatsOption : Lean.Option Bool

structure Aesop.RuleStats : Type

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

instance Aesop.instInhabitedRuleStats : Inhabited RuleStats

instance Aesop.RuleStats.instToString : ToString RuleStats

inductive Aesop.ScriptGenerated : Type

• none : ScriptGenerated
• staticallyStructured (perfect hasMVar : Bool) : ScriptGenerated
• dynamicallyStructured (perfect hasMVar : Bool) : ScriptGenerated

instance Aesop.instInhabitedScriptGenerated : Inhabited ScriptGenerated

def Aesop.ScriptGenerated.toString : ScriptGenerated → String

def Aesop.ScriptGenerated.toString.go (b : Bool) : String

def Aesop.ScriptGenerated.isNontrivial : ScriptGenerated → Bool

structure Aesop.Stats : Type

• total : Nanos
• configParsing : Nanos
• ruleSetConstruction : Nanos
• search : Nanos
• ruleSelection : Nanos
• script : Nanos
• scriptGenerated : ScriptGenerated
• ruleStats : Array RuleStats

instance Aesop.instInhabitedStats : Inhabited Stats

def Aesop.Stats.empty : Stats

instance Aesop.Stats.instEmptyCollection : EmptyCollection Stats

structure Aesop.RuleStatsTotals : Type

• numSuccessful : Nat

  Number of successful applications of a rule.

• numFailed : Nat

  Number of failed applications of a rule.

• elapsedSuccessful : Nanos

  Total elapsed time of successful applications of a rule.

• elapsedFailed : Nanos

  Total elapsed time of failed applications of a rule.

def Aesop.RuleStatsTotals.empty : RuleStatsTotals

instance Aesop.RuleStatsTotals.instEmptyCollection : EmptyCollection RuleStatsTotals

def Aesop.RuleStatsTotals.compareByTotalElapsed (x y : RuleStatsTotals) : Ordering

def Aesop.Stats.ruleStatsTotals (p : Stats) (init : Std.HashMap DisplayRuleName RuleStatsTotals := ∅) : Std.HashMap DisplayRuleName RuleStatsTotals

def Aesop.sortRuleStatsTotals (ts : Array (DisplayRuleName × RuleStatsTotals)) : Array (DisplayRuleName × RuleStatsTotals)

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

@[reducible, inline]

abbrev Aesop.StatsRef : Type

class Aesop.MonadStats (m : Type → Type) extends Lean.MonadOptions m : Type 1

• getOptions : m Options
• modifyGetStats {α : Type} : (Stats → α × Stats) → m α
• getStats : m Stats
• modifyStats : (Stats → Stats) → m Unit

instance Aesop.instMonadStatsStateRefT' {m : Type → Type} {ω σ : Type} [MonadStats m] : MonadStats (StateRefT' ω σ m)

instance Aesop.instMonadStatsReaderT {m : Type → Type} {α : Type} [MonadStats m] : MonadStats (ReaderT α m)

instance Aesop.instMonadStatsOfMonadOptionsOfMonadStateOfStats {m : Type → Type} [Lean.MonadOptions m] [MonadStateOf Stats m] : MonadStats m

@[always_inline]

def Aesop.isStatsCollectionEnabled {m : Type → Type} [Monad m] [Lean.MonadOptions m] : m Bool

@[always_inline]

def Aesop.isStatsTracingEnabled {m : Type → Type} [Monad m] [Lean.MonadOptions m] : m Bool

@[always_inline]

def Aesop.isStatsCollectionOrTracingEnabled {m : Type → Type} [Monad m] [Lean.MonadOptions m] : m Bool

@[always_inline]

def Aesop.profiling {m : Type → Type} [Monad m] [MonadStats m] [MonadLiftT BaseIO m] {α : Type} (recordStats : Stats → α → Nanos → Stats) (x : m α) : m α

@[always_inline]

def Aesop.profilingRuleSelection {m : Type → Type} [Monad m] [MonadStats m] [MonadLiftT BaseIO m] {α : Type} : m α → m α

@[always_inline]

def Aesop.profilingRule {m : Type → Type} [Monad m] [MonadStats m] [MonadLiftT BaseIO m] {α : Type} (rule : DisplayRuleName) (wasSuccessful : α → Bool) : m α → m α

def Aesop.modifyCurrentStats {m : Type → Type} [Monad m] [MonadStats m] (f : Stats → Stats) : m Unit

def Aesop.recordScriptGenerated {m : Type → Type} [Monad m] [MonadStats m] (x : ScriptGenerated) : m Unit