aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/cic.mli11
-rw-r--r--checker/closure.ml3
-rw-r--r--checker/environ.ml11
-rw-r--r--checker/subtyping.ml19
-rw-r--r--checker/typeops.ml2
-rw-r--r--checker/values.ml12
-rw-r--r--interp/declare.ml13
-rw-r--r--interp/discharge.ml7
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--kernel/cClosure.ml6
-rw-r--r--kernel/declarations.ml21
-rw-r--r--kernel/declareops.ml19
-rw-r--r--kernel/entries.ml6
-rw-r--r--kernel/environ.ml11
-rw-r--r--kernel/indtypes.ml67
-rw-r--r--kernel/indtypes.mli6
-rw-r--r--kernel/inductive.ml4
-rw-r--r--kernel/nativecode.ml11
-rw-r--r--kernel/nativelambda.ml3
-rw-r--r--kernel/subtyping.ml5
-rw-r--r--kernel/typeops.ml2
-rw-r--r--plugins/extraction/extraction.ml8
-rw-r--r--pretyping/detyping.ml3
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/inductiveops.ml16
-rw-r--r--pretyping/nativenorm.ml7
-rw-r--r--pretyping/unification.ml10
-rw-r--r--printing/prettyp.ml4
-rw-r--r--printing/printmod.ml2
-rw-r--r--tactics/tacticals.ml4
-rw-r--r--vernac/record.ml6
31 files changed, 174 insertions, 131 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index 3304b032e..a890f2cef 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -207,7 +207,7 @@ type inline = int option
always transparent. *)
type projection_body = {
- proj_ind : MutInd.t;
+ proj_ind : inductive;
proj_npars : int;
proj_arg : int;
proj_type : constr; (* Type under params *)
@@ -252,9 +252,10 @@ type recarg =
type wf_paths = recarg Rtree.t
-type record_body = (Id.t * Constant.t array * projection_body array) option
- (* The body is empty for non-primitive records, otherwise we get its
- binder name in projections and list of projections if it is primitive. *)
+type record_info =
+| NotRecord
+| FakeRecord
+| PrimRecord of (Id.t * Constant.t array * projection_body array) array
type regular_inductive_arity = {
mind_user_arity : constr;
@@ -322,7 +323,7 @@ type mutual_inductive_body = {
mind_packets : one_inductive_body array; (** The component of the mutual inductive block *)
- mind_record : record_body option; (** Whether the inductive type has been declared as a record. *)
+ mind_record : record_info; (** Whether the inductive type has been declared as a record. *)
mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *)
diff --git a/checker/closure.ml b/checker/closure.ml
index b9ae4daa8..2dcc1a984 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -619,7 +619,8 @@ let drop_parameters depth n argstk =
let eta_expand_ind_stack env ind m s (f, s') =
let mib = lookup_mind (fst ind) env in
match mib.mind_record with
- | Some (Some (_,projs,pbs)) when mib.mind_finite <> CoFinite ->
+ | PrimRecord info when mib.mind_finite <> CoFinite ->
+ let (_, projs, pbs) = info.(snd ind) in
(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
let pars = mib.mind_nparams in
diff --git a/checker/environ.ml b/checker/environ.ml
index 3d5fac806..ba1eb0ddb 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -192,11 +192,12 @@ let add_mind kn mib env =
(MutInd.to_string kn);
let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
let new_projections = match mib.mind_record with
- | None | Some None -> env.env_globals.env_projections
- | Some (Some (id, kns, pbs)) ->
- Array.fold_left2 (fun projs kn pb ->
- Cmap_env.add kn pb projs)
- env.env_globals.env_projections kns pbs
+ | NotRecord | FakeRecord -> env.env_globals.env_projections
+ | PrimRecord projs ->
+ Array.fold_left (fun accu (id, kns, pbs) ->
+ Array.fold_left2 (fun accu kn pb ->
+ Cmap_env.add kn pb accu) accu kns pbs)
+ env.env_globals.env_projections projs
in
let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in
let new_inds_eq = if KerName.equal kn1 kn2 then
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index f4ae02084..a22af4e0f 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -126,7 +126,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
in
let eq_projection_body p1 p2 =
let check eq f = if not (eq (f p1) (f p2)) then error () in
- check MutInd.equal (fun x -> x.proj_ind);
+ check eq_ind (fun x -> x.proj_ind);
check (==) (fun x -> x.proj_npars);
check (==) (fun x -> x.proj_arg);
check (eq_constr) (fun x -> x.proj_type);
@@ -218,16 +218,19 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
(* we check that records and their field names are preserved. *)
let record_equal x y =
match x, y with
- | None, None -> true
- | Some None, Some None -> true
- | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) ->
- Id.equal id1 id2 &&
- Array.for_all2 Constant.UserOrd.equal p1 p2 &&
- Array.for_all2 eq_projection_body pb1 pb2
+ | NotRecord, NotRecord -> true
+ | FakeRecord, FakeRecord -> true
+ | PrimRecord info1, PrimRecord info2 ->
+ let check (id1, p1, pb1) (id2, p2, pb2) =
+ Id.equal id1 id2 &&
+ Array.for_all2 Constant.UserOrd.equal p1 p2 &&
+ Array.for_all2 eq_projection_body pb1 pb2
+ in
+ Array.equal check info1 info2
| _, _ -> false
in
check record_equal (fun mib -> mib.mind_record);
- if mib1.mind_record != None then begin
+ if mib1.mind_record != NotRecord then begin
let rec names_prod_letin t = match t with
| Prod(n,_,t) -> n::(names_prod_letin t)
| LetIn(n,_,_,t) -> n::(names_prod_letin t)
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 18f07dc0b..345ee5b8f 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -203,7 +203,7 @@ let judge_of_projection env p c ct =
try find_rectype env ct
with Not_found -> error_case_not_inductive env (c, ct)
in
- assert(MutInd.equal pb.proj_ind (fst ind));
+ assert(eq_ind pb.proj_ind ind);
let ty = subst_instance_constr u pb.proj_type in
substl (c :: List.rev args) ty
diff --git a/checker/values.ml b/checker/values.ml
index 31e65729b..4f28d6e44 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 07651f61f86d91b22ff7056c6a8d86bc checker/cic.mli
+MD5 42fb0781dc5f7f2cbe3ca127f8249264 checker/cic.mli
*)
@@ -225,7 +225,7 @@ let v_cst_def =
let v_projbody =
v_tuple "projection_body"
- [|v_cst;Int;Int;v_constr|]
+ [|v_ind;Int;Int;v_constr|]
let v_typing_flags =
v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
@@ -274,8 +274,10 @@ let v_one_ind = v_tuple "one_inductive_body"
Any|]
let v_finite = v_enum "recursivity_kind" 3
-let v_mind_record = Annot ("mind_record",
- Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |])))
+
+let v_record_info =
+ v_sum "record_info" 2
+ [| [| Array (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]) |] |]
let v_ind_pack_univs =
v_sum "abstract_inductive_universes" 0
@@ -283,7 +285,7 @@ let v_ind_pack_univs =
let v_ind_pack = v_tuple "mutual_inductive_body"
[|Array v_one_ind;
- v_mind_record;
+ v_record_info;
v_finite;
Int;
v_section_ctxt;
diff --git a/interp/declare.ml b/interp/declare.ml
index aa737239b..e79cc6079 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -383,11 +383,14 @@ let inInductive : inductive_obj -> obj =
rebuild_function = infer_inductive_subtyping }
let declare_projections univs mind =
+ (** FIXME: handle mutual records *)
+ let mind = (mind, 0) in
let env = Global.env () in
- let spec,_ = Inductive.lookup_mind_specif env (mind,0) in
+ let spec,_ = Inductive.lookup_mind_specif env mind in
match spec.mind_record with
- | Some (Some (_, kns, _)) ->
- let projs = Inductiveops.compute_projections env (mind, 0) in
+ | PrimRecord info ->
+ let _, kns, _ = info.(0) in
+ let projs = Inductiveops.compute_projections env mind in
Array.iter2 (fun kn (term, types) ->
let id = Label.to_id (Constant.label kn) in
let univs = match univs with
@@ -410,8 +413,8 @@ let declare_projections univs mind =
assert (Constant.equal kn kn')
) kns projs;
true, true
- | Some None -> true,false
- | None -> false,false
+ | FakeRecord -> true,false
+ | NotRecord -> false,false
(* for initial declaration *)
let declare_mind mie =
diff --git a/interp/discharge.ml b/interp/discharge.ml
index e16a955d9..0e44a8b46 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -111,9 +111,10 @@ let process_inductive info modlist mib =
let section_decls' = Context.Named.map discharge section_decls in
let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
let record = match mib.mind_record with
- | Some (Some (id, _, _)) -> Some (Some id)
- | Some None -> Some None
- | None -> None
+ | PrimRecord info ->
+ Some (Some (Array.map pi1 info))
+ | FakeRecord -> Some None
+ | NotRecord -> None
in
{ mind_entry_record = record;
mind_entry_finite = mib.mind_finite;
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 74618a290..5bf46282f 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -113,7 +113,7 @@ let type_of_global_ref gr =
"var" ^ type_of_logical_kind (Decls.variable_kind v)
| Globnames.IndRef ind ->
let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
- if mib.Declarations.mind_record <> None then
+ if mib.Declarations.mind_record <> Declarations.NotRecord then
begin match mib.Declarations.mind_finite with
| Finite -> "indrec"
| BiFinite -> "rec"
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index c9362bce6..1d5142a5c 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -820,10 +820,12 @@ let drop_parameters depth n argstk =
constructor is partially applied.
*)
let eta_expand_ind_stack env ind m s (f, s') =
+ let open Declarations in
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
- | Some (Some (_,projs,pbs)) when
+ | PrimRecord infos when
mib.Declarations.mind_finite == Declarations.BiFinite ->
+ let (_, projs, _) = infos.(snd ind) in
(* (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
@@ -834,7 +836,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
term = FProj (Projection.make p true, right) }) projs in
argss, [Zapp hstack]
- | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
+ | PrimRecord _ | NotRecord | FakeRecord -> raise Not_found (* disallow eta-exp for non-primitive records *)
let rec project_nth_arg n argstk =
match argstk with
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7bd7d6c9c..58fb5d66b 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -50,7 +50,7 @@ type inline = int option
always transparent. *)
type projection_body = {
- proj_ind : MutInd.t;
+ proj_ind : inductive;
proj_npars : int;
proj_arg : int; (** Projection index, starting from 0 *)
proj_type : types; (* Type under params *)
@@ -109,13 +109,22 @@ v}
*)
(** Record information:
- If the record is not primitive, then None
- Otherwise, we get:
+ If the type is not a record, then NotRecord
+ If the type is a non-primitive record, then FakeRecord
+ If it is a primitive record, for every type in the block, we get:
- The identifier for the binder name of the record in primitive projections.
- The constants associated to each projection.
- - The checked projection bodies. *)
+ - The checked projection bodies.
-type record_body = (Id.t * Constant.t array * projection_body array) option
+ The kernel does not exploit the difference between [NotRecord] and
+ [FakeRecord]. It is mostly used by extraction, and should be extruded from
+ the kernel at some point.
+*)
+
+type record_info =
+| NotRecord
+| FakeRecord
+| PrimRecord of (Id.t * Constant.t array * projection_body array) array
type regular_inductive_arity = {
mind_user_arity : types;
@@ -181,7 +190,7 @@ type mutual_inductive_body = {
mind_packets : one_inductive_body array; (** The component of the mutual inductive block *)
- mind_record : record_body option; (** The record information *)
+ mind_record : record_info; (** The record information *)
mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 1b73096f7..3e6c4858e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -84,7 +84,7 @@ let subst_const_def sub def = match def with
| OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o)
let subst_const_proj sub pb =
- { pb with proj_ind = subst_mind sub pb.proj_ind;
+ { pb with proj_ind = subst_ind sub pb.proj_ind;
proj_type = subst_mps sub pb.proj_type;
}
@@ -208,14 +208,21 @@ 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 (id, ps, pb as r) =
- let ps' = Array.Smart.map (subst_constant sub) ps in
- let pb' = Array.Smart.map (subst_const_proj sub) pb in
- if ps' == ps && pb' == pb then r
+let subst_mind_record sub r = match r with
+| NotRecord -> NotRecord
+| FakeRecord -> FakeRecord
+| PrimRecord infos ->
+ let map (id, ps, pb as info) =
+ let ps' = Array.Smart.map (subst_constant sub) ps in
+ let pb' = Array.Smart.map (subst_const_proj sub) pb in
+ if ps' == ps && pb' == pb then info
else (id, ps', pb')
+ in
+ let infos' = Array.Smart.map map infos in
+ if infos' == infos then r else PrimRecord infos'
let subst_mind_body sub mib =
- { mind_record = Option.Smart.map (Option.Smart.map (subst_mind_record sub)) mib.mind_record ;
+ { mind_record = subst_mind_record sub mib.mind_record ;
mind_finite = mib.mind_finite ;
mind_ntypes = mib.mind_ntypes ;
mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 3c555f8c7..724ed9ec7 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -49,9 +49,9 @@ type one_inductive_entry = {
mind_entry_lc : constr list }
type mutual_inductive_entry = {
- mind_entry_record : (Id.t option) option;
- (** Some (Some id): primitive record with id the binder name of the record
- in projections.
+ mind_entry_record : (Id.t array option) option;
+ (** Some (Some ids): primitive records with ids the binder name of each
+ record in their respective projections. Not used by the kernel.
Some None: non-primitive record *)
mind_entry_finite : Declarations.recursivity_kind;
mind_entry_params : (Id.t * local_entry) list;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2d6c9117b..0e34a7165 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -515,11 +515,12 @@ let template_polymorphic_pind (ind,u) env =
let add_mind_key kn (mind, _ as mind_key) env =
let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
let new_projections = match mind.mind_record with
- | None | Some None -> env.env_globals.env_projections
- | Some (Some (id, kns, pbs)) ->
- Array.fold_left2 (fun projs kn pb ->
- Cmap_env.add kn pb projs)
- env.env_globals.env_projections kns pbs
+ | NotRecord | FakeRecord -> env.env_globals.env_projections
+ | PrimRecord projs ->
+ Array.fold_left (fun accu (id, kns, pbs) ->
+ Array.fold_left2 (fun accu kn pb ->
+ Cmap_env.add kn pb accu) accu kns pbs)
+ env.env_globals.env_projections projs
in
let new_globals =
{ env.env_globals with
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 14f2a3d8f..e63f43849 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -797,15 +797,23 @@ 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_projections ((kn, _ as ind), u) nparamargs params
- mind_consnrealdecls mind_consnrealargs paramslet ctx =
+let compute_projections (kn, i as ind) mib =
+ let pkt = mib.mind_packets.(i) in
+ let u = match mib.mind_universes with
+ | Monomorphic_ind _ -> Univ.Instance.empty
+ | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx
+ | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi)
+ 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
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 paramsletsubst =
(* [Ind inst] is typed in context [params-wo-let] *)
- let inst' = rel_list 0 nparamargs in
+ let inst' = rel_list 0 mib.mind_nparams in
(* {params-wo-let |- subst:params] *)
let subst = subst_of_rel_context_instance paramslet inst' in
(* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *)
@@ -839,7 +847,7 @@ let compute_projections ((kn, _ as ind), u) nparamargs params
(* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
to [params, x:I |- t(proj1 x,..,projj x)] *)
let fterm = mkProj (Projection.make kn false, mkRel 1) in
- let body = { proj_ind = fst ind; proj_npars = nparamargs;
+ let body = { proj_ind = ind; proj_npars = mib.mind_nparams;
proj_arg = i; proj_type = projty; } in
(i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst)
| Anonymous -> raise UndefinableExpansion
@@ -932,33 +940,9 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
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 (Some rid) when pkt.mind_kelim == all_sorts
- && Array.length pkt.mind_consnames == 1
- && pkt.mind_consnrealargs.(0) > 0 ->
- (** The elimination criterion ensures that all projections can be defined. *)
- let u =
- match aiu with
- | Monomorphic_ind _ -> Univ.Instance.empty
- | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx
- | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi)
- in
- let indsp = ((kn, 0), u) in
- let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
- (try
- let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
- let kns, projs =
- compute_projections indsp nparamargs paramsctxt
- pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
- in Some (Some (rid, kns, projs))
- with UndefinableExpansion -> Some None)
- | Some _ -> Some None
- | None -> None
- in
- (* Build the mutual inductive *)
- { mind_record = isrecord;
+ let mib =
+ (* Build the mutual inductive *)
+ { mind_record = NotRecord;
mind_ntypes = ntypes;
mind_finite = isfinite;
mind_hyps = hyps;
@@ -970,6 +954,27 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
mind_private = prv;
mind_typing_flags = Environ.typing_flags env;
}
+ in
+ let record_info = match isrecord with
+ | Some (Some rid) ->
+ let is_record pkt =
+ pkt.mind_kelim == all_sorts
+ && Array.length pkt.mind_consnames == 1
+ && pkt.mind_consnrealargs.(0) > 0
+ in
+ (** The elimination criterion ensures that all projections can be defined. *)
+ if Array.for_all is_record packets then
+ let map i id =
+ let kn, projs = compute_projections (kn, i) mib in
+ (id, kn, projs)
+ in
+ try PrimRecord (Array.mapi map rid)
+ with UndefinableExpansion -> FakeRecord
+ else FakeRecord
+ | Some None -> FakeRecord
+ | None -> NotRecord
+ in
+ { mib with mind_record = record_info }
(************************************************************************)
(************************************************************************)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 45228e35e..7c36dac67 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -43,7 +43,5 @@ val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_induct
val enforce_indices_matter : unit -> unit
val is_indices_matter : unit -> bool
-val compute_projections : pinductive ->
- int -> Context.Rel.t -> int array -> int array ->
- Context.Rel.t -> Context.Rel.t ->
- (Constant.t array * projection_body array)
+val compute_projections : inductive ->
+ mutual_inductive_body -> (Constant.t array * projection_body array)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 090acdf16..9130b8778 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -293,8 +293,8 @@ 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 (Some _) -> true
- | _ -> false
+ | PrimRecord _ -> true
+ | NotRecord | FakeRecord -> false
let build_dependent_inductive ind (_,mip) params =
let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 8257dc8b8..6821fc980 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1965,6 +1965,7 @@ let compile_mind prefix ~interactive mb mind stack =
in
let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in
let add_proj j acc pb =
+ let () = assert (eq_ind ind pb.proj_ind) in
let tbl = ob.mind_reloc_tbl in
(* Building info *)
let ci = { ci_ind = ind; ci_npar = nparams;
@@ -1985,12 +1986,14 @@ let compile_mind prefix ~interactive mb mind stack =
let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in
let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in
- let gn = Gproj ("", (pb.proj_ind, j), pb.proj_arg) in
+ let gn = Gproj ("", ind, pb.proj_arg) in
Glet (gn, mkMLlam [|c_uid|] code) :: acc
in
let projs = match mb.mind_record with
- | None | Some None -> []
- | Some (Some (id, kns, pbs)) -> Array.fold_left_i add_proj [] pbs
+ | NotRecord | FakeRecord -> []
+ | PrimRecord info ->
+ let _, _, pbs = info.(i) in
+ Array.fold_left_i add_proj [] pbs
in
projs @ constructors @ gtype :: accu :: stack
in
@@ -2052,7 +2055,7 @@ let compile_deps env sigma prefix ~interactive init t =
| Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
| Proj (p,c) ->
let pb = lookup_projection p env in
- let init = compile_mind_deps env prefix ~interactive init pb.proj_ind in
+ let init = compile_mind_deps env prefix ~interactive init (fst pb.proj_ind) in
aux env lvl init c
| Case (ci, p, c, ac) ->
let mind = fst ci.ci_ind in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 0325a00b4..a809e1b18 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -520,8 +520,7 @@ let rec lambda_of_constr env sigma c =
| Proj (p, c) ->
let pb = lookup_projection p !global_env in
- (** FIXME: handle mutual records *)
- let ind = (pb.proj_ind, 0) in
+ let ind = pb.proj_ind in
let prefix = get_mind_prefix !global_env (fst ind) in
mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|]
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 8cf588c3e..13701d489 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -226,8 +226,9 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
else error NotEqualInductiveAliases
end;
(* we check that records and their field names are preserved. *)
- check (fun mib -> mib.mind_record <> None) (==) (fun x -> RecordFieldExpected x);
- if mib1.mind_record <> None then begin
+ (** FIXME: this check looks nonsense *)
+ check (fun mib -> mib.mind_record <> NotRecord) (==) (fun x -> RecordFieldExpected x);
+ if mib1.mind_record <> NotRecord then begin
let rec names_prod_letin t = match kind t with
| Prod(n,_,t) -> n::(names_prod_letin t)
| LetIn(n,_,_,t) -> n::(names_prod_letin t)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 325d5cecd..34ed2afb2 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -301,7 +301,7 @@ let type_of_projection env p c ct =
try find_rectype env ct
with Not_found -> error_case_not_inductive env (make_judge c ct)
in
- assert(MutInd.equal pb.proj_ind (fst ind));
+ assert(eq_ind pb.proj_ind ind);
let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in
substl (c :: CList.rev args) ty
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 3a61c7747..71e09992c 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -488,7 +488,7 @@ and extract_really_ind env kn mib =
Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l))
then raise (I Singleton);
if List.is_empty l then raise (I Standard);
- if Option.is_empty mib.mind_record then raise (I Standard);
+ if mib.mind_record == Declarations.NotRecord then raise (I Standard);
(* Now we're sure it's a record. *)
(* First, we find its field names. *)
let rec names_prod t = match Constr.kind t with
@@ -1069,8 +1069,7 @@ let extract_constant env kn cb =
| false -> mk_typ (get_body c)
| true ->
let pb = lookup_projection (Projection.make kn false) env in
- (** FIXME: handle mutual records *)
- let ind = (pb.Declarations.proj_ind, 0) in
+ let ind = pb.Declarations.proj_ind in
let bodies = Inductiveops.legacy_match_projection env ind in
let body = bodies.(pb.Declarations.proj_arg) in
mk_typ (EConstr.of_constr body))
@@ -1086,8 +1085,7 @@ let extract_constant env kn cb =
| false -> mk_def (get_body c)
| true ->
let pb = lookup_projection (Projection.make kn false) env in
- (** FIXME: handle mutual records *)
- let ind = (pb.Declarations.proj_ind, 0) in
+ let ind = pb.Declarations.proj_ind in
let bodies = Inductiveops.legacy_match_projection env ind in
let body = bodies.(pb.Declarations.proj_arg) in
mk_def (EConstr.of_constr body))
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index fe49d64c7..23a985dc3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -690,8 +690,7 @@ and detype_r d flags avoid env sigma t =
let c' =
try
let pb = Environ.lookup_projection p (snd env) in
- (** FIXME: handle mutual records *)
- let ind = (pb.Declarations.proj_ind, 0) in
+ let ind = pb.Declarations.proj_ind 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
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6d08f66c1..88a91af88 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -984,9 +984,11 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
else UnifFailure(evd,(*dummy*)NotSameHead)
and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
+ let open Declarations in
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
- | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite ->
+ | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite ->
+ let (_, projs, _) = info.(snd ind) in
let pars = mib.Declarations.mind_nparams in
(try
let l1' = Stack.tail pars sk1 in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1003f86c5..d599afe69 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -277,8 +277,8 @@ let projection_nparams p = projection_nparams_env (Global.env ()) 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 =
@@ -346,8 +346,10 @@ let get_constructors env (ind,params) =
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
+ | PrimRecord infos ->
+ let (_, projs, _) = infos.(snd (fst ind)) in
+ Some projs
+ | NotRecord | FakeRecord -> None
let make_case_or_project env sigma indf ci pred c branches =
let open EConstr in
@@ -460,7 +462,7 @@ let build_branch_type env sigma dep p cs =
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 compute_projections env (kn, i as ind) =
let open Term in
let mib = Environ.lookup_mind kn env in
let indu = match mib.mind_universes with
@@ -470,9 +472,9 @@ let compute_projections env (kn, _ as ind) =
mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx))
in
let x = match mib.mind_record with
- | None | Some None ->
+ | NotRecord | FakeRecord ->
anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
- | Some (Some (id, _, _)) -> Name id
+ | PrimRecord info-> Name (pi1 (info.(i)))
in
(** FIXME: handle mutual records *)
let pkt = mib.mind_packets.(0) in
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 4b8e0e096..7319846fb 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -188,12 +188,13 @@ let branch_of_switch lvl ans bs =
bs ci in
Array.init (Array.length tbl) branch
-let get_proj env ((mind, _n), i) =
+let get_proj env ((mind, n), i) =
let mib = Environ.lookup_mind mind env in
match mib.mind_record with
- | None | Some None ->
+ | NotRecord | FakeRecord ->
CErrors.anomaly (Pp.strbrk "Return type is not a primitive record")
- | Some (Some (_, projs, _)) ->
+ | PrimRecord info ->
+ let _, projs, _ = info.(n) in
Projection.make projs.(i) true
let rec nf_val env sigma v typ =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5cf6e4b26..4ba5d2794 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -656,10 +656,12 @@ let rec is_neutral env sigma ts t =
let is_eta_constructor_app env sigma ts f l1 term =
match EConstr.kind sigma f with
- | Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
+ | Construct (((_, i as ind), j), u) when j == 1 ->
+ let open Declarations in
let mib = lookup_mind (fst ind) env in
(match mib.Declarations.mind_record with
- | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite &&
+ | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite &&
+ let (_, projs, _) = info.(i) in
Array.length projs == Array.length l1 - mib.Declarations.mind_nparams ->
(** Check that the other term is neutral *)
is_neutral env sigma ts term
@@ -667,11 +669,13 @@ let is_eta_constructor_app env sigma ts f l1 term =
| _ -> false
let eta_constructor_app env sigma f l1 term =
+ let open Declarations in
match EConstr.kind sigma f with
| Construct (((_, i as ind), j), u) ->
let mib = lookup_mind (fst ind) env in
(match mib.Declarations.mind_record with
- | Some (Some (_, projs, _)) ->
+ | PrimRecord info ->
+ let (_, projs, _) = info.(i) in
let npars = mib.Declarations.mind_nparams in
let pars, l1' = Array.chop npars l1 in
let arg = Array.append pars [|term|] in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 5e5d00362..f926e8275 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -246,13 +246,13 @@ let print_type_in_type ref =
else []
let print_primitive_record recflag mipv = function
- | Some (Some (_, ps,_)) ->
+ | PrimRecord _ ->
let eta = match recflag with
| CoFinite | Finite -> str" without eta conversion"
| BiFinite -> str " with eta conversion"
in
[Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
- | _ -> []
+ | FakeRecord | NotRecord -> []
let print_primitive ref =
match ref with
diff --git a/printing/printmod.ml b/printing/printmod.ml
index be8bc1357..3f95dcfb6 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -217,7 +217,7 @@ let print_record env mind mib udecl =
)
let pr_mutual_inductive_body env mind mib udecl =
- if mib.mind_record <> None && not !Flags.raw_print then
+ if mib.mind_record != NotRecord && not !Flags.raw_print then
print_record env mind mib udecl
else
print_mutual_inductive env mind mib udecl
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f34c83ae7..837865e64 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -753,8 +753,8 @@ module New = struct
let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
let isrec,mkelim =
match (Global.lookup_mind (fst (fst ind))).mind_record with
- | None -> true,gl_make_elim
- | Some _ -> false,gl_make_case_dep
+ | NotRecord -> true,gl_make_elim
+ | FakeRecord | PrimRecord _ -> false,gl_make_case_dep
in
general_elim_then_using mkelim isrec None tac None ind (c, t)
end
diff --git a/vernac/record.ml b/vernac/record.ml
index 940859723..a97a1662e 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -292,8 +292,8 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
if !primitive_flag then
let is_primitive =
match mib.mind_record with
- | Some (Some _) -> true
- | Some None | None -> false
+ | PrimRecord _ -> true
+ | FakeRecord | NotRecord -> false
in
if not is_primitive then
warn_non_primitive_record (env,indsp);
@@ -403,7 +403,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
in
let mie =
{ mind_entry_params = List.map degenerate_decl params;
- mind_entry_record = Some (if !primitive_flag then Some binder_name else None);
+ mind_entry_record = Some (if !primitive_flag then Some [|binder_name|] else None);
mind_entry_finite = finite;
mind_entry_inds = [mie_ind];
mind_entry_private = None;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 22:24:20 +0000