From 3a6b08286ac78c674d6d3e3073b38de26a610fdc Mon Sep 17 00:00:00 2001 From: mlasson Date: Mon, 22 Jun 2015 21:14:20 +0200 Subject: Template polymorphism: A bug-fix for Bug #4258 Reviewed by M. Sozeau This commit fixes template polymorphism and makes it more precise, applying to non-linear uses of the same universe in parameters of template-polymorphic inductives. See bug report and https://github.com/coq/coq/pull/69 for full details. I also removed some deadcode in checker/inductive.ml. I do not know if it is also necessary to fix checker/indtypes.ml. --- kernel/indtypes.ml | 39 +++++++++++---------------------------- 1 file changed, 11 insertions(+), 28 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 6b909824ba..e80a3a5a42 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -175,36 +175,19 @@ let cumulate_arity_large_levels env sign = let is_impredicative env u = is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet) +(* 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. *) -- cgit v1.2.3 From e1f5a499c43ec0d7b7ebe696941217fb503e2596 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 9 Jul 2015 16:09:29 +0200 Subject: Kernel: primitive projections handling of let-ins Fixes bug #4176 (actually two bugs in one) Correct computation of the type of primitive projections in presence of let-ins. --- kernel/indtypes.ml | 57 ++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 40 insertions(+), 17 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e80a3a5a42..31c0e83c84 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -646,10 +646,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 @@ -662,34 +680,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) @@ -775,12 +798,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 From 9c732a5c878bac2592cb397aca3d17cfefdcd023 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 Jul 2015 01:13:59 +0200 Subject: Option -type-in-type: added support in checker and making it contaminating in vo files (this was not done yet in 24d0027f0 and 090fffa57b). Reused field "engagement" to carry information about both impredicativity of set and type in type. For the record: maybe some further checks to do around the sort of the inductive types in coqchk? --- kernel/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 31c0e83c84..9c79009dba 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -173,7 +173,7 @@ 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 -- cgit v1.2.3