Fix recall pretty-print in proof lists (Refs #931)

[jsiek]

Refs #931

Summary

Picking up the next sub-bug from the remaining lib/ parse-fail set. A fresh local sweep of lib/*.pf round-trip on today's main showed 7 parse-fails, of which 5 share a root cause in PRecall's pretty-printer being too lax.

PRecall.__str__ produces recall <fact1>, <fact2>, ... which is term-greedy at the parser level: its parse_nonempty_term_list is comma-greedy, and the embedded parse_term happily reads | (an add-level operator aliased to ∪) and in (a compare-level operator, used for set membership). So when the pretty-printer emits a PRecall inside a |-separated proof list, a ,-separated proof tuple, or just before an in keyword, the next separator gets consumed by the inner term parse and reparsing trips with expected a term, not "recall". Concrete repros from lib/:

• lib/IntAddSub.pf: source simplify with (recall y < x) | (recall not (x < y)) was pretty-printed without the parens.
• lib/NatDiv.pf: source apply less_trans to (recall k' < m), (recall m < j') was pretty-printed as bare apply less_trans to recall k' < m, recall m < j'.
• lib/NatDiv.pf (later): replace symmetric (recall k = j') in recall P(j') lost the parens around the symmetric (recall ...) argument, so the in was consumed by the inner term parse at compare level.

Fix: add a _proof_list_item_str helper in abstract_syntax/proofs.py that wraps such proofs in parens when emitted as an element of a |-separated proof list (SimplifyGoal/SimplifyFact/RewriteGoal/RewriteFact), a ,-separated proof tuple (PTuple), or just before an in keyword (replace ... in ... already wraps the equations list). The helper recurses through PSymmetric/PTransitive/PHelpUse so a proof whose trailing sub-proof is PRecall is also wrapped. Parens are a no-op for the parser (LPAR proof RPAR returns the inner proof unchanged), so the canonical AST is unaffected.

Four lib/ files (IntAddSub.pf, Maps.pf, NatLess.pf, UIntLess.pf) move from parse-fail to OK on the round-trip sweep and join PARSER_ROUND_TRIP_FILES, together with a synthetic recall_list_roundtrip.pf fixture covering the three surface shapes (replace ... | ..., apply ... to ..., ..., replace symmetric ... in ...).

Remaining lib/ parse-fails after this PR: IntMult.pf (a Cases proof falls back to the dataclass repr for lack of a __str__) and NatDiv.pf (an obtain ... where ... from ...; choose ... block is being flattened with semicolons by the pretty-printer). Both are independent pretty-printer bugs that #931 already tracks; this PR doesn't try to address them. UIntAdd.pf transitions from parse-fail to AST-drift (its apply ... to (X), (Y) PTuple is now pretty-printable but a separate ModusPonens-vs-PTuple bug surfaces — also a follow-up).

Test plan

• python3.13 deduce.py test/should-validate/recall_list_roundtrip.pf validates
• python3.13 test-deduce.py --equiv --serial passes (parser equivalence + round-trip)
• make static passes
• python3.13 test-deduce.py passes
• Local sweep: lib/ round-trip parse-fails drop from 7 to 2

Claude session — fallback UUID: fb5a58da-9dd0-4c1f-a373-595087fe7edb

🤖 Generated with Claude Code