Keep qvar in template poly entry and declarations

checker/checkInductive.ml

@@ -21,44 +21,55 @@ exception InductiveMismatch of MutInd.t * string
 
 let check mind field b = if not b then raise (InductiveMismatch (mind,field))
 
+let template_univ_entry {template_context; template_defaults=default_univs; _} =
+  Entries.Template_ind_entry {uctx = AbstractContext.repr template_context; default_univs}
+
 let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
   let open Entries in
   let nparams = List.length mb.mind_params_ctxt in (* include letins *)
   let mind_entry_record = match mb.mind_record with
     | NotRecord -> None | FakeRecord -> Some None
     | PrimRecord data -> Some (Some (Array.map (fun (x,_,_,_) -> x) data))
   in
-  let check_template ind = match ind.mind_arity with
-  | RegularArity _ -> false
-  | TemplateArity _ -> true
-  in
-  let mind_entry_template = Array.exists check_template mb.mind_packets in
-  let () = if mind_entry_template then assert (Array.for_all check_template mb.mind_packets) in
+  let template = Option.map template_univ_entry mb.mind_template in
   let mind_entry_universes = match mb.mind_universes with
     | Monomorphic ->
-      (* We only need to rebuild the set of constraints for template polymorphic
-        inductive types. The set of monomorphic constraints is already part of
-        the graph at that point, but we need to emulate a broken bound variable
-        mechanism for template inductive types. *)
-      begin match mb.mind_template with
+      begin match template with
       | None -> Monomorphic_ind_entry
-      | Some ctx ->
-        let pseudo_sort_poly = ctx.template_pseudo_sort_poly in
-        Template_ind_entry {univs=ctx.template_context; pseudo_sort_poly}
+      | Some template -> template
       end
     | Polymorphic auctx -> Polymorphic_ind_entry (AbstractContext.repr auctx)
   in
   let ntyps = Array.length mb.mind_packets in
+  let mind_entry_params = match mb.mind_template with
+    | None -> mb.mind_params_ctxt
+    | Some template ->
+      let open Context.Rel.Declaration in
+      let rec fix_params acc params template = match params, template with
+        | [], [] -> acc
+        | (LocalDef _ as d) :: params , _ ->
+          fix_params (d::acc) params template
+        | (LocalAssum _ as d) :: params, None :: template ->
+          fix_params (d :: acc) params template
+        | LocalAssum (na, t) :: params, Some s :: template ->
+          let ctx, _ = Term.destArity t in
+          let d = LocalAssum (na, Term.mkArity (ctx, s)) in
+          fix_params (d :: acc) params template
+        | _ :: _, [] | [], _ :: _ -> assert false
+      in
+      fix_params [] (List.rev mb.mind_params_ctxt) template.template_param_arguments
+  in
   let mind_entry_inds = Array.map_to_list (fun ind ->
-      let mind_entry_arity = match ind.mind_arity with
-        | RegularArity ar ->
-          let ctx, arity = Term.decompose_prod_n_decls nparams ar.mind_user_arity in
+      let mind_entry_arity =
+        match mb.mind_template with
+        | None ->
+          let ctx, arity = Term.decompose_prod_n_decls nparams ind.mind_user_arity in
           ignore ctx; (* we will check that the produced user_arity is equal to the input *)
           arity
-        | TemplateArity ar ->
+        | Some template ->
           let ctx = ind.mind_arity_ctxt in
           let ctx = List.firstn (List.length ctx - nparams) ctx in
-          Term.mkArity (ctx, ar.template_level)
+          Term.mkArity (ctx, template.template_concl)
       in
       {
         mind_entry_typename = ind.mind_typename;
@@ -77,34 +88,25 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
   {
     mind_entry_record;
     mind_entry_finite = mb.mind_finite;
-    mind_entry_params = mb.mind_params_ctxt;
+    mind_entry_params;
     mind_entry_inds;
     mind_entry_universes;
     mind_entry_variance;
     mind_entry_private = mb.mind_private;
   }
 
-let check_arity env ar1 ar2 = match ar1, ar2 with
-  | RegularArity ar, RegularArity {mind_user_arity;mind_sort} ->
-    Constr.equal ar.mind_user_arity mind_user_arity &&
-    Sorts.equal ar.mind_sort mind_sort
-  | TemplateArity ar, TemplateArity {template_level} ->
-    UGraph.check_leq_sort (universes env) template_level ar.template_level
-    (* template_level is inferred by indtypes, so functor application can produce a smaller one *)
-  | (RegularArity _ | TemplateArity _), _ -> assert false
-
-let check_template_pseudo_sort_poly a b =
-  match a, b with
-  | TemplatePseudoSortPoly, TemplatePseudoSortPoly
-  | TemplateUnivOnly, TemplateUnivOnly -> true
-  | (TemplatePseudoSortPoly | TemplateUnivOnly), _ -> false
+let check_abstract_uctx a b =
+  eq_sizes (AbstractContext.size a) (AbstractContext.size b)
+  && Constraints.equal (UContext.constraints @@ AbstractContext.repr a)
+    (UContext.constraints @@ AbstractContext.repr b)
 
 let check_template ar1 ar2 = match ar1, ar2 with
 | None, None -> true
-| Some ar, Some {template_context; template_param_arguments; template_pseudo_sort_poly} ->
-  List.equal Bool.equal ar.template_param_arguments template_param_arguments &&
-  ContextSet.equal template_context ar.template_context &&
-  check_template_pseudo_sort_poly template_pseudo_sort_poly ar.template_pseudo_sort_poly
+| Some ar, Some {template_context; template_param_arguments; template_concl; template_defaults} ->
+  List.equal (Option.equal Sorts.equal) ar.template_param_arguments template_param_arguments &&
+  check_abstract_uctx template_context ar.template_context &&
+  Sorts.equal ar.template_concl template_concl &&
+  Instance.equal ar.template_defaults template_defaults
 | None, Some _ | Some _, None -> false
 
 (* if the generated inductive is squashed the original one must be squashed *)
@@ -146,16 +148,17 @@ let eq_reloc_tbl = Array.equal (fun x y -> Int.equal (fst x) (fst y) && Int.equa
 let eq_in_context (ctx1, t1) (ctx2, t2) =
   Context.Rel.equal Sorts.relevance_equal Constr.equal ctx1 ctx2 && Constr.equal t1 t2
 
-let check_packet env mind ind
-    { mind_typename; mind_arity_ctxt; mind_arity; mind_consnames; mind_user_lc;
+let check_packet mind ind
+    { mind_typename; mind_arity_ctxt; mind_user_arity; mind_sort; mind_consnames; mind_user_lc;
       mind_nrealargs; mind_nrealdecls; mind_squashed; mind_nf_lc;
       mind_consnrealargs; mind_consnrealdecls; mind_recargs; mind_relevance;
       mind_nb_constant; mind_nb_args; mind_reloc_tbl } =
   let check = check mind in
 
   ignore mind_typename; (* passed through *)
   check "mind_arity_ctxt" (Context.Rel.equal Sorts.relevance_equal Constr.equal ind.mind_arity_ctxt mind_arity_ctxt);
-  check "mind_arity" (check_arity env ind.mind_arity mind_arity);
+  check "mind_arity" (Constr.equal ind.mind_user_arity mind_user_arity);
+  check "mind_sort" (Sorts.equal ind.mind_sort mind_sort);
   ignore mind_consnames; (* passed through *)
   check "mind_user_lc" (Array.equal Constr.equal ind.mind_user_lc mind_user_lc);
   check "mind_nrealargs" Int.(equal ind.mind_nrealargs mind_nrealargs);
@@ -205,7 +208,7 @@ let check_inductive env mind mb =
   in
   let check = check mind in
 
-  Array.iter2 (check_packet env mind) mb.mind_packets mind_packets;
+  Array.iter2 (check_packet mind) mb.mind_packets mind_packets;
   check "mind_record" (check_same_record mb.mind_record mind_record);
   check "mind_finite" (mb.mind_finite == mind_finite);
   check "mind_ntypes" Int.(equal mb.mind_ntypes mind_ntypes);

checker/values.ml

@@ -321,11 +321,13 @@ let v_oracle =
     v_pred v_proj_repr;
   |]
 
-let v_template_arity =
-  v_tuple "template_arity" [|v_sort|]
-
 let v_template_universes =
-  v_tuple "template_universes" [|v_list v_bool;v_context_set; v_bool|]
+  v_tuple "template_universes" [|
+    v_list (v_opt v_sort);
+    v_sort;
+    v_abs_context;
+    v_instance;
+  |]
 
 let v_primitive =
   v_enum "primitive" 63 (* Number of constructors of the CPrimitives.t type *)
@@ -417,18 +419,13 @@ let v_wfp =
       [|v_int;v_array v_wfp|] (* Rtree.Rec *)
     |]))
 
-let v_mono_ind_arity =
-  v_tuple "monomorphic_inductive_arity" [|v_constr;v_sort|]
-
-let v_ind_arity = v_sum "inductive_arity" 0
-  [|[|v_mono_ind_arity|];[|v_template_arity|]|]
-
 let v_squash_info = v_sum "squash_info" 1 [|[|v_set v_quality|]|]
 
 let v_one_ind = v_tuple "one_inductive_body"
   [|v_id;
     v_rctxt;
-    v_ind_arity;
+    v_sort;
+    v_constr;
     v_array v_id;
     v_array v_constr;
     v_int;

dev/ci/user-overlays/20178-SkySkimmer-template-entry-qvar.sh

@@ -0,0 +1,9 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi template-entry-qvar 20178
+
+overlay equations https://github.com/SkySkimmer/Coq-Equations template-entry-qvar 20178
+
+overlay coq_lsp https://github.com/SkySkimmer/coq-lsp template-entry-qvar 20178
+
+overlay metacoq https://github.com/SkySkimmer/metacoq template-entry-qvar 20178
+
+overlay paramcoq https://github.com/SkySkimmer/paramcoq template-entry-qvar 20178

engine/evd.ml

@@ -1207,8 +1207,8 @@ let nf_univ_variables evd =
   let uctx = UState.normalize_variables evd.universes in
   {evd with universes = uctx}
 
-let collapse_sort_variables evd =
-  let universes = UState.collapse_sort_variables evd.universes in
+let collapse_sort_variables ?except evd =
+  let universes = UState.collapse_sort_variables ?except evd.universes in
   { evd with universes }
 
 let minimize_universes ?(collapse_sort_variables=true) evd =
@@ -1720,6 +1720,7 @@ module MiniEConstr = struct
     let univ_value l =
       UnivFlex.normalize_univ_variable lsubst l
     in
+    let relevance_value r = UState.nf_relevance sigma.universes r in
     let qvar_value q = UState.nf_qvar sigma.universes q in
     let next s = { s with evc_lift = s.evc_lift + 1 } in
     let find clos id = match Id.Map.find_opt id clos.evc_map with
@@ -1792,7 +1793,7 @@ module MiniEConstr = struct
         self nclos c
       end
     | _ ->
-      UnivSubst.map_universes_opt_subst_with_binders next self qvar_value univ_value clos c
+      UnivSubst.map_universes_opt_subst_with_binders next self relevance_value qvar_value univ_value clos c
     in
     let clos = {
       evc_lift = 0;

engine/evd.mli

@@ -612,7 +612,7 @@ val with_sort_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a UnivGen.in_sor
 
 val nf_univ_variables : evar_map -> evar_map
 
-val collapse_sort_variables : evar_map -> evar_map
+val collapse_sort_variables : ?except:Sorts.QVar.Set.t -> evar_map -> evar_map
 
 val fix_undefined_variables : evar_map -> evar_map
 

engine/uState.ml

@@ -45,7 +45,7 @@ module QState : sig
   val is_above_prop : elt -> t -> bool
   val undefined : t -> QVar.Set.t
   val collapse_above_prop : to_prop:bool -> t -> t
-  val collapse : t -> t
+  val collapse : ?except:QVar.Set.t -> t -> t
   val pr : (QVar.t -> Pp.t) -> t -> Pp.t
   val of_set : QVar.Set.t -> t
 end =
@@ -188,9 +188,9 @@ let collapse_above_prop ~to_prop m =
   in
   { named = m.named; qmap = QMap.mapi map m.qmap; above = QSet.empty }
 
-let collapse m =
+let collapse ?(except=QSet.empty) m =
   let map q v = match v with
-  | None -> if QSet.mem q m.named then None else Some (QConstant QType)
+  | None -> if QSet.mem q m.named || QSet.mem q except then None else Some (QConstant QType)
   | Some _ -> v
   in
   { named = m.named; qmap = QMap.mapi map m.qmap; above = QSet.empty }
@@ -342,7 +342,8 @@ let sort_context_set uctx =
 
 let constraints uctx = snd uctx.local
 
-let compute_instance_binders (qrev,urev) inst =
+let compute_instance_binders uctx inst =
+  let (qrev,urev) = snd uctx.names in
   let qinst, uinst = Instance.to_array inst in
   let qmap = function
     | QVar q ->
@@ -359,7 +360,7 @@ let compute_instance_binders (qrev,urev) inst =
 
 let context uctx =
   let qvars = QState.undefined uctx.sort_variables in
-  UContext.of_context_set (compute_instance_binders (snd uctx.names)) qvars uctx.local
+  UContext.of_context_set (compute_instance_binders uctx) qvars uctx.local
 
 type named_universes_entry = universes_entry * UnivNames.universe_binders
 
@@ -459,7 +460,7 @@ let nf_universes uctx c =
   | Evar (evk, args) ->
     let args' = SList.Smart.map (self ()) args in
     if args == args' then c else Constr.mkEvar (evk, args')
-  | _ -> UnivSubst.map_universes_opt_subst_with_binders ignore self (nf_qvar uctx) nf_univ () c
+  | _ -> UnivSubst.map_universes_opt_subst_with_binders ignore self (nf_relevance uctx) (nf_qvar uctx) nf_univ () c
   in
   self ()  c
 
@@ -899,6 +900,31 @@ let check_implication uctx cstrs cstrs' =
       Pp.(str "Universe constraints are not implied by the ones declared: " ++
           Constraints.pr (pr_uctx_level uctx) cstrs')
 
+let check_template_univ_decl uctx ~template_qvars decl =
+  let () =
+    match List.filter (fun q -> not @@ QVar.Set.mem q template_qvars) decl.univdecl_qualities with
+    | (_ :: _) as qvars ->
+      CErrors.user_err
+        Pp.(str "Qualities " ++ prlist_with_sep spc (pr_uctx_qvar uctx) qvars ++
+            str " cannot be template.")
+    | [] ->
+      if not (QVar.Set.equal template_qvars (QState.undefined uctx.sort_variables))
+      then CErrors.anomaly Pp.(str "Bugged template univ declaration.")
+  in
+  let levels, csts = uctx.local in
+  let () =
+    let prefix = decl.univdecl_instance in
+    if not decl.univdecl_extensible_instance
+    then check_universe_context_set ~prefix levels uctx.names
+  in
+  if decl.univdecl_extensible_constraints then uctx.local
+  else begin
+    check_implication uctx
+      decl.univdecl_constraints
+      csts;
+    levels, decl.univdecl_constraints
+  end
+
 let check_mono_univ_decl uctx decl =
   (* Note: if [decl] is [default_univ_decl], behave like [uctx.local] *)
   let () =
@@ -925,7 +951,7 @@ let check_poly_univ_decl uctx decl =
   let levels, csts = uctx.local in
   let qvars = QState.undefined uctx.sort_variables in
   let inst = universe_context_inst decl qvars levels uctx.names in
-  let nas = compute_instance_binders (snd uctx.names) inst in
+  let nas = compute_instance_binders uctx inst in
   let csts = if decl.univdecl_extensible_constraints then csts
     else begin
       check_implication uctx
@@ -1191,8 +1217,8 @@ let fix_undefined_variables uctx =
 let collapse_above_prop_sort_variables ~to_prop uctx =
   { uctx with sort_variables = QState.collapse_above_prop ~to_prop uctx.sort_variables }
 
-let collapse_sort_variables uctx =
-  { uctx with sort_variables = QState.collapse uctx.sort_variables }
+let collapse_sort_variables ?except uctx =
+  { uctx with sort_variables = QState.collapse ?except uctx.sort_variables }
 
 let minimize uctx =
   let open UnivMinim in
@@ -1229,7 +1255,7 @@ let check_univ_decl_rev uctx decl =
   let levels, csts = uctx.local in
   let qvars = QState.undefined uctx.sort_variables in
   let inst = universe_context_inst_decl decl qvars levels uctx.names in
-  let nas = compute_instance_binders (snd uctx.names) inst in
+  let nas = compute_instance_binders uctx inst in
   let () =
     check_implication uctx
     csts

engine/uState.mli

@@ -93,6 +93,8 @@ val univ_entry : poly:bool -> t -> named_universes_entry
 val universe_binders : t -> UnivNames.universe_binders
 (** Return local names of universes. *)
 
+val compute_instance_binders : t -> UVars.Instance.t -> UVars.bound_names
+
 val nf_qvar : t -> QVar.t -> Quality.t
 (** Returns the normal form of the sort variable. *)
 
@@ -226,7 +228,7 @@ val minimize : t -> t
 
 val collapse_above_prop_sort_variables : to_prop:bool -> t -> t
 
-val collapse_sort_variables : t -> t
+val collapse_sort_variables : ?except:QVar.Set.t -> t -> t
 
 type ('a, 'b, 'c) gen_universe_decl = {
   univdecl_qualities : 'a;
@@ -258,6 +260,8 @@ val check_uctx_impl : fail:(Pp.t -> unit) -> t -> t -> unit
 
 val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
 
+val check_template_univ_decl : t -> template_qvars:QVar.Set.t -> universe_decl -> Univ.ContextSet.t
+
 (** {5 TODO: Document me} *)
 
 val update_sigma_univs : t -> UGraph.t -> t