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/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/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 b571197c418e..062dad942c38 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 @@ -1033,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/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/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 310792fd2010..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,9 +1354,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 = - extern_glob_sort (Evd.universe_binders sigma) - (detype_sort ~universes ~qualities sigma s) +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 = let avoid = make_avoid goal_concl_style env in diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 8bf6b3fe1cd7..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 -> 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/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..ed933a3b2956 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 @@ -35,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 @@ -229,6 +239,7 @@ module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor) module Detype = struct type t = { universes : bool; + sorts : bool; qualities : bool; relevances : bool; evar_instances : bool; @@ -246,6 +257,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; @@ -340,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; @@ -356,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(); @@ -372,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 4b7c7f2efb57..a28aa5dcf78a 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; @@ -83,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 *) @@ -112,8 +116,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 8379352eca6a..a97da2e37903 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) @@ -131,11 +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 ?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 ~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 b855f8a1e3dc..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 -> ?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/printing/reversiblePrinting.ml b/printing/reversiblePrinting.ml new file mode 100644 index 000000000000..8bf00f93fbc8 --- /dev/null +++ b/printing/reversiblePrinting.ml @@ -0,0 +1,300 @@ +(************************************************************************) +(* * 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, 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 + 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 }; + { 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 ] + +(* 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/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}. 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. diff --git a/test-suite/output/ReversiblePrinting.out b/test-suite/output/ReversiblePrinting.out new file mode 100644 index 000000000000..b619ba54340d --- /dev/null +++ b/test-suite/output/ReversiblePrinting.out @@ -0,0 +1,66 @@ +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.51} + : Type@{ReversiblePrinting.51+1} +pid + : forall A : Type, A -> A +idT@{Prop ; _} + : 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 +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 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 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.100} + : Type@{ReversiblePrinting.100+1} diff --git a/test-suite/output/ReversiblePrinting.v b/test-suite/output/ReversiblePrinting.v new file mode 100644 index 000000000000..fd8e463dfb6f --- /dev/null +++ b/test-suite/output/ReversiblePrinting.v @@ -0,0 +1,130 @@ +(* 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]. + 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. +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. + +(* 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. +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.