Merge PR #17836: Kernel sort polymorphism

Reviewed-by: ppedrot
Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: silene
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

checker/checkInductive.ml

@@ -12,6 +12,7 @@ open Declarations
 open Environ
 open Names
 open Univ
+open UVars
 open Util
 
 [@@@ocaml.warning "+9+27"]
@@ -181,7 +182,7 @@ let check_inductive env mind mb =
   check "mind_finite" (mb.mind_finite == mind_finite);
   check "mind_ntypes" Int.(equal mb.mind_ntypes mind_ntypes);
   check "mind_hyps" (List.is_empty mind_hyps);
-  check "mind_univ_hyps" (Univ.Instance.is_empty mind_univ_hyps);
+  check "mind_univ_hyps" (UVars.Instance.is_empty mind_univ_hyps);
   check "mind_nparams" Int.(equal mb.mind_nparams mind_nparams);
 
   check "mind_nparams_rec" (mb.mind_nparams_rec <= mind_nparams_rec);
@@ -191,7 +192,7 @@ let check_inductive env mind mb =
   check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt);
   ignore mind_universes; (* Indtypes did the necessary checking *)
   check "mind_template" (check_template mb.mind_template mind_template);
-  check "mind_variance" (Option.equal (Array.equal Univ.Variance.equal)
+  check "mind_variance" (Option.equal (Array.equal UVars.Variance.equal)
                            mb.mind_variance mind_variance);
   check "mind_sec_variance" (Option.is_empty mind_sec_variance);
   ignore mind_private; (* passed through Indtypes *)

checker/checker.ml

@@ -245,7 +245,7 @@ let explain_exn = function
     let msg =
       if CDebug.(get_flag misc) then
         str "." ++ spc() ++
-          UGraph.explain_universe_inconsistency Univ.Level.raw_pr i
+          UGraph.explain_universe_inconsistency Sorts.QVar.raw_pr Univ.Level.raw_pr i
       else
         mt() in
       hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
@@ -288,11 +288,13 @@ let explain_exn = function
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
       | IllFormedRecBody _ -> str"IllFormedRecBody"
       | IllTypedRecBody _ -> str"IllTypedRecBody"
+      | UnsatisfiedQConstraints _ -> str"UnsatisfiedQConstraints"
       | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"
       | DisallowedSProp -> str"DisallowedSProp"
       | BadBinderRelevance _ -> str"BadBinderRelevance"
       | BadCaseRelevance _ -> str"BadCaseRelevance"
       | BadInvert -> str"BadInvert"
+      | UndeclaredQualities _ -> str"UndeclaredQualities"
       | UndeclaredUniverse _ -> str"UndeclaredUniverse"
       | BadVariance _ -> str "BadVariance"
       | UndeclaredUsedVariables _ -> str "UndeclaredUsedVariables"

checker/mod_checking.ml

@@ -41,7 +41,7 @@ let check_constant_declaration env opac kn cb opacify =
          ones in const_universes should not be needed *)
       false, env
     | Polymorphic auctx ->
-      let ctx = Univ.AbstractContext.repr auctx in
+      let ctx = UVars.AbstractContext.repr auctx in
       (* [env] contains De Bruijn universe variables *)
       let env = push_context ~strict:false ctx env in
       true, env

checker/values.ml

@@ -94,6 +94,12 @@ let v_level = v_tuple "level" [|Int;v_raw_level|]
 let v_expr = v_tuple "levelexpr" [|v_level;Int|]
 let v_univ = List v_expr
 
+let v_qvar = v_sum "qvar" 0 [|[|Int|];[|String;Int|]|]
+
+let v_constant_quality = v_enum "constant_quality" 3
+
+let v_quality = v_sum "quality" 0 [|[|v_qvar|];[|v_constant_quality|]|]
+
 let v_cstrs =
   Annot
     ("Univ.constraints",
@@ -103,16 +109,16 @@ let v_cstrs =
 
 let v_variance = v_enum "variance" 3
 
-let v_instance = Annot ("instance", Array v_level)
-let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|]
+let v_instance = Annot ("instance", v_pair (Array v_quality) (Array v_level))
+let v_abs_context = v_tuple "abstract_universe_context" [|v_pair (Array v_name) (Array v_name); v_cstrs|]
 let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
 (** kernel/term *)
 
-let v_sort = v_sum "sort" 3 (*SProp, Prop, Set*) [|[|v_univ(*Type*)|]|]
+let v_sort = v_sum "sort" 3 (*SProp, Prop, Set*) [|[|v_univ(*Type*)|];[|v_qvar;v_univ(*QSort*)|]|]
 let v_sortfam = v_enum "sorts_family" 4
 
-let v_relevance = v_sum "relevance" 2 [||]
+let v_relevance = v_sum "relevance" 2 [|[|v_qvar|]|]
 let v_binder_annot x = v_tuple "binder_annot" [|x;v_relevance|]
 
 let v_puniverses v = v_tuple "punivs" [|v;v_instance|]
@@ -126,7 +132,7 @@ let v_caseinfo =
 
 let v_cast = v_enum "cast_kind" 3
 
-let v_proj_repr = v_tuple "projection_repr" [|v_ind;v_bool;Int;Int;v_id|]
+let v_proj_repr = v_tuple "projection_repr" [|v_ind;Int;Int;v_id|]
 let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
 
 let v_uint63 =
@@ -150,7 +156,7 @@ let rec v_constr =
     [|v_caseinfo;v_instance; Array v_constr; v_case_return; v_case_invert; v_constr; Array v_case_branch|]; (* Case *)
     [|v_fix|]; (* Fix *)
     [|v_cofix|]; (* CoFix *)
-    [|v_proj;v_constr|]; (* Proj *)
+    [|v_proj;v_relevance;v_constr|]; (* Proj *)
     [|v_uint63|]; (* Int *)
     [|Float64|]; (* Float *)
     [|v_instance;Array v_constr;v_constr;v_constr|] (* Array *)

dev/bench/bench.sh

@@ -63,9 +63,9 @@ check_variable () {
 : "${old_ocaml_version:=4.09.1}"
 : "${new_coq_repository:=$CI_REPOSITORY_URL}"
 : "${old_coq_repository:=$CI_REPOSITORY_URL}"
-: "${new_coq_opam_archive_git_uri:=https://github.com/coq/opam-coq-archive.git}"
+: "${new_coq_opam_archive_git_uri:=https://github.com/skyskimmer/opam-coq-archive.git}"
 : "${old_coq_opam_archive_git_uri:=https://github.com/coq/opam-coq-archive.git}"
-: "${new_coq_opam_archive_git_branch:=master}"
+: "${new_coq_opam_archive_git_branch:=sort-poly}"
 : "${old_coq_opam_archive_git_branch:=master}"
 : "${num_of_iterations:=1}"
 : "${timeout:=3h}"

dev/ci/user-overlays/17836-SkySkimmer-sort-poly.sh

@@ -0,0 +1,33 @@
+overlay bedrock2 https://github.com/SkySkimmer/bedrock2 sort-poly 17836
+
+overlay rewriter https://github.com/SkySkimmer/rewriter sort-poly 17836
+
+overlay fiat_crypto https://github.com/SkySkimmer/fiat-crypto sort-poly 17836
+
+overlay waterproof https://github.com/SkySkimmer/coq-waterproof sort-poly 17836
+
+overlay tactician https://github.com/SkySkimmer/coq-tactician sort-poly 17836
+
+overlay serapi https://github.com/SkySkimmer/coq-serapi sort-poly 17836
+
+overlay quickchick https://github.com/SkySkimmer/QuickChick sort-poly 17836
+
+overlay paramcoq https://github.com/SkySkimmer/paramcoq sort-poly 17836
+
+overlay unicoq https://github.com/SkySkimmer/unicoq sort-poly 17836
+
+overlay mtac2 https://github.com/SkySkimmer/Mtac2 sort-poly 17836
+
+overlay lean_importer https://github.com/SkySkimmer/coq-lean-import sort-poly 17836
+
+overlay equations https://github.com/SkySkimmer/Coq-Equations sort-poly 17836
+
+overlay elpi https://github.com/SkySkimmer/coq-elpi sort-poly 17836
+
+overlay coqhammer https://github.com/SkySkimmer/coqhammer sort-poly 17836
+
+overlay coq_dpdgraph https://github.com/SkySkimmer/coq-dpdgraph sort-poly 17836
+
+overlay metacoq https://github.com/SkySkimmer/metacoq sort-poly 17836
+
+overlay coq_lsp https://github.com/SkySkimmer/coq-lsp sort-poly 17836

dev/doc/changes.md

@@ -67,7 +67,7 @@ In general, code can be adapted by:
 
 ### Universes
 
-- Type `Univ.UContext` now embeds universe user names, generally
+- Type `UVars.UContext` now embeds universe user names, generally
   resulting in more concise code.
 
 - Renaming `Univ.Constraint` into `Univ.Constraints`

dev/doc/universes.md

@@ -6,7 +6,7 @@ to the API of Coq. First and foremost, the term language changes, as
 global references now carry a universe level substitution:
 
 ~~~ocaml
-type 'a puniverses = 'a * Univ.Instance.t
+type 'a puniverses = 'a * UVars.Instance.t
 type pconstant = constant puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
@@ -35,7 +35,7 @@ universes etc.. Structures are hashconsed (with a hack to take care
 of the fact that deserialization breaks sharing).
 
   Definitions (constants, inductives) now carry around not only
-constraints but also the universes they introduced (a Univ.UContext.t).
+constraints but also the universes they introduced (a UVars.UContext.t).
 There is another kind of contexts `Univ.ContextSet.t`, the latter has
 a set of universes, while the former has serialized the levels in an
 array, and is used for polymorphic objects. Both have "reified"

dev/include_printers

@@ -14,6 +14,7 @@
 #install_printer  (* univ context *) ppaucontext;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
+#install_printer  (* qvar set *) ppqvarset;;
 #install_printer  (* univ set *) ppuniverse_set;;
 #install_printer  (* univ instance *) ppuniverse_instance;;
 #install_printer  (* univ subst *) ppuniverse_subst;;

dev/top_printers.dbg

@@ -69,6 +69,7 @@ install_printer Top_printers.ppuni
 install_printer Top_printers.ppesorts
 install_printer Top_printers.ppqvar
 install_printer Top_printers.ppuni_level
+install_printer Top_printers.ppqvarset
 install_printer Top_printers.ppuniverse_set
 install_printer Top_printers.ppuniverse_instance
 install_printer Top_printers.ppuniverse_context

dev/top_printers.ml

@@ -16,6 +16,7 @@ open Pp
 open Names
 open Libnames
 open Univ
+open UVars
 open Environ
 open Printer
 open Constr
@@ -256,19 +257,21 @@ let pproof p = pp(Proof.pr_proof p)
 
 let ppuni u = pp(Universe.raw_pr u)
 let ppuni_level u = pp (Level.raw_pr u)
-let ppqvar q = pp (QVar.pr q)
+let ppqvar q = pp (QVar.raw_pr q)
 let ppesorts s = pp (Sorts.debug_print (Evd.MiniEConstr.ESorts.unsafe_to_sorts s))
 
-let prlev l = UnivNames.pr_with_global_universes l
+let prlev l = UnivNames.pr_level_with_global_universes l
+let prqvar q = Sorts.QVar.raw_pr q
+let ppqvarset l = pp (hov 1 (str "{" ++ prlist_with_sep spc QVar.raw_pr (QVar.Set.elements l) ++ str "}"))
 let ppuniverse_set l = pp (Level.Set.pr prlev l)
-let ppuniverse_instance l = pp (Instance.pr prlev l)
-let ppuniverse_context l = pp (pr_universe_context prlev l)
+let ppuniverse_instance l = pp (Instance.pr prqvar prlev l)
+let ppuniverse_context l = pp (pr_universe_context prqvar prlev l)
 let ppuniverse_context_set l = pp (pr_universe_context_set prlev l)
 let ppuniverse_subst l = pp (UnivSubst.pr_universe_subst Level.raw_pr l)
 let ppuniverse_opt_subst l = pp (UnivFlex.pr Level.raw_pr l)
 let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst Level.raw_pr l)
 let ppevar_universe_context l = pp (Termops.pr_evar_universe_context l)
-let ppconstraints c = pp (pr_constraints Level.raw_pr c)
+let ppconstraints c = pp (Constraints.pr Level.raw_pr c)
 let ppuniverseconstraints c = pp (UnivProblem.Set.pr c)
 let ppuniverse_context_future c =
   let ctx = Future.force c in
@@ -280,14 +283,16 @@ let ppnamedcontextval e =
   pp (pr_named_context env sigma (named_context_of_val e))
 
 let ppaucontext auctx =
-  let nas = AbstractContext.names auctx in
-  let prlev l = match Level.var_index l with
+  let qnas, unas = AbstractContext.names auctx in
+  let prgen pr var_index nas l = match var_index l with
     | Some n -> (match nas.(n) with
-        | Anonymous -> prlev l
+        | Anonymous -> pr l
         | Name id -> Id.print id)
-    | None -> prlev l
+    | None -> pr l
   in
-  pp (pr_universe_context prlev (AbstractContext.repr auctx))
+  let prqvar l = prgen prqvar Sorts.QVar.var_index qnas l in
+  let prlev l = prgen prlev Level.var_index unas l in
+  pp (pr_universe_context prqvar prlev (AbstractContext.repr auctx))
 
 
 let ppenv e = pp
@@ -342,7 +347,7 @@ let constr_display csr =
   | Construct (((sp,i),j),u) ->
       "MutConstruct(("^(MutInd.to_string sp)^","^(string_of_int i)^"),"
       ^","^(universes_display u)^(string_of_int j)^")"
-  | Proj (p, c) -> "Proj("^(Constant.to_string (Projection.constant p))^","^term_display c ^")"
+  | Proj (p, r, c) -> "Proj("^(Constant.to_string (Projection.constant p))^","^term_display c ^")"
   | Case (ci,u,pms,(_,p),iv,c,bl) ->
       "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
       ^(array_display (Array.map snd bl))^")"
@@ -374,6 +379,9 @@ let constr_display csr =
   and univ_display u =
     incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Universe.raw_pr u ++ fnl ())
 
+  and quality_display q =
+    incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Sorts.Quality.raw_pr q ++ fnl ())
+
   and level_display u =
     incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.raw_pr u ++ fnl ())
 
@@ -386,8 +394,15 @@ let constr_display csr =
     | QSort (q, u) -> univ_display u; Printf.sprintf "QSort(%s, %i)" (Sorts.QVar.to_string q) !cnt
 
   and universes_display l =
+    let qs, us = Instance.to_array l in
+    let qs = Array.fold_right (fun x i ->
+        quality_display x;
+        (string_of_int !cnt)^
+        (if not(i="") then (" "^i) else ""))
+        qs ""
+    in
     Array.fold_right (fun x i -> level_display x; (string_of_int !cnt)^(if not(i="")
-        then (" "^i) else "")) (Instance.to_array l) ""
+        then (" "^i) else "")) us (if qs = "" then "" else (qs^" | "))
 
   and name_display x = match x.binder_name with
     | Name id -> "Name("^(Id.to_string id)^")"
@@ -440,7 +455,7 @@ let print_pure_constr csr =
       sp_con_display c;
       print_string ","; universes_display u;
       print_string ")"
-  | Proj (p,c') -> print_string "Proj(";
+  | Proj (p,_,c') -> print_string "Proj(";
       sp_con_display (Projection.constant p);
       print_string ",";
       box_display c';
@@ -526,7 +541,9 @@ let print_pure_constr csr =
   and box_display c = open_hovbox 1; term_display c; close_box()
 
   and universes_display u =
-    Array.iter (fun u -> print_space (); pp (Level.raw_pr u)) (Instance.to_array u)
+    let qs, us = Instance.to_array u in
+    Array.iter (fun u -> print_space (); pp (Sorts.Quality.raw_pr u)) qs;
+    Array.iter (fun u -> print_space (); pp (Level.raw_pr u)) us
 
   and sort_display = function
     | SProp -> print_string "SProp"
@@ -535,7 +552,7 @@ let print_pure_constr csr =
     | Type u -> open_hbox();
         print_string "Type("; pp (Universe.raw_pr u); print_string ")"; close_box()
     | QSort (q, u) -> open_hbox();
-        print_string "QSort("; pp (QVar.pr q); print_string ", "; pp (Universe.raw_pr u); print_string ")"; close_box()
+        print_string "QSort("; pp (QVar.raw_pr q); print_string ", "; pp (Universe.raw_pr u); print_string ")"; close_box()
 
   and name_display x = match x.binder_name with
     | Name id -> print_string (Id.to_string id)

dev/top_printers.mli

@@ -147,18 +147,19 @@ val ppuni_level : Univ.Level.t -> unit (* raw *)
 val ppqvar : Sorts.QVar.t -> unit
 val ppesorts : EConstr.ESorts.t -> unit
 val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *)
+val ppqvarset : Sorts.QVar.Set.t -> unit
 val ppuniverse_set : Univ.Level.Set.t -> unit
-val ppuniverse_instance : Univ.Instance.t -> unit
-val ppuniverse_context : Univ.UContext.t -> unit
-val ppaucontext : Univ.AbstractContext.t -> unit
+val ppuniverse_instance : UVars.Instance.t -> unit
+val ppuniverse_context : UVars.UContext.t -> unit
+val ppaucontext : UVars.AbstractContext.t -> unit
 val ppuniverse_context_set : Univ.ContextSet.t -> unit
 val ppuniverse_subst : UnivSubst.universe_subst -> unit
 val ppuniverse_opt_subst : UState.universe_opt_subst -> unit
 val ppuniverse_level_subst : Univ.universe_level_subst -> unit
 val ppevar_universe_context : UState.t -> unit
 val ppconstraints : Univ.Constraints.t -> unit
 val ppuniverseconstraints : UnivProblem.Set.t -> unit
-val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
+val ppuniverse_context_future : UVars.UContext.t Future.computation -> unit
 val ppuniverses : UGraph.t -> unit
 
 val ppnamedcontextval : Environ.named_context_val -> unit

doc/changelog/01-kernel/17836-sort-poly.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  :ref:`sort-polymorphism` makes it possible to share common constructs
+  over `Type` `Prop` and `SProp`
+  (`#17836 <https://github.com/coq/coq/pull/17836>`_,
+  by Gaëtan Gilbert).