diff --git a/Aesop/Script/Main.lean b/Aesop/Script/Main.lean index 13868ad..12ae8ec 100644 --- a/Aesop/Script/Main.lean +++ b/Aesop/Script/Main.lean @@ -35,12 +35,16 @@ where structureStatic : MetaM (Option (SScript × ScriptGenerated)) := do let tacticState ← preState.runMetaM' $ TacticState.mkInitial goal let (sscript, perfect) ← uscript.toSScriptStatic tacticState - pure $ some (sscript, .staticallyStructured perfect) + let gen := + .staticallyStructured (perfect := perfect) (hasMVar := proofHasMVar) + pure $ some (sscript, gen) structureDynamic : MetaM (Option (SScript × ScriptGenerated)) := do let some (script, perfect) ← uscript.toSScriptDynamic preState goal | return none - return some (script, .dynamicallyStructured perfect) + let gen := + .dynamicallyStructured (perfect := perfect) (hasMVar := proofHasMVar) + return some (script, gen) end Script diff --git a/Aesop/Stats/Basic.lean b/Aesop/Stats/Basic.lean index e9c7507..7800aed 100644 --- a/Aesop/Stats/Basic.lean +++ b/Aesop/Stats/Basic.lean @@ -38,17 +38,26 @@ end RuleStats inductive ScriptGenerated | none - | staticallyStructured (perfect : Bool) - | dynamicallyStructured (perfect : Bool) + | staticallyStructured (perfect : Bool) (hasMVar : Bool) + | dynamicallyStructured (perfect : Bool) (hasMVar : Bool) deriving Inhabited -def ScriptGenerated.toString : ScriptGenerated → String +namespace ScriptGenerated + +protected def toString : ScriptGenerated → String | none => "no" - | staticallyStructured perfect => s!"with {go perfect} static structuring" - | dynamicallyStructured perfect => s!"with {go perfect} dynamic structuring" + | staticallyStructured perfect _ => s!"with {go perfect} static structuring" + | dynamicallyStructured perfect _ => s!"with {go perfect} dynamic structuring" where go b := if b then "perfect" else "imperfect" +def isNontrivial : ScriptGenerated → Bool + | none => false + | staticallyStructured (hasMVar := hasMVar) .. + | dynamicallyStructured (hasMVar := hasMVar) .. => hasMVar + +end ScriptGenerated + structure Stats where total : Nanos configParsing : Nanos diff --git a/Aesop/Stats/Report.lean b/Aesop/Stats/Report.lean index 7f128b4..c8c2761 100644 --- a/Aesop/Stats/Report.lean +++ b/Aesop/Stats/Report.lean @@ -11,21 +11,17 @@ open Lean namespace Aesop -namespace StatsArray - -def filterPercentile [Ord α] (f : Stats → α) (percentile : Percent) - (stats : StatsArray) : StatsArray := - let stats := stats.qsort λ s₁ s₂ => compare (f s₁.stats) (f s₂.stats) |>.isLT - let n := stats.usize.toUInt64.toFloat * percentile.toFloat |>.toUInt64.toNat - stats.shrink n - -def filterOptPercentile [Ord α] (f : Stats → α) (percentile? : Option Percent) - (stats : StatsArray) : StatsArray := - match percentile? with - | none => stats - | some percentile => stats.filterPercentile f percentile - -end StatsArray +/-- Assumes that `xs` is ascending. We use a simple nearest-rank definition of +percentiles. -/ +def sortedPercentileD (p : Percent) (dflt : α) (xs : Array α) : α := + if xs.size == 0 then + dflt + else + let rank := xs.size.toFloat * p.toFloat |>.ceil.toUInt64.toNat |>.min (xs.size - 1) + xs[rank]?.getD dflt + +def sortedMedianD (dflt : α) (xs : Array α) : α := + sortedPercentileD ⟨0.5⟩ dflt xs abbrev StatsReport := StatsArray → Format @@ -34,9 +30,6 @@ namespace StatsReport local instance : ToString Nanos := ⟨Nanos.printAsMillis⟩ -private def fmtTime (n : Nanos) (samples : Nat) : Format := - f!"{n} [{if samples == 0 then 0 else n / samples}]" - def default : StatsReport := λ statsArray => Id.run do let mut total := 0 let mut configParsing := 0 @@ -56,8 +49,8 @@ def default : StatsReport := λ statsArray => Id.run do ruleStats := stats.ruleStatsTotals (init := ruleStats) let samples := statsArray.size f!"Statistics for {statsArray.size} Aesop calls in current and imported modules\n\ - Displaying totals and [averages] in milliseconds\n\ - Total time: {fmtTime total samples}\n\ + Displaying totals and [averages]\n\ + Total Aesop time: {fmtTime total samples}\n\ Config parsing: {fmtTime configParsing samples}\n\ Rule set construction: {fmtTime ruleSetConstruction samples}\n\ Rule selection: {fmtTime ruleSelection samples}\n\ @@ -65,6 +58,9 @@ def default : StatsReport := λ statsArray => Id.run do Search: {fmtTime search samples}\n\ Rules:{Std.Format.indentD $ fmtRuleStats $ sortRuleStatsTotals $ ruleStats.toArray}" where + fmtTime (n : Nanos) (samples : Nat) : Format := + f!"{n} [{if samples == 0 then 0 else n / samples}]" + fmtRuleStats (stats : Array (DisplayRuleName × RuleStatsTotals)) : Format := Id.run do let fmtSection (n : Nanos) (samples : Nat) : Format := @@ -78,34 +74,35 @@ where {" "}failed: {fmtSection totals.elapsedFailed totals.numFailed}\n" return fmt -def scriptsCore (percentile? : Option Percent := none) (nSlowest := 30) : +def scriptsCore (nSlowest := 30) (nontrivialOnly := false) : StatsReport := λ statsArray => Id.run do - let statsArray := statsArray.filterOptPercentile (·.script) percentile? - let mut totalTime := 0 - let mut scriptTime := 0 - let mut generated := 0 + let statsArray := + if nontrivialOnly then + statsArray.filter (·.stats.scriptGenerated.isNontrivial) + else + statsArray let mut staticallyStructured := 0 let mut perfectlyStaticallyStructured := 0 let mut dynamicallyStructured := 0 let mut perfectlyDynamicallyStructured := 0 + let mut totalTimes := Array.mkEmpty statsArray.size + let mut scriptTimes := Array.mkEmpty statsArray.size for stats in statsArray do let stats := stats.stats - totalTime := totalTime + stats.total - scriptTime := scriptTime + stats.script + totalTimes := totalTimes.push stats.total match stats.scriptGenerated with | .none => pure () - | .staticallyStructured perfect => - generated := generated + 1 + | .staticallyStructured perfect .. => + scriptTimes := scriptTimes.push stats.script staticallyStructured := staticallyStructured + 1 if perfect then perfectlyStaticallyStructured := perfectlyStaticallyStructured + 1 - | .dynamicallyStructured perfect => - generated := generated + 1 + | .dynamicallyStructured perfect .. => + scriptTimes := scriptTimes.push stats.script dynamicallyStructured := dynamicallyStructured + 1 if perfect then perfectlyDynamicallyStructured := perfectlyDynamicallyStructured + 1 - let samples := statsArray.size let slowest := statsArray.qsort (λ s₁ s₂ => s₁.stats.script > s₂.stats.script) let slowest := slowest[:nSlowest].toArray let nSlowest := min slowest.size nSlowest @@ -116,16 +113,10 @@ def scriptsCore (percentile? : Option Percent := none) (nSlowest := 30) : | none => f!"?:?" f!"{e.fileName}:{pos}: script {e.stats.script}, total {e.stats.total}, type {fmtScriptGenerated e.stats.scriptGenerated}" - let pctStr := - if let some pct := percentile? then - s!" (percentile by script generation time: {pct})" - else - "" - f!"Statistics for {statsArray.size} Aesop calls in current and imported modules{pctStr}\n\ - Durations are given as totals and [averages] in milliseconds\n\ - Total time: {fmtTime totalTime samples}\n\ - Script generation time: {fmtTime scriptTime samples}\n\ - Scripts generated: {generated}\n\ + f!"Statistics for {statsArray.size} Aesop calls{if nontrivialOnly then f!" with nontrivial script generation" else ""} in current and imported modules\n\ + Total Aesop time: {fmtTimes totalTimes}\n\ + Script generation time: {fmtTimes scriptTimes}\n\ + Scripts generated: {scriptTimes.size}\n\ - Statically structured: {staticallyStructured}\n" ++ f!" - perfectly: {perfectlyStaticallyStructured}\n\ - Dynamically structured: {dynamicallyStructured}\n" ++ @@ -136,11 +127,22 @@ def scriptsCore (percentile? : Option Percent := none) (nSlowest := 30) : where fmtScriptGenerated : ScriptGenerated → Format | .none => "" - | .staticallyStructured perfect => f!"static (perfect: {perfect})" - | .dynamicallyStructured perfect => f!"dynamic (perfect: {perfect})" - -def scripts := scriptsCore -def scripts99 := scriptsCore (percentile? := some ⟨0.99⟩) -def scripts95 := scriptsCore (percentile? := some ⟨0.95⟩) + | .staticallyStructured perfect _ => f!"static (perfect: {perfect})" + | .dynamicallyStructured perfect _ => f!"dynamic (perfect: {perfect})" + + fmtTimes (ns : Array Nanos) : Format := + let ns := ns.qsortOrd + let total : Nanos := ns.foldl (init := 0) (· + ·) + let average := if ns.size == 0 then 0 else total / ns.size + let min := ns[0]?.getD 0 + let max := ns[ns.size - 1]?.getD 0 + let median := sortedMedianD 0 ns + let pct80 := sortedPercentileD ⟨0.80⟩ 0 ns + let pct95 := sortedPercentileD ⟨0.95⟩ 0 ns + let pct99 := sortedPercentileD ⟨0.99⟩ 0 ns + f!"{total} (min = {min}, avg = {average}, median = {median}, 80pct = {pct80}, 95pct = {pct95}, 99pct = {pct99}, max = {max})" + +def scripts := scriptsCore +def scriptsNontrivial := scriptsCore (nontrivialOnly := true) end Aesop.StatsReport