write_stmt_use in axiom_use.rs hates uncompressed proofs. #160
Description
This is two problems: the loop statement runs out-of-bounds and always starts with i = 1 .
The canonical test is set.mm/miu.mm which has both zero-length wffs and a single uncompressed proof at the end of the file where out-of-bounds errors hit the EOF.
If you had code like:
impl StatementRef<'_> {
/// Iterates over explicit label content of proof.
/// Implicit references to floating and essential hypotheses are ignored.
/// Uncompressed proofs will often reference the same label multiple times.
pub fn for_proof_statement_labels(&self, mut per_label: impl FnMut(&[u8])) {
let len = self.proof_len();
if len <= 0 {
return;
}
let token = self.proof_slice_at(0);
if token == b"(" {
// Compressed proof has label-containing preamble between parentheses
for index in 1..len {
let token = self.proof_slice_at(index);
if token == b")" {
break;
}
per_label(token);
}
return;
}
// Uncompressed proof is nothing but statement-labels
per_label(token);
for index in 1..len {
per_label(self.proof_slice_at(index))
}
}
}
Then you could replace this code which assumes compressed proofs:
let mut i = 1;
loop {
let tk = sref.proof_slice_at(i);
i += 1;
if tk == b")" {
break;
}
if let Some(usage2) = stmt_use_map.get(tk) {
usage |= usage2
}
}
with:
sref.for_proof_statement_labels(|tk| {
if let Some(usage2) = stmt_use_map.get(tk) {
usage |= usage2
}
});