structure Aesop.ForwardInstantiationStats : Type

• matches : Nat
• hyps : Nat

@[instance_reducible]

instance Aesop.instInhabitedForwardInstantiationStats : Inhabited ForwardInstantiationStats

Equations

• Aesop.instInhabitedForwardInstantiationStats = { default := Aesop.instInhabitedForwardInstantiationStats.default }

@[instance_reducible]

instance Aesop.instToJsonForwardInstantiationStats : Lean.ToJson ForwardInstantiationStats

Equations

• Aesop.instToJsonForwardInstantiationStats = { toJson := Aesop.instToJsonForwardInstantiationStats.toJson }

def Aesop.instToJsonForwardInstantiationStats.toJson : ForwardInstantiationStats → Lean.Json

Equations

• Aesop.instToJsonForwardInstantiationStats.toJson x✝ = Lean.Json.mkObj [[("matches", Lean.toJson x✝.matches)], [("hyps", Lean.toJson x✝.hyps)]].flatten

structure Aesop.ForwardClusterStateStats : Type

• slots : Nat
• instantiationStats : Array ForwardInstantiationStats

@[instance_reducible]

instance Aesop.instInhabitedForwardClusterStateStats : Inhabited ForwardClusterStateStats

Equations

• Aesop.instInhabitedForwardClusterStateStats = { default := Aesop.instInhabitedForwardClusterStateStats.default }

@[instance_reducible]

instance Aesop.instToJsonForwardClusterStateStats : Lean.ToJson ForwardClusterStateStats

Equations

• Aesop.instToJsonForwardClusterStateStats = { toJson := Aesop.instToJsonForwardClusterStateStats.toJson }

def Aesop.instToJsonForwardClusterStateStats.toJson : ForwardClusterStateStats → Lean.Json

Equations

• Aesop.instToJsonForwardClusterStateStats.toJson x✝ = Lean.Json.mkObj [[("slots", Lean.toJson x✝.slots)], [("instantiationStats", Lean.toJson x✝.instantiationStats)]].flatten

structure Aesop.ForwardRuleStateStats : Type

• ruleName : RuleName
• clusterStateStats : Array ForwardClusterStateStats

@[instance_reducible]

instance Aesop.instInhabitedForwardRuleStateStats : Inhabited ForwardRuleStateStats

Equations

• Aesop.instInhabitedForwardRuleStateStats = { default := Aesop.instInhabitedForwardRuleStateStats.default }

def Aesop.instToJsonForwardRuleStateStats.toJson : ForwardRuleStateStats → Lean.Json

Equations

• Aesop.instToJsonForwardRuleStateStats.toJson x✝ = Lean.Json.mkObj [[("ruleName", Lean.toJson x✝.ruleName)], [("clusterStateStats", Lean.toJson x✝.clusterStateStats)]].flatten

@[instance_reducible]

instance Aesop.instToJsonForwardRuleStateStats : Lean.ToJson ForwardRuleStateStats

Equations

• Aesop.instToJsonForwardRuleStateStats = { toJson := Aesop.instToJsonForwardRuleStateStats.toJson }

structure Aesop.ForwardStateStats : Type

• ruleStateStats : Array ForwardRuleStateStats

@[instance_reducible]

instance Aesop.instInhabitedForwardStateStats : Inhabited ForwardStateStats

Equations

• Aesop.instInhabitedForwardStateStats = { default := Aesop.instInhabitedForwardStateStats.default }

def Aesop.instToJsonForwardStateStats.toJson : ForwardStateStats → Lean.Json

Equations

• Aesop.instToJsonForwardStateStats.toJson x✝ = Lean.Json.mkObj [[("ruleStateStats", Lean.toJson x✝.ruleStateStats)]].flatten

@[instance_reducible]

instance Aesop.instToJsonForwardStateStats : Lean.ToJson ForwardStateStats

Equations

• Aesop.instToJsonForwardStateStats = { toJson := Aesop.instToJsonForwardStateStats.toJson }

inductive Aesop.GoalKind : Type

• preNorm : GoalKind
• postNorm : GoalKind

@[instance_reducible]

instance Aesop.instInhabitedGoalKind : Inhabited GoalKind

Equations

• Aesop.instInhabitedGoalKind = { default := Aesop.instInhabitedGoalKind.default }

def Aesop.instToJsonGoalKind.toJson : GoalKind → Lean.Json

Equations

• Aesop.instToJsonGoalKind.toJson Aesop.GoalKind.preNorm = Lean.toJson "preNorm"
• Aesop.instToJsonGoalKind.toJson Aesop.GoalKind.postNorm = Lean.toJson "postNorm"

@[instance_reducible]

instance Aesop.instToJsonGoalKind : Lean.ToJson GoalKind

Equations

• Aesop.instToJsonGoalKind = { toJson := Aesop.instToJsonGoalKind.toJson }

structure Aesop.GoalStats : Type

• goalId : Nat
• goalKind : GoalKind
• lctxSize : Nat

  Number of fvars in the local context, excluding implementation detail fvars.

• depth : Nat

  This goal's depth in the search tree.

• forwardStateStats : ForwardStateStats

@[instance_reducible]

instance Aesop.instInhabitedGoalStats : Inhabited GoalStats

Equations

• Aesop.instInhabitedGoalStats = { default := Aesop.instInhabitedGoalStats.default }

def Aesop.instToJsonGoalStats.toJson : GoalStats → Lean.Json

Equations

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

@[instance_reducible]

instance Aesop.instToJsonGoalStats : Lean.ToJson GoalStats

Equations

• Aesop.instToJsonGoalStats = { toJson := Aesop.instToJsonGoalStats.toJson }

structure Aesop.RuleStats : Type

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

@[instance_reducible]

instance Aesop.instInhabitedRuleStats : Inhabited RuleStats

Equations

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

def Aesop.instToJsonRuleStats.toJson : RuleStats → Lean.Json

Equations

• Aesop.instToJsonRuleStats.toJson x✝ = Lean.Json.mkObj [[("rule", Lean.toJson x✝.rule)], [("elapsed", Lean.toJson x✝.elapsed)], [("successful", Lean.toJson x✝.successful)]].flatten

@[instance_reducible]

instance Aesop.instToJsonRuleStats : Lean.ToJson RuleStats

Equations

• Aesop.instToJsonRuleStats = { toJson := Aesop.instToJsonRuleStats.toJson }

@[instance_reducible]

instance Aesop.RuleStats.instToString : ToString RuleStats

Equations

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

inductive Aesop.ScriptGenerated.Method : Type

• static : Method
• dynamic : Method

@[instance_reducible]

instance Aesop.ScriptGenerated.instInhabitedMethod : Inhabited Method

Equations

• Aesop.ScriptGenerated.instInhabitedMethod = { default := Aesop.ScriptGenerated.instInhabitedMethod.default }

@[instance_reducible]

instance Aesop.ScriptGenerated.instToJsonMethod : Lean.ToJson Method

Equations

• Aesop.ScriptGenerated.instToJsonMethod = { toJson := Aesop.ScriptGenerated.instToJsonMethod.toJson }

def Aesop.ScriptGenerated.instToJsonMethod.toJson : Method → Lean.Json

Equations

• Aesop.ScriptGenerated.instToJsonMethod.toJson Aesop.ScriptGenerated.Method.static = Lean.toJson "static"
• Aesop.ScriptGenerated.instToJsonMethod.toJson Aesop.ScriptGenerated.Method.dynamic = Lean.toJson "dynamic"

@[instance_reducible]

instance Aesop.instToStringMethod : ToString ScriptGenerated.Method

Equations

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

structure Aesop.ScriptGenerated : Type

• method : Method
• perfect : Bool
• hasMVar : Bool

@[instance_reducible]

instance Aesop.instInhabitedScriptGenerated : Inhabited ScriptGenerated

Equations

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

@[instance_reducible]

instance Aesop.instToJsonScriptGenerated : Lean.ToJson ScriptGenerated

Equations

• Aesop.instToJsonScriptGenerated = { toJson := Aesop.instToJsonScriptGenerated.toJson }

def Aesop.instToJsonScriptGenerated.toJson : ScriptGenerated → Lean.Json

Equations

• Aesop.instToJsonScriptGenerated.toJson x✝ = Lean.Json.mkObj [[("method", Lean.toJson x✝.method)], [("perfect", Lean.toJson x✝.perfect)], [("hasMVar", Lean.toJson x✝.hasMVar)]].flatten

def Aesop.ScriptGenerated.toString (g : ScriptGenerated) : String

Equations

• g.toString = toString "with " ++ toString (if g.perfect = true then "perfect" else "imperfect") ++ toString " " ++ toString g.method ++ toString " structuring"

structure Aesop.Stats : Type

• total : Nanos
• configParsing : Nanos
• ruleSetConstruction : Nanos
• search : Nanos
• ruleSelection : Nanos
• script : Nanos
• forwardState : Nanos
• scriptGenerated : Option ScriptGenerated
• ruleStats : Array RuleStats
• goalStats : Array GoalStats

@[instance_reducible]

instance Aesop.instInhabitedStats : Inhabited Stats

Equations

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

def Aesop.Stats.empty : Stats

Equations

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

@[instance_reducible]

instance Aesop.Stats.instEmptyCollection : EmptyCollection 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 : 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

Equations

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

@[instance_reducible]

instance Aesop.RuleStatsTotals.instEmptyCollection : EmptyCollection RuleStatsTotals

Equations

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

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

Equations

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

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.

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

Equations

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

def Aesop.Stats.trace (p : Stats) (opt : 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 Options
• getOptionsUnrestricted : m Options
• modifyGetStats {α : Type} : (Stats → α × Stats) → m α
• getStats : m Stats
• modifyStats : (Stats → Stats) → m Unit

@[instance_reducible]

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.

@[instance_reducible]

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.

@[instance_reducible]

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.

@[always_inline]

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

Equations

• Aesop.enableStatsCollection = (fun (opts : Lean.Options) => Lean.Option.get opts Aesop.aesop.collectStats) <$> Lean.getOptions

@[always_inline]

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

Equations

• Aesop.enableStatsTracing = Aesop.TraceOption.stats.isEnabled

@[always_inline]

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

Equations

• Aesop.enableStatsFile = do let __do_lift ← Lean.getOptions pure (Lean.Option.get __do_lift Aesop.aesop.stats.file != "")

@[always_inline]

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

Equations

• Aesop.enableStats = (Aesop.enableStatsCollection <||> Aesop.enableStatsTracing <||> Aesop.enableStatsFile)

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

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

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

@[always_inline]

def Aesop.profilingForwardState {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.

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

Equations

• Aesop.modifyStatsIfEnabled f = do let __do_lift ← Aesop.enableStats if __do_lift = true then Aesop.modifyStats f else pure ()

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.