From 92a059026329cf98f3286e0f72ec30c0f411ad45 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 14 Jun 2024 14:40:29 +0200 Subject: [PATCH] About: print information about squashing of inductives --- test-suite/output/Inductive.out | 39 +++++++++++++++++++++++++ test-suite/output/Inductive.v | 27 +++++++++++++++++ vernac/prettyp.ml | 52 +++++++++++++++++++++++++++++++++ 3 files changed, 118 insertions(+) diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 0167f085fa36..01248d6cf834 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -32,3 +32,42 @@ The command has indeed failed with message: Parameters should be syntactically the same for each record type. Type "B" has no parameters but type "Inductive" has parameters "A". +or : Prop -> Prop -> Prop + +or is not universe polymorphic +or may only be eliminated to produce values whose type is SProp or Prop. +Arguments or (A B)%type_scope +Expands to: Inductive Coq.Init.Logic.or +sunit : SProp + +sunit is not universe polymorphic +sunit may only be eliminated to produce values whose type is SProp. +Expands to: Inductive Inductive.sunit +sempty@{q | } : Type@{q | Set} +(* q | |= *) + +sempty is universe polymorphic +sempty@{q | } may only be eliminated to produce values whose type is in sort quality q, + unless instantiated such that the quality SProp + is equal to the instantiation of q, + or to Prop or Type if q is instantiated to Type. +Expands to: Inductive Inductive.sempty +ssig@{q1 q2 q3 | a b} : +forall A : Type@{q1 | a}, (A -> Type@{q2 | b}) -> Type@{q3 | max(a,b)} +(* q1 q2 q3 | a b |= *) + +ssig is universe polymorphic +ssig@{q1 q2 q3 | a b} may only be eliminated to produce values whose type is in sort quality q3, + unless instantiated such that the qualities q1, q2 and Prop + are equal to the instantiation of q3, + or to Prop or Type if q3 is instantiated to Type. +Arguments ssig A%type_scope B%function_scope +Expands to: Inductive Inductive.ssig +BoxP@{q | a} : Type@{q | a} -> Prop +(* q | a |= *) + +BoxP is universe polymorphic +BoxP@{q | a} may only be eliminated to produce values whose type is SProp or Prop, + unless instantiated such that the quality q is SProp or Prop. +Arguments BoxP A%type_scope +Expands to: Inductive Inductive.BoxP diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v index d96774aad3d3..2abc434402eb 100644 --- a/test-suite/output/Inductive.v +++ b/test-suite/output/Inductive.v @@ -29,3 +29,30 @@ Module DiffParams. Fail Inductive B := { x : nat } with Inductive A := { y : nat }. End DiffParams. + +(* print squash info + (can't test impredicative set squashes in this file) *) + +About or. + +Inductive sunit : SProp := stt. + +About sunit. + +Set Universe Polymorphism. + +Polymorphic Inductive sempty@{q| |} : Type@{q|Set} := . + +About sempty. + +Polymorphic Inductive ssig@{q1 q2 q3|a b|} + (A:Type@{q1|a}) + (B:A -> Type@{q2|b}) + : Type@{q3|max(a,b)} + := sexist (a:A) (b:B a). + +About ssig. + +Polymorphic Inductive BoxP@{q|a|} (A:Type@{q|a}) : Prop := boxP (_:A). + +About BoxP. diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index b3990370cf4a..78f64319d60e 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -208,6 +208,57 @@ let print_polymorphism env ref = ++ if !Detyping.print_universes then h (pr_template_variables template_variables) else mt() else str "not universe polymorphic") ] +let print_squash env ref udecl = match ref with + | GlobRef.IndRef ind -> + let _, mip = Inductive.lookup_mind_specif env ind in + begin match mip.mind_squashed with + | None -> [] + | Some squash -> + let univs = Environ.universes_of_global env ref in + let bl = Printer.universe_binders_with_opt_names univs udecl in + let sigma = Evd.from_ctx (UState.of_names bl) in + let inst = if fst @@ UVars.AbstractContext.size univs = 0 then mt() + else Printer.pr_universe_instance sigma (UVars.make_abstract_instance univs) + in + let inds = match mip.mind_arity with + | TemplateArity _ -> assert false + | RegularArity a -> a.mind_sort + in + let target = match inds with + | SProp -> str "SProp" + | Prop -> str "SProp or Prop" + | Set -> str "SProp, Prop or Set" + | Type _ -> str "not in a variable sort quality" + | QSort (q,_) -> str "in sort quality " ++ Termops.pr_evd_qvar sigma q + in + let unless = match squash with + | AlwaysSquashed -> str "." + | SometimesSquashed qs -> + let target = match inds with + | SProp | Prop | Set -> target + | Type _ -> str "instantiated to constant qualities" + | QSort (q,_) -> + let ppq = Termops.pr_evd_qvar sigma q in + str "equal to the instantiation of " ++ ppq ++ pr_comma() ++ + str "or to Prop or Type if " ++ ppq ++ str " is instantiated to Type" + in + let qs = Sorts.Quality.Set.elements qs in + let quality_s, is_s = match qs with + | [_] -> "quality", "is" + | _ -> "qualities", "are" + in + (* this reads kinda weird when qs is singleton of a constant quality, we get eg + "quality Prop is equal to the instantiation of q" *) + pr_comma () ++ + hov 0 (str "unless instantiated such that the " ++ str quality_s ++ str " " ++ + pr_enum (Sorts.Quality.pr (Termops.pr_evd_qvar sigma)) qs ++ + spc() ++ str is_s ++ str " " ++ target ++ str ".") + in + [hv 2 (hov 1 (pr_global ref ++ inst) ++ str " may only be eliminated to produce values whose type is " ++ + target ++ unless)] + end + | _ -> [] + let print_prop_but_default_dep_elim ref = match ref with | GlobRef.IndRef ind -> @@ -950,6 +1001,7 @@ let print_about_global_reference ?loc env ref udecl = pr_infos_list (print_ref env false ref udecl :: blankline :: print_polymorphism env ref @ + print_squash env ref udecl @ print_name_infos env ref @ print_reduction_behaviour ref @ print_opacity env ref @