Skip to content

Pretty-printer: parenthesize not X operands of infix ops (closes #987)#989

Merged
jsiek merged 1 commit into
mainfrom
claude/suspicious-lamport-7fe4e6
Jun 18, 2026
Merged

Pretty-printer: parenthesize not X operands of infix ops (closes #987)#989
jsiek merged 1 commit into
mainfrom
claude/suspicious-lamport-7fe4e6

Conversation

@jsiek

@jsiek jsiek commented Jun 17, 2026

Copy link
Copy Markdown
Owner

Summary

precedence returned None for the IfThen(_, _, _, Bool false) AST
that desugars not X (and the X ≠ Y sugar). So op_arg_str never
wrapped a not X argument of =, <, +, etc. — but the parsers'
NOT branch consumes parse_term_equal, meaning the printed
(not (P and Q)) = (...) reparsed as not ((P and Q) = (...)) with
the outer connective flipping from = to not. De Morgan's laws
(lib/Base.pf:not_and, not_or, double_neg) were the canonical
witnesses; the sweep found the same drift in 14 other lib/ files.

Return 0 from precedence for the not X shape so it is strictly
below every infix_precedence value (1..8), forcing parens in
op_arg_str.

  • test/should-validate/not_paren_roundtrip.pf: De Morgan-shaped
    regression fixture covering (not (P and Q)) = ((not P) or (not Q))
    and the dual.
  • test-deduce.py: register the new fixture under
    PARSER_ROUND_TRIP_FILES and promote lib/Base.pf from the
    equivalence-only block into the round-trip block (it round-trips
    cleanly with the fix).

Closes #987. Refs #931.

The sweep also surfaced four other unrelated drift categories in
lib/ (public-import visibility, apply IH[…] to … AllElim/
ApplyDefsFact nesting, the set literal, and apply f to a, apply g to b PTuple flattening); those are tracked together in #988 and not
touched here.

Test plan

  • make static — ruff + mypy (incl. --no-site-packages) clean
  • python3.13 test-deduce.py --equiv — passes (curated grammar
    corpus + pretty-print round trip)
  • python3.13 test-deduce.py — full local suite passes
    (cli + lib + passable + errors + warns + equiv, 141s)

Claude session — fallback UUID: c957d956-19db-4a98-882f-cc68756db73b

🤖 Generated with Claude Code

`precedence` returned `None` for the `IfThen(_, _, _, Bool false)` AST
that desugars `not X` (and the `X ≠ Y` sugar). So `op_arg_str` never
wrapped a `not X` argument of `=`, `<`, `+`, etc. -- but the parsers'
`NOT` branch consumes `parse_term_equal`, meaning the printed
`(not (P and Q)) = (...)` reparsed as `not ((P and Q) = (...))` with
the outer connective flipping from `=` to `not`. De Morgan's laws
(`lib/Base.pf:not_and`, `not_or`, `double_neg`) were the canonical
witnesses; the sweep found the same drift in 14 other `lib/` files.

Return `0` from `precedence` for the `not X` shape so it is strictly
below every `infix_precedence` value (1..8), forcing parens in
`op_arg_str`.

- `test/should-validate/not_paren_roundtrip.pf`: De Morgan-shaped
  regression fixture covering `(not (P and Q)) = ((not P) or (not Q))`
  and the dual.
- `test-deduce.py`: register the new fixture under
  `PARSER_ROUND_TRIP_FILES` and promote `lib/Base.pf` from the
  equivalence-only block into the round-trip block (it round-trips
  cleanly with the fix).

Refs #931.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
@jsiek jsiek merged commit 81c477f into main Jun 18, 2026
9 checks passed
@jsiek jsiek deleted the claude/suspicious-lamport-7fe4e6 branch June 18, 2026 01:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Pretty-printer drops parens around not X operands of =/infix ops

1 participant