1 files changed, 126 insertions, 31 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 05c40dbd..ad1ffa35 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -27,9 +27,7 @@ open Impargs
 open Reductionops
 open Indtypes
 open Pretyping
-open Evarutil
 open Indschemes
-open Misctypes
 open Context.Rel.Declaration
 open Entries
 
@@ -46,8 +44,8 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
         user_err ?loc
          (strbrk"Cannot infer the non constant arguments of the conclusion of "
           ++ Id.print cs ++ str ".");
-      let args = List.map (fun id -> CAst.(make ?loc @@ CRef(make ?loc @@ Ident id,None))) params in
-      CAppExpl ((None,CAst.make ?loc @@ Ident name,None),List.rev args)
+      let args = List.map (fun id -> CAst.(make ?loc @@ CRef(qualid_of_ident ?loc id,None))) params in
+      CAppExpl ((None,qualid_of_ident ?loc name,None),List.rev args)
   | c -> c
   )
 
@@ -128,7 +126,7 @@ let make_conclusion_flexible sigma ty poly =
   else sigma
 
 let is_impredicative env u =
-  u = Prop Null || (is_impredicative_set env && u = Prop Pos)
+  u = Prop || (is_impredicative_set env && u = Set)
 
 let interp_ind_arity env sigma ind =
   let c = intern_gen IsType env sigma ind.ind_arity in
@@ -148,7 +146,6 @@ let interp_cstrs env sigma impls mldata arity ind =
   let sigma, (ctyps'', cimpls) =
     on_snd List.split @@
     List.fold_left_map (fun sigma l ->
-        on_snd (on_fst EConstr.Unsafe.to_constr) @@
         interp_type_evars_impls env sigma ~impls l) sigma ctyps' in
   sigma, (cnames, ctyps'', cimpls)
 
@@ -159,7 +156,7 @@ let sign_level env evd sign =
       | LocalDef _ -> lev, push_rel d env
       | LocalAssum _ ->
         let s = destSort (Reduction.whd_all env
-                            (EConstr.Unsafe.to_constr (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d))))))
+                            (EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d)))))
         in
         let u = univ_of_sort s in
           (Univ.sup u lev, push_rel d env))
@@ -178,10 +175,76 @@ let is_flexible_sort evd u =
   | Some l -> Evd.is_flexible_level evd l
   | None -> false
 
+(**********************************************************************)
+(* Tools for template polymorphic inductive types                         *)
+
+(* Miscellaneous functions to remove or test local univ assumed to
+   occur only in the le constraints *)
+
+(*
+   Solve a system of universe constraint of the form
+
+   u_s11, ..., u_s1p1, w1 <= u1
+   ...
+   u_sn1, ..., u_snpn, wn <= un
+
+where
+
+  - the ui (1 <= i <= n) are universe variables,
+  - the sjk select subsets of the ui for each equations,
+  - the wi are arbitrary complex universes that do not mention the ui.
+*)
+
+let is_direct_sort_constraint s v = match s with
+  | Some u -> Univ.univ_level_mem u v
+  | None -> false
+
+let solve_constraints_system levels level_bounds =
+  let open Univ in
+  let levels =
+    Array.mapi (fun i o ->
+      match o with
+      | Some u ->
+        (match Universe.level u with
+        | Some u -> Some u
+        | _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None)
+      | None -> None)
+      levels in
+  let v = Array.copy level_bounds in
+  let nind = Array.length v in
+  let clos = Array.map (fun _ -> Int.Set.empty) levels in
+  (* First compute the transitive closure of the levels dependencies *)
+  for i=0 to nind-1 do
+    for j=0 to nind-1 do
+      if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
+        clos.(i) <- Int.Set.add j clos.(i);
+    done;
+  done;
+  let rec closure () =
+    let continue = ref false in
+      Array.iteri (fun i deps ->
+        let deps' =
+          Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps
+        in
+          if Int.Set.equal deps deps' then ()
+          else (clos.(i) <- deps'; continue := true))
+        clos;
+      if !continue then closure ()
+      else ()
+  in
+  closure ();
+  for i=0 to nind-1 do
+    for j=0 to nind-1 do
+      if not (Int.equal i j) && Int.Set.mem j clos.(i) then
+        (v.(i) <- Universe.sup v.(i) level_bounds.(j));
+    done;
+  done;
+  v
+
 let inductive_levels env evd poly arities inds =
   let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
   let levels = List.map (fun (x,(ctx,a)) ->
-    if a = Prop Null then None
+    if a = Prop then None
     else Some (univ_of_sort a)) destarities
   in
   let cstrs_levels, min_levels, sizes =
@@ -206,8 +269,8 @@ let inductive_levels env evd poly arities inds =
   in
   (* Take the transitive closure of the system of constructors *)
   (* level constraints and remove the recursive dependencies *)
-  let levels' = Universes.solve_constraints_system (Array.of_list levels)
-    (Array.of_list cstrs_levels) (Array.of_list min_levels)
+  let levels' = solve_constraints_system (Array.of_list levels)
+    (Array.of_list cstrs_levels)
   in
   let evd, arities =
     CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
@@ -234,14 +297,14 @@ let inductive_levels env evd poly arities inds =
            (** "Polymorphic" type constraint and more than one constructor,
                should not land in Prop. Add constraint only if it would
                land in Prop directly (no informative arguments as well). *)
-            Evd.set_leq_sort env evd (Prop Pos) du
+            Evd.set_leq_sort env evd Set du
           else evd
         in
         let duu = Sorts.univ_of_sort du in
         let evd =
           if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then
             if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then
-              Evd.set_eq_sort env evd (Prop Null) du
+              Evd.set_eq_sort env evd Prop du
             else evd
           else Evd.set_eq_sort env evd (Type cu) du
         in
@@ -263,14 +326,17 @@ let check_param = function
 | CLocalPattern {CAst.loc} ->
     Loc.raise ?loc (Stream.Error "pattern with quote not allowed here")
 
-let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
+let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
-  let env0 = Global.env() in
+  if not (List.is_empty uparamsl) && not (List.is_empty notations)
+  then user_err (str "Inductives with uniform parameters may not have attached notations.");
   let pl = (List.hd indl).ind_univs in
-  let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in
+  let sigma, decl = interp_univ_decl_opt env0 pl in
+  let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) =
+    interp_context_evars env0 sigma uparamsl in
   let sigma, (impls, ((env_params, ctx_params), userimpls)) =
-    interp_context_evars env0 sigma paramsl
+    interp_context_evars ~impl_env:uimpls env_uparams sigma paramsl
   in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
@@ -282,15 +348,15 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in
 
   let fullarities = List.map (fun (c, _, _) -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in
-  let env_ar = push_types env0 indnames fullarities in
+  let env_ar = push_types env_uparams indnames fullarities in
   let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
 
   (* Compute interpretation metadatas *)
   let indimpls = List.map (fun (_, _, impls) -> userimpls @
     lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
   let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
-  let impls = compute_internalization_env env0 sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
-  let ntn_impls = compute_internalization_env env0 sigma (Inductive (params,true)) indnames fullarities indimpls in
+  let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
+  let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
 
   let sigma, constructors =
@@ -301,23 +367,44 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
      List.fold_left3_map (fun sigma -> interp_cstrs env_ar_params sigma impls) sigma mldatas arities indl)
      () in
 
+  (* generalize over the uniform parameters *)
+  let nparams = Context.Rel.length ctx_params in
+  let nuparams = Context.Rel.length ctx_uparams in
+  let uargs = Context.Rel.to_extended_vect EConstr.mkRel 0 ctx_uparams in
+  let uparam_subst =
+    List.init (List.length indl) EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs))
+    @ List.init nuparams EConstr.(fun i -> mkRel (i + 1)) in
+  let generalize_constructor c = EConstr.Unsafe.to_constr (EConstr.Vars.substnl uparam_subst nparams c) in
+  let constructors = List.map (fun (cnames,ctypes,cimpls) ->
+                         (cnames,List.map generalize_constructor ctypes,cimpls))
+                       constructors
+  in
+  let ctx_params = ctx_params @ ctx_uparams in
+  let userimpls = useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) userimpls) in
+  let indimpls = List.map (fun iimpl -> useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) iimpl)) indimpls in
+  let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in
+  let env_ar = push_types env0 indnames fullarities in
+  let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
+
   (* Try further to solve evars, and instantiate them *)
-  let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in
+  let sigma = solve_remaining_evars all_and_fail_flags env_params sigma (Evd.from_env env_params) in
   (* Compute renewed arities *)
-  let sigma, nf = nf_evars_and_universes sigma in
+  let sigma = Evd.minimize_universes sigma in
+  let nf = Evarutil.nf_evars_universes sigma in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
   let arities = List.map EConstr.(to_constr sigma) arities in
   let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in
   let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in
-  let sigma, nf' = nf_evars_and_universes sigma in
-  let arities = List.map nf' arities in
-  let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
+  let sigma = Evd.minimize_universes sigma in
+  let nf = Evarutil.nf_evars_universes sigma in
+  let arities = List.map nf arities in
+  let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
   let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
   let uctx = Evd.check_univ_decl ~poly sigma decl in
-  List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities;
-  Context.Rel.iter (fun c -> check_evars env0 Evd.empty sigma (EConstr.of_constr c)) ctx_params;
+  List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities;
+  Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params;
   List.iter (fun (_,ctyps,_) ->
-    List.iter (fun c -> check_evars env_ar_params Evd.empty sigma (EConstr.of_constr c)) ctyps)
+    List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps)
     constructors;
 
   (* Build the inductive entries *)
@@ -357,6 +444,9 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
       InferCumulativity.infer_inductive env_ar mind_ent
    else mind_ent), Evd.universe_binders sigma, impls
 
+let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
+  interp_mutual_inductive_gen (Global.env()) ([],paramsl,indl) notations cum poly prv finite
+
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
   List.equal local_binder_eq bl1 bl2
@@ -378,7 +468,7 @@ let extract_params indl =
 let extract_inductive indl =
   List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> {
     ind_name = indname; ind_univs = pl;
-    ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar;
+    ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) ar;
     ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc
   }) indl
 
@@ -439,10 +529,15 @@ type one_inductive_impls =
   Impargs.manual_explicitation list (* for inds *)*
   Impargs.manual_explicitation list list (* for constrs *)
 
-let do_mutual_inductive indl cum poly prv finite =
-  let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
+type uniform_inductive_flag =
+  | UniformParameters
+  | NonUniformParameters
+
+let do_mutual_inductive indl cum poly prv ~uniform finite =
+  let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
-  let mie,pl,impls = interp_mutual_inductive indl ntns cum poly prv finite in
+  let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in
+  let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) indl ntns cum poly prv finite in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (declare_mutual_inductive_with_eliminations mie pl impls);
   (* Declare the possible notations of inductive types *)