#![allow(dead_code)]
use std::collections::BTreeMap;
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Tactic {
Leaf(String),
Sorry,
Seq(Vec<Tactic>),
First(Vec<Tactic>),
Induction {
target: String,
arms: Vec<InductionArm>,
},
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct InductionArm {
pub pattern: String,
pub body: Tactic,
}
impl Tactic {
pub fn raw(lines: Vec<String>) -> Tactic {
Tactic::Seq(lines.into_iter().map(Tactic::Leaf).collect())
}
pub fn raw_dedented(lines: Vec<String>) -> Tactic {
Tactic::raw(relative_dedent(&lines))
}
pub fn render(&self) -> Vec<String> {
self.render_indent(0)
}
pub fn render_body(&self) -> Vec<String> {
let tree = minimize::apply(self);
let strip = tree.leaf_min_indent().unwrap_or(0);
tree.strip_leaf_indent(strip).render_indent(1)
}
fn leaf_min_indent(&self) -> Option<usize> {
match self {
Tactic::Leaf(s) => s
.lines()
.filter(|l| !l.trim().is_empty())
.map(leading_spaces)
.min(),
Tactic::Sorry => None,
Tactic::Seq(ts) | Tactic::First(ts) => {
ts.iter().filter_map(Tactic::leaf_min_indent).min()
}
Tactic::Induction { arms, .. } => {
arms.iter().filter_map(|a| a.body.leaf_min_indent()).min()
}
}
}
fn strip_leaf_indent(self, n: usize) -> Tactic {
match self {
Tactic::Leaf(s) => Tactic::Leaf(
s.lines()
.map(|l| {
let k = leading_spaces(l).min(n);
l[k..].to_string()
})
.collect::<Vec<_>>()
.join("\n"),
),
Tactic::Sorry => Tactic::Sorry,
Tactic::Seq(ts) => {
Tactic::Seq(ts.into_iter().map(|t| t.strip_leaf_indent(n)).collect())
}
Tactic::First(ts) => {
Tactic::First(ts.into_iter().map(|t| t.strip_leaf_indent(n)).collect())
}
Tactic::Induction { target, arms } => Tactic::Induction {
target,
arms: arms
.into_iter()
.map(|a| InductionArm {
pattern: a.pattern,
body: a.body.strip_leaf_indent(n),
})
.collect(),
},
}
}
fn render_indent(&self, indent: usize) -> Vec<String> {
let pad = " ".repeat(indent);
match self {
Tactic::Leaf(s) if s.is_empty() => vec![String::new()],
Tactic::Leaf(s) if !s.contains('\n') => vec![format!("{pad}{s}")],
Tactic::Leaf(s) => s.lines().map(|l| format!("{pad}{l}")).collect(),
Tactic::Sorry => vec![format!("{pad}sorry")],
Tactic::Seq(steps) => steps.iter().flat_map(|t| t.render_indent(indent)).collect(),
Tactic::First(branches) => render_first(branches, indent),
Tactic::Induction { target, arms } => {
let mut out = vec![format!("{pad}induction {target} with")];
for arm in arms {
let body = arm.body.render_indent(indent + 1);
if body.len() == 1 {
out.push(format!(
"{pad}| {} => {}",
arm.pattern,
body[0].trim_start()
));
} else {
out.push(format!("{pad}| {} =>", arm.pattern));
out.extend(body);
}
}
out
}
}
}
pub fn collapse_firsts(self, pick: &mut impl FnMut(&[Tactic]) -> Option<usize>) -> Tactic {
match self {
leaf @ (Tactic::Leaf(_) | Tactic::Sorry) => leaf,
Tactic::Seq(steps) => {
Tactic::Seq(steps.into_iter().map(|t| t.collapse_firsts(pick)).collect())
}
Tactic::First(branches) => match pick(&branches) {
Some(i) if i < branches.len() => {
branches.into_iter().nth(i).unwrap().collapse_firsts(pick)
}
_ => Tactic::First(
branches
.into_iter()
.map(|t| t.collapse_firsts(pick))
.collect(),
),
},
Tactic::Induction { target, arms } => Tactic::Induction {
target,
arms: arms
.into_iter()
.map(|a| InductionArm {
pattern: a.pattern,
body: a.body.collapse_firsts(pick),
})
.collect(),
},
}
}
pub fn first_count(&self) -> usize {
match self {
Tactic::Leaf(_) | Tactic::Sorry => 0,
Tactic::Seq(ts) => ts.iter().map(Tactic::first_count).sum(),
Tactic::First(bs) => 1 + bs.iter().map(Tactic::first_count).sum::<usize>(),
Tactic::Induction { arms, .. } => arms.iter().map(|a| a.body.first_count()).sum(),
}
}
fn instrument_markers(self, next: &mut usize) -> Tactic {
match self {
leaf @ (Tactic::Leaf(_) | Tactic::Sorry) => leaf,
Tactic::Seq(ts) => {
Tactic::Seq(ts.into_iter().map(|t| t.instrument_markers(next)).collect())
}
Tactic::First(branches) => {
let idx = *next;
*next += 1;
Tactic::First(
branches
.into_iter()
.enumerate()
.map(|(b, branch)| {
let inner = branch.instrument_markers(next);
Tactic::Seq(vec![
Tactic::Leaf(format!("trace \"AVERMIN:{idx}:{b}\"")),
inner,
])
})
.collect(),
)
}
Tactic::Induction { target, arms } => Tactic::Induction {
target,
arms: arms
.into_iter()
.map(|a| InductionArm {
pattern: a.pattern,
body: a.body.instrument_markers(next),
})
.collect(),
},
}
}
fn collapse_by_index(self, next: &mut usize, winners: &BTreeMap<usize, usize>) -> Tactic {
match self {
leaf @ (Tactic::Leaf(_) | Tactic::Sorry) => leaf,
Tactic::Seq(ts) => Tactic::Seq(
ts.into_iter()
.map(|t| t.collapse_by_index(next, winners))
.collect(),
),
Tactic::First(branches) => {
let idx = *next;
*next += 1;
let n = branches.len();
let winner = winners.get(&idx).copied().filter(|&w| w < n);
let mut chosen = None;
let mut kept: Vec<Tactic> = Vec::with_capacity(branches.len());
for (b, branch) in branches.into_iter().enumerate() {
let collapsed = branch.collapse_by_index(next, winners);
match winner {
Some(w) if w == b => chosen = Some(collapsed),
Some(_) => {}
None => kept.push(collapsed),
}
}
match chosen {
Some(t) => t,
None => Tactic::First(kept),
}
}
Tactic::Induction { target, arms } => Tactic::Induction {
target,
arms: arms
.into_iter()
.map(|a| InductionArm {
pattern: a.pattern,
body: a.body.collapse_by_index(next, winners),
})
.collect(),
},
}
}
}
fn leading_spaces(l: &str) -> usize {
l.len() - l.trim_start().len()
}
fn relative_dedent(lines: &[String]) -> Vec<String> {
let min = lines
.iter()
.filter(|l| !l.trim().is_empty())
.map(|l| leading_spaces(l))
.min()
.unwrap_or(0);
lines
.iter()
.map(|l| {
if l.trim().is_empty() {
String::new()
} else {
l[min..].to_string()
}
})
.collect()
}
fn render_first(branches: &[Tactic], indent: usize) -> Vec<String> {
let pad = " ".repeat(indent);
let rendered: Vec<Vec<String>> = branches.iter().map(|b| b.render_indent(0)).collect();
let all_single = rendered.iter().all(|b| b.len() == 1);
if all_single {
let parts: Vec<String> = branches
.iter()
.zip(&rendered)
.map(|(b, lines)| match b {
Tactic::Sorry => "sorry".to_string(),
_ => format!("({})", lines[0].trim_start()),
})
.collect();
vec![format!("{pad}first | {}", parts.join(" | "))]
} else {
let mut out = vec![format!("{pad}first")];
for (b, lines) in branches.iter().zip(&rendered) {
match b {
Tactic::Sorry => out.push(format!("{pad}| sorry")),
_ if lines.len() == 1 => out.push(format!("{pad}| ({})", lines[0].trim_start())),
_ => {
out.push(format!("{pad}| ("));
for l in relative_dedent(lines) {
if l.is_empty() {
out.push(String::new());
} else {
out.push(format!("{pad} {l}"));
}
}
out.push(format!("{pad})"));
}
}
}
out
}
}
pub mod minimize {
use super::{BTreeMap, Tactic};
use std::cell::RefCell;
#[derive(Clone)]
enum Mode {
Off,
Instrument,
Collapse(BTreeMap<usize, usize>),
}
thread_local! {
static STATE: RefCell<(Mode, usize)> = const { RefCell::new((Mode::Off, 0)) };
}
pub fn begin_instrument() {
STATE.with(|s| *s.borrow_mut() = (Mode::Instrument, 0));
}
pub fn begin_collapse(winners: BTreeMap<usize, usize>) {
STATE.with(|s| *s.borrow_mut() = (Mode::Collapse(winners), 0));
}
pub fn end() {
STATE.with(|s| *s.borrow_mut() = (Mode::Off, 0));
}
pub(super) fn apply(t: &Tactic) -> Tactic {
STATE.with(|s| {
let mut st = s.borrow_mut();
let mode = st.0.clone();
let mut counter = st.1;
let out = match mode {
Mode::Off => t.clone(),
Mode::Instrument => t.clone().instrument_markers(&mut counter),
Mode::Collapse(winners) => t.clone().collapse_by_index(&mut counter, &winners),
};
st.1 = counter;
out
})
}
pub fn parse_winners(build_output: &str) -> BTreeMap<usize, usize> {
let mut winners: BTreeMap<usize, usize> = BTreeMap::new();
for line in build_output.lines() {
let Some(pos) = line.find("AVERMIN:") else {
continue;
};
let rest = &line[pos + "AVERMIN:".len()..];
let mut it = rest.split(|c: char| !c.is_ascii_digit());
let (Some(i), Some(b)) = (it.next(), it.next()) else {
continue;
};
let (Ok(idx), Ok(branch)) = (i.parse::<usize>(), b.parse::<usize>()) else {
continue;
};
let e = winners.entry(idx).or_insert(branch);
*e = (*e).max(branch);
}
winners
}
}
pub mod speculative {
use std::cell::RefCell;
use std::collections::HashSet;
#[derive(Clone, PartialEq)]
enum Mode {
Off,
Probe,
}
thread_local! {
static STATE: RefCell<(Mode, Option<HashSet<String>>, HashSet<String>)> =
RefCell::new((Mode::Off, None, HashSet::new()));
}
pub fn begin_probe() {
STATE.with(|s| {
let mut st = s.borrow_mut();
st.0 = Mode::Probe;
st.2 = HashSet::new();
});
}
pub fn set_committed(closed: HashSet<String>) {
STATE.with(|s| {
let mut st = s.borrow_mut();
st.0 = Mode::Off;
st.1 = Some(closed);
});
}
pub fn clear() {
STATE.with(|s| *s.borrow_mut() = (Mode::Off, None, HashSet::new()));
}
pub fn admits(id: &str, default: bool) -> bool {
STATE.with(|s| {
let st = s.borrow();
match st.0 {
Mode::Probe => true,
Mode::Off => match st.1.as_ref() {
Some(set) => set.contains(id),
None => default,
},
}
})
}
pub fn probing() -> bool {
STATE.with(|s| s.borrow().0 == Mode::Probe)
}
pub fn record_probed(id: &str) {
STATE.with(|s| {
s.borrow_mut().2.insert(id.to_string());
});
}
pub fn probed_ids() -> HashSet<String> {
STATE.with(|s| s.borrow().2.clone())
}
pub fn parse_failures(build_output: &str) -> HashSet<String> {
const MARKER: &str = "AVERSPEC_SORRY:";
let mut failed = HashSet::new();
for line in build_output.lines() {
let Some(pos) = line.find(MARKER) else {
continue;
};
let rest = &line[pos + MARKER.len()..];
let id: String = rest
.chars()
.take_while(|c| c.is_alphanumeric() || *c == '_' || *c == '.')
.collect();
if !id.is_empty() {
failed.insert(id);
}
}
failed
}
}
#[cfg(test)]
mod tests {
use super::*;
fn leaf(s: &str) -> Tactic {
Tactic::Leaf(s.to_string())
}
#[test]
fn renders_flat_portfolio_inline_with_bare_sorry() {
let t = Tactic::Seq(vec![
leaf("intro a b"),
Tactic::First(vec![
leaf("simp only [String.add_eq_append, String.length_append] <;> omega"),
Tactic::Sorry,
]),
]);
assert_eq!(
t.render(),
vec![
"intro a b".to_string(),
"first | (simp only [String.add_eq_append, String.length_append] <;> omega) | sorry"
.to_string(),
]
);
}
#[test]
fn renders_grind_wrapped_two_level_portfolio() {
let inner = Tactic::First(vec![
leaf("exact AverMap.len_set_ge_one _ _ _"),
Tactic::Sorry,
]);
let t = Tactic::Seq(vec![
leaf("intro m k v"),
Tactic::First(vec![leaf("grind [_root_.after]; done"), inner]),
]);
assert_eq!(
t.render(),
vec![
"intro m k v".to_string(),
"first | (grind [_root_.after]; done) | (first | (exact AverMap.len_set_ge_one _ _ _) | sorry)".to_string(),
]
);
}
#[test]
fn renders_induction_arms() {
let t = Tactic::Seq(vec![
leaf("intro xs"),
Tactic::Induction {
target: "xs".to_string(),
arms: vec![
InductionArm {
pattern: "nil".to_string(),
body: Tactic::First(vec![leaf("simp [f]"), Tactic::Sorry]),
},
InductionArm {
pattern: "cons h t ih".to_string(),
body: leaf("simp_all [f]"),
},
],
},
]);
assert_eq!(
t.render(),
vec![
"intro xs".to_string(),
"induction xs with".to_string(),
"| nil => first | (simp [f]) | sorry".to_string(),
"| cons h t ih => simp_all [f]".to_string(),
]
);
}
#[test]
fn first_count_is_preorder_total() {
let t = Tactic::Seq(vec![
Tactic::First(vec![leaf("a"), Tactic::Sorry]),
Tactic::Induction {
target: "xs".to_string(),
arms: vec![InductionArm {
pattern: "cons h t".to_string(),
body: Tactic::First(vec![leaf("b"), leaf("c")]),
}],
},
]);
assert_eq!(t.first_count(), 2);
}
#[test]
fn render_body_is_byte_identical_for_baked_raw() {
let baked = vec![
" intro xs".to_string(),
" induction xs with".to_string(),
" | nil => simp".to_string(),
" | cons h t ih =>".to_string(),
" simp [ih]".to_string(),
];
let body = Tactic::raw(baked.clone());
assert_eq!(body.render_body(), baked);
}
#[test]
fn render_body_lays_out_grind_wrapped_first_at_two_space() {
let body = Tactic::Seq(vec![
leaf("intro a b"),
Tactic::First(vec![
leaf("grind [f]; done"),
Tactic::raw(vec![
" simp [f]".to_string(),
" omega".to_string(),
" sorry".to_string(),
]),
]),
]);
assert_eq!(
body.render_body(),
vec![
" intro a b".to_string(),
" first".to_string(),
" | (grind [f]; done)".to_string(),
" | (".to_string(),
" simp [f]".to_string(),
" omega".to_string(),
" sorry".to_string(),
" )".to_string(),
]
);
}
#[test]
fn collapse_firsts_picks_the_winning_branch() {
let t = Tactic::Seq(vec![
leaf("intro a b"),
Tactic::First(vec![
leaf("the_winner <;> omega"),
leaf("loser"),
Tactic::Sorry,
]),
]);
let mut pick = |_branches: &[Tactic]| Some(0usize);
let minimized = t.collapse_firsts(&mut pick);
assert_eq!(
minimized.render(),
vec!["intro a b".to_string(), "the_winner <;> omega".to_string()]
);
}
#[test]
fn speculative_parse_failures_reads_fn_law_ids() {
let log = "\
info: F.lean:50:5: AVERSPEC_SORRY:parseArrayElems.renderJsonListElemsRoundtrip
info: F.lean:62:5: AVERSPEC_SORRY:parseObjFields.renderJsonEntriesFieldsRoundtrip
warning: declaration uses 'sorry'
";
let failed = super::speculative::parse_failures(log);
assert!(failed.contains("parseArrayElems.renderJsonListElemsRoundtrip"));
assert!(failed.contains("parseObjFields.renderJsonEntriesFieldsRoundtrip"));
assert_eq!(failed.len(), 2);
assert!(!failed.contains("sumList.sumAllZero"));
}
#[test]
fn speculative_admits_only_committed_in_off_mode() {
use super::speculative;
speculative::clear();
assert!(!speculative::admits("f.law", false));
assert!(speculative::admits("g.two", true));
assert!(!speculative::probing());
speculative::begin_probe();
assert!(speculative::probing());
assert!(speculative::admits("f.law", false));
assert!(speculative::admits("g.two", true));
assert!(speculative::probed_ids().is_empty());
speculative::record_probed("f.law");
speculative::record_probed("g.two");
assert!(speculative::probed_ids().contains("f.law"));
let mut closed = std::collections::HashSet::new();
closed.insert("f.law".to_string());
speculative::set_committed(closed);
assert!(!speculative::probing());
assert!(speculative::admits("f.law", false));
assert!(!speculative::admits("g.two", true));
speculative::clear();
assert!(!speculative::admits("f.law", false));
}
#[test]
fn parse_winners_takes_max_branch_per_index() {
let log = "\
info: F.lean:3:5: AVERMIN:0:0
info: F.lean:4:5: AVERMIN:0:1
info: G.lean:9:5: AVERMIN:1:0
info: F.lean:4:5: AVERMIN:0:1
warning: declaration uses 'sorry'
";
let w = minimize::parse_winners(log);
assert_eq!(w.get(&0), Some(&1));
assert_eq!(w.get(&1), Some(&0));
assert_eq!(w.len(), 2);
}
#[test]
fn instrument_markers_number_firsts_in_preorder() {
let inner = Tactic::First(vec![leaf("a"), Tactic::Sorry]);
let t = Tactic::First(vec![leaf("grind; done"), inner]);
let mut next = 0;
let instrumented = t.instrument_markers(&mut next);
assert_eq!(next, 2); let rendered = instrumented.render().join("\n");
assert!(rendered.contains("AVERMIN:0:0"));
assert!(rendered.contains("AVERMIN:0:1"));
assert!(rendered.contains("AVERMIN:1:0"));
assert!(rendered.contains("AVERMIN:1:1"));
}
#[test]
fn collapse_by_index_keeps_winner_and_stays_index_aligned() {
let inner = Tactic::First(vec![leaf("a"), Tactic::Sorry]);
let t = Tactic::Seq(vec![
leaf("intro x"),
Tactic::First(vec![leaf("grind; done"), inner]),
]);
let winners = BTreeMap::from([(0usize, 1usize), (1usize, 0usize)]);
let mut next = 0;
let collapsed = t.collapse_by_index(&mut next, &winners);
assert_eq!(next, 2); assert_eq!(
collapsed.render(),
vec!["intro x".to_string(), "a".to_string()]
);
}
#[test]
fn collapse_to_the_sorry_floor_keeps_the_sorry() {
let portfolio = || {
Tactic::Seq(vec![
leaf("intro a b"),
Tactic::First(vec![leaf("grind; done"), leaf("simp_all"), Tactic::Sorry]),
])
};
minimize::begin_collapse(BTreeMap::from([(0usize, 2usize)]));
let collapsed = portfolio().render_body();
minimize::end();
assert_eq!(
collapsed,
vec![" intro a b".to_string(), " sorry".to_string()]
);
}
#[test]
fn render_body_round_trips_instrument_then_collapse() {
let grind_wrap = || {
Tactic::Seq(vec![
leaf("intro a b"),
Tactic::First(vec![
leaf("grind [f]; done"),
Tactic::raw_dedented(vec![" simp [f]".to_string(), " sorry".to_string()]),
]),
])
};
minimize::begin_instrument();
let instrumented = grind_wrap().render_body().join("\n");
minimize::end();
assert!(instrumented.contains("AVERMIN:0:0"));
assert!(instrumented.contains("AVERMIN:0:1"));
minimize::begin_collapse(BTreeMap::from([(0usize, 1usize)]));
let collapsed = grind_wrap().render_body();
minimize::end();
assert_eq!(
collapsed,
vec![
" intro a b".to_string(),
" simp [f]".to_string(),
" sorry".to_string(),
]
);
assert_eq!(
grind_wrap().render_body(),
vec![
" intro a b".to_string(),
" first".to_string(),
" | (grind [f]; done)".to_string(),
" | (".to_string(),
" simp [f]".to_string(),
" sorry".to_string(),
" )".to_string(),
]
);
}
}