def Aesop.sortedPercentileD {α : Type u_1} (p : Percent) (dflt : α) (xs : Array α) : α

Assumes that xs is ascending. We use a simple nearest-rank definition of percentiles.

Equations

• Aesop.sortedPercentileD p dflt xs = if (xs.size == 0) = true then dflt else let rank := (xs.size.toFloat * p.toFloat).ceil.toUInt64.toNat.min (xs.size - 1); xs[rank]?.getD dflt

def Aesop.sortedMedianD {α : Type u_1} (dflt : α) (xs : Array α) : α

Equations

• Aesop.sortedMedianD dflt xs = Aesop.sortedPercentileD { toFloat := 0.5 } dflt xs

@[reducible, inline]

abbrev Aesop.StatsReport : Type

Equations

• Aesop.StatsReport = (Aesop.StatsArray → Std.Format)

def Aesop.StatsReport.instToStringNanos : ToString Nanos

Equations

• Aesop.StatsReport.instToStringNanos = { toString := Aesop.Nanos.printAsMillis }

def Aesop.StatsReport.default : StatsReport

Equations

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

def Aesop.StatsReport.default.fmtTime (n : Nanos) (samples : Nat) : Std.Format

Equations

• Aesop.StatsReport.default.fmtTime n samples = Std.format "" ++ Std.format n ++ Std.format " [" ++ Std.format (if (samples == 0) = true then 0 else n / samples) ++ Std.format "]"

def Aesop.StatsReport.default.fmtRuleStats (stats : Array (DisplayRuleName × RuleStatsTotals)) : Std.Format

Equations

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

def Aesop.StatsReport.scriptsCore (nSlowest : Nat := 30) (nontrivialOnly : Bool := false) : StatsReport

Equations

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

def Aesop.StatsReport.scriptsCore.fmtScriptGenerated : ScriptGenerated → Std.Format

Equations

• Aesop.StatsReport.scriptsCore.fmtScriptGenerated Aesop.ScriptGenerated.none = Std.Format.text "<none>"
• Aesop.StatsReport.scriptsCore.fmtScriptGenerated (Aesop.ScriptGenerated.staticallyStructured perfect hasMVar) = Std.format "static (perfect: " ++ Std.format perfect ++ Std.format ")"
• Aesop.StatsReport.scriptsCore.fmtScriptGenerated (Aesop.ScriptGenerated.dynamicallyStructured perfect hasMVar) = Std.format "dynamic (perfect: " ++ Std.format perfect ++ Std.format ")"

def Aesop.StatsReport.scriptsCore.fmtTimes (ns : Array Nanos) : Std.Format

Equations

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

def Aesop.StatsReport.scripts : StatsReport

Equations

• Aesop.StatsReport.scripts = Aesop.StatsReport.scriptsCore

def Aesop.StatsReport.scriptsNontrivial : StatsReport

Equations

• Aesop.StatsReport.scriptsNontrivial = Aesop.StatsReport.scriptsCore 30 true