From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- pretyping/inductiveops.ml | 154 ++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 129 insertions(+), 25 deletions(-) (limited to 'pretyping/inductiveops.ml') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 97aa82e4..0fa573b9 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -51,7 +51,7 @@ let arities_of_constructors env (ind,u as indu) = type inductive_family = pinductive * constr list let make_ind_family (mis, params) = (mis,params) -let dest_ind_family (mis,params) = (mis,params) +let dest_ind_family (mis,params) : inductive_family = (mis,params) let map_ind_family f (mis,params) = (mis, List.map f params) @@ -269,16 +269,14 @@ let allowed_sorts env (kn,i as ind) = let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_kelim -let projection_nparams_env env p = - let pb = lookup_projection p env in - pb.proj_npars +let projection_nparams_env _ p = Projection.npars p -let projection_nparams p = projection_nparams_env (Global.env ()) p +let projection_nparams p = Projection.npars p let has_dependent_elim mib = match mib.mind_record with - | Some (Some _) -> mib.mind_finite == BiFinite - | _ -> true + | PrimRecord _ -> mib.mind_finite == BiFinite + | NotRecord | FakeRecord -> true (* Annotation for cases *) let make_case_info env ind style = @@ -303,7 +301,7 @@ type constructor_summary = { cs_cstr : pconstructor; cs_params : constr list; cs_nargs : int; - cs_args : Context.Rel.t; + cs_args : Constr.rel_context; cs_concl_realargs : constr array } @@ -343,41 +341,39 @@ let get_constructors env (ind,params) = Array.init (Array.length mip.mind_consnames) (fun j -> get_constructor (ind,mib,mip,params) (j+1)) -let get_projections env (ind,params) = - let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in - match mib.mind_record with - | Some (Some (id, projs, pbs)) -> Some projs - | _ -> None +let get_projections = Environ.get_projections let make_case_or_project env sigma indf ci pred c branches = let open EConstr in - let projs = get_projections env indf in + let projs = get_projections env (fst (fst indf)) in match projs with | None -> (mkCase (ci, pred, c, branches)) | Some ps -> assert(Array.length branches == 1); + let na, ty, t = destLambda sigma pred in let () = - let _, _, t = destLambda sigma pred in let (ind, _), _ = dest_ind_family indf in let mib, _ = Inductive.lookup_mind_specif env ind in if (* dependent *) not (Vars.noccurn sigma 1 t) && not (has_dependent_elim mib) then user_err ~hdr:"make_case_or_project" Pp.(str"Dependent case analysis not allowed" ++ - str" on inductive type " ++ Names.MutInd.print (fst ind)) + str" on inductive type " ++ Termops.Internal.print_constr_env env sigma (mkInd ind)) in let branch = branches.(0) in let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in - let n, subst = + let n, len, ctx = List.fold_right - (fun decl (i, subst) -> + (fun decl (i, j, ctx) -> 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, Vars.substl subst b :: subst)) - ctx (0, []) - in Vars.substl subst br + | LocalAssum (na, ty) -> + let t = mkProj (Projection.make ps.(i) true, mkRel j) in + (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx) + | LocalDef (na, b, ty) -> + (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx)) + ctx (0, 1, []) + in + mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx) (* substitution in a signature *) @@ -454,6 +450,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, i as ind) = + let open Term in + let mib = Environ.lookup_mind kn env in + let u = match mib.mind_universes with + | Monomorphic_ind _ -> Instance.empty + | Polymorphic_ind auctx -> make_abstract_instance auctx + | Cumulative_ind acumi -> + make_abstract_instance (ACumulativityInfo.univ_context acumi) + in + 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))) + 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, 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 + 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 indu = mkIndU (ind, u) 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 = pkt.mind_consnrealdecls; + ci_cstr_nargs = pkt.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 (proj_arg, 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 + (proj_arg, j+1, pbs, subst) + | LocalAssum (na,t) -> + match na 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 + (* 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 + (proj_arg + 1, 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 (0, 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 @@ -629,6 +729,10 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = env evdref scl ar.template_level (ctx,ar.template_param_levels) in !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl)) +let type_of_projection_constant env (p,u) = + let pty = lookup_projection p env in + Vars.subst_instance_constr u pty + let type_of_projection_knowing_arg env sigma p c ty = let c = EConstr.Unsafe.to_constr c in let IndType(pars,realargs) = @@ -637,7 +741,7 @@ let type_of_projection_knowing_arg env sigma p c ty = raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type") in let (_,u), pars = dest_ind_family pars in - substl (c :: List.rev pars) (Typeops.type_of_projection_constant env (p,u)) + substl (c :: List.rev pars) (type_of_projection_constant env (p,u)) (***********************************************) (* Guard condition *) -- cgit v1.2.3