Imported Upstream version 8.5~beta3+dfsg

1 files changed, 57 insertions, 52 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 6b909824..8b03df64 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -173,38 +173,21 @@ let cumulate_arity_large_levels env sign =
     sign (Universe.type0m,env))
 
 let is_impredicative env u =
-  is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet)
+  is_type0m_univ u || (is_type0_univ u && is_impredicative_set env)
 
+(* Returns the list [x_1, ..., x_n] of levels contributing to template
+   polymorphism. The elements x_k is None if the k-th parameter (starting
+   from the most recent and ignoring let-definitions) is not contributing 
+   or is Some u_k if its level is u_k and is contributing. *)
 let param_ccls params =
-  let has_some_univ u = function
-    | Some v when Univ.Level.equal u v -> true
-    | _ -> false
+  let fold acc = function (_, None, p) -> 
+      (let c = strip_prod_assum p in
+      match kind_of_term c with
+        | Sort (Type u) -> Univ.Universe.level u
+        | _ -> None) :: acc
+    | _ -> acc 
   in
-  let remove_some_univ u = function
-    | Some v when Univ.Level.equal u v -> None
-    | x -> x
-  in
-  let fold l (_, b, p) = match b with
-  | None ->
-    (* Parameter contributes to polymorphism only if explicit Type *)
-    let c = strip_prod_assum p in
-    (* Add Type levels to the ordered list of parameters contributing to *)
-    (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
-    begin match kind_of_term c with
-    | Sort (Type u) ->
-      (match Univ.Universe.level u with
-      | Some u ->
-	if List.exists (has_some_univ u) l then
-          None :: List.map (remove_some_univ u) l
-	else
-          Some u :: l
-      | None -> None :: l)
-    | _ ->
-      None :: l
-    end
-  | _ -> l
-  in
-    List.fold_left fold [] params
+  List.fold_left fold [] params
 
 (* Type-check an inductive definition. Does not check positivity
    conditions. *)
@@ -302,8 +285,7 @@ let typecheck_inductive env mie =
       let full_polymorphic () = 
 	let defu = Term.univ_of_sort def_level in
 	let is_natural =
-	  type_in_type env || (check_leq (universes env') infu defu &&
-	    not (is_type0m_univ defu && not is_unit))
+	  type_in_type env || (check_leq (universes env') infu defu)
 	in
 	let _ =
 	  (** Impredicative sort, always allow *)
@@ -356,7 +338,7 @@ type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
   | LocalNotConstructor
-  | LocalNonPar of int * int
+  | LocalNonPar of int * int * int
 
 exception IllFormedInd of ill_formed_ind
 
@@ -377,9 +359,9 @@ let explain_ind_err id ntyp env nbpar c nargs err =
     | LocalNotConstructor ->
 	raise (InductiveError
 		 (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nbpar,nargs)))
-    | LocalNonPar (n,l) ->
+    | LocalNonPar (n,i,l) ->
 	raise (InductiveError
-		 (NonPar (env,c',n,mkRel (nbpar-n+1), mkRel (l+nbpar))))
+		 (NonPar (env,c',n,mkRel i, mkRel (l+nbpar))))
 
 let failwith_non_pos n ntypes c =
   for k = n to n + ntypes - 1 do
@@ -408,7 +390,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
     | _::hyps ->
         match kind_of_term (whd_betadeltaiota env lpar.(k)) with
 	  | Rel w when Int.equal w index -> check (k-1) (index+1) hyps
-	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
+	  | _ -> raise (IllFormedInd (LocalNonPar (k+1, index-n+nhyps+1, l)))
   in check (nparams-1) (n-nhyps) hyps;
   if not (Array.for_all (noccur_between n ntypes) largs') then
     failwith_non_pos_vect n ntypes largs'
@@ -663,10 +645,28 @@ exception UndefinableExpansion
     build an expansion function.
     The term built is expecting to be substituted first by 
     a substitution of the form [params, x : ind params] *)
-let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
-    mind_consnrealdecls mind_consnrealargs ctx =
+let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
+    mind_consnrealdecls mind_consnrealargs paramslet ctx =
   let mp, dp, l = repr_mind kn in
-  let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in
+  (** We build a substitution smashing the lets in the record parameters so
+      that typechecking projections requires just a substitution and not
+      matching with a parameter context. *)
+  let indty, paramsletsubst =
+    let subst, inst = 
+      List.fold_right
+	(fun (na, b, t) (subst, inst) ->
+	 match b with
+	 | None -> (mkRel 1 :: List.map (lift 1) subst,
+		   mkRel 1 :: List.map (lift 1) inst)
+	 | Some b -> (substl subst b) :: subst, List.map (lift 1) inst)
+	paramslet ([], [])
+    in
+    let subst = (* For the record parameter: *)
+      mkRel 1 :: List.map (lift 1) subst
+    in
+    let ty = mkApp (mkIndU indu, CArray.rev_of_list inst) in
+      ty, subst
+  in
   let ci = 
     let print_info =
       { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
@@ -679,34 +679,39 @@ let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
   let len = List.length ctx in
   let x = Name x in
   let compat_body ccl i = 
-    (* [ccl] is defined in context [params;x:rp] *)
-    (* [ccl'] is defined in context [params;x:rp;x:rp] *)
+    (* [ccl] is defined in context [params;x:indty] *)
+    (* [ccl'] is defined in context [params;x:indty;x:indty] *)
     let ccl' = liftn 1 2 ccl in
-    let p = mkLambda (x, lift 1 rp, ccl') in
+    let p = mkLambda (x, lift 1 indty, ccl') in
     let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
     let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
-      it_mkLambda_or_LetIn (mkLambda (x,rp,body)) params
+      it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
   in
-  let projections (na, b, t) (i, j, kns, pbs, subst) =
+  let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) =
     match b with
-    | Some c -> (i, j+1, kns, pbs, substl subst c :: subst)
+    | Some c -> (i, j+1, kns, pbs, substl subst c :: subst,
+		substl letsubst c :: subst)
     | None ->
       match na with
       | Name id ->
 	let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
+	let projty = substl letsubst (liftn 1 j t) in
 	let ty = substl subst (liftn 1 j t) in
 	let term = mkProj (Projection.make kn true, mkRel 1) in
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
 	let compat = compat_body ty (j - 1) in
-	let etab = it_mkLambda_or_LetIn (mkLambda (x, rp, term)) params in
-	let etat = it_mkProd_or_LetIn (mkProd (x, rp, ty)) params in
+	let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
+	let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
 	let body = { proj_ind = fst ind; proj_npars = nparamargs;
-		     proj_arg = i; proj_type = ty; proj_eta = etab, etat; 
+		     proj_arg = i; proj_type = projty; proj_eta = etab, etat; 
 		     proj_body = compat } in
-	  (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: subst)
+	  (i + 1, j + 1, kn :: kns, body :: pbs,
+	   fterm :: subst, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
   in
-  let (_, _, kns, pbs, subst) = List.fold_right projections ctx (0, 1, [], [], []) in
+  let (_, _, kns, pbs, subst, letsubst) =
+    List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
+  in
     Array.of_list (List.rev kns),
     Array.of_list (List.rev pbs)
 
@@ -792,12 +797,12 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 	else Univ.Instance.empty 
       in
       let indsp = ((kn, 0), u) in
-      let rctx, _ = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
+      let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
 	(try 
-	   let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in
+	   let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
 	   let kns, projs = 
 	     compute_projections indsp pkt.mind_typename rid nparamargs params
-	       pkt.mind_consnrealdecls pkt.mind_consnrealargs fields
+	       pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
 	   in Some (Some (rid, kns, projs))
 	 with UndefinableExpansion -> Some None)
     | Some _ -> Some None