source
opaque Aesop.collectStatsOption :
Lean.Option Bool
source
structure Aesop.RuleStats :
Type

- rule : DisplayRuleName
- elapsed : Nanos
- successful : Bool

Instances For

source
instance Aesop.instInhabitedRuleStats :
Inhabited RuleStats
Equations

- Aesop.instInhabitedRuleStats = { default := Aesop.instInhabitedRuleStats.default }

source
def Aesop.instInhabitedRuleStats.default :
RuleStats
Equations

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

Instances For

source
instance Aesop.RuleStats.instToString :
ToString RuleStats
Equations

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

source
inductive Aesop.ScriptGenerated :
Type

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

Instances For

source
instance Aesop.instInhabitedScriptGenerated :
Inhabited ScriptGenerated
Equations

- Aesop.instInhabitedScriptGenerated = { default := Aesop.instInhabitedScriptGenerated.default }

source
def Aesop.instInhabitedScriptGenerated.default :
ScriptGenerated
Equations

- Aesop.instInhabitedScriptGenerated.default = Aesop.ScriptGenerated.none

Instances For

source
def Aesop.ScriptGenerated.toString :
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"

Instances For

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

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

Instances For

source
structure Aesop.Stats :
Type

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

Instances For

source
def Aesop.instInhabitedStats.default :
Stats
Equations

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

Instances For

source
instance Aesop.instInhabitedStats :
Inhabited Stats
Equations

- Aesop.instInhabitedStats = { default := Aesop.instInhabitedStats.default }

source
def Aesop.Stats.empty :
Stats
Equations

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

Instances For

source
instance Aesop.Stats.instEmptyCollection :
EmptyCollection Stats
Equations

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

source
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.

Instances For

source
def Aesop.RuleStatsTotals.empty :
RuleStatsTotals
Equations

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

Instances For

source
instance Aesop.RuleStatsTotals.instEmptyCollection :
EmptyCollection RuleStatsTotals
Equations

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

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
@[reducible, inline]
abbrev Aesop.StatsRef :
Type
Equations

- Aesop.StatsRef = IO.Ref Aesop.Stats

Instances For

source
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

Instances

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

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

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

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

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

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

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

Instances For

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

- Aesop.isStatsTracingEnabled = Aesop.TraceOption.stats.isEnabled

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

- Aesop.modifyCurrentStats f = do let __do_lift ← Aesop.isStatsCollectionEnabled if __do_lift = true then Aesop.modifyStats f else pure PUnit.unit

Instances For

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

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

Instances For