From 4341f37cf3c51ed82c23f05846c8e6e8823d3cd6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 10 Mar 2016 19:02:16 +0100 Subject: Primitive projections: protect kernel from erroneous definitions. E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive records with eta for which conversion is incomplete. - Eta-conversion only applies to BiFinite inductives - Finiteness information is now checked by the kernel (the constructor types must be strictly non recursive for BiFinite declarations). --- kernel/closure.ml | 2 +- kernel/indtypes.ml | 19 ++++++++++++------- pretyping/evarconv.ml | 2 +- printing/prettyp.ml | 4 ++-- test-suite/success/primitiveproj.v | 16 +--------------- 5 files changed, 17 insertions(+), 26 deletions(-) diff --git a/kernel/closure.ml b/kernel/closure.ml index 2ba80d8362..93e63d0fb5 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -784,7 +784,7 @@ let eta_expand_ind_stack env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (Some (_,projs,pbs)) when - mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> + mib.Declarations.mind_finite == Decl_kinds.BiFinite -> (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) let pars = mib.Declarations.mind_nparams in diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 49e8583158..acf5ab17d3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -452,7 +452,7 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else (* The recursive function that checks positivity and builds the list of recursive arguments *) -let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc = +let check_positivity_one recursive (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc = let lparams = rel_context_length hyps in let nmr = rel_context_nhyps hyps in (* Checking the (strict) positivity of a constructor argument type [c] *) @@ -538,6 +538,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname | Prod (na,b,d) -> let () = assert (List.is_empty largs) in + if not recursive && not (noccur_between n ntypes b) then + raise (InductiveError BadEntry); let nmr',recarg = check_pos ienv nmr b in let ienv' = ienv_push_var ienv (na,b,mk_norec) in check_constr_rec ienv' nmr' (recarg::lrec) d @@ -570,9 +572,11 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname and nmr' = array_min nmr irecargs_nmr in (nmr', mk_paths (Mrec ind) irecargs) -let check_positivity kn env_ar params inds = +let check_positivity kn env_ar params finite inds = let ntypes = Array.length inds in - let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in + let recursive = finite != Decl_kinds.BiFinite in + let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) + (Rtree.mk_rec_calls ntypes) in let lra_ind = Array.rev_to_list rc in let lparams = rel_context_length params in let nmr = rel_context_nhyps params in @@ -581,7 +585,7 @@ let check_positivity kn env_ar params inds = List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in let nargs = rel_context_nhyps sign - nmr in - check_positivity_one ienv params (kn,i) nargs lcnames lc + check_positivity_one recursive ienv params (kn,i) nargs lcnames lc in let irecargs_nmr = Array.mapi check_one inds in let irecargs = Array.map snd irecargs_nmr @@ -807,10 +811,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re mind_reloc_tbl = rtbl; } in let packets = Array.map2 build_one_packet inds recargs in - let pkt = packets.(0) in + let pkt = packets.(0) in let isrecord = match isrecord with - | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 + | Some (Some rid) when pkt.mind_kelim == all_sorts + && Array.length pkt.mind_consnames == 1 && pkt.mind_consnrealargs.(0) > 0 -> (** The elimination criterion ensures that all projections can be defined. *) let u = @@ -851,7 +856,7 @@ let check_inductive env kn mie = (* First type-check the inductive definition *) let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in (* Then check positivity conditions *) - let (nmr,recargs) = check_positivity kn env_ar_par params inds in + let (nmr,recargs) = check_positivity kn env_ar_par params mie.mind_entry_finite inds in (* Build the inductive packets *) build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 637a9e50e0..690b974be5 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -854,7 +854,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> + | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fd51fd6b0f..4d9d40ae08 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -215,8 +215,8 @@ let print_polymorphism ref = let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with - | Decl_kinds.CoFinite -> mt () - | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion" + | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt () + | Decl_kinds.BiFinite -> str " and has eta conversion" in [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."] | _ -> [] diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 281d707cb3..b5e6ccd618 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -35,10 +35,6 @@ Set Implicit Arguments. Check nat. -(* Inductive X (U:Type) := Foo (k : nat) (x : X U). *) -(* Parameter x : X nat. *) -(* Check x.(k). *) - Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }. Parameter x:X nat. @@ -49,18 +45,8 @@ Inductive Y := { next : option Y }. Check _.(next) : option Y. Lemma eta_ind (y : Y) : y = Build_Y y.(next). -Proof. reflexivity. Defined. - -Variable t : Y. - -Fixpoint yn (n : nat) (y : Y) : Y := - match n with - | 0 => t - | S n => {| next := Some (yn n y) |} - end. +Proof. Fail reflexivity. Abort. -Lemma eta_ind' (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}. -Proof. reflexivity. Defined. (* -- cgit v1.2.3