- rule : Aesop.DisplayRuleName
- elapsed : Aesop.Nanos
- successful : Bool
Instances For
Equations
- Aesop.instInhabitedRuleStats = { default := { rule := default, elapsed := default, successful := default } }
Equations
- One or more equations did not get rendered due to their size.
- none: Aesop.ScriptGenerated
- staticallyStructured: Bool → Bool → Aesop.ScriptGenerated
- dynamicallyStructured: Bool → Bool → Aesop.ScriptGenerated
Instances For
Equations
- Aesop.instInhabitedScriptGenerated = { default := Aesop.ScriptGenerated.none }
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
Equations
- Aesop.ScriptGenerated.toString.go b = if b = true then "perfect" else "imperfect"
Instances For
Equations
- Aesop.ScriptGenerated.none.isNontrivial = false
- (Aesop.ScriptGenerated.staticallyStructured perfect hasMVar).isNontrivial = hasMVar
- (Aesop.ScriptGenerated.dynamicallyStructured perfect hasMVar).isNontrivial = hasMVar
Instances For
- 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
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Aesop.Stats.empty = { total := 0, configParsing := 0, ruleSetConstruction := 0, search := 0, ruleSelection := 0, script := 0, scriptGenerated := Aesop.ScriptGenerated.none, ruleStats := #[] }
Instances For
Equations
- Aesop.Stats.instEmptyCollection = { emptyCollection := Aesop.Stats.empty }
- 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.
Instances For
Equations
- Aesop.RuleStatsTotals.empty = { numSuccessful := 0, numFailed := 0, elapsedSuccessful := 0, elapsedFailed := 0 }
Instances For
Equations
- Aesop.RuleStatsTotals.instEmptyCollection = { emptyCollection := Aesop.RuleStatsTotals.empty }
def
Aesop.RuleStatsTotals.compareByTotalElapsed
(x : Aesop.RuleStatsTotals)
(y : Aesop.RuleStatsTotals)
:
Equations
- Aesop.RuleStatsTotals.compareByTotalElapsed = compareOn fun (totals : Aesop.RuleStatsTotals) => totals.elapsedSuccessful + totals.elapsedFailed
Instances For
def
Aesop.Stats.ruleStatsTotals
(p : Aesop.Stats)
(init : optParam (Std.HashMap Aesop.DisplayRuleName Aesop.RuleStatsTotals) ∅)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
Equations
Instances For
- monadLift : {α : Type} → ST IO.RealWorld α → m α
- getOptions : m Lean.Options
- readStatsRef : m Aesop.StatsRef
Instances
@[always_inline]
Equations
- Aesop.isStatsCollectionEnabled = (fun (opts : Lean.Options) => Lean.Option.get opts Aesop.collectStatsOption) <$> Lean.getOptions
Instances For
@[always_inline]
Equations
- Aesop.isStatsTracingEnabled = Aesop.TraceOption.stats.isEnabled
Instances For
@[always_inline]
def
Aesop.isStatsCollectionOrTracingEnabled
{m : Type → Type}
[Monad m]
[Lean.MonadOptions m]
:
m Bool
Equations
Instances For
@[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.
Instances For
@[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.
Instances For
@[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.
Instances For
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.
Instances For
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.