diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 5 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 6 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 8 | ||||
| -rw-r--r-- | pretyping/indrec.mli | 3 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 104 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 12 |
6 files changed, 129 insertions, 9 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index df89d9eac..5a54c6f05 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -690,7 +690,10 @@ and detype_r d flags avoid env sigma t = let c' = try let pb = Environ.lookup_projection p (snd env) in - let body = pb.Declarations.proj_body in + (** FIXME: handle mutual records *) + let ind = (pb.Declarations.proj_ind, 0) in + let bodies = Inductiveops.legacy_match_projection (snd env) ind in + let body = bodies.(pb.Declarations.proj_arg) in let ty = Retyping.get_type_of (snd env) sigma c in let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in let body' = strip_lam_assum body in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 8ecec30cf..11cfd2040 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -414,8 +414,10 @@ let loc_of_glob_constr c = c.CAst.loc (**********************************************************************) (* Alpha-renaming *) +exception UnsoundRenaming + let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l -let test_id l id = if collide_id l id then raise Not_found +let test_id l id = if collide_id l id then raise UnsoundRenaming let test_na l na = Name.iter (test_id l) na let update_subst na l = @@ -429,8 +431,6 @@ let update_subst na l = else na,l) na (na,l) -exception UnsoundRenaming - let rename_var l id = try let id' = Id.List.assoc id l in diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 27b029aad..4ab932723 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -304,7 +304,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = process_constr env 0 f (List.rev cstr.cs_args, recargs) (* Main function *) -let mis_make_indrec env sigma listdepkind mib u = +let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let evdref = ref sigma in @@ -469,7 +469,7 @@ let mis_make_indrec env sigma listdepkind mib u = (* Body on make_one_rec *) let ((indi,u),mibi,mipi,dep,kind) = List.nth listdepkind p in - if (mis_is_recursive_subset + if force_mutual || (mis_is_recursive_subset (List.map (fun ((indi,u),_,_,_,_) -> snd indi) listdepkind) mipi.mind_recargs) then @@ -558,7 +558,7 @@ let check_arities env listdepkind = [] listdepkind in true -let build_mutual_induction_scheme env sigma = function +let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function | ((mind,u),dep,s)::lrecspec -> let (mib,mip) = lookup_mind_specif env mind in if dep && not (Inductiveops.has_dependent_elim mib) then @@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function lrecspec) in let _ = check_arities env listdepkind in - mis_make_indrec env sigma listdepkind mib u + mis_make_indrec env sigma ~force_mutual listdepkind mib u | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types.") let build_induction_scheme env sigma pind dep kind = diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index d87a19d28..de9d3a0ab 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -47,7 +47,8 @@ val build_induction_scheme : env -> evar_map -> pinductive -> (** Builds mutual (recursive) induction schemes *) val build_mutual_induction_scheme : - env -> evar_map -> (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list + env -> evar_map -> ?force_mutual:bool -> + (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list (** Scheme combinators *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index f839d5b98..1003f86c5 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -456,6 +456,110 @@ let build_branch_type env sigma dep p cs = (**************************************************) +(** From a rel context describing the constructor arguments, + 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 env (kn, _ as ind) = + let open Term in + let mib = Environ.lookup_mind kn env in + let indu = match mib.mind_universes with + | Monomorphic_ind _ -> mkInd ind + | Polymorphic_ind ctx -> mkIndU (ind, make_abstract_instance ctx) + | Cumulative_ind ctx -> + mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx)) + in + let x = match mib.mind_record with + | None | Some None -> + anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") + | Some (Some (id, _, _)) -> Name id + in + (** FIXME: handle mutual records *) + let pkt = mib.mind_packets.(0) in + let { mind_consnrealargs; mind_consnrealdecls } = pkt in + let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in + let rctx, _ = decompose_prod_assum (subst1 indu pkt.mind_nf_lc.(0)) in + let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in + let mp, dp, l = MutInd.repr3 kn 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 = + (* [ty] = [Ind inst] is typed in context [params] *) + let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in + let ty = mkApp (indu, inst) in + (* [Ind inst] is typed in context [params-wo-let] *) + ty + in + let ci = + let print_info = + { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in + { ci_ind = ind; + ci_npar = nparamargs; + ci_cstr_ndecls = mind_consnrealdecls; + ci_cstr_nargs = mind_consnrealargs; + ci_pp_info = print_info } + in + let len = List.length ctx in + let compat_body ccl i = + (* [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 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,indty,body)) params + in + let projections decl (j, pbs, subst) = + match decl with + | LocalDef (na,c,t) -> + (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *) + let c = liftn 1 j c in + (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params, x:I |- c(params,proj1 x,..,projj x)] *) + let c1 = substl subst c in + (* From [params, x:I |- subst:field1,..,fieldj] + to [params, x:I |- subst:field1,..,fieldj+1] where [subst] + is represented with instance of field1 last *) + let subst = c1 :: subst in + (j+1, pbs, subst) + | LocalAssum (na,t) -> + match na with + | Name id -> + let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in + (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)] + to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *) + let t = liftn 1 j t in + (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)] + to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *) + (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)] + to [params, x:I |- t(proj1 x,..,projj x)] *) + let ty = substl subst 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, indty, term)) params in + let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in + let body = (etab, etat, compat) in + (j + 1, body :: pbs, fterm :: subst) + | Anonymous -> + anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") + in + let (_, pbs, subst) = + List.fold_right projections ctx (1, [], []) + in + Array.rev_of_list pbs + +let legacy_match_projection env ind = + Array.map pi3 (compute_projections env ind) + +let compute_projections ind mib = + let ans = compute_projections ind mib in + Array.map (fun (prj, ty, _) -> (prj, ty)) ans + +(**************************************************) + let extract_mrectype sigma t = let open EConstr in let (t, l) = decompose_app sigma t in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index b0d714b03..aa53f7e67 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -194,6 +194,18 @@ val make_case_or_project : val make_default_case_info : env -> case_style -> inductive -> case_info i*) +val compute_projections : Environ.env -> inductive -> (constr * types) array +(** Given a primitive record type, for every field computes the eta-expanded + projection and its type. *) + +val legacy_match_projection : Environ.env -> inductive -> constr array +(** Given a record type, computes the legacy match-based projection of the + projections. + + BEWARE: such terms are ill-typed, and should thus only be used in upper + layers. The kernel will probably badly fail if presented with one of + those. *) + (********************) val type_of_inductive_knowing_conclusion : |