Reversible printing with sort printing and anonymous sort quality variables (combines #22155, #22283, #22310) - #22311
Draft
JasonGross wants to merge 4 commits into
Draft
Conversation
…erms, escalating printing options when not Add five mutually exclusive flags — Printing Reversible Up To Unification, Up To Conversion, Up To Conversion Modulo Universe Unification, Up To Conversion Modulo Universes, and Up To Conversion Modulo Sorts And Universes — under which the printer checks each printed term by reparsing and re-elaborating it and comparing the result against the original at the selected strictness. When the check fails, printing options are escalated until the printed form becomes reversible; if no combination suffices, a reversible-printing warning is emitted. Comparison modes: - Up To Unification: the reparse must unify with the original. - Up To Conversion: conversion, strict on universes. - Up To Conversion Modulo Universe Unification: conversion threading universe unification through the evar map (fails when e.g. a fresh flexible level cannot be equated with an algebraic universe). - Up To Conversion Modulo Universes: conversion ignoring universe levels and instance level components while requiring sort qualities to agree (SProp/Prop/Type distinct; quality variables compare structurally, so sort-polymorphic instances whose omission would change the elaborated quality are kept). - Up To Conversion Modulo Sorts And Universes: conversion ignoring sorts and universes entirely (Reductionops.is_conv_nounivs), the laxest of the conversion-based checks. Includes output tests, reference-manual documentation and a changelog entry. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
coqbot-app
Bot
added
the
needs: full CI
JasonGross
added
kind: enhancement
Like Set Printing Universes but showing only the sort structure:
plain sorts (Type, SProp, Prop, Set) print as usual, sort variables
that would otherwise be hidden are displayed with their universe
levels replaced by _, e.g. Type@{s;_}, and universe instances of
polymorphic references are displayed when they carry sort qualities
(e.g. f@{q ; _}) and stay hidden otherwise.
Fixes rocq-prover#22153
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
When the flag is on, sort quality variables that cannot be referred to
by name print as "_" (which parses back, denoting a fresh quality
variable) instead of their raw α-names (which cannot be parsed back).
Named quality variables are printed by name as usual.
Implemented as a new anonymous_qvars field of PrintingFlags.Extern
(forced off by raw printing), applied in the GQuality fallback of
Constrextern.extern_glob_quality and threaded through sorts, universe
instances and relevance marks; Constrextern.extern_sort and
Printer.pr_sort gain a corresponding argument.
Also extend the sort grammar to accept "_" as an anonymous quality in
sort annotations (Type@{_ ; u}): previously "_" was accepted as a
quality only in universe instances, so the anonymous form printed for
a sort could not be parsed back ("_" parsed as a universe level and
the ";" was rejected). Docgram regenerated accordingly.
Includes output tests, reference-manual documentation and a changelog
entry.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
…rsible-printing ladder
Extend the reversible-printing escalation ladder so that sort qualities
and sort quality variables can be made explicit when they are what keeps
a printed term from re-parsing.
Two rungs are inserted after implicit arguments: a sort rung (Detype.sorts)
that shows a sort-polymorphic instance at sort level, and a rung that
additionally prints sort quality variables anonymously (Extern.anonymous_qvars),
because an unnamed quality variable otherwise prints as a raw, unparsable
alpha-name whereas "_" re-parses to a fresh quality variable that
unification can match. The anon-qvars commit in this stack also adds the
"Type@{_ ; u}" sort-annotation grammar, so "_" now parses as a sort
quality inside a sort as well as in a universe instance; a bare
sort-polymorphic constant therefore round-trips fully (both its instance
and the sort in its type) with no warning under this rung.
At each universes rung the anonymous-quality-variable form is tried first
and then without it, since anonymizing a quality variable can itself be
what breaks re-parsing (the "_" re-parses to a fresh variable, which
round-trips only when unification can match it). Rungs remain ordered by
explicitness rather than being cumulative, and raw printing stays faithful
with anonymous quality variables off.
The ladder order is now: coercions, implicit arguments, sorts,
sorts + anonymous quality variables, notations off, universes + anonymous
quality variables, universes, universes without notations + anonymous
quality variables, universes without notations, parentheses, raw.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
JasonGross
force-pushed
the
reversible-printing-full-stack
branch
from
July 27, 2026 04:33
37170dd to
014a05e
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Combines #22155, #22283, and #22310 with an integration commit so reversible printing can expose sort qualities and sort quality variables when needed for round-tripping:
Set Printing Sorts. It displays sort structure while anonymizing hidden sort-quality universe levels as_, for exampleType@{s ; _}, and shows polymorphic-reference universe instances that carry sort qualities. It coexists with the existingPrinting Sort Qualitiesflag.Printing Reversible …flags. Printed terms are re-parsed, re-elaborated, and compared with the original; options escalate until the term round-trips or areversible-printingwarning is emitted.Set Printing Sort Quality Variables Anonymously, printing unnamed variables as the reparsable_rather than raw, unparsable α-names. It also accepts_inside sort annotations such asType@{_ ; u}.Escalation ladder
Each rung is standalone rather than cumulative:
coercions → implicit arguments → sorts → sorts + anonymous quality variables → notations off → universes + anonymous quality variables → universes → universes without notations + anonymous quality variables → universes without notations → parentheses → raw (
Printing All+ universes + parentheses).Anonymous quality variables come first at applicable rungs because an unnamed variable has no reparsable name. With
Type@{_ ; u},_works both in an instance annotation (idT@{_ ; _}) and in the type's sort (Type@{_ ; _}). The following non-anonymous rung remains necessary because_creates a fresh variable and only round-trips when unification can match it. Raw printing keeps anonymous quality variables off.This draft must not merge before #22155, #22283, and #22310; it will be rebased onto them after they merge.
Written by Claude (Anthropic AI) at the request of and under the supervision of @JasonGross.
🤖 Generated with Claude Code
Wordsmithed by Codex.