From 32c83676c96ae4a218de0bec75d2f3353381dfb3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 28 Aug 2014 19:49:16 +0200 Subject: Change the way primitive projections are declared to the kernel. Now kernel/indtypes builds the corresponding terms (has to be trusted) while translate_constant just binds a constant name to the already entered projection body, avoiding the dubious "check" of user given terms. "case" Pattern-matching on primitive records is now disallowed, and the default scheme is implemented using projections and eta (all elimination tactics now use projections as well). Elaborate "let (x, y) := p in t" using let bindings for the projections of p too. --- kernel/closure.ml | 27 +++++++++---------- kernel/cooking.ml | 3 +++ kernel/declarations.mli | 8 +++--- kernel/declareops.ml | 8 +++--- kernel/entries.mli | 2 +- kernel/indtypes.ml | 69 +++++++++++++++++++++++++++++++++++-------------- kernel/indtypes.mli | 5 ++-- kernel/inductive.ml | 11 ++++++-- kernel/inductive.mli | 3 +++ kernel/term_typing.ml | 61 +++++++++++-------------------------------- kernel/typeops.ml | 1 - 11 files changed, 104 insertions(+), 94 deletions(-) (limited to 'kernel') diff --git a/kernel/closure.ml b/kernel/closure.ml index 6dacb7818..fcbe939a9 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -866,22 +866,19 @@ let rec get_parameters depth n argstk = let eta_expand_ind_stacks env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (exp,projs) when Array.length projs > 0 + | Some (projs,pbs) when Array.length projs > 0 && mib.Declarations.mind_finite -> - let primitive = Environ.is_projection projs.(0) env in - if primitive then - (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> - arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) - let pars = mib.Declarations.mind_nparams in - let right = fapp_stack (f, s') in - let (depth, args, s) = strip_update_shift_app m s in - (** Try to drop the params, might fail on partially applied constructors. *) - let argss = try_drop_parameters depth pars args in - let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *) - term = FProj (p, right) }) projs in - argss, [Zapp hstack] - else raise Not_found (* disallow eta-exp for non-primitive records *) - | _ -> raise Not_found + (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> + arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) + let pars = mib.Declarations.mind_nparams in + let right = fapp_stack (f, s') in + let (depth, args, s) = strip_update_shift_app m s in + (** Try to drop the params, might fail on partially applied constructors. *) + let argss = try_drop_parameters depth pars args in + let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *) + term = FProj (p, right) }) projs in + argss, [Zapp hstack] + | _ -> raise Not_found (* disallow eta-exp for non-primitive records *) let rec project_nth_arg n argstk = match argstk with diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 3dd782342..2d316fc1d 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -215,6 +215,8 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = in let projection pb = let c' = abstract_constant_body (expmod pb.proj_body) hyps in + let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in + let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in let ((mind, _), _), n' = try let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in @@ -229,6 +231,7 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = in let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; + proj_eta = etab, etat; proj_type = ty'; proj_body = c' } in let univs = UContext.union abs_ctx univs in diff --git a/kernel/declarations.mli b/kernel/declarations.mli index f76f401b4..2c516cafd 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -53,7 +53,8 @@ type projection_body = { proj_npars : int; proj_arg : int; proj_type : types; (* Type under params *) - proj_body : constr; (* For compatibility, the match version *) + proj_eta : constr * types; (* Eta-expanded term and type *) + proj_body : constr; (* For compatibility with VMs only, the match version *) } type constant_def = @@ -152,9 +153,10 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : (constr * constant array) option; + mind_record : (constant array * projection_body array) option; (** Whether the inductive type has been declared as a record, - In that case we get its canonical eta-expansion and list of projections. *) + In the case it is primitive we get its projection names and checked + projection bodies, otherwise both arrays are empty. *) mind_finite : bool; (** Whether the type is inductive or coinductive *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index f583bff64..5b937207f 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -237,11 +237,11 @@ let subst_mind_packet sub mbp = mind_nb_args = mbp.mind_nb_args; mind_reloc_tbl = mbp.mind_reloc_tbl } -let subst_mind_record sub (c, ps as r) = - let c' = subst_mps sub c in +let subst_mind_record sub (ps, pb as r) = let ps' = Array.smartmap (subst_constant sub) ps in - if c' == c && ps' == ps then r - else (c', ps') + let pb' = Array.smartmap (subst_const_proj sub) pb in + if ps' == ps && pb' == pb then r + else (ps', pb') let subst_mind_body sub mib = { mind_record = Option.smartmap (subst_mind_record sub) mib.mind_record ; diff --git a/kernel/entries.mli b/kernel/entries.mli index 244637acd..5fa0527ef 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -63,7 +63,7 @@ type definition_entry = { const_entry_type : types option; const_entry_polymorphic : bool; const_entry_universes : Univ.universe_context; - const_entry_proj : bool; + const_entry_proj : (mutual_inductive * int) option; const_entry_opaque : bool; const_entry_inline_code : bool } diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 18ebc2aa0..715bdb5da 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -661,24 +661,50 @@ exception UndefinableExpansion 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_expansion ((kn, _ as ind), u) params ctx = +let compute_projections ((kn, _ as ind), u as indsp) nparamargs params + mind_consnrealdecls mind_consnrealargs ctx = let mp, dp, l = repr_mind kn in - let make_proj id = Constant.make1 (KerName.make mp dp (Label.of_id id)) in - let projections acc (na, b, t) = + let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in + let ci = + let print_info = { ind_nargs = 0; 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 x = Name (id_of_string "r") in + let compat_body ccl i = + (* [ccl] is defined in context [params;x:rp] *) + (* [ccl'] is defined in context [params;x:rp;x:rp] *) + let ccl' = liftn 1 2 ccl in + let p = mkLambda (x, lift 1 rp, ccl') in + let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in + let body = mkCase (ci, p, mkRel 1, [|branch|]) in + it_mkLambda_or_LetIn (mkLambda (x,rp,body)) params + in + let projections (na, b, t) (i, j, kns, pbs, subst) = match b with - | Some c -> acc - | None -> + | Some c -> (i, j+1, kns, pbs, c :: subst) + | None -> match na with - | Name id -> make_proj id :: acc + | 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 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; + proj_arg = i; proj_type = ty; proj_eta = etab, etat; + proj_body = compat } in + (i + 1, j + 1, kn :: kns, body :: pbs, term :: subst) | Anonymous -> raise UndefinableExpansion in - let projs = List.fold_left projections [] ctx in - let projarr = Array.of_list projs in - let exp = - mkApp (mkConstructU ((ind, 1),u), - Array.append (rel_appvect 1 params) - (Array.map (fun p -> mkProj (p, mkRel 1)) projarr)) - in exp, projarr + let (_, _, kns, pbs, subst) = List.fold_right projections ctx (0, 1, [], [], []) in + Array.of_list (List.rev kns), + Array.of_list (List.rev pbs) let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in @@ -750,18 +776,21 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re mind_reloc_tbl = rtbl; } in let packets = Array.map2 build_one_packet inds recargs in + let pkt = packets.(0) in let isrecord = match isrecord with - | Some true -> (* || (Array.length pkt.mind_consnames = 1 && *) - let pkt = packets.(0) in + | Some true when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 -> + (** The elimination criterion ensures that all projections can be defined. *) let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in let u = if p then Univ.UContext.instance ctx else Univ.Instance.empty in (try - let exp = compute_expansion ((kn, 0), u) params - (List.firstn pkt.mind_consnrealdecls.(0) rctx) - in Some exp - with UndefinableExpansion -> (Some (mkProp, [||]))) - | Some false -> Some (mkProp, [||]) + let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in + let kns, projs = + compute_projections ((kn, 0), u) nparamargs params + pkt.mind_consnrealdecls pkt.mind_consnrealargs fields + in Some (kns, projs) + with UndefinableExpansion -> Some ([||], [||])) + | Some _ -> Some ([||], [||]) | None -> None in (* Build the mutual inductive *) diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 8730a3045..85e6a6327 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -41,5 +41,6 @@ val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutua val enforce_indices_matter : unit -> unit val is_indices_matter : unit -> bool -val compute_expansion : pinductive -> - Context.rel_context -> Context.rel_context -> (constr * constant array) +val compute_projections : pinductive -> int -> Context.rel_context -> int array -> int array -> + Context.rel_context -> + (constant array * projection_body array) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 6ddddeb05..189c2f4d2 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -294,6 +294,12 @@ let get_instantiated_arity (ind,u) (mib,mip) params = let elim_sorts (_,mip) = mip.mind_kelim +let is_private (mib,_) = mib.mind_private = Some true +let is_primitive_record (mib,_) = + match mib.mind_record with + | Some (projs, _) when Array.length projs > 0 -> true + | _ -> false + let extended_rel_list n hyps = let rec reln l p = function | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps @@ -391,12 +397,13 @@ let type_case_branches env (pind,largs) pj c = (* Checking the case annotation is relevent *) let check_case_info env (indsp,u) ci = - let (mib,mip) = lookup_mind_specif env indsp in + let (mib,mip as spec) = lookup_mind_specif env indsp in if not (eq_ind indsp ci.ci_ind) || not (Int.equal mib.mind_nparams ci.ci_npar) || not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls) || - not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs) + not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs) || + is_primitive_record spec then raise (TypeError(env,WrongCaseInfo((indsp,u),ci))) (************************************************************************) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index bac242f82..55236700d 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -53,6 +53,9 @@ val type_of_inductive_knowing_parameters : val elim_sorts : mind_specif -> sorts_family list +val is_private : mind_specif -> bool +val is_primitive_record : mind_specif -> bool + (** Return type as quoted by the user *) val constrained_type_of_constructor : pconstructor -> mind_specif -> types constrained diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 843d8f8a3..b603610ce 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -107,39 +107,6 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) - -let check_projection env kn usubst body = - let cannot_recognize () = error ("Cannot recognize a projection") in - let ctx, m = decompose_lam_assum body in - let () = if not (isCase m) then cannot_recognize () in - let ci, p, c, b = destCase m in - let (mib, oib as _specif) = Inductive.lookup_mind_specif env ci.ci_ind in - let recinfo = match mib.mind_record with - | None -> - error ("Trying to declare a primitive projection for a non-record inductive type") - | Some (_, r) -> r - in - let n = mib.mind_nparams in - let () = - if n + 1 != List.length ctx || - not (isRel c) || destRel c != 1 || Array.length b != 1 || - not (isLambda p) - then cannot_recognize () - in - let (na, t, ty) = destLambda (Vars.subst1 mkProp p) in - let argctx, p = decompose_lam_assum b.(0) in - (* No need to check the lambdas as the case is well-formed *) - let () = if not (isRel p) then cannot_recognize () in - let var = destRel p in - let () = if not (var <= Array.length recinfo) then cannot_recognize () in - let arg = Array.length recinfo - var in - let () = if not (eq_con_chk recinfo.(arg) kn) then cannot_recognize () in - let pb = { proj_ind = fst ci.ci_ind; - proj_npars = n; - proj_arg = arg; - proj_type = Vars.subst_univs_level_constr usubst ty; - proj_body = Vars.subst_univs_level_constr usubst body } - in pb let subst_instance_j s j = { uj_val = Vars.subst_univs_level_constr s j.uj_val; @@ -186,19 +153,21 @@ let infer_declaration env kn dcl = let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in let def, typ, proj = - if c.const_entry_proj then - (** This should be the projection defined as a match. *) - let j = infer env body in - let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in - (** We check it does indeed have the shape of a projection. *) - let pb = check_projection env (Option.get kn) usubst body in - (** We build the eta-expanded form. *) - let context, m = decompose_lam_n_assum (pb.proj_npars + 1) body in - let body' = mkProj (Option.get kn, mkRel 1) in - let body = it_mkLambda_or_LetIn body' context in - Def (Mod_subst.from_val (hcons_constr (Vars.subst_univs_level_constr usubst body))), - typ, Some pb - else + match c.const_entry_proj with + | Some (ind, i) -> (* Bind c to a checked primitive projection *) + let mib, _ = Inductive.lookup_mind_specif env (ind,0) in + let kn, pb = + match mib.mind_record with + | Some (kns, pbs) -> + if i < Array.length pbs then + kns.(i), pbs.(i) + else assert false + | None -> assert false + in + let term = Vars.subst_univs_level_constr usubst (fst pb.proj_eta) in + let typ = Vars.subst_univs_level_constr usubst (snd pb.proj_eta) in + Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb + | None -> let j = infer env body in let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in diff --git a/kernel/typeops.ml b/kernel/typeops.ml index cb0c429a9..fa7dd105c 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -388,7 +388,6 @@ let judge_of_projection env p cj = assert(eq_mind pb.proj_ind (fst ind)); let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in let ty = substl (cj.uj_val :: List.rev args) ty in - (* TODO: Universe polymorphism for projections *) {uj_val = mkProj (p,cj.uj_val); uj_type = ty} -- cgit v1.2.3