aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/closure.ml27
-rw-r--r--kernel/cooking.ml3
-rw-r--r--kernel/declarations.mli8
-rw-r--r--kernel/declareops.ml8
-rw-r--r--kernel/entries.mli2
-rw-r--r--kernel/indtypes.ml69
-rw-r--r--kernel/indtypes.mli5
-rw-r--r--kernel/inductive.ml11
-rw-r--r--kernel/inductive.mli3
-rw-r--r--kernel/term_typing.ml61
-rw-r--r--kernel/typeops.ml1
-rw-r--r--library/declare.ml4
-rw-r--r--plugins/extraction/extraction.ml2
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/indrec.ml23
-rw-r--r--pretyping/inductiveops.ml6
-rw-r--r--pretyping/inductiveops.mli2
-rw-r--r--pretyping/pretyping.ml68
-rw-r--r--pretyping/tacred.ml13
-rw-r--r--pretyping/tacred.mli4
-rw-r--r--pretyping/unification.ml2
-rw-r--r--proofs/proof_global.ml2
-rw-r--r--toplevel/command.ml4
-rw-r--r--toplevel/ind_tables.ml2
-rw-r--r--toplevel/indschemes.ml2
-rw-r--r--toplevel/obligations.ml2
-rw-r--r--toplevel/record.ml28
27 files changed, 215 insertions, 149 deletions
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}
diff --git a/library/declare.ml b/library/declare.ml
index b80ceb6e6..a18a6a60b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -199,7 +199,7 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types
{ const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff);
const_entry_secctx = None;
const_entry_type = types;
- const_entry_proj = false;
+ const_entry_proj = None;
const_entry_polymorphic = poly;
const_entry_universes = univs;
const_entry_opaque = opaque;
@@ -244,7 +244,7 @@ let declare_sideff env fix_exn se =
const_entry_feedback = None;
const_entry_polymorphic = cb.const_polymorphic;
const_entry_universes = univs;
- const_entry_proj = false;
+ const_entry_proj = None;
});
cst_hyps = [] ;
cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition;
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 498b33b63..d2e95a74b 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -215,7 +215,7 @@ let oib_equal o1 o2 =
Array.equal Id.equal o1.mind_consnames o2.mind_consnames
let eq_record x y =
- Option.equal (fun (x, y) (x', y') -> eq_constr x x') x y
+ Option.equal (fun (x, y) (x', y') -> Array.for_all2 eq_constant x x') x y
let mib_equal m1 m2 =
Array.equal oib_equal m1.mind_packets m1.mind_packets &&
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 04c69d74a..627a954f9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -760,7 +760,7 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),
and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
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 pars = mib.Declarations.mind_nparams in
(try
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 81b5c9ad8..547268ef0 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -60,7 +60,11 @@ let check_privacy_block mib =
let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
let lnamespar = Vars.subst_instance_context u mib.mind_params_ctxt in
- let () = check_privacy_block mib in
+ let indf = make_ind_family(pind, Termops.extended_rel_list 0 lnamespar) in
+ let constrs = get_constructors env indf in
+ let projs = get_projections env indf in
+
+ let () = if Option.is_empty projs then check_privacy_block mib in
let () =
if not (Sorts.List.mem kind (elim_sorts specif)) then
raise
@@ -73,8 +77,6 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
(* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
let env' = push_rel_context lnamespar env in
- let indf = make_ind_family(pind, Termops.extended_rel_list 0 lnamespar) in
- let constrs = get_constructors env indf in
let rec add_branch env k =
if Int.equal k (Array.length mip.mind_consnames) then
@@ -97,11 +99,16 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
(Anonymous,depind,pbody))
arsign
in
- it_mkLambda_or_LetIn_name env'
- (mkCase (ci, lift ndepar p,
- mkRel 1,
- Termops.rel_vect ndepar k))
- deparsign
+ let obj =
+ match projs with
+ | None -> mkCase (ci, lift ndepar p, mkRel 1,
+ Termops.rel_vect ndepar k)
+ | Some ps ->
+ let term = mkApp (mkRel 2, Array.map (fun p -> mkProj (p, mkRel 1)) ps) in
+ let ty = mkApp (mkRel 3, [| mkRel 1 |]) in
+ mkCast (term, DEFAULTcast, ty)
+ in
+ it_mkLambda_or_LetIn_name env' obj deparsign
else
let cs = lift_constructor (k+1) constrs.(k) in
let t = build_branch_type env dep (mkRel (k+1)) cs in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 34243f499..913afb219 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -331,6 +331,12 @@ 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 (projs, pbs) when Array.length projs > 0 -> Some projs
+ | _ -> None
+
(* substitution in a signature *)
let substnl_rel_context subst n sign =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 03d41015b..124f3a34e 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -140,6 +140,8 @@ val get_constructor :
int -> constructor_summary
val get_arity : env -> inductive_family -> rel_context * sorts_family
val get_constructors : env -> inductive_family -> constructor_summary array
+val get_projections : env -> inductive_family -> constant array option
+
val build_dependent_constructor : constructor_summary -> constr
val build_dependent_inductive : env -> inductive_family -> constr
val make_arity_signature : env -> bool -> inductive_family -> rel_context
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cb3e81efe..56a667115 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -678,25 +678,46 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
error_case_not_inductive_loc cloc env !evdref cj
in
let cstrs = get_constructors env indf in
- if not (Int.equal (Array.length cstrs) 1) then
- user_err_loc (loc,"",str "Destructing let is only for inductive types" ++
- str " with one constructor.");
- let cs = cstrs.(0) in
- if not (Int.equal (List.length nal) cs.cs_nargs) then
- user_err_loc (loc,"", str "Destructing let on this type expects " ++
- int cs.cs_nargs ++ str " variables.");
- let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
- (List.rev nal) cs.cs_args in
- let env_f = push_rel_context fsign env in
- (* Make dependencies from arity signature impossible *)
- let arsgn =
- let arsgn,_ = get_arity env indf in
- if not !allow_anonymous_refs then
- List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
- else arsgn
- in
- let psign = (na,None,build_dependent_inductive env indf)::arsgn in
- let nar = List.length arsgn in
+ if not (Int.equal (Array.length cstrs) 1) then
+ user_err_loc (loc,"",str "Destructing let is only for inductive types" ++
+ str " with one constructor.");
+ let cs = cstrs.(0) in
+ if not (Int.equal (List.length nal) cs.cs_nargs) then
+ user_err_loc (loc,"", str "Destructing let on this type expects " ++
+ int cs.cs_nargs ++ str " variables.");
+ let fsign, record =
+ match get_projections env indf with
+ | None -> List.map2 (fun na (_,c,t) -> (na,c,t))
+ (List.rev nal) cs.cs_args, false
+ | Some ps ->
+ let rec aux n k names l =
+ match names, l with
+ | na :: names, ((_, None, t) :: l) ->
+ (na, Some (lift (cs.cs_nargs - n) (mkProj (ps.(cs.cs_nargs - k), cj.uj_val))), t)
+ :: aux (n+1) (k + 1) names l
+ | na :: names, ((_, c, t) :: l) ->
+ (na, c, t) :: aux (n+1) k names l
+ | [], [] -> []
+ | _ -> assert false
+ in aux 1 1 (List.rev nal) cs.cs_args, true
+ in
+ let obj ind p v f =
+ if not record then
+ let f = it_mkLambda_or_LetIn f fsign in
+ let ci = make_case_info env (fst ind) LetStyle in
+ mkCase (ci, p, cj.uj_val,[|f|])
+ else it_mkLambda_or_LetIn f fsign
+ in
+ let env_f = push_rel_context fsign env in
+ (* Make dependencies from arity signature impossible *)
+ let arsgn =
+ let arsgn,_ = get_arity env indf in
+ if not !allow_anonymous_refs then
+ List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
+ else arsgn
+ in
+ let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+ let nar = List.length arsgn in
(match po with
| Some p ->
let env_p = push_rel_context psign env in
@@ -710,18 +731,16 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
let lp = lift cs.cs_nargs p in
let fty = hnf_lam_applist env !evdref lp inst in
let fj = pretype (mk_tycon fty) env_f evdref lvar d in
- let f = it_mkLambda_or_LetIn fj.uj_val fsign in
let v =
let ind,_ = dest_ind_family indf in
- let ci = make_case_info env (fst ind) LetStyle in
Typing.check_allowed_sort env !evdref ind cj.uj_val p;
- mkCase (ci, p, cj.uj_val,[|f|]) in
+ obj ind p cj.uj_val fj.uj_val
+ in
{ uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
| None ->
let tycon = lift_tycon cs.cs_nargs tycon in
let fj = pretype tycon env_f evdref lvar d in
- let f = it_mkLambda_or_LetIn fj.uj_val fsign in
let ccl = nf_evar !evdref fj.uj_type in
let ccl =
if noccur_between 1 cs.cs_nargs ccl then
@@ -733,9 +752,8 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
let v =
let ind,_ = dest_ind_family indf in
- let ci = make_case_info env (fst ind) LetStyle in
Typing.check_allowed_sort env !evdref ind cj.uj_val p;
- mkCase (ci, p, cj.uj_val,[|f|])
+ obj ind p cj.uj_val fj.uj_val
in { uj_val = v; uj_type = ccl })
| GIf (loc,c,(na,po),b1,b2) ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index a2791f7a2..d1ab5b15d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1110,9 +1110,18 @@ let pattern_occs loccs_trm env sigma c =
(* Used in several tactics. *)
let check_privacy env ind =
- if (fst (Inductive.lookup_mind_specif env (fst ind))).Declarations.mind_private = Some true then
- errorlabstrm "" (str "case analysis on a private type")
+ let spec = Inductive.lookup_mind_specif env (fst ind) in
+ if Inductive.is_private spec then
+ errorlabstrm "" (str "case analysis on a private type.")
else ind
+
+let check_not_primitive_record env ind =
+ let spec = Inductive.lookup_mind_specif env (fst ind) in
+ if Inductive.is_primitive_record spec then
+ errorlabstrm "" (str "case analysis on a primitive record type: " ++
+ str "use projections or let instead.")
+ else ind
+
(* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
return name, B and t' *)
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 91364c4ae..6d12d5d44 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -103,3 +103,7 @@ val e_contextually : bool -> occurrences * constr_pattern ->
(** Returns the same inductive if it is allowed for pattern-matching
raises an error otherwise. **)
val check_privacy : env -> inductive puniverses -> inductive puniverses
+
+(** Returns the same inductive if it is not a primitive record
+ raises an error otherwise. **)
+val check_not_primitive_record : env -> inductive puniverses -> inductive puniverses
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index aee7be981..46f65271f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -471,7 +471,7 @@ let eta_constructor_app env f l1 term =
| Construct (((_, i as ind), j), u) ->
let mib = lookup_mind (fst ind) env in
(match mib.Declarations.mind_record with
- | Some (exp,projs) ->
+ | Some (projs, _) ->
let pars = mib.Declarations.mind_nparams in
let l1' = Array.sub l1 pars (Array.length l1 - pars) in
let l2 = Array.map (fun p -> mkProj (p, term)) projs in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 52282375f..b619eafab 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -317,7 +317,7 @@ let close_proof ?feedback_id ~now fpl =
const_entry_opaque = true;
const_entry_universes = univs;
const_entry_polymorphic = poly;
- const_entry_proj = false})
+ const_entry_proj = None})
fpl initial_goals in
{ id = pid; entries = entries; persistence = strength; universes = universes },
Ephemeron.get terminator
diff --git a/toplevel/command.ml b/toplevel/command.ml
index a675fe028..b10a4da06 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -578,7 +578,9 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
constrimpls)
impls;
if_verbose msg_info (minductive_message names);
- if mie.mind_entry_private == None then declare_default_schemes mind;
+ if mie.mind_entry_private == None
+ && not (mie.mind_entry_record = Some true)
+ then declare_default_schemes mind;
mind
type one_inductive_impls =
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 6f3f5cc49..1f09d7620 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -126,7 +126,7 @@ let define internal id c p univs =
const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = None;
- const_entry_proj = false;
+ const_entry_proj = None;
const_entry_polymorphic = p;
const_entry_universes = Evd.evar_context_universe_context ctx;
const_entry_opaque = false;
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index d7d6b4c6d..d413564a9 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -120,7 +120,7 @@ let define id internal ctx c t =
{ const_entry_body = c;
const_entry_secctx = None;
const_entry_type = t;
- const_entry_proj = false;
+ const_entry_proj = None;
const_entry_polymorphic = true;
const_entry_universes = Evd.universe_context ctx;
const_entry_opaque = false;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 47aa2688d..18e85266e 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -629,7 +629,7 @@ let declare_obligation prg obl body ty uctx =
{ const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = if List.is_empty ctx then ty else None;
- const_entry_proj = false;
+ const_entry_proj = None;
const_entry_polymorphic = poly;
const_entry_universes = uctx;
const_entry_opaque = opaque;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 302fe6280..2fbe7483f 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -219,13 +219,13 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
let x = match name with Some n -> Name n | None -> Namegen.named_hd (Global.env()) r Anonymous in
let fields = instantiate_possibly_recursive_type indu paramdecls fields in
let lifted_fields = Termops.lift_rel_context 1 fields in
- let (_,kinds,sp_projs,_) =
+ let (_,_,kinds,sp_projs,_) =
List.fold_left3
- (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
- let (sp_projs,subst) =
+ (fun (nfi,i,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
+ let (sp_projs,i,subst) =
match fi with
| Anonymous ->
- (None::sp_projs,NoProjection fi::subst)
+ (None::sp_projs,i,NoProjection fi::subst)
| Name fid ->
try
let ccl = subst_projection fid subst ti in
@@ -247,8 +247,9 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
let kn =
try
let makeprim =
- if !primitive_flag && optci = None then true
- else false
+ if !primitive_flag && optci = None then
+ Some (fst indsp, i)
+ else None
in
let cie = {
const_entry_body =
@@ -280,12 +281,12 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
applist (mkConstU (kn,u),proj_args)
in
- (Some kn::sp_projs, Projection constr_fip::subst)
+ (Some kn::sp_projs, i+1, Projection constr_fip::subst)
with NotDefinable why ->
warning_or_error coe indsp why;
- (None::sp_projs,NoProjection fi::subst) in
- (nfi-1,(fi, Option.is_empty optci)::kinds,sp_projs,subst))
- (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
+ (None::sp_projs,i,NoProjection fi::subst) in
+ (nfi-1,i,(fi, Option.is_empty optci)::kinds,sp_projs,subst))
+ (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
in (kinds,sp_projs)
let structure_signature ctx =
@@ -341,6 +342,13 @@ let declare_structure finite infer poly ctx id idbuild paramimpls params arity f
let cstr = (rsp,1) in
let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
let build = ConstructRef cstr in
+ let () =
+ if !primitive_flag then
+ (* declare_mutual won't have tried to define the eliminations, we do it now that
+ the projections have been defined. *)
+ Indschemes.declare_default_schemes kn
+ else ()
+ in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
rsp
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 06:10:40 +0000