diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-10 12:56:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-10 13:01:24 +0200 |
| commit | 6624459e492164b3d189e3518864379ff985bf8c (patch) | |
| tree | 9fc004c5f25927f671667d0cf5475061b306e1f0 | |
| parent | c2fa953889cf7bcef9c369d175e156855ac0be2e (diff) | |
Fix generation of inductive elimination principle for primitive records.
Let r.(p) be a strict subterm of r during the guardness check.
| -rw-r--r-- | kernel/indtypes.ml | 4 | ||||
| -rw-r--r-- | kernel/inductive.ml | 7 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 25 |
3 files changed, 30 insertions, 6 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 2e9a81d98..4feec40e8 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -686,14 +686,14 @@ let compute_projections ((kn, _ as ind), u as indsp) n nparamargs params in let projections (na, b, t) (i, j, kns, pbs, subst) = match b with - | Some c -> (i, j+1, kns, pbs, c :: subst) + | Some c -> (i, j+1, kns, pbs, substl subst c :: subst) | None -> match na with | Name id -> let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in let ty = substl subst (liftn 1 j t) in let term = mkProj (kn, mkRel 1) in - let compat = compat_body ty i 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 body = { proj_ind = fst ind; proj_npars = nparamargs; diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 6975544ac..58909ce01 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -814,6 +814,13 @@ let rec subterm_specif renv stack t = (* Metas and evars are considered OK *) | (Meta _|Evar _) -> Dead_code + | Proj (p, c) -> + let subt = subterm_specif renv stack c in + (match subt with + | Subterm (s, wf) -> Subterm (Strict, wf) + | Dead_code -> Dead_code + | Not_subterm -> Not_subterm) + (* Other terms are not subterms *) | _ -> Not_subterm diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 54f76fa33..0cbfa7597 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -378,10 +378,27 @@ let mis_make_indrec env sigma listdepkind mib u = (Anonymous,depind',concl)) arsign' in - it_mkLambda_or_LetIn_name env - (mkCase (ci, pred, - mkRel 1, - branches)) + let obj = + let projs = get_projections env indf in + match projs with + | None -> (mkCase (ci, pred, + mkRel 1, + branches)) + | Some ps -> + let branch = branches.(0) in + let ctx, br = decompose_lam_assum branch in + let n, subst = + List.fold_right (fun (na,b,t) (i, subst) -> + if b == None then + let t = mkProj (ps.(i), mkRel 1) in + (i + 1, t :: subst) + else (i, mkRel 0 :: subst)) + ctx (0, []) + in + let term = substl subst br in + term + in + it_mkLambda_or_LetIn_name env obj (Termops.lift_rel_context nrec deparsign) in |