diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 46 |
1 files changed, 40 insertions, 6 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 403dcfd1a3..214e19fecf 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Univ @@ -269,6 +269,11 @@ let projection_nparams_env env p = let projection_nparams p = projection_nparams_env (Global.env ()) p +let has_dependent_elim mib = + match mib.mind_record with + | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite + | _ -> true + (* Annotation for cases *) let make_case_info env ind style = let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -338,6 +343,35 @@ let get_projections env (ind,params) = | Some (Some (id, projs, pbs)) -> Some projs | _ -> None +let make_case_or_project env indf ci pred c branches = + let projs = get_projections env indf in + match projs with + | None -> (mkCase (ci, pred, c, branches)) + | Some ps -> + assert(Array.length branches == 1); + let () = + let _, _, t = destLambda pred in + let (ind, _), _ = dest_ind_family indf in + let mib, _ = Inductive.lookup_mind_specif env ind in + if (* dependent *) not (noccurn 1 t) && + not (has_dependent_elim mib) then + errorlabstrm "make_case_or_project" + Pp.(str"Dependent case analysis not allowed" ++ + str" on inductive type " ++ Names.MutInd.print (fst ind)) + in + let branch = branches.(0) in + let ctx, br = decompose_lam_n_assum (Array.length ps) branch in + let n, subst = + List.fold_right + (fun decl (i, subst) -> + match decl with + | LocalAssum (na, t) -> + let t = mkProj (Projection.make ps.(i) true, c) in + (i + 1, t :: subst) + | LocalDef (na, b, t) -> (i, substl subst b :: subst)) + ctx (0, []) + in substl subst br + (* substitution in a signature *) let substnl_rel_context subst n sign = @@ -417,7 +451,7 @@ let extract_mrectype t = | _ -> raise Not_found let find_mrectype_vect env sigma c = - let (t, l) = decompose_appvect (whd_betadeltaiota env sigma c) in + let (t, l) = decompose_appvect (whd_all env sigma c) in match kind_of_term t with | Ind ind -> (ind, l) | _ -> raise Not_found @@ -426,7 +460,7 @@ let find_mrectype env sigma c = let (ind, v) = find_mrectype_vect env sigma c in (ind, Array.to_list v) let find_rectype env sigma c = - let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in + let (t, l) = decompose_app (whd_all env sigma c) in match kind_of_term t with | Ind (ind,u as indu) -> let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -436,7 +470,7 @@ let find_rectype env sigma c = | _ -> raise Not_found let find_inductive env sigma c = - let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in + let (t, l) = decompose_app (whd_all env sigma c) in match kind_of_term t with | Ind ind when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite -> @@ -444,7 +478,7 @@ let find_inductive env sigma c = | _ -> raise Not_found let find_coinductive env sigma c = - let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in + let (t, l) = decompose_app (whd_all env sigma c) in match kind_of_term t with | Ind ind when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite -> @@ -458,7 +492,7 @@ let find_coinductive env sigma c = let is_predicate_explicitly_dep env pred arsign = let rec srec env pval arsign = - let pv' = whd_betadeltaiota env Evd.empty pval in + let pv' = whd_all env Evd.empty pval in match kind_of_term pv', arsign with | Lambda (na,t,b), (LocalAssum _)::arsign -> srec (push_rel_assum (na,t) env) b arsign |