From 96cfce29349343bb40e6b6079dae63ce1e7fa768 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 21 Jul 2026 00:56:48 +0000 Subject: [PATCH 1/4] Add Printing Reversible flags: check printed terms reparse to equal terms, escalating printing options when not MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- .../22283-reversible-printing-Added.rst | 11 + .../proof-engine/vernacular-commands.rst | 95 ++++++ printing/printer.ml | 29 +- printing/reversiblePrinting.ml | 286 ++++++++++++++++++ printing/reversiblePrinting.mli | 35 +++ test-suite/output/ReversiblePrinting.out | 62 ++++ test-suite/output/ReversiblePrinting.v | 106 +++++++ 7 files changed, 619 insertions(+), 5 deletions(-) create mode 100644 doc/changelog/08-vernac-commands-and-options/22283-reversible-printing-Added.rst create mode 100644 printing/reversiblePrinting.ml create mode 100644 printing/reversiblePrinting.mli create mode 100644 test-suite/output/ReversiblePrinting.out create mode 100644 test-suite/output/ReversiblePrinting.v diff --git a/doc/changelog/08-vernac-commands-and-options/22283-reversible-printing-Added.rst b/doc/changelog/08-vernac-commands-and-options/22283-reversible-printing-Added.rst new file mode 100644 index 000000000000..63e102200fa7 --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/22283-reversible-printing-Added.rst @@ -0,0 +1,11 @@ +- **Added:** + flags ``Printing Reversible Up To Unification``, + ``Printing Reversible Up To Conversion Modulo Sorts And Universes``, + ``Printing Reversible Up To Conversion Modulo Universes``, + ``Printing Reversible Up To Conversion Modulo Universe Unification`` and + ``Printing Reversible Up To Conversion``, which check, each time a term + is printed, that the printed form can be parsed and elaborated back to + a term equal to the original one up to the selected equivalence, and + progressively turn more printing options on until this is the case + (`#22283 `_, + written by Claude (Anthropic), for Jason Gross). diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 5d990b2bd188..53fcac6a89e0 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1164,6 +1164,101 @@ Printing constructions in full This flag is off by default. +.. _reversible-printing: + +Checking that printed terms can be parsed back (reversible printing) +-------------------------------------------------------------------- + +Because notations, hidden implicit arguments, hidden coercions or hidden +universe instances can make different terms print alike, the printed form +of a term cannot always be parsed and elaborated back to the term it +stands for. Rather than unconditionally making printing fully explicit as +:flag:`Printing All` does, the following flags keep the current printing +options, but check, each time a term is printed, that its printed form +can be parsed and elaborated back to a term equal to the original one, up +to the equivalence selected by the flag; when the check fails, printing +options are progressively turned on — first :flag:`Printing Coercions`, +then :flag:`Printing Implicit`, then unsetting :flag:`Printing Notations`, +then :flag:`Printing Universes` (first with, then without notations), +then :flag:`Printing Parentheses` and finally all the options implied by +:flag:`Printing All` — until the printed form passes the check. + +These five flags are mutually exclusive: setting one of them unsets the +others, and unsetting the currently set one turns the checks off +entirely. All are off by default. Since every displayed term is re-parsed +and re-elaborated (possibly several times), printing can become +noticeably more expensive when one of these flags is set. + +.. flag:: Printing Reversible Up To Unification + + The re-parsed form must unify with the original term: holes standing + for arguments that are not printed and universes introduced by the + re-elaboration may be instantiated by unifying against the original + term. This is the most permissive of the five checks; it accepts any + printed form that can denote the original term, even if only in a + context where the expected type is known. + + .. warn:: The printed form of this term could not be re-parsed and re-elaborated to an equal term (up to ...), even with all printing options turned on. + + If no printed form, however explicit, passes the check, the most + explicit one is printed anyway and this warning is emitted. This + happens for instance for terms mentioning universes that cannot be + referred to by name, such as the sort of ``Check Type``. + +.. flag:: Printing Reversible Up To Conversion Modulo Sorts And Universes + + The printed form must re-elaborate on its own (without help from the + original term) to a term with no unresolved holes, and that term must + be convertible to the original one when sorts and universes are + ignored entirely: sort qualities (``SProp``, ``Prop``, ``Type``), + universe levels and universe instances may all differ. This is the + laxest of the conversion-based checks; in particular, unlike + :flag:`Printing Reversible Up To Conversion Modulo Universes` below, + it accepts a printed form whose re-elaboration lives at a different + sort quality than the original term. + +.. flag:: Printing Reversible Up To Conversion Modulo Universes + + The printed form must re-elaborate on its own (without help from the + original term) to a term with no unresolved holes, and that term must + be convertible to the original one when universe levels (and the level + components of universe instances) are ignored, but *sort qualities + must agree*: ``Set`` and ``Type@{u}`` are accepted, but ``Prop``, + ``SProp`` and ``Type`` are pairwise distinguished. With this flag, + implicit arguments that can only be inferred from the type of the + original term get printed, and the universe levels of sorts (such as + the sort of ``Check Type``) generally do not, but the *sort quality* + part of a polymorphic instance is kept when it would otherwise + re-elaborate to a different quality. + +.. flag:: Printing Reversible Up To Conversion Modulo Universe Unification + + Like :flag:`Printing Reversible Up To Conversion Modulo Universes`, + but instead of ignoring universe levels it lets the universes (and + sort qualities) introduced by the re-elaboration be unified against + the original ones, enforcing new universe (in)equalities as needed. + This is stricter than + :flag:`Printing Reversible Up To Conversion Modulo Universes` on + universe levels — a universe level cannot be unified with an + algebraic universe, so the sort of ``Check Type`` is printed + explicitly — but laxer on sort qualities, which get unified rather + than required to match syntactically. + +.. flag:: Printing Reversible Up To Conversion + + Like :flag:`Printing Reversible Up To Conversion Modulo Universe + Unification`, but no new universe constraints are enforced: the + universe (in)equalities needed for convertibility must already be + valid in the current universe graph. With this flag, universe + instances of polymorphic constants generally need to be printed + (turning on :flag:`Printing Universes` for the terms where they + matter). + +For all five flags, when the printed expression stands for a term (as +opposed to a type), the types of the original and re-elaborated terms +are compared as well, so that, e.g., a printed form whose re-elaboration +lives at a different universe instance is not considered reversible. + .. _controlling-typing-flags: Controlling Typing Flags diff --git a/printing/printer.ml b/printing/printer.ml index 8379352eca6a..0a7ff287e35f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -45,15 +45,32 @@ let current_extern = PrintingFlags.Extern.current and only names of goal/section variables and rel names that do _not_ occur in the scope of the binder to be printed are avoided. *) +(* When a [Printing Reversible] flag is set, the externalization is + checked for reparsability and the printing flags are possibly made + more explicit accordingly, hence rendering uses the flags returned + by [ReversiblePrinting.checked_extern]. *) +let checked_extern_constr ?inctx ?scope ~flags env sigma t = + ReversiblePrinting.checked_extern ~flags + ~extern:(fun ~flags -> extern_constr ?inctx ?scope ~flags env sigma t) + ~kind:ReversiblePrinting.Term env sigma t + +let checked_extern_type ?goal_concl_style ?impargs ~flags env sigma t = + ReversiblePrinting.checked_extern ~flags + ~extern:(fun ~flags -> extern_type ?goal_concl_style ~flags env sigma ?impargs t) + ~kind:ReversiblePrinting.Type env sigma t + let pr_econstr_n_env ?inctx ?scope ?(flags=current_combined()) env sigma n t = + let flags, c = checked_extern_constr ?inctx ?scope ~flags env sigma t in let ppflags = Ppconstr.of_printing_flags flags in - pr_constr_expr_n ~flags:ppflags env sigma n (extern_constr ?inctx ?scope ~flags env sigma t) + pr_constr_expr_n ~flags:ppflags env sigma n c let pr_econstr_env ?inctx ?scope ?(flags=current_combined()) env sigma t = + let flags, c = checked_extern_constr ?inctx ?scope ~flags env sigma t in let ppflags = Ppconstr.of_printing_flags flags in - pr_constr_expr ~flags:ppflags env sigma (extern_constr ?inctx ?scope ~flags env sigma t) + pr_constr_expr ~flags:ppflags env sigma c let pr_leconstr_env ?inctx ?scope ?(flags=current_combined()) env sigma t = + let flags, c = checked_extern_constr ?inctx ?scope ~flags env sigma t in let ppflags = Ppconstr.of_printing_flags flags in - Ppconstr.pr_lconstr_expr ~flags:ppflags env sigma (extern_constr ?inctx ?scope ~flags env sigma t) + Ppconstr.pr_lconstr_expr ~flags:ppflags env sigma c let pr_constr_n_env ?inctx ?scope ?flags env sigma n c = pr_econstr_n_env ?inctx ?scope ?flags env sigma n (EConstr.of_constr c) @@ -73,11 +90,13 @@ let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env let pr_etype_env ?goal_concl_style ?(flags=current_combined()) env sigma t = + let flags, c = checked_extern_type ?goal_concl_style ~flags env sigma t in let ppflags = Ppconstr.of_printing_flags flags in - pr_constr_expr ~flags:ppflags env sigma (extern_type ?goal_concl_style ~flags env sigma t) + pr_constr_expr ~flags:ppflags env sigma c let pr_letype_env ?goal_concl_style ?(flags=current_combined()) env sigma ?impargs t = + let flags, c = checked_extern_type ?goal_concl_style ?impargs ~flags env sigma t in let ppflags = Ppconstr.of_printing_flags flags in - pr_lconstr_expr ~flags:ppflags env sigma (extern_type ?goal_concl_style ~flags env sigma ?impargs t) + pr_lconstr_expr ~flags:ppflags env sigma c let pr_type_env ?goal_concl_style ?flags env sigma c = pr_etype_env ?goal_concl_style ?flags env sigma (EConstr.of_constr c) diff --git a/printing/reversiblePrinting.ml b/printing/reversiblePrinting.ml new file mode 100644 index 000000000000..3895c19d8713 --- /dev/null +++ b/printing/reversiblePrinting.ml @@ -0,0 +1,286 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* true + | (UpToUnification | UpToConversionModuloSortsAndUniverses + | UpToConversionModuloUniverses + | UpToConversionModuloUniverseUnification | UpToConversion), _ -> false + +let current_mode : mode option ref = ref None + +(* These flags behave like a radio button: setting one unsets the + others; unsetting the one currently set disables the check. *) +let declare_mode_option key mode = + let open Goptions in + declare_bool_option { + optstage = Summary.Stage.Interp; + optdepr = None; + optkey = key; + optread = (fun () -> match !current_mode with + | Some m -> mode_eq m mode + | None -> false); + optwrite = (fun b -> + if b then current_mode := Some mode + else match !current_mode with + | Some m when mode_eq m mode -> current_mode := None + | _ -> ()); + } + +let () = declare_mode_option + ["Printing";"Reversible";"Up";"To";"Unification"] UpToUnification +let () = declare_mode_option + ["Printing";"Reversible";"Up";"To";"Conversion";"Modulo";"Sorts";"And";"Universes"] + UpToConversionModuloSortsAndUniverses +let () = declare_mode_option + ["Printing";"Reversible";"Up";"To";"Conversion";"Modulo";"Universes"] + UpToConversionModuloUniverses +let () = declare_mode_option + ["Printing";"Reversible";"Up";"To";"Conversion";"Modulo";"Universe";"Unification"] + UpToConversionModuloUniverseUnification +let () = declare_mode_option + ["Printing";"Reversible";"Up";"To";"Conversion"] UpToConversion + +let pr_mode = function + | UpToUnification -> Pp.str "unification" + | UpToConversionModuloSortsAndUniverses -> + Pp.str "conversion modulo sorts and universes" + | UpToConversionModuloUniverses -> Pp.str "conversion modulo universes" + | UpToConversionModuloUniverseUnification -> + Pp.str "conversion modulo universe unification" + | UpToConversion -> Pp.str "conversion" + +let warn_not_reversible = + CWarnings.create ~name:"reversible-printing" + (fun mode -> + Pp.(strbrk "The printed form of this term could not be re-parsed \ + and re-elaborated to an equal term (up to " ++ pr_mode mode ++ + strbrk "), even with all printing options turned on.")) + +let lconstr_eoi = Procq.eoi_entry Procq.Constr.lconstr + +(* Successively more explicit printing flags: coercions, implicit + arguments, no notations, universes (first with, then without + notations), parentheses, ending with the equivalent of + [Printing All] plus [Printing Universes] and [Printing + Parentheses]. Unsetting notations is tried after implicit arguments + and before universes, but is not kept when escalating to universes: + configurations are ordered by explicitness, not included in each + other. Only extern/detype-level flags and the [parentheses] flag may + vary along the ladder: the rendering of the returned [constr_expr] + must be fully determined by the returned flags (see + [Ppconstr.of_printing_flags]). *) +let ladder flags = + let open PrintingFlags in + let e0 = flags.extern in + let e1 = { e0 with Extern.coercions = true } in + let e2 = { e1 with Extern.implicits = true; Extern.implicits_defensive = true } in + let e3 = { e2 with Extern.notations = false } in + let d4 = { flags.detype with Detype.universes = true } in + let e5 = { e3 with Extern.parentheses = true } in + let raw = make_raw flags in + let raw = { detype = { raw.detype with Detype.universes = true }; + extern = { raw.extern with Extern.parentheses = true } } in + [ flags; + { flags with extern = e1 }; + { flags with extern = e2 }; + { flags with extern = e3 }; + { detype = d4; extern = e2 }; + { detype = d4; extern = e3 }; + { detype = d4; extern = e5 }; + raw ] + +(* Reparsing a term can spuriously emit warnings (e.g. deprecation + warnings for notations it reuses); silence them during the check. *) +let no_warnings f = + let saved = CWarnings.get_flags () in + CWarnings.set_flags "-all"; + try let v = f () in CWarnings.set_flags saved; v + with e -> + let e = Exninfo.capture e in + CWarnings.set_flags saved; + Exninfo.iraise e + +(* Conversion for the [UpToConversionModuloUniverses] mode: universe + levels (and the level components of universe instances) are ignored, + but sort qualities must agree. So [Set] and [Type@{u}] (both of + [QType] quality) are accepted, and [Type@{u}] vs [Type@{v}] is + accepted, but [Prop], [SProp] and [Type] are pairwise rejected; the + quality components of instances (for sort-polymorphic constants) must + also agree. This lets [Check Type] print plain [Type] while still + catching a reparse whose sort quality differs from the original. *) +let modulo_universes_compare = + let open Conversion in + let compare_sorts _pb s1 s2 () = + if Sorts.Quality.equal (Sorts.quality s1) (Sorts.quality s2) + then Result.Ok () else Result.Error None + in + let compare_instances ~flex:_ i1 i2 () = + let (q1, _), (q2, _) = UVars.Instance.to_array i1, UVars.Instance.to_array i2 in + if CArray.equal Sorts.Quality.equal q1 q2 + then Result.Ok () else Result.Error None + in + let compare_cumul_instances _pb _variance i1 i2 () = + compare_instances ~flex:false i1 i2 () + in + { compare_sorts; compare_instances; compare_cumul_instances } + +(* No [eq_constr_nounivs] fast-path here: it would treat sorts of + different qualities as equal, defeating the sort-sensitivity we want. *) +let is_conv_modulo_universes env sigma t1 t2 = + let evars = Evd.evar_handler sigma in + let t1 = EConstr.Unsafe.to_constr t1 in + let t2 = EConstr.Unsafe.to_constr t2 in + let env = Environ.set_universes (Evd.universes sigma) env in + match Conversion.generic_conv ~l2r:false Conversion.CONV ~evars + TransparentState.full env ((), modulo_universes_compare) t1 t2 with + | Result.Ok () -> true + | Result.Error None -> false + | Result.Error (Some e) -> Util.Empty.abort e + +let reparses ~mode ~kind ~flags env sigma t expr = + try + no_warnings begin fun () -> + let ppflags = Ppconstr.of_printing_flags flags in + let str = Pp.string_of_ppcmds (Ppconstr.pr_lconstr_expr ~flags:ppflags env sigma expr) in + let expr = Procq.parse_string lconstr_eoi str in + let expected_type = match kind with + | Type -> Pretyping.IsType + | Term -> Pretyping.WithoutTypeConstraint + in + let sigma', t' = Constrintern.interp_open_constr ~expected_type env sigma expr in + let no_new_undefined () = + Evar.Set.for_all (fun ev -> Evd.mem sigma ev) + (Evarutil.undefined_evars_of_term sigma' t') + in + (* Conversion (and unification) of terms does not imply that they + have convertible types (e.g. binder types of lambdas are not + compared), so for terms we compare the types too. For [Type] + kind we do not compare the (algebraic) sorts the types live + in, as elaboration is anyway allowed to pick different such + sorts for the very same expression. *) + let pairs = match kind with + | Type -> [t', t] + | Term -> + let ty' = Retyping.get_type_of env sigma' t' in + let ty = Retyping.get_type_of env sigma' t in + [ty', ty; t', t] + in + match mode with + | UpToUnification -> + let sigma' = List.fold_left (fun sigma' (t', t) -> + Evarconv.unify_delay env sigma' t' t) sigma' pairs in + let (_ : Evd.evar_map) = Evarconv.solve_unif_constraints_with_heuristics env sigma' in + true + | UpToConversionModuloSortsAndUniverses -> + (* Convertibility ignoring sorts and universes entirely + ([Reductionops.is_conv_nounivs]): unlike modulo universes + below, even sort qualities need not agree, so e.g. dropping a + sort-polymorphic instance whose omission changes the + elaborated quality is accepted. *) + no_new_undefined () && + List.for_all (fun (t', t) -> Reductionops.is_conv_nounivs env sigma' t' t) pairs + | UpToConversionModuloUniverses -> + (* Convertibility ignoring universe levels (and the level + components of instances) but requiring sort qualities to + agree. Unlike a conversion enforcing universe equalities, + this accepts e.g. a freshly elaborated [Type@{v}] against the + original [Type@{u+1}], where [v] is a plain level that cannot + be set equal to the algebraic [u+1]; but it still rejects a + reparse whose sort quality differs (e.g. [Prop] vs [Type]). *) + no_new_undefined () && + List.for_all (fun (t', t) -> is_conv_modulo_universes env sigma' t' t) pairs + | UpToConversionModuloUniverseUnification -> + (* Convertibility enforcing universe unification: the universes + introduced by the reparsing may be unified against the + original ones through the evar map, but a universe level + cannot be set equal to an algebraic universe, so e.g. [Check + Type] does not check under this mode. *) + no_new_undefined () && + (let rec conv sigma' = function + | [] -> true + | (t', t) :: pairs -> + match Reductionops.infer_conv ~pb:Conversion.CONV env sigma' t' t with + | Some sigma' -> conv sigma' pairs + | None -> false + in + conv sigma' pairs) + | UpToConversion -> + no_new_undefined () && + List.for_all (fun (t', t) -> Reductionops.is_conv env sigma' t' t) pairs + end + with e when CErrors.noncritical e -> false + +(* Printing terms while checking reversibility (e.g. from the + elaboration of the reparsed term) must not recursively trigger the + check. *) +let in_check = ref false + +let checked_extern ~flags ~extern ~kind env sigma t = + match !current_mode with + | None -> flags, extern ~flags + | Some _ when !in_check -> flags, extern ~flags + | Some mode -> + in_check := true; + try + let rec aux = function + | [] -> assert false + | [flags] -> + let expr = extern ~flags in + if not (reparses ~mode ~kind ~flags env sigma t expr) then + warn_not_reversible mode; + (flags, expr) + | flags :: rest -> + let expr = extern ~flags in + if reparses ~mode ~kind ~flags env sigma t expr then (flags, expr) + else aux rest + in + let v = aux (ladder flags) in + in_check := false; + v + with e -> + let e = Exninfo.capture e in + in_check := false; + Exninfo.iraise e diff --git a/printing/reversiblePrinting.mli b/printing/reversiblePrinting.mli new file mode 100644 index 000000000000..e1d4def428cb --- /dev/null +++ b/printing/reversiblePrinting.mli @@ -0,0 +1,35 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* + extern:(flags:PrintingFlags.t -> Constrexpr.constr_expr) -> + kind:kind -> Environ.env -> Evd.evar_map -> EConstr.constr -> + PrintingFlags.t * Constrexpr.constr_expr diff --git a/test-suite/output/ReversiblePrinting.out b/test-suite/output/ReversiblePrinting.out new file mode 100644 index 000000000000..db216c41f3d7 --- /dev/null +++ b/test-suite/output/ReversiblePrinting.out @@ -0,0 +1,62 @@ +eq_refl + : 0 = 0 +eq_refl + : 0 = 0 +@eq_refl nat 0 + : 0 = 0 +Printing Reversible Up To Unification is off +Printing Reversible Up To Conversion Modulo Sorts And Universes is off +Printing Reversible Up To Conversion Modulo Universe Unification is off +Printing Reversible Up To Conversion is on +pid@{u} + : forall A : Type@{u}, A -> A +pid + : forall A : Type, A -> A +Type + : Type +pid + : forall A : Type, A -> A +File "./output/ReversiblePrinting.v", line 50, characters 0-11: +Warning: The printed form of this term could not be re-parsed and +re-elaborated to an equal term (up to +conversion modulo universe unification), even with all printing options +turned on. [reversible-printing,default] +File "./output/ReversiblePrinting.v", line 50, characters 0-11: +Warning: The printed form of this term could not be re-parsed and +re-elaborated to an equal term (up to +conversion modulo universe unification), even with all printing options +turned on. [reversible-printing,default] +Type@{ReversiblePrinting.47} + : Type@{ReversiblePrinting.47+1} +pid + : forall A : Type, A -> A +idT@{Prop ; Set} + : forall A : Prop, A -> A +idT + : forall A : Prop, A -> A +idT + : forall A : Prop, A -> A +Type + : Type +@eq_refl nat 0 + : 0 = 0 +eq_refl + : 0 = 0 +2 * 3 + : nat +Nat.add 2 3 + : nat +1 goal + + ============================ + @eq_refl nat 0 = @eq_refl nat 0 +File "./output/ReversiblePrinting.v", line 106, characters 0-11: +Warning: The printed form of this term could not be re-parsed and +re-elaborated to an equal term (up to conversion), even with all printing +options turned on. [reversible-printing,default] +File "./output/ReversiblePrinting.v", line 106, characters 0-11: +Warning: The printed form of this term could not be re-parsed and +re-elaborated to an equal term (up to conversion), even with all printing +options turned on. [reversible-printing,default] +Type@{ReversiblePrinting.88} + : Type@{ReversiblePrinting.88+1} diff --git a/test-suite/output/ReversiblePrinting.v b/test-suite/output/ReversiblePrinting.v new file mode 100644 index 000000000000..0dcd10a14dc5 --- /dev/null +++ b/test-suite/output/ReversiblePrinting.v @@ -0,0 +1,106 @@ +(* Printing Reversible Up To Unification / Conversion Modulo Sorts And + Universes / Conversion Modulo Universes / Conversion Modulo Universe + Unification / Conversion: printing options get progressively turned + on until the printed form re-parses and re-elaborates to an equal + term. *) + +(* Baseline: no check, hidden arguments are not re-inferable from the + printed form alone. *) +Check @eq_refl nat 0. + +(* Unification is enough to re-infer the hidden arguments from the + original term, so nothing needs to be made explicit. *) +Set Printing Reversible Up To Unification. +Check @eq_refl nat 0. + +(* Standalone re-elaboration of [eq_refl] leaves unresolved holes, so + implicit arguments get printed. *) +Set Printing Reversible Up To Conversion. +Check @eq_refl nat 0. + +(* The five flags behave like a radio button. *) +Test Printing Reversible Up To Unification. +Test Printing Reversible Up To Conversion Modulo Sorts And Universes. +Test Printing Reversible Up To Conversion Modulo Universe Unification. +Test Printing Reversible Up To Conversion. + +(* Universe instances: re-elaboration introduces a fresh flexible + universe. Unifying it with the original instance is fine up to + conversion modulo universes, but not up to strict conversion, which + requires the instance to be printed. *) +Polymorphic Definition pid@{u} (A : Type@{u}) (a : A) := a. +Universe u. +Check pid@{u}. +Set Printing Reversible Up To Conversion Modulo Universes. +Check pid@{u}. +(* [Check Type] prints its type as [Type@{u+1}] (an algebraic universe); + re-elaborating the plain [Type] yields a fresh level. Up to conversion + modulo universes these are equal, so [Type] prints with no annotation + and no warning (contrast with the strict conversion case below). *) +Check Type. + +(* Conversion Modulo Universe Unification: universes introduced by the + reparse may be unified against the original ones, but a level cannot + be unified with an algebraic universe. So [pid@{u}] still prints + plainly (fresh level unifies with [u])... *) +Set Printing Reversible Up To Conversion Modulo Universe Unification. +Check pid@{u}. +(* ...but [Check Type] does not check (fresh level vs algebraic [u+1]), + so it warns and escalates, unlike modulo universes above. *) +Check Type. + +Set Printing Reversible Up To Unification. +Check pid@{u}. + +(* Sort qualities must elaborate the same under modulo universes, even + though universe levels need not. [idT] is polymorphic over a sort + quality [s]; used at [Prop], its printed form must keep the sort + instance, because dropping it re-elaborates [idT] at a fresh quality + (defaulting to [Type], quality [QType]) which differs from [Prop]. *) +Set Universe Polymorphism. +Definition idT@{s;u} (A : Type@{s;u}) (a : A) := a. +Set Printing Reversible Up To Conversion Modulo Universes. +Check idT@{Prop;Set}. +(* Modulo universe unification is laxer on sorts: the fresh sort quality + is unified with [Prop], so the instance drops to plain [idT]. *) +Set Printing Reversible Up To Conversion Modulo Universe Unification. +Check idT@{Prop;Set}. +(* Modulo sorts and universes ignores sort qualities as well as + universe levels, so the instance also drops, even though the + re-elaboration of plain [idT] lives at quality Type rather than + Prop... *) +Set Printing Reversible Up To Conversion Modulo Sorts And Universes. +Check idT@{Prop;Set}. +(* ...and [Check Type] prints plainly, as with modulo universes... *) +Check Type. +(* ...but re-elaboration is still standalone, so hidden arguments that + cannot be re-inferred from the printed form alone get printed. *) +Check @eq_refl nat 0. +Unset Universe Polymorphism. + +(* Unsetting the active flag turns the check off entirely (unsetting a + flag other than the active one would be a no-op). *) +Unset Printing Reversible Up To Conversion Modulo Sorts And Universes. +Check @eq_refl nat 0. + +(* A printing-only notation that does not print what it parses is + detected and bypassed by turning notations off. *) +Set Printing Reversible Up To Unification. +Module LyingNotation. + Notation "x ** y" := (Nat.mul x y) (at level 40). + Set Warnings "-notation-overridden". + Notation "x ** y" := (Nat.add x y) (at level 40, only printing). + Check 2 * 3. + Check 2 + 3. +End LyingNotation. + +(* Goal display is checked too. *) +Set Printing Reversible Up To Conversion. +Goal @eq_refl nat 0 = eq_refl. +Show. +Abort. + +(* Sort universes of [Check Type] cannot be re-parsed at all (their + names are not declared), so a warning is emitted and the most + explicit form is printed. *) +Check Type. From b5ed0226160191b4f725ec8911aec8e4e90c25ff Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 22 Jun 2026 15:40:28 +0000 Subject: [PATCH 2/4] feat: add Set Printing Sorts option 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/rocq#22153 Co-Authored-By: Claude Opus 4.6 Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw --- .../22155-printing-sorts-Added.rst | 9 ++ doc/sphinx/addendum/universe-polymorphism.rst | 12 +++ interp/constrextern.ml | 4 +- interp/constrextern.mli | 2 +- pretyping/detyping.ml | 27 ++++-- pretyping/detyping.mli | 2 +- pretyping/printingFlags.ml | 5 ++ pretyping/printingFlags.mli | 4 +- printing/printer.ml | 5 +- printing/printer.mli | 2 +- test-suite/output/PrintingSorts.out | 87 +++++++++++++++++++ test-suite/output/PrintingSorts.v | 79 +++++++++++++++++ 12 files changed, 222 insertions(+), 16 deletions(-) create mode 100644 doc/changelog/08-vernac-commands-and-options/22155-printing-sorts-Added.rst create mode 100644 test-suite/output/PrintingSorts.out create mode 100644 test-suite/output/PrintingSorts.v diff --git a/doc/changelog/08-vernac-commands-and-options/22155-printing-sorts-Added.rst b/doc/changelog/08-vernac-commands-and-options/22155-printing-sorts-Added.rst new file mode 100644 index 000000000000..9d16fc43c17f --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/22155-printing-sorts-Added.rst @@ -0,0 +1,9 @@ +- **Added:** + Added ``Printing Sorts`` flag, which displays sort variables that are + otherwise hidden (e.g. ``Type@{s;_}``) as well as universe instances + carrying sort qualities, with universe level variables replaced by ``_``, + making the sort structure visible without exposing internal universe + level names + (`#22155 `_, + fixes `#22153 `_, + by Jason Gross). diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index b571197c418e..3cd17f68d2fe 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -596,6 +596,18 @@ Printing universes terms apparently identical but internally different in the Calculus of Inductive Constructions. +.. flag:: Printing Sorts + + Turn this :term:`flag` on to display sort variables that are otherwise + hidden, with universe level variables replaced by ``_``. Sorts without + sort variables (:g:`Type`, :g:`SProp`, :g:`Prop`, :g:`Set`) are printed + as usual, while sorts at a sort variable are printed like ``Type@{s;_}`` + (or ``Type@{_}`` when :flag:`Printing Sort Qualities` is off). Universe + instances of polymorphic references are displayed when they contain sort + qualities (with ``_`` in place of the universe levels) and stay hidden + otherwise. Compared to :flag:`Printing Universes`, this makes the sort + structure visible without exposing internal universe level names. + .. cmd:: Print {? Sorted } Universes {? Subgraph ( {* @debug_univ_name } ) } {? {| With | Without } Constraint Sources } {? @string } :name: Print Universes diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 310792fd2010..75da90654218 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1346,9 +1346,9 @@ let extern_type ?(goal_concl_style=false) ~(flags:PrintingFlags.t) env sigma ?im let r = Detyping.detype Detyping.Later ~isgoal:goal_concl_style ~avoid ~flags:flags.detype env sigma t in extern_glob_type ?impargs (extern_env ~flags:flags.extern env sigma) r -let extern_sort ~universes ~qualities sigma s = +let extern_sort ~universes ~sorts ~qualities sigma s = extern_glob_sort (Evd.universe_binders sigma) - (detype_sort ~universes ~qualities sigma s) + (detype_sort ~universes ~sorts ~qualities sigma s) let extern_closed_glob ?(goal_concl_style=false) ?(inctx=false) ?scope ~(flags:PrintingFlags.t) env sigma t = let avoid = make_avoid goal_concl_style env in diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 8bf6b3fe1cd7..aadf473e9d13 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -53,7 +53,7 @@ val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val extern_type : ?goal_concl_style:bool -> flags:PrintingFlags.t -> env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> types -> constr_expr -val extern_sort : universes:bool -> qualities:bool -> Evd.evar_map -> Sorts.t -> sort_expr +val extern_sort : universes:bool -> sorts:bool -> qualities:bool -> Evd.evar_map -> Sorts.t -> sort_expr val extern_rel_context : flags:PrintingFlags.t -> env -> Evd.evar_map -> rel_context -> local_binder_expr list diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index bd26d665607c..ffd19daa4f39 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -273,18 +273,19 @@ let detype_quality sigma q = let detype_universe sigma u = UNamed (List.map (on_fst (detype_level_name sigma)) (Univ.Universe.repr u)) -let detype_sort ~universes ~qualities sigma = function +let anon_univ = UAnonymous {rigid=UState.univ_flexible} + +let detype_sort ~universes ~sorts ~qualities sigma = function | SProp -> glob_SProp_sort | Prop -> glob_Prop_sort | Set -> glob_Set_sort | Type u -> - (if universes - then None, detype_universe sigma u + (if universes then None, detype_universe sigma u else glob_Type_sort) | GSort (q, u) -> let q = Some (GQuality (QGlobal q)) in if universes then q, detype_universe sigma u - else q, UAnonymous {rigid=UState.univ_flexible} + else q, anon_univ | VSort (q, u) -> if universes then let q = if qualities || Evd.is_rigid_qvar sigma q then @@ -293,11 +294,14 @@ let detype_sort ~universes ~qualities sigma = function in q, detype_universe sigma u else if Evd.is_rigid_qvar sigma q then - Some (detype_qvar sigma q), UAnonymous {rigid=UState.univ_flexible} + Some (detype_qvar sigma q), anon_univ + else if sorts then + let q = if qualities then Some (detype_qvar sigma q) else None in + q, anon_univ else glob_Type_sort let detype_sort_f ~flags sigma s = - detype_sort ~universes:flags.flg.universes ~qualities:flags.flg.qualities sigma s + detype_sort ~universes:flags.flg.universes ~sorts:flags.flg.sorts ~qualities:flags.flg.qualities sigma s let detype_relevance_info ~flags sigma na = if not flags.DetypeFlags.relevances then None @@ -740,15 +744,22 @@ type binder_kind = BProd | BLambda | BLetIn (* Main detyping function *) let detype_instance ~flags sigma l = - if not flags.flg.universes then None + if not flags.flg.universes && not flags.flg.sorts then None else let l = EInstance.kind sigma l in if UVars.Instance.is_empty l then None - else + else if flags.flg.universes then let qs, us = UVars.Instance.to_array l in let qs = List.map (detype_quality sigma) (Array.to_list qs) in let us = List.map (detype_level sigma) (Array.to_list us) in Some (qs, us) + else + let qs, us = UVars.Instance.to_array l in + if Array.is_empty qs then None + else + let qs = List.map (detype_quality sigma) (Array.to_list qs) in + let us = List.map (fun _ -> anon_univ) (Array.to_list us) in + Some (qs, us) let delay (type a) (d : a delay) (f : a delay -> _ -> _ -> _ -> _ -> _ -> a glob_constr_r) flags env avoid sigma t : a glob_constr_g = match d with diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 58681f0bd883..19076f353149 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -36,7 +36,7 @@ val detype : 'a delay -> flags:PrintingFlags.Detype.t -> ?isgoal:bool -> ?avoid:'g Namegen.Generator.input -> env -> evar_map -> constr -> 'a glob_constr_g -val detype_sort : universes:bool -> qualities:bool -> evar_map -> Sorts.t -> glob_sort +val detype_sort : universes:bool -> sorts:bool -> qualities:bool -> evar_map -> Sorts.t -> glob_sort val detype_rel_context : 'a delay -> flags:PrintingFlags.Detype.t -> diff --git a/pretyping/printingFlags.ml b/pretyping/printingFlags.ml index ea2bfa5cbb96..c79fed75ffd2 100644 --- a/pretyping/printingFlags.ml +++ b/pretyping/printingFlags.ml @@ -28,6 +28,9 @@ let raw_print = make_flag ["Printing";"All"] false (* XXX why does extern look at this flag? *) let print_universes = make_flag ["Printing";"Universes"] false +(* detyping: like Printing Universes but anonymizes universe variables *) +let print_sorts = make_flag ["Printing";"Sorts"] false + (* detyping *) let { Goptions.get = print_sort_quality } = Goptions.declare_bool_option_and_ref @@ -229,6 +232,7 @@ module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor) module Detype = struct type t = { universes : bool; + sorts : bool; qualities : bool; relevances : bool; evar_instances : bool; @@ -246,6 +250,7 @@ module Detype = struct let current_ignore_raw () = { universes = !print_universes; + sorts = !print_sorts; qualities = print_sort_quality(); relevances = print_relevances(); evar_instances = !print_evar_arguments; diff --git a/pretyping/printingFlags.mli b/pretyping/printingFlags.mli index 4b7c7f2efb57..73d36a3a12ef 100644 --- a/pretyping/printingFlags.mli +++ b/pretyping/printingFlags.mli @@ -11,6 +11,7 @@ module Detype : sig type t = { universes : bool; + sorts : bool; (** Should we print hidden sort quality variables? *) qualities : bool; relevances : bool; @@ -112,8 +113,9 @@ val current : unit -> t val current_ignore_raw : unit -> t -(** The following flag is still accessed directly, but not when printing constr. *) +(** The following flags are still accessed directly, but not when printing constr. *) val print_universes : bool ref +val print_sorts : bool ref module PrintingInductiveMake (_ : sig val encode : Environ.env -> Libnames.qualid -> Names.inductive diff --git a/printing/printer.ml b/printing/printer.ml index 0a7ff287e35f..ceb8291d87b2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -150,11 +150,12 @@ let pr_cases_pattern ?(flags=current_extern()) t = pr_cases_pattern_expr ~flags:ppflags (extern_cases_pattern ~flags Names.Id.Set.empty t) -let pr_sort ?universes ?qualities sigma s = +let pr_sort ?universes ?sorts ?qualities sigma s = let flags = PrintingFlags.Detype.current() in let universes = Option.default flags.universes universes in + let sorts = Option.default flags.sorts sorts in let qualities = Option.default flags.qualities qualities in - pr_sort_expr (extern_sort ~universes ~qualities sigma s) + pr_sort_expr (extern_sort ~universes ~sorts ~qualities sigma s) let () = Termops.Internal.set_print_constr (fun env sigma t -> pr_leconstr_env ~flags:(current_combined()) env sigma t) diff --git a/printing/printer.mli b/printing/printer.mli index b855f8a1e3dc..3f7950df14f2 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -138,7 +138,7 @@ val pr_uninstantiated_constr_pattern_env : ?flags:PrintingFlags.Extern.t -> val pr_cases_pattern : ?flags:PrintingFlags.Extern.t -> cases_pattern -> Pp.t -val pr_sort : ?universes:bool -> ?qualities:bool -> evar_map -> Sorts.t -> Pp.t +val pr_sort : ?universes:bool -> ?sorts:bool -> ?qualities:bool -> evar_map -> Sorts.t -> Pp.t (** Universe constraints *) diff --git a/test-suite/output/PrintingSorts.out b/test-suite/output/PrintingSorts.out new file mode 100644 index 000000000000..d38876e8c124 --- /dev/null +++ b/test-suite/output/PrintingSorts.out @@ -0,0 +1,87 @@ +S + : Type@{s ; _} +T + : Type +S + : Type@{s ; _} +T + : Type +S + : Type@{s ; Set} +T + : Type@{T.u0} +P + : Prop +Q + : Set +R + : SProp +pid + : forall A : Type, A -> A +plist + : Type -> Type +pid + : forall A : Type, A -> A +pid + : forall A : Type, A -> A +plist + : Type -> Type +pnil + : forall A : Type, plist A +pcons + : forall A : Type, A -> plist A -> plist A +pid@{PrintingSorts.39} + : forall A : Type@{PrintingSorts.39}, A -> A +(* {PrintingSorts.39} | +Normalized constraints: + {PrintingSorts.39} | *) +plist@{PrintingSorts.40} + : Type@{PrintingSorts.40} -> Type@{max(Set,PrintingSorts.40)} +(* {PrintingSorts.40} | +Normalized constraints: + {PrintingSorts.40} | *) +spid + : forall A : Type, A -> A +sbox + : Type -> Type +spid@{α12 ; _} + : forall A : Type@{α12 ; _}, A -> A +spid@{α13 ; _} + : forall A : Type@{α13 ; _}, A -> A +sbox@{α14 ; _} + : Type@{α14 ; _} -> Type +spack@{α15 ; _} + : forall A : Type@{α15 ; _}, A -> sbox@{α15 ; _} A +spid@{α16 ; PrintingSorts.56} + : forall A : Type@{α16 ; PrintingSorts.56}, A -> A +(* {α16}; {PrintingSorts.56} | +Collapsed sorts: + α16 := Type +Normalized constraints: + {PrintingSorts.56} | *) +spid@{α17 ; PrintingSorts.57} + : forall A : Type@{α17 ; PrintingSorts.57}, A -> A +(* {α17}; {PrintingSorts.57} | +Collapsed sorts: + α17 := Type +Normalized constraints: + {PrintingSorts.57} | *) +sbox@{α18 ; PrintingSorts.58} + : Type@{α18 ; PrintingSorts.58} -> Type@{PrintingSorts.58} +(* {α18}; {PrintingSorts.58} | +Collapsed sorts: + α18 := Type +Normalized constraints: + {PrintingSorts.58} | *) +spack@{α19 ; PrintingSorts.59} + : forall A : Type@{α19 ; PrintingSorts.59}, + A -> sbox@{α19 ; PrintingSorts.59} A +(* {α19}; {PrintingSorts.59} | +Collapsed sorts: + α19 := Type +Normalized constraints: + {PrintingSorts.59} | *) +spid@{Prop ; _} + : forall A : Prop, A -> A +spid@{Type ; _} + : forall A : Set, A -> A diff --git a/test-suite/output/PrintingSorts.v b/test-suite/output/PrintingSorts.v new file mode 100644 index 000000000000..30c442cbf3fb --- /dev/null +++ b/test-suite/output/PrintingSorts.v @@ -0,0 +1,79 @@ +Sort s. +Axiom S : Type@{s;Set}. +Axiom T : Type. + +(* Without Printing Sorts or Printing Universes *) +Check S. +Check T. + +(* With Printing Sorts: sort variables visible, universe levels anonymized *) +Set Printing Sorts. +Check S. +Check T. +Unset Printing Sorts. + +(* With Printing Universes: full names *) +Set Printing Universes. +Check S. +Check T. +Unset Printing Universes. + +(* Set, Prop, SProp still print as usual with Printing Sorts on, + not as Type@{Prop ; _} or similar *) +Axiom P : Prop. +Axiom Q : Set. +Axiom R : SProp. + +Set Printing Sorts. +Check P. +Check Q. +Check R. +Unset Printing Sorts. + +(* Universe-polymorphic definitions and inductives *) +#[universes(polymorphic)] Definition pid@{u} (A : Type@{u}) (a : A) := a. +#[universes(polymorphic)] Inductive plist@{u} (A : Type@{u}) := pnil | pcons (a : A) (l : plist A). + +Check pid. +Check plist. + +Set Printing Sorts. +Check pid. +Check @pid. +Check plist. +Check pnil. +Check pcons. +Unset Printing Sorts. + +Set Printing Universes. +Check pid. +Check plist. +Unset Printing Universes. + +(* Sort-polymorphic definitions and inductives *) +#[universes(polymorphic)] Definition spid@{s;u} (A : Type@{s;u}) (a : A) := a. +#[universes(polymorphic)] Inductive sbox@{s;u} (A : Type@{s;u}) := spack (a : A). + +Check spid. +Check sbox. + +Set Printing Sorts. +Check spid. +Check @spid. +Check sbox. +Check spack. +Unset Printing Sorts. + +Set Printing Universes. +Check spid. +Check @spid. +Check sbox. +Check spack. +Unset Printing Universes. + +(* Instances at concrete qualities: the quality shows in the instance, + but the sorts in the type still print as usual *) +Set Printing Sorts. +Check spid@{Prop;Set}. +Check spid@{Type;Set}. +Unset Printing Sorts. From 531aa6ccd89b7c74ab0ce1f9cdf32ba90a8b54d3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 27 Jul 2026 03:13:08 +0000 Subject: [PATCH 3/4] Add Set Printing Sort Quality Variables Anonymously MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- .../22310-printing-anon-qvars-Added.rst | 7 +++ doc/sphinx/addendum/universe-polymorphism.rst | 10 ++++ doc/sphinx/language/core/sorts.rst | 1 + doc/tools/docgram/common.edit_mlg | 1 + doc/tools/docgram/fullGrammar | 1 + doc/tools/docgram/orderedGrammar | 1 + interp/constrextern.ml | 50 +++++++++++-------- interp/constrextern.mli | 2 +- parsing/g_constr.mlg | 9 ++++ pretyping/printingFlags.ml | 12 +++++ pretyping/printingFlags.mli | 3 ++ printing/printer.ml | 6 ++- printing/printer.mli | 2 +- test-suite/output/PrintingAnonQVars.out | 30 +++++++++++ test-suite/output/PrintingAnonQVars.v | 27 ++++++++++ 15 files changed, 137 insertions(+), 25 deletions(-) create mode 100644 doc/changelog/08-vernac-commands-and-options/22310-printing-anon-qvars-Added.rst create mode 100644 test-suite/output/PrintingAnonQVars.out create mode 100644 test-suite/output/PrintingAnonQVars.v diff --git a/doc/changelog/08-vernac-commands-and-options/22310-printing-anon-qvars-Added.rst b/doc/changelog/08-vernac-commands-and-options/22310-printing-anon-qvars-Added.rst new file mode 100644 index 000000000000..3ae41028e8f7 --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/22310-printing-anon-qvars-Added.rst @@ -0,0 +1,7 @@ +- **Added:** + flag ``Printing Sort Quality Variables Anonymously``, which prints + sort quality variables that cannot be referred to by name as ``_`` + (which can be parsed back, denoting a fresh quality variable) + instead of their raw ``α``-names (which cannot) + (`#22310 `_, + written by Claude (Anthropic), for Jason Gross). diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 3cd17f68d2fe..062dad942c38 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -1045,6 +1045,16 @@ It means that `s` and `s'` can respectively be instantiated to e.g., `Type` and become at the end of the definition unless it is unified with another rigid quality). +.. flag:: Printing Sort Quality Variables Anonymously + + When this :term:`flag` is on (it is off by default), sort quality + variables that cannot be referred to by name are printed as ``_`` + (which, when parsed back, denotes a fresh quality variable) instead + of their raw representation — ``α`` followed by a number — which + cannot be parsed back. Quality variables that have a name (such as + the ``s`` of a ``@{s;u}`` universe declaration, in contexts where it + is bound) are printed by name as usual. + Explicit Sorts --------------- diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst index 23d2bb4a6f4e..6035911b254e 100644 --- a/doc/sphinx/language/core/sorts.rst +++ b/doc/sphinx/language/core/sorts.rst @@ -18,6 +18,7 @@ Sorts | Type | Type @%{ _ %} | Type @%{ {? @qualid {| %| | ; } } @universe %} + | Type @%{ _ ; @universe %} universe ::= max ( {+, @universe_expr } ) | _ | @universe_expr diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index f77ad63b4829..9139c5b1a39f 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -170,6 +170,7 @@ DELETE: [ | test_leftsquarebracket_equal | test_old_sort_qvar | test_sort_qvar +| test_sort_anon_qvar | test_ltac2_ident | test_doublepipe_univ_decl | test_doublepipe_cumul_univ_decl diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index a8310f63de8c..4821e02b9716 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -29,6 +29,7 @@ sort: [ | "Type" "@{" "_" "}" | "Type" "@{" test_old_sort_qvar reference "|" universe "}" | "Type" "@{" test_sort_qvar reference ";" universe "}" +| "Type" "@{" test_sort_anon_qvar "_" ";" universe "}" | "Type" "@{" universe "}" ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index a88d50b82330..b254ff8589af 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -285,6 +285,7 @@ sort: [ | "Type" | "Type" "@{" "_" "}" | "Type" "@{" OPT [ qualid [ "|" | ";" ] ] universe "}" +| "Type" "@{" "_" ";" universe "}" ] universe: [ diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 75da90654218..37475a6e9840 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -787,36 +787,44 @@ let extern_glob_sort_name uvars = function | None -> CRawType u end -let extern_glob_quality uvars = function +let extern_glob_quality ~anon uvars = function | GLocalQVar {v=Anonymous;loc} -> CQAnon loc | GLocalQVar {v=Name id; loc} -> CQVar (qualid_of_ident ?loc id) | GRawQVar q -> CRawQuality (QVar q) | GQuality q -> begin match UnivNames.qualid_of_quality uvars q with | Some qid -> CQVar qid - | None -> CRawQuality q + | None -> + (* A quality variable with no name has no parsable form; print it + as "_" (a fresh quality variable when parsed back) when + [anon]. *) + match q with + | QVar _ when anon -> CQAnon None + | _ -> CRawQuality q end -let extern_relevance uvars = function +let extern_relevance ~anon uvars = function | GRelevant -> CRelevant | GIrrelevant -> CIrrelevant - | GRelevanceVar q -> CRelevanceVar (extern_glob_quality uvars q) + | GRelevanceVar q -> CRelevanceVar (extern_glob_quality ~anon uvars q) -let extern_relevance_info uvars = Option.map (extern_relevance uvars) +let extern_relevance_info ~anon uvars = Option.map (extern_relevance ~anon uvars) -let extern_glob_sort uvars (q, l) = - Option.map (extern_glob_quality uvars) q, +let extern_glob_sort ~anon uvars (q, l) = + Option.map (extern_glob_quality ~anon uvars) q, map_glob_sort_gen (List.map (on_fst (extern_glob_sort_name uvars))) l -let extern_instance uvars = function +let extern_instance ~anon uvars = function | Some (ql,ul) -> - let ql = List.map (extern_glob_quality uvars) ql in + let ql = List.map (extern_glob_quality ~anon uvars) ql in let ul = List.map (map_glob_sort_gen (extern_glob_sort_name uvars)) ul in Some (ql,ul) | None -> None -let extern_ref {vars; uvars} ref us = +let anon_qvars eenv = eenv.flags.ExternFlags.anonymous_qvars + +let extern_ref ({vars; uvars; _} as eenv) ref us = extern_global (select_stronger_impargs (implicits_of_global ref)) - (extern_reference vars ref) (extern_instance uvars us) + (extern_reference vars ref) (extern_instance ~anon:(anon_qvars eenv) uvars us) let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) @@ -926,7 +934,7 @@ let rec extern depth0 inctx scopes (eenv:extern_env) r = (* Otherwise... *) extern_applied_ref ~flags inctx (select_stronger_impargs (implicits_of_global ref)) - (ref,extern_reference ?loc eenv.vars ref) (extern_instance eenv.uvars us) args) + (ref,extern_reference ?loc eenv.vars ref) (extern_instance ~anon:(anon_qvars eenv) eenv.uvars us) args) | GProj (f,params,c) -> extern_applied_proj depth inctx scopes eenv f params c args | _ -> @@ -1030,7 +1038,7 @@ let rec extern depth0 inctx scopes (eenv:extern_env) r = in CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl)) - | GSort s -> CSort (extern_glob_sort eenv.uvars s) + | GSort s -> CSort (extern_glob_sort ~anon:(anon_qvars eenv) eenv.uvars s) | GHole e -> CHole (Some e) @@ -1056,7 +1064,7 @@ let rec extern depth0 inctx scopes (eenv:extern_env) r = | GArray(u,t,def,ty) -> CArray( - extern_instance eenv.uvars u, + extern_instance ~anon:(anon_qvars eenv) eenv.uvars u, Array.map (extern depth inctx scopes eenv) t, extern depth inctx scopes eenv def, extern_typ depth scopes eenv ty) @@ -1070,7 +1078,7 @@ and sub_extern depth inctx (subentry,(_,scopes)) = extern depth inctx (subentry, and factorize_prod depth scopes eenv na r bk t c = let implicit_type = is_reserved_type ~flags:eenv.flags na t in - let r = extern_relevance_info eenv.uvars r in + let r = extern_relevance_info ~anon:(anon_qvars eenv) eenv.uvars r in let aty = extern_typ depth scopes eenv t in let eenv = add_vname eenv na in let store, get = set_temporary_memory () in @@ -1107,7 +1115,7 @@ and factorize_prod depth scopes eenv na r bk t c = and factorize_lambda depth inctx scopes eenv na r bk t c = let implicit_type = is_reserved_type ~flags:eenv.flags na t in - let r = extern_relevance_info eenv.uvars r in + let r = extern_relevance_info ~anon:(anon_qvars eenv) eenv.uvars r in let aty = extern_typ depth scopes eenv t in let eenv = add_vname eenv na in let store, get = set_temporary_memory () in @@ -1150,7 +1158,7 @@ and extern_local_binder depth scopes eenv = function let (assums,ids,l) = extern_local_binder depth scopes (on_eenv_vars (Name.fold_right Id.Set.add na) eenv) l in (assums,na::ids, - CLocalDef(CAst.make na, extern_relevance_info eenv.uvars r, extern depth false scopes eenv bd, + CLocalDef(CAst.make na, extern_relevance_info ~anon:(anon_qvars eenv) eenv.uvars r, extern depth false scopes eenv bd, Option.map (extern_typ depth scopes eenv) ty) :: l) | GLocalAssum (na,r,bk,ty) -> @@ -1167,7 +1175,7 @@ and extern_local_binder depth scopes eenv = function | (assums,ids,l) -> let ty = if implicit_type then hole else ty in (na::assums,na::ids, - CLocalAssum([CAst.make na],extern_relevance_info eenv.uvars r,Default bk,ty) :: l)) + CLocalAssum([CAst.make na],extern_relevance_info ~anon:(anon_qvars eenv) eenv.uvars r,Default bk,ty) :: l)) | GLocalPattern ((p,_),_,bk,_) -> let p = mkCPatOr (List.map (extern_cases_pattern ~flags:eenv.flags eenv.vars) p) in @@ -1305,7 +1313,7 @@ and extern_applied_proj depth inctx scopes eenv (cst,us) params c extraargs = let args = extern_args (extern depth true) eenv args in let imps = select_stronger_impargs (implicits_of_global ref) in let f = extern_reference eenv.vars ref in - let us = extern_instance eenv.uvars us in + let us = extern_instance ~anon:(anon_qvars eenv) eenv.uvars us in extern_projection ~flags:eenv.flags inctx (f,us) nparams args imps let extern inctx scopes eenv c : constr_expr = extern (init_depth eenv.flags) inctx scopes eenv c @@ -1346,8 +1354,8 @@ let extern_type ?(goal_concl_style=false) ~(flags:PrintingFlags.t) env sigma ?im let r = Detyping.detype Detyping.Later ~isgoal:goal_concl_style ~avoid ~flags:flags.detype env sigma t in extern_glob_type ?impargs (extern_env ~flags:flags.extern env sigma) r -let extern_sort ~universes ~sorts ~qualities sigma s = - extern_glob_sort (Evd.universe_binders sigma) +let extern_sort ~universes ~sorts ~qualities ~anonymous_qvars sigma s = + extern_glob_sort ~anon:anonymous_qvars (Evd.universe_binders sigma) (detype_sort ~universes ~sorts ~qualities sigma s) let extern_closed_glob ?(goal_concl_style=false) ?(inctx=false) ?scope ~(flags:PrintingFlags.t) env sigma t = diff --git a/interp/constrextern.mli b/interp/constrextern.mli index aadf473e9d13..0b3120f584f3 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -53,7 +53,7 @@ val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val extern_type : ?goal_concl_style:bool -> flags:PrintingFlags.t -> env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> types -> constr_expr -val extern_sort : universes:bool -> sorts:bool -> qualities:bool -> Evd.evar_map -> Sorts.t -> sort_expr +val extern_sort : universes:bool -> sorts:bool -> qualities:bool -> anonymous_qvars:bool -> Evd.evar_map -> Sorts.t -> sort_expr val extern_rel_context : flags:PrintingFlags.t -> env -> Evd.evar_map -> rel_context -> local_binder_expr list diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 48811ac6efb1..4d99293a5bd3 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -92,6 +92,12 @@ let test_sort_qvar = lk_ident >> lk_list lk_field >> lk_kw ";" end +let test_sort_anon_qvar = + let open Procq.Lookahead in + to_entry "test_sort_anon_qvar" begin + lk_kw "_" >> lk_kw ";" + end + let test_record_nowith = let open Procq.Lookahead in to_entry "test_record_nowith" begin @@ -163,6 +169,9 @@ GRAMMAR EXTEND Gram | "Type"; "@{"; test_sort_qvar; q = reference; ";"; u = universe; "}" -> { Some (CQVar q), u } + | "Type"; "@{"; test_sort_anon_qvar; "_"; ";"; u = universe; "}" -> { + Some (CQAnon (Some loc)), u + } | "Type"; "@{"; u = universe; "}" -> { None, u } ] ] ; sort_quality_or_set: diff --git a/pretyping/printingFlags.ml b/pretyping/printingFlags.ml index c79fed75ffd2..ed933a3b2956 100644 --- a/pretyping/printingFlags.ml +++ b/pretyping/printingFlags.ml @@ -38,6 +38,13 @@ let { Goptions.get = print_sort_quality } = ~value:true () +(* extern *) +let { Goptions.get = print_anonymous_qvars } = + Goptions.declare_bool_option_and_ref + ~key:["Printing";"Sort";"Quality";"Variables";"Anonymously"] + ~value:false + () + (* detyping *) let print_evar_arguments = make_flag ["Printing";"Existential";"Instances"] false @@ -345,6 +352,9 @@ module Extern = struct coercions : bool; parentheses : bool; notations : bool; + (* Print sort quality variables that have no name as "_" instead of + their raw (unparsable) α-names *) + anonymous_qvars : bool; raw_literals : bool; projections : bool; float : bool; @@ -361,6 +371,7 @@ module Extern = struct coercions = !print_coercions; parentheses = !print_parentheses; notations = not !print_no_symbol; + anonymous_qvars = print_anonymous_qvars(); raw_literals = !print_raw_literal; projections = !print_projections; float = print_float(); @@ -377,6 +388,7 @@ module Extern = struct coercions = true; raw_literals = true; notations = false; + anonymous_qvars = false; projections = false; factorize_eqns = FactorizeEqns.make_raw flags.factorize_eqns; } diff --git a/pretyping/printingFlags.mli b/pretyping/printingFlags.mli index 73d36a3a12ef..a28aa5dcf78a 100644 --- a/pretyping/printingFlags.mli +++ b/pretyping/printingFlags.mli @@ -84,6 +84,9 @@ module Extern : sig coercions : bool; parentheses : bool; notations : bool; + (** Print sort quality variables that have no name as ["_"] instead + of their raw (unparsable) α-names. *) + anonymous_qvars : bool; (* primitive tokens, like strings *) raw_literals : bool; (* This governs printing of projections using the dot notation symbols *) diff --git a/printing/printer.ml b/printing/printer.ml index ceb8291d87b2..a97da2e37903 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -150,12 +150,14 @@ let pr_cases_pattern ?(flags=current_extern()) t = pr_cases_pattern_expr ~flags:ppflags (extern_cases_pattern ~flags Names.Id.Set.empty t) -let pr_sort ?universes ?sorts ?qualities sigma s = +let pr_sort ?universes ?sorts ?qualities ?anonymous_qvars sigma s = let flags = PrintingFlags.Detype.current() in let universes = Option.default flags.universes universes in let sorts = Option.default flags.sorts sorts in let qualities = Option.default flags.qualities qualities in - pr_sort_expr (extern_sort ~universes ~sorts ~qualities sigma s) + let anonymous_qvars = + Option.default (current_extern()).PrintingFlags.Extern.anonymous_qvars anonymous_qvars in + pr_sort_expr (extern_sort ~universes ~sorts ~qualities ~anonymous_qvars sigma s) let () = Termops.Internal.set_print_constr (fun env sigma t -> pr_leconstr_env ~flags:(current_combined()) env sigma t) diff --git a/printing/printer.mli b/printing/printer.mli index 3f7950df14f2..8f572d49afb8 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -138,7 +138,7 @@ val pr_uninstantiated_constr_pattern_env : ?flags:PrintingFlags.Extern.t -> val pr_cases_pattern : ?flags:PrintingFlags.Extern.t -> cases_pattern -> Pp.t -val pr_sort : ?universes:bool -> ?sorts:bool -> ?qualities:bool -> evar_map -> Sorts.t -> Pp.t +val pr_sort : ?universes:bool -> ?sorts:bool -> ?qualities:bool -> ?anonymous_qvars:bool -> evar_map -> Sorts.t -> Pp.t (** Universe constraints *) diff --git a/test-suite/output/PrintingAnonQVars.out b/test-suite/output/PrintingAnonQVars.out new file mode 100644 index 000000000000..176cf44ab90b --- /dev/null +++ b/test-suite/output/PrintingAnonQVars.out @@ -0,0 +1,30 @@ +idT@{α2 ; PrintingAnonQVars.22} + : forall A : Type@{α2 ; PrintingAnonQVars.22}, A -> A +(* {α2}; {PrintingAnonQVars.22} | +Collapsed sorts: + α2 := Type +Normalized constraints: + {PrintingAnonQVars.22} | *) +idT@{_ ; PrintingAnonQVars.23} + : forall A : Type@{_ ; PrintingAnonQVars.23}, A -> A +(* {α3}; {PrintingAnonQVars.23} | +Collapsed sorts: + α3 := Type +Normalized constraints: + {PrintingAnonQVars.23} | *) +idT@{s ; u} = +fun (A : Type@{s ; _}) (a : A) => a + : forall A : Type@{s ; _}, A -> A + +Arguments idT A%_type_scope a +idT@{s ; u} : forall A : Type@{s ; _}, A -> A + +idT is universe polymorphic +Arguments idT A%_type_scope a +idT is transparent +Expands to: Constant PrintingAnonQVars.idT +Declared in library PrintingAnonQVars, line 5, characters 11-14 +Type + : Type +idT + : forall A : Type, A -> A diff --git a/test-suite/output/PrintingAnonQVars.v b/test-suite/output/PrintingAnonQVars.v new file mode 100644 index 000000000000..28c994a889f1 --- /dev/null +++ b/test-suite/output/PrintingAnonQVars.v @@ -0,0 +1,27 @@ +(* Printing Sort Quality Variables Anonymously: sort quality variables + that have no name print as "_" (which parses back, denoting a fresh + quality variable) instead of their raw α-names (which do not). *) +Set Universe Polymorphism. +Definition idT@{s;u} (A : Type@{s;u}) (a : A) := a. + +(* Under Printing Universes, the fresh quality variable of the + instance (and of the displayed sort) prints as a raw α-name by + default... *) +Set Printing Universes. +Check idT. +(* ...and as _ under the flag. *) +Set Printing Sort Quality Variables Anonymously. +Check idT. +Unset Printing Universes. + +(* Named quality variables are unaffected: the binder name is kept. *) +Print idT. +About idT. + +Unset Printing Sort Quality Variables Anonymously. + +(* The anonymous form parses back: "_" is accepted as the sort quality + of a sort annotation (it was already accepted in universe + instances), denoting a fresh quality variable. *) +Check Type@{_ ; Set}. +Check idT@{_ ; Set}. From 014a05e7e6acf1cd111b5797d59736763362f3df Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 27 Jul 2026 04:33:13 +0000 Subject: [PATCH 4/4] Integrate sort printing and anonymous quality variables into the reversible-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 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- printing/reversiblePrinting.ml | 34 +++++++++++++++++------- test-suite/output/ReversiblePrinting.out | 18 ++++++++----- test-suite/output/ReversiblePrinting.v | 26 +++++++++++++++++- 3 files changed, 60 insertions(+), 18 deletions(-) diff --git a/printing/reversiblePrinting.ml b/printing/reversiblePrinting.ml index 3895c19d8713..8bf00f93fbc8 100644 --- a/printing/reversiblePrinting.ml +++ b/printing/reversiblePrinting.ml @@ -102,22 +102,32 @@ let warn_not_reversible = let lconstr_eoi = Procq.eoi_entry Procq.Constr.lconstr (* Successively more explicit printing flags: coercions, implicit - arguments, no notations, universes (first with, then without - notations), parentheses, ending with the equivalent of - [Printing All] plus [Printing Universes] and [Printing - Parentheses]. Unsetting notations is tried after implicit arguments - and before universes, but is not kept when escalating to universes: - configurations are ordered by explicitness, not included in each - other. Only extern/detype-level flags and the [parentheses] flag may - vary along the ladder: the rendering of the returned [constr_expr] - must be fully determined by the returned flags (see - [Ppconstr.of_printing_flags]). *) + arguments, sorts, no notations, universes, parentheses, ending with + the equivalent of [Printing All] plus [Printing Universes] and + [Printing Parentheses]. Sorts are tried right after implicit + arguments; the next rung additionally prints sort quality variables + anonymously, because an unnamed quality variable otherwise prints as + a raw α-name that cannot be reparsed, whereas [_] reparses to a fresh + quality variable that unification can match. Unsetting notations is + tried after sorts and before universes. At each universes rung, + anonymous quality variables are tried first and then without them, in + case anonymizing a quality variable is itself what breaks reparsing. + Configurations are ordered by explicitness, not included in each + other: notations are not kept off once universes are shown, and + [anonymous_qvars] is turned back off whenever it did not help. Raw + printing stays faithful, with [anonymous_qvars] off. Only + extern/detype-level flags and the [parentheses] flag may vary along + the ladder: the rendering of the returned [constr_expr] must be fully + determined by the returned flags (see [Ppconstr.of_printing_flags]). *) let ladder flags = let open PrintingFlags in let e0 = flags.extern in let e1 = { e0 with Extern.coercions = true } in let e2 = { e1 with Extern.implicits = true; Extern.implicits_defensive = true } in + let e2a = { e2 with Extern.anonymous_qvars = true } in let e3 = { e2 with Extern.notations = false } in + let e3a = { e3 with Extern.anonymous_qvars = true } in + let ds = { flags.detype with Detype.sorts = true } in let d4 = { flags.detype with Detype.universes = true } in let e5 = { e3 with Extern.parentheses = true } in let raw = make_raw flags in @@ -126,8 +136,12 @@ let ladder flags = [ flags; { flags with extern = e1 }; { flags with extern = e2 }; + { detype = ds; extern = e2 }; + { detype = ds; extern = e2a }; { flags with extern = e3 }; + { detype = d4; extern = e2a }; { detype = d4; extern = e2 }; + { detype = d4; extern = e3a }; { detype = d4; extern = e3 }; { detype = d4; extern = e5 }; raw ] diff --git a/test-suite/output/ReversiblePrinting.out b/test-suite/output/ReversiblePrinting.out index db216c41f3d7..b619ba54340d 100644 --- a/test-suite/output/ReversiblePrinting.out +++ b/test-suite/output/ReversiblePrinting.out @@ -26,11 +26,11 @@ Warning: The printed form of this term could not be re-parsed and re-elaborated to an equal term (up to conversion modulo universe unification), even with all printing options turned on. [reversible-printing,default] -Type@{ReversiblePrinting.47} - : Type@{ReversiblePrinting.47+1} +Type@{ReversiblePrinting.51} + : Type@{ReversiblePrinting.51+1} pid : forall A : Type, A -> A -idT@{Prop ; Set} +idT@{Prop ; _} : forall A : Prop, A -> A idT : forall A : Prop, A -> A @@ -46,17 +46,21 @@ eq_refl : nat Nat.add 2 3 : nat +idT@{Prop ; _} + : forall A : Prop, A -> A +idT@{_ ; _} + : forall A : Type@{_ ; _}, A -> A 1 goal ============================ @eq_refl nat 0 = @eq_refl nat 0 -File "./output/ReversiblePrinting.v", line 106, characters 0-11: +File "./output/ReversiblePrinting.v", line 130, characters 0-11: Warning: The printed form of this term could not be re-parsed and re-elaborated to an equal term (up to conversion), even with all printing options turned on. [reversible-printing,default] -File "./output/ReversiblePrinting.v", line 106, characters 0-11: +File "./output/ReversiblePrinting.v", line 130, characters 0-11: Warning: The printed form of this term could not be re-parsed and re-elaborated to an equal term (up to conversion), even with all printing options turned on. [reversible-printing,default] -Type@{ReversiblePrinting.88} - : Type@{ReversiblePrinting.88+1} +Type@{ReversiblePrinting.100} + : Type@{ReversiblePrinting.100+1} diff --git a/test-suite/output/ReversiblePrinting.v b/test-suite/output/ReversiblePrinting.v index 0dcd10a14dc5..fd8e463dfb6f 100644 --- a/test-suite/output/ReversiblePrinting.v +++ b/test-suite/output/ReversiblePrinting.v @@ -56,7 +56,10 @@ Check pid@{u}. though universe levels need not. [idT] is polymorphic over a sort quality [s]; used at [Prop], its printed form must keep the sort instance, because dropping it re-elaborates [idT] at a fresh quality - (defaulting to [Type], quality [QType]) which differs from [Prop]. *) + (defaulting to [Type], quality [QType]) which differs from [Prop]. + The sort rung supplies the instance at sort level ([idT@{Prop ; _}], + universe hidden), which already re-parses, so escalating to the full + universe instance is not needed. *) Set Universe Polymorphism. Definition idT@{s;u} (A : Type@{s;u}) (a : A) := a. Set Printing Reversible Up To Conversion Modulo Universes. @@ -94,6 +97,27 @@ Module LyingNotation. Check 2 + 3. End LyingNotation. +(* Sort printing composes with the ladder. With sort printing on, the + instance of a sort-polymorphic constant used at a concrete quality is + shown at sort level ([Prop], with the universe hidden as [_]); this + re-parses (an instance accepts [_] in universe position), so no + escalation or warning is needed. *) +Set Printing Reversible Up To Unification. +Set Printing Sorts. +Check idT@{Prop;Set}. +(* A bare sort-polymorphic constant exposes a sort quality *variable*, + which prints by default as a raw, unparsable alpha-name. The ladder's + anonymous rung prints it as [_] instead, both in the instance + ([idT@{_ ; _}]) and inside the type's sort annotation + ([Type@{_ ; _}]); the quality [_] re-parses to a fresh quality + variable and the universe [_] to a fresh universe, both of which + unification matches, so the whole term round-trips with no warning. + (The [_] quality in a *sort annotation* parses thanks to the grammar + extension this stack adds; without it the type would not re-parse and + the check would escalate and warn.) *) +Check idT. +Unset Printing Sorts. + (* Goal display is checked too. *) Set Printing Reversible Up To Conversion. Goal @eq_refl nat 0 = eq_refl.