opaque Aesop.collectStatsOption : Lean.Option Bool

structure Aesop.RuleStats : Type

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

instance Aesop.instInhabitedRuleStats : Inhabited Aesop.RuleStats

Equations

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

instance Aesop.RuleStats.instToString : ToString Aesop.RuleStats

Equations

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

inductive Aesop.ScriptGenerated : Type

• none: Aesop.ScriptGenerated
• staticallyStructured: Bool → Bool → Aesop.ScriptGenerated
• dynamicallyStructured: Bool → Bool → Aesop.ScriptGenerated

instance Aesop.instInhabitedScriptGenerated : Inhabited Aesop.ScriptGenerated

Equations

• Aesop.instInhabitedScriptGenerated = { default := Aesop.ScriptGenerated.none }

def Aesop.ScriptGenerated.toString : Aesop.ScriptGenerated → String

Equations

• Aesop.ScriptGenerated.none.toString = "no"
• (Aesop.ScriptGenerated.staticallyStructured perfect hasMVar).toString = toString "with " ++ toString (Aesop.ScriptGenerated.toString.go perfect) ++ toString " static structuring"
• (Aesop.ScriptGenerated.dynamicallyStructured perfect hasMVar).toString = toString "with " ++ toString (Aesop.ScriptGenerated.toString.go perfect) ++ toString " dynamic structuring"

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

Equations

• Aesop.ScriptGenerated.toString.go b = if b = true then "perfect" else "imperfect"

def Aesop.ScriptGenerated.isNontrivial : Aesop.ScriptGenerated → Bool

Equations

• Aesop.ScriptGenerated.none.isNontrivial = false
• (Aesop.ScriptGenerated.staticallyStructured perfect hasMVar).isNontrivial = hasMVar
• (Aesop.ScriptGenerated.dynamicallyStructured perfect hasMVar).isNontrivial = hasMVar

structure Aesop.Stats : Type

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

instance Aesop.instInhabitedStats : Inhabited Aesop.Stats

Equations

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

def Aesop.Stats.empty : Aesop.Stats

Equations

• Aesop.Stats.empty = { total := 0, configParsing := 0, ruleSetConstruction := 0, search := 0, ruleSelection := 0, script := 0, scriptGenerated := Aesop.ScriptGenerated.none, ruleStats := #[] }

instance Aesop.Stats.instEmptyCollection : EmptyCollection Aesop.Stats

Equations

• Aesop.Stats.instEmptyCollection = { emptyCollection := Aesop.Stats.empty }

structure Aesop.RuleStatsTotals : Type

• numSuccessful : Nat

  Number of successful applications of a rule.

• numFailed : Nat

  Number of failed applications of a rule.

• elapsedSuccessful : Aesop.Nanos

  Total elapsed time of successful applications of a rule.

• elapsedFailed : Aesop.Nanos

  Total elapsed time of failed applications of a rule.

def Aesop.RuleStatsTotals.empty : Aesop.RuleStatsTotals

Equations

• Aesop.RuleStatsTotals.empty = { numSuccessful := 0, numFailed := 0, elapsedSuccessful := 0, elapsedFailed := 0 }

instance Aesop.RuleStatsTotals.instEmptyCollection : EmptyCollection Aesop.RuleStatsTotals

Equations

• Aesop.RuleStatsTotals.instEmptyCollection = { emptyCollection := Aesop.RuleStatsTotals.empty }

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

Equations

• Aesop.RuleStatsTotals.compareByTotalElapsed = compareOn fun (totals : Aesop.RuleStatsTotals) => totals.elapsedSuccessful + totals.elapsedFailed

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

Equations

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

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev Aesop.StatsRef : Type

Equations

• Aesop.StatsRef = IO.Ref Aesop.Stats

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

• getOptions : m Lean.Options
• instLift : MonadLiftT BaseIO m
• readStatsRef : m Aesop.StatsRef

instance Aesop.instMonadLiftBaseIOOfMonadStats {m : Type → Type} [Aesop.MonadStats m] : MonadLift BaseIO m

Equations

• Aesop.instMonadLiftBaseIOOfMonadStats = { monadLift := fun {α : Type} => monadLift }

@[always_inline]

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

Equations

• Aesop.isStatsCollectionEnabled = (fun (opts : Lean.Options) => Lean.Option.get opts Aesop.collectStatsOption) <$> Lean.getOptions

@[always_inline]

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

Equations

• Aesop.isStatsTracingEnabled = Aesop.TraceOption.stats.isEnabled

@[always_inline]

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

Equations

• Aesop.isStatsCollectionOrTracingEnabled = (Aesop.isStatsCollectionEnabled <||> Aesop.isStatsTracingEnabled)

@[always_inline]

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

Equations

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

@[always_inline]

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

Equations

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

@[always_inline]

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

Equations

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

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

Equations

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

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

Equations

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