From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- kernel/indtypes.ml | 109 ++++++++++++++++++++++++++++------------------------- 1 file changed, 57 insertions(+), 52 deletions(-) (limited to 'kernel/indtypes.ml') 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 -- cgit v1.2.3