Add Printing Reversible flags: check printed terms reparse to equal terms, escalating printing options when not

[JasonGross]

Written by Claude (Anthropic AI) at the request of and under the supervision of @JasonGross.

What

Five new mutually-exclusive flags (setting one unsets the others):

• Set Printing Reversible Up To Unification
• Set Printing Reversible Up To Conversion Modulo Sorts And Universes
• Set Printing Reversible Up To Conversion Modulo Universes
• Set Printing Reversible Up To Conversion Modulo Universe Unification
• Set Printing Reversible Up To Conversion

When one is set, every term print (Printer.pr_econstr_env & friends: Check, Print, About, goal display, error messages, ...) goes through a reparsability check: the externalized term is rendered to a string, parsed back (with a fresh end-of-input variant of the lconstr entry), re-elaborated with interp_open_constr, and compared to the original term up to the selected equivalence. When the check fails, printing options are progressively turned on — coercions, implicit arguments, unsetting notations, universes (first with, then without notations), parentheses, and finally the raw-print options of Printing All — until the printed form passes; if none does, the most explicit form is used and a reversible-printing warning is emitted.

The five equivalences:

1. Up To Unification: the reparsed form (with holes for unprinted arguments and fresh flexible universes) must unify with the original term. Accepts any printed form that can denote the original term in a context where the expected type is known; the most permissive check.
2. Up To Conversion Modulo Sorts And Universes: the printed form must re-elaborate standalone with no unresolved holes, to a term convertible with the original when sorts and universes are ignored entirely (Reductionops.is_conv_nounivs): sort qualities, universe levels and universe instances may all differ. The laxest of the conversion-based checks.
3. Up To Conversion Modulo Universes: standalone re-elaboration as above, convertible when universe levels (and the level components of universe instances) are ignored but sort qualities must agree (a dedicated Conversion.generic_conv comparator): Set vs Type@{u} is accepted, Prop/SProp/Type are pairwise distinguished, and the quality components of instances are compared structurally — so a sort-polymorphic instance whose omission would change the elaborated quality stays printed.
4. Up To Conversion Modulo Universe Unification: standalone re-elaboration, convertible while threading universe unification through the evar map (Reductionops.infer_conv): the universes (and sort qualities) introduced by the reparse may be unified against the original ones. Not comparable with the two previous modes in strictness: stricter on levels (a fresh level cannot be unified with an algebraic universe, so e.g. the sort of Check Type escalates), laxer than Modulo Universes on qualities (they get unified rather than compared).
5. Up To Conversion: as above, but the universe (in)equalities must already hold in the current graph (Reductionops.is_conv) — universe instances of polymorphic constants generally get printed.

Since neither conversion nor unification of two terms compares their types (kernel conversion does not compare lambda binder types, which is only complete when both sides share a type), the types of the original and reparsed terms are compared too when the printed expression stands for a term.

Example (from the test)

Check @eq_refl nat 0.
(* eq_refl : 0 = 0                    -- baseline *)
Set Printing Reversible Up To Unification.
Check @eq_refl nat 0.
(* eq_refl : 0 = 0                    -- unification re-infers the hidden args *)
Set Printing Reversible Up To Conversion.
Check @eq_refl nat 0.
(* @eq_refl nat 0 : 0 = 0             -- standalone elaboration needs them *)

Polymorphic Definition pid@{u} (A : Type@{u}) (a : A) := a.
Universe u.
Check pid@{u}.
(* pid@{u} : forall A : Type@{u}, A -> A   -- strict conversion *)
Set Printing Reversible Up To Conversion Modulo Universes.
Check pid@{u}.
(* pid : forall A : Type, A -> A           -- universe levels are ignored *)
Check Type.
(* Type : Type                             -- Type@{u+1} vs fresh level: fine here,
                                              warns+escalates under strict conversion
                                              and under universe unification *)

Set Universe Polymorphism.
Definition idT@{s;u} (A : Type@{s;u}) (a : A) := a.
Check idT@{Prop;Set}.
(* idT@{Prop ; Set} : forall A : Prop, A -> A  -- modulo universes: dropping the
                                                  instance would change the sort quality *)
Set Printing Reversible Up To Conversion Modulo Sorts And Universes.
Check idT@{Prop;Set}.
(* idT : forall A : Prop, A -> A               -- sorts ignored too, instance drops *)

A printing-only notation that does not print what it parses escalates to unsetting notation printing (2 + 3 displayed through a lying notation gets printed as Nat.add 2 3); goal display is checked as well (see test-suite/output/ReversiblePrinting.v).

Implementation notes

• New module printing/reversiblePrinting.ml; printing already depends on parsing, so the roundtrip really goes through the parser (catching printer/parser grammar mismatches), not just through re-internalization of the constr_expr.
• The ladder is expressed over the PrintingFlags.t records introduced recently, and Printer renders the chosen constr_expr with the flags that were used to produce it, so what is checked is exactly what is displayed.
• The Modulo Universes comparator has no eq_constr_nounivs fast-path: that would treat sorts of different qualities as equal and erase exactly the sort-sensitivity that distinguishes it from Modulo Sorts And Universes.
• Warnings that the re-elaboration itself would emit (e.g. deprecations) are silenced during the check; the check is guarded against reentrancy (terms printed while checking, e.g. inside caught elaboration errors, are not themselves checked).
• Failures of parsing/elaboration at a given rung simply move to the next rung; only critical exceptions escape.

Caveats

• Printing gets noticeably more expensive when a flag is set (each displayed term is re-parsed and re-elaborated, possibly several times); the flags are off by default and meant as a debugging/robustness aid.
• Terms printed under a nonempty scope stack (e.g. some Arguments-scoped subterm printers) are reparsed without that scope, which can cause spurious escalation.
• Sort universes that cannot be referred to by name (e.g. Check Type) are inherently unreparsable under strict conversion and under universe unification (but not under the two modulo-universes modes, which ignore the levels) and produce the warning there.

🤖 Generated with Claude Code

https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b