diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 43 |
1 files changed, 27 insertions, 16 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 4c02dc0f09..678aebfbe6 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -15,6 +15,7 @@ open Univ open Term open Constr open Vars +open Context open Termops open Declarations open Declareops @@ -60,6 +61,8 @@ let lift_inductive_family n = liftn_inductive_family n 1 let substnl_ind_family l n = map_ind_family (substnl l n) +let relevance_of_inductive_family env ((ind,_),_ : inductive_family) = + Inductive.relevance_of_inductive env ind type inductive_type = IndType of inductive_family * EConstr.constr list @@ -75,6 +78,9 @@ let lift_inductive_type n = liftn_inductive_type n 1 let substnl_ind_type l n = map_inductive_type (EConstr.Vars.substnl l n) +let relevance_of_inductive_type env (IndType (indf, _)) = + relevance_of_inductive_family env indf + let mkAppliedInd (IndType ((ind,params), realargs)) = let open EConstr in let ind = on_snd EInstance.make ind in @@ -101,7 +107,8 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j = and nconstr = Array.length mip.mind_consnames in let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in if j > nconstr then user_err Pp.(str "Not enough constructors in the type."); - substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1)) + let (ctx, cty) = specif.(j - 1) in + substl (List.init ntypes make_Ik) (subst_instance_constr u (Term.it_mkProd_or_LetIn cty ctx)) (* Number of constructors *) @@ -275,13 +282,12 @@ let has_dependent_elim mib = | NotRecord | FakeRecord -> true (* Annotation for cases *) -let make_case_info env ind style = +let make_case_info env ind r style = let (mib,mip) = Inductive.lookup_mind_specif env ind in let ind_tags = Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in let cstr_tags = - Array.map2 (fun c n -> - let d,_ = decompose_prod_assum c in + Array.map2 (fun (d, _) n -> Context.Rel.to_tags (List.firstn n d)) mip.mind_nf_lc mip.mind_consnrealdecls in let print_info = { ind_tags; cstr_tags; style } in @@ -289,6 +295,7 @@ let make_case_info env ind style = ci_npar = mib.mind_nparams; ci_cstr_ndecls = mip.mind_consnrealdecls; ci_cstr_nargs = mip.mind_consnrealargs; + ci_relevance = r; ci_pp_info = print_info } (*s Useful functions *) @@ -419,12 +426,14 @@ let build_dependent_inductive env ((ind, params) as indf) = (* builds the arity of an elimination predicate in sort [s] *) let make_arity_signature env sigma dep indf = - let (arsign,_) = get_arity env indf in + let (arsign,s) = get_arity env indf in + let r = Sorts.relevance_of_sort_family s in + let anon = make_annot Anonymous r in let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in if dep then (* We need names everywhere *) Namegen.name_context env sigma - ((LocalAssum (Anonymous,EConstr.of_constr (build_dependent_inductive env indf)))::arsign) + ((LocalAssum (anon,EConstr.of_constr (build_dependent_inductive env indf)))::arsign) (* Costly: would be better to name once for all at definition time *) else (* No need to enforce names *) @@ -457,12 +466,15 @@ let compute_projections env (kn, i as ind) = let x = match mib.mind_record with | NotRecord | FakeRecord -> anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") - | PrimRecord info-> Name (pi1 (info.(i))) + | PrimRecord info -> + let id, _, _, _ = info.(i) in + make_annot (Name id) mib.mind_packets.(i).mind_relevance in let pkt = mib.mind_packets.(i) in let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in - let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in + let ctx, cty = pkt.mind_nf_lc.(0) in + let rctx, _ = decompose_prod_assum (substl subst (Term.it_mkProd_or_LetIn cty ctx)) in let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in (* We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not @@ -490,7 +502,7 @@ let compute_projections env (kn, i as ind) = let subst = c1 :: subst in (proj_arg, j+1, pbs, subst) | LocalAssum (na,t) -> - match na with + match na.binder_name with | Name id -> let lab = Label.of_id id in let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab in @@ -600,7 +612,7 @@ let is_predicate_explicitly_dep env sigma pred arsign = From Coq > 8.2, using or not the effective dependency of the predicate is parametrable! *) - begin match na with + begin match na.binder_name with | Anonymous -> false | Name _ -> true end @@ -622,9 +634,7 @@ let set_pattern_names env sigma ind brv = let (mib,mip) = Inductive.lookup_mind_specif env ind in let arities = Array.map - (fun c -> - Context.Rel.length ((prod_assum c)) - - mib.mind_nparams) + (fun (d, _) -> List.length d - mib.mind_nparams) mip.mind_nf_lc in Array.map2 (set_names env sigma) arities brv @@ -644,9 +654,10 @@ let type_case_branches_with_names env sigma indspec p c = (* Type of Case predicates *) let arity_of_case_predicate env (ind,params) dep k = - let arsign,_ = get_arity env (ind,params) in + let arsign,s = get_arity env (ind,params) in + let r = Sorts.relevance_of_sort_family s in let mind = build_dependent_inductive env (ind,params) in - let concl = if dep then mkArrow mind (mkSort k) else mkSort k in + let concl = if dep then mkArrow mind r (mkSort k) else mkSort k in Term.it_mkProd_or_LetIn concl arsign (***********************************************) @@ -721,7 +732,7 @@ let control_only_guard env sigma c = match kind c with | CoFix (_,(_,_,_) as cofix) -> Inductive.check_cofix e cofix - | Fix (_,(_,_,_) as fix) -> + | Fix fix -> Inductive.check_fix e fix | _ -> () in |