Documentation

Aesop.Stats.Basic

structure Aesop.ForwardInstantiationStats :

matches : Nat
hyps : Nat

Instances For

@[instance_reducible]

instance Aesop.instInhabitedForwardInstantiationStats :

Inhabited ForwardInstantiationStats

@[instance_reducible]

instance Aesop.instToJsonForwardInstantiationStats :

Lean.ToJson ForwardInstantiationStats

def Aesop.instToJsonForwardInstantiationStats.toJson :

ForwardInstantiationStats → Lean.Json

Instances For

structure Aesop.ForwardClusterStateStats :

slots : Nat
instantiationStats : Array ForwardInstantiationStats

Instances For

@[instance_reducible]

instance Aesop.instInhabitedForwardClusterStateStats :

Inhabited ForwardClusterStateStats

@[instance_reducible]

instance Aesop.instToJsonForwardClusterStateStats :

Lean.ToJson ForwardClusterStateStats

def Aesop.instToJsonForwardClusterStateStats.toJson :

ForwardClusterStateStats → Lean.Json

Instances For

structure Aesop.ForwardRuleStateStats :

ruleName : RuleName
clusterStateStats : Array ForwardClusterStateStats

Instances For

@[instance_reducible]

instance Aesop.instInhabitedForwardRuleStateStats :

Inhabited ForwardRuleStateStats

def Aesop.instToJsonForwardRuleStateStats.toJson :

ForwardRuleStateStats → Lean.Json

Instances For

@[instance_reducible]

instance Aesop.instToJsonForwardRuleStateStats :

Lean.ToJson ForwardRuleStateStats

structure Aesop.ForwardStateStats :

ruleStateStats : Array ForwardRuleStateStats

Instances For

@[instance_reducible]

instance Aesop.instInhabitedForwardStateStats :

Inhabited ForwardStateStats

def Aesop.instToJsonForwardStateStats.toJson :

ForwardStateStats → Lean.Json

Instances For

@[instance_reducible]

instance Aesop.instToJsonForwardStateStats :

Lean.ToJson ForwardStateStats

inductive Aesop.GoalKind :

preNorm : GoalKind
postNorm : GoalKind

Instances For

@[instance_reducible]

instance Aesop.instInhabitedGoalKind :

Inhabited GoalKind

def Aesop.instToJsonGoalKind.toJson :

GoalKind → Lean.Json

Instances For

@[instance_reducible]

instance Aesop.instToJsonGoalKind :

Lean.ToJson GoalKind

structure Aesop.GoalStats :

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

Instances For

@[instance_reducible]

instance Aesop.instInhabitedGoalStats :

Inhabited GoalStats

def Aesop.instToJsonGoalStats.toJson :

GoalStats → Lean.Json

Instances For

@[instance_reducible]

instance Aesop.instToJsonGoalStats :

Lean.ToJson GoalStats

structure Aesop.RuleStats :

rule : DisplayRuleName
elapsed : Nanos
successful : Bool

Instances For

@[instance_reducible]

instance Aesop.instInhabitedRuleStats :

Inhabited RuleStats

def Aesop.instToJsonRuleStats.toJson :

RuleStats → Lean.Json

Instances For

@[instance_reducible]

instance Aesop.instToJsonRuleStats :

Lean.ToJson RuleStats

@[instance_reducible]

instance Aesop.RuleStats.instToString :

ToString RuleStats

inductive Aesop.ScriptGenerated.Method :

static : Method
dynamic : Method

Instances For

@[instance_reducible]

instance Aesop.ScriptGenerated.instInhabitedMethod :

Inhabited Method

@[instance_reducible]

instance Aesop.ScriptGenerated.instToJsonMethod :

Lean.ToJson Method

def Aesop.ScriptGenerated.instToJsonMethod.toJson :

Method → Lean.Json

Instances For

@[instance_reducible]

instance Aesop.instToStringMethod :

ToString ScriptGenerated.Method

structure Aesop.ScriptGenerated :

method : Method
perfect : Bool
hasMVar : Bool

Instances For

@[instance_reducible]

instance Aesop.instInhabitedScriptGenerated :

Inhabited ScriptGenerated

@[instance_reducible]

instance Aesop.instToJsonScriptGenerated :

Lean.ToJson ScriptGenerated

def Aesop.instToJsonScriptGenerated.toJson :

ScriptGenerated → Lean.Json

Instances For

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

Instances For

structure Aesop.Stats :

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

Instances For

@[instance_reducible]

instance Aesop.instInhabitedStats :

Inhabited Stats

def Aesop.Stats.empty :

Instances For

@[instance_reducible]

instance Aesop.Stats.instEmptyCollection :

EmptyCollection Stats

structure Aesop.RuleStatsTotals :

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

def Aesop.RuleStatsTotals.empty :

RuleStatsTotals

Instances For

@[instance_reducible]

instance Aesop.RuleStatsTotals.instEmptyCollection :

EmptyCollection RuleStatsTotals

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

Instances For

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

Std.HashMap DisplayRuleName RuleStatsTotals

Instances For

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

Array (DisplayRuleName × RuleStatsTotals)

Instances For

def Aesop.Stats.trace (p : Stats) (opt : TraceOption) :

Lean.CoreM Unit

Instances For

@[reducible, inline]

abbrev Aesop.StatsRef :

Instances For

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

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

Instances

@[instance_reducible]

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

MonadStats (StateRefT' ω σ m)

@[instance_reducible]

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

MonadStats (ReaderT α m)

@[instance_reducible]

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

@[always_inline]

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

Instances For

@[always_inline]

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

Instances For

@[always_inline]

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

Instances For

@[always_inline]

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

Instances For

@[always_inline]

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

m α

Instances For

@[always_inline]

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

m α → m α

Instances For

@[always_inline]

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

m α → m α

Instances For

@[always_inline]

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

m α → m α

Instances For

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

Instances For

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

Instances For