aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml117
-rw-r--r--kernel/cClosure.mli2
-rw-r--r--kernel/cooking.ml21
-rw-r--r--kernel/cooking.mli1
-rw-r--r--kernel/declarations.ml24
-rw-r--r--kernel/declareops.ml22
-rw-r--r--kernel/entries.ml11
-rw-r--r--kernel/environ.ml13
-rw-r--r--kernel/esubst.ml23
-rw-r--r--kernel/esubst.mli7
-rw-r--r--kernel/indtypes.ml120
-rw-r--r--kernel/indtypes.mli6
-rw-r--r--kernel/inductive.ml4
-rw-r--r--kernel/names.ml11
-rw-r--r--kernel/nativecode.ml11
-rw-r--r--kernel/nativelambda.ml3
-rw-r--r--kernel/subtyping.ml5
-rw-r--r--kernel/term_typing.ml84
-rw-r--r--kernel/typeops.ml2
19 files changed, 238 insertions, 249 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 1d8861cbc..1d5142a5c 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -587,78 +587,95 @@ let mk_clos_deep clos_fun env t =
let mk_clos2 = mk_clos_deep mk_clos
(* The inverse of mk_clos_deep: move back to constr *)
-let rec to_constr constr_fun lfts v =
+let rec to_constr lfts v =
match v.term with
| FRel i -> mkRel (reloc_rel i lfts)
| FFlex (RelKey p) -> mkRel (reloc_rel p lfts)
| FFlex (VarKey x) -> mkVar x
| FAtom c -> exliftn lfts c
| FCast (a,k,b) ->
- mkCast (constr_fun lfts a, k, constr_fun lfts b)
+ mkCast (to_constr lfts a, k, to_constr lfts b)
| FFlex (ConstKey op) -> mkConstU op
| FInd op -> mkIndU op
| FConstruct op -> mkConstructU op
| FCaseT (ci,p,c,ve,env) ->
- mkCase (ci, constr_fun lfts (mk_clos env p),
- constr_fun lfts c,
- Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve)
- | FFix ((op,(lna,tys,bds)),e) ->
+ if is_subs_id env && is_lift_id lfts then
+ mkCase (ci, p, to_constr lfts c, ve)
+ else
+ let subs = comp_subs lfts env in
+ mkCase (ci, subst_constr subs p,
+ to_constr lfts c,
+ Array.map (fun b -> subst_constr subs b) ve)
+ | FFix ((op,(lna,tys,bds)) as fx, e) ->
+ if is_subs_id e && is_lift_id lfts then
+ mkFix fx
+ else
let n = Array.length bds in
- let ftys = Array.Fun1.map mk_clos e tys in
- let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in
- let lfts' = el_liftn n lfts in
- mkFix (op, (lna, Array.Fun1.map constr_fun lfts ftys,
- Array.Fun1.map constr_fun lfts' fbds))
- | FCoFix ((op,(lna,tys,bds)),e) ->
+ let subs_ty = comp_subs lfts e in
+ let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in
+ let tys = Array.Fun1.map subst_constr subs_ty tys in
+ let bds = Array.Fun1.map subst_constr subs_bd bds in
+ mkFix (op, (lna, tys, bds))
+ | FCoFix ((op,(lna,tys,bds)) as cfx, e) ->
+ if is_subs_id e && is_lift_id lfts then
+ mkCoFix cfx
+ else
let n = Array.length bds in
- let ftys = Array.Fun1.map mk_clos e tys in
- let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in
- let lfts' = el_liftn (Array.length bds) lfts in
- mkCoFix (op, (lna, Array.Fun1.map constr_fun lfts ftys,
- Array.Fun1.map constr_fun lfts' fbds))
+ let subs_ty = comp_subs lfts e in
+ let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in
+ let tys = Array.Fun1.map subst_constr subs_ty tys in
+ let bds = Array.Fun1.map subst_constr subs_bd bds in
+ mkCoFix (op, (lna, tys, bds))
| FApp (f,ve) ->
- mkApp (constr_fun lfts f,
- Array.Fun1.map constr_fun lfts ve)
+ mkApp (to_constr lfts f,
+ Array.Fun1.map to_constr lfts ve)
| FProj (p,c) ->
- mkProj (p,constr_fun lfts c)
+ mkProj (p,to_constr lfts c)
- | FLambda _ ->
- let (na,ty,bd) = destFLambda mk_clos2 v in
- mkLambda (na, constr_fun lfts ty,
- constr_fun (el_lift lfts) bd)
+ | FLambda (len, tys, f, e) ->
+ if is_subs_id e && is_lift_id lfts then
+ Term.compose_lam (List.rev tys) f
+ else
+ let subs = comp_subs lfts e in
+ let tys = List.mapi (fun i (na, c) -> na, subst_constr (subs_liftn i subs) c) tys in
+ let f = subst_constr (subs_liftn len subs) f in
+ Term.compose_lam (List.rev tys) f
| FProd (n,t,c) ->
- mkProd (n, constr_fun lfts t,
- constr_fun (el_lift lfts) c)
+ mkProd (n, to_constr lfts t,
+ to_constr (el_lift lfts) c)
| FLetIn (n,b,t,f,e) ->
- let fc = mk_clos2 (subs_lift e) f in
- mkLetIn (n, constr_fun lfts b,
- constr_fun lfts t,
- constr_fun (el_lift lfts) fc)
+ let subs = comp_subs (el_lift lfts) (subs_lift e) in
+ mkLetIn (n, to_constr lfts b,
+ to_constr lfts t,
+ subst_constr subs f)
| FEvar ((ev,args),env) ->
- mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args)
- | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a
+ let subs = comp_subs lfts env in
+ mkEvar(ev,Array.map (fun a -> subst_constr subs a) args)
+ | FLIFT (k,a) -> to_constr (el_shft k lfts) a
| FCLOS (t,env) ->
- let fr = mk_clos2 env t in
- let unfv = update v fr.norm fr.term in
- to_constr constr_fun lfts unfv
+ if is_subs_id env && is_lift_id lfts then t
+ else
+ let subs = comp_subs lfts env in
+ subst_constr subs t
| FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*)
+and subst_constr subst c = match Constr.kind c with
+| Rel i ->
+ begin match expand_rel i subst with
+ | Inl (k, lazy v) -> Vars.lift k v
+ | Inr (m, _) -> mkRel m
+ end
+| _ ->
+ Constr.map_with_binders Esubst.subs_lift subst_constr subst c
+
+and comp_subs el s =
+ Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s
+
(* This function defines the correspondance between constr and
fconstr. When we find a closure whose substitution is the identity,
then we directly return the constr to avoid possibly huge
reallocation. *)
-let term_of_fconstr =
- let rec term_of_fconstr_lift lfts v =
- match v.term with
- | FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t
- | FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts ->
- Term.compose_lam (List.rev tys) f
- | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> mkFix fx
- | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> mkCoFix cfx
- | _ -> to_constr term_of_fconstr_lift lfts v in
- term_of_fconstr_lift el_id
-
-
+let term_of_fconstr c = to_constr el_id c
(* fstrong applies unfreeze_fun recursively on the (freeze) term and
* yields a term. Assumes that the unfreeze_fun never returns a
@@ -803,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
@@ -817,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/cClosure.mli b/kernel/cClosure.mli
index 63daa4a7c..f8f98f0ab 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -244,6 +244,6 @@ val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr
-val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
+val to_constr : lift -> fconstr -> constr
(** End of cbn debug section i*)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 5783453e6..c7a84f617 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -126,16 +126,15 @@ let expmod_constr cache modlist c =
| Not_found -> Constr.map substrec c)
| Proj (p, c') ->
- (try
- let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in
- let make c = Projection.make c (Projection.unfolded p) in
- match kind p' with
- | Const (p',_) -> mkProj (make p', substrec c')
- | App (f, args) ->
- (match kind f with
- | Const (p', _) -> mkProj (make p', substrec c')
- | _ -> assert false)
- | _ -> assert false
+ (try
+ (** No need to expand parameters or universes for projections *)
+ let map cst =
+ let _ = Cmap.find cst (fst modlist) in
+ pop_con cst
+ in
+ let p = Projection.map map p in
+ let c' = substrec c' in
+ mkProj (p, c')
with Not_found -> Constr.map substrec c)
| _ -> Constr.map substrec c
@@ -156,7 +155,6 @@ type inline = bool
type result = {
cook_body : constant_def;
cook_type : types;
- cook_proj : bool;
cook_universes : constant_universes;
cook_inline : inline;
cook_context : Context.Named.t option;
@@ -230,7 +228,6 @@ let cook_constant ~hcons env { from = cb; info } =
{
cook_body = body;
cook_type = typ;
- cook_proj = cb.const_proj;
cook_universes = univs;
cook_inline = cb.const_inline_code;
cook_context = Some const_hyps;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 0d907f3de..76c79335f 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,7 +21,6 @@ type inline = bool
type result = {
cook_body : constant_def;
cook_type : types;
- cook_proj : bool;
cook_universes : constant_universes;
cook_inline : inline;
cook_context : Context.Named.t option;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7bd70c050..58fb5d66b 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -50,12 +50,10 @@ 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 *)
- proj_eta : constr * types; (* Eta-expanded term and type *)
- proj_body : constr; (* For compatibility with VMs only, the match version *)
}
(* Global declarations (i.e. constants) can be either: *)
@@ -87,7 +85,6 @@ type constant_body = {
const_type : types;
const_body_code : Cemitcodes.to_patch_substituted option;
const_universes : constant_universes;
- const_proj : bool;
const_inline_code : bool;
const_typing_flags : typing_flags; (** The typing options which
were used for
@@ -112,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;
@@ -184,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 75c0e5b4c..3e6c4858e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -84,9 +84,9 @@ 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;
- proj_body = subst_const_type sub pb.proj_body }
+ }
let subst_const_body sub cb =
assert (List.is_empty cb.const_hyps); (* we're outside sections *)
@@ -100,7 +100,6 @@ let subst_const_body sub cb =
{ const_hyps = [];
const_body = body';
const_type = type';
- const_proj = cb.const_proj;
const_body_code =
Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
const_universes = cb.const_universes;
@@ -209,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 94da00c7e..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;
@@ -95,14 +95,9 @@ type inline = int option (* inlining level, None for no inlining *)
type parameter_entry =
Context.Named.t option * types in_constant_universes_entry * inline
-type projection_entry = {
- proj_entry_ind : MutInd.t;
- proj_entry_arg : int }
-
type 'a constant_entry =
| DefinitionEntry of 'a definition_entry
| ParameterEntry of parameter_entry
- | ProjectionEntry of projection_entry
(** {6 Modules } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index fb89576dd..0e34a7165 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -490,7 +490,7 @@ let lookup_projection cst env =
Cmap_env.find (Projection.constant cst) env.env_globals.env_projections
let is_projection cst env =
- (lookup_constant cst env).const_proj
+ Cmap_env.mem cst env.env_globals.env_projections
(* Mutual Inductives *)
let polymorphic_ind (mind,i) env =
@@ -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/esubst.ml b/kernel/esubst.ml
index 4b8edf63f..9fc3b11d7 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -134,6 +134,29 @@ let rec exp_rel lams k subs =
let expand_rel k subs = exp_rel 0 k subs
+let rec subs_map f = function
+| ESID _ as s -> s
+| CONS (x, s) -> CONS (Array.map f x, subs_map f s)
+| SHIFT (n, s) -> SHIFT (n, subs_map f s)
+| LIFT (n, s) -> LIFT (n, subs_map f s)
+
+let rec lift_subst mk_cl s1 s2 = match s1 with
+| ELID -> subs_map (fun c -> mk_cl ELID c) s2
+| ELSHFT(s, k) -> subs_shft(k, lift_subst mk_cl s s2)
+| ELLFT (k, s) ->
+ match s2 with
+ | CONS(x,s') ->
+ CONS(CArray.Fun1.map mk_cl s1 x, lift_subst mk_cl s1 s')
+ | ESID n -> lift_subst mk_cl s (ESID (n + k))
+ | SHIFT(k',s') ->
+ if k<k'
+ then subs_shft(k, lift_subst mk_cl s (subs_shft(k'-k, s')))
+ else subs_shft(k', lift_subst mk_cl (el_liftn (k-k') s) s')
+ | LIFT(k',s') ->
+ if k<k'
+ then subs_liftn k (lift_subst mk_cl s (subs_liftn (k'-k) s'))
+ else subs_liftn k' (lift_subst mk_cl (el_liftn (k-k') s) s')
+
let rec comp mk_cl s1 s2 =
match (s1, s2) with
| _, ESID _ -> s1
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index a674c425a..475b64f47 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -72,3 +72,10 @@ val el_liftn : int -> lift -> lift
val el_lift : lift -> lift
val reloc_rel : int -> lift -> int
val is_lift_id : lift -> bool
+
+(** Lift applied to substitution: [lift_subst mk_clos el s] computes a
+ substitution equivalent to applying el then s. Argument
+ mk_clos is used when a closure has to be created, i.e. when
+ el is applied on an element of s.
+*)
+val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 439acd15b..e63f43849 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -797,65 +797,43 @@ 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 as indu) n x 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 indty, paramsletsubst =
- (* [ty] = [Ind inst] is typed in context [params] *)
- let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
- let ty = mkApp (mkIndU indu, inst) in
+ 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)] *)
let subst = (* For the record parameter: *)
mkRel 1 :: List.map (lift 1) subst in
- ty, subst
- 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 x = Name x 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
+ subst
in
- let projections decl (i, j, kns, pbs, subst, letsubst) =
+ let projections decl (i, j, kns, pbs, letsubst) =
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
- (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *)
let c2 = substl letsubst c in
(* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)]
to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *)
let letsubst = c2 :: letsubst in
- (i, j+1, kns, pbs, subst, letsubst)
+ (i, j+1, kns, pbs, letsubst)
| LocalAssum (na,t) ->
match na with
| Name id ->
@@ -868,21 +846,14 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
let projty = substl letsubst t in
(* 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 = { proj_ind = fst ind; proj_npars = nparamargs;
- proj_arg = i; proj_type = projty; proj_eta = etab, etat;
- proj_body = compat } in
- (i + 1, j + 1, kn :: kns, body :: pbs,
- fterm :: subst, fterm :: letsubst)
+ 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
in
- let (_, _, kns, pbs, subst, letsubst) =
- List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
+ let (_, _, kns, pbs, letsubst) =
+ List.fold_right projections ctx (0, 1, [], [], paramsletsubst)
in
Array.of_list (List.rev kns),
Array.of_list (List.rev pbs)
@@ -969,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 pkt.mind_typename rid 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;
@@ -1007,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 5a38172c2..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 -> Id.t -> Id.t ->
- 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/names.ml b/kernel/names.ml
index 597061278..1d2a7c4ce 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -17,7 +17,7 @@
the module system, Aug 2002 *)
(* Abstraction over the type of constant for module inlining by Claudio
Sacerdoti, Nov 2004 *)
-(* Miscellaneous features or improvements by Hugo Herbelin,
+(* Miscellaneous features or improvements by Hugo Herbelin,
Élie Soubiran, ... *)
open Pp
@@ -364,7 +364,6 @@ module MPmap = CMap.Make(ModPath)
module KerName = struct
type t = {
- canary : Canary.t;
modpath : ModPath.t;
dirpath : DirPath.t;
knlabel : Label.t;
@@ -372,16 +371,14 @@ module KerName = struct
(** Lazily computed hash. If unset, it is set to negative values. *)
}
- let canary = Canary.obj
-
type kernel_name = t
let make modpath dirpath knlabel =
- { modpath; dirpath; knlabel; refhash = -1; canary; }
+ { modpath; dirpath; knlabel; refhash = -1; }
let repr kn = (kn.modpath, kn.dirpath, kn.knlabel)
let make2 modpath knlabel =
- { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; canary; }
+ { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; }
let modpath kn = kn.modpath
let label kn = kn.knlabel
@@ -437,7 +434,7 @@ module KerName = struct
* (string -> string)
let hashcons (hmod,hdir,hstr) kn =
let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in
- { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; }
+ { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; }
let eq kn1 kn2 =
kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
kn1.knlabel == kn2.knlabel
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/term_typing.ml b/kernel/term_typing.ml
index db1109e75..bad449731 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -179,36 +179,36 @@ let rec is_nth_suffix n l suf =
| _ :: l -> is_nth_suffix (pred n) l suf
(* Given the list of signatures of side effects, checks if they match.
- * I.e. if they are ordered descendants of the current revstruct *)
+ * I.e. if they are ordered descendants of the current revstruct.
+ Returns the number of effects that can be trusted. *)
let check_signatures curmb sl =
- let is_direct_ancestor (sl, curmb) (mb, how_many) =
- match curmb with
- | None -> None, None
- | Some curmb ->
+ let is_direct_ancestor accu (mb, how_many) =
+ match accu with
+ | None -> None
+ | Some (n, curmb) ->
try
let mb = CEphemeron.get mb in
- match sl with
- | None -> sl, None
- | Some n ->
- if is_nth_suffix how_many mb curmb
- then Some (n + how_many), Some mb
- else None, None
- with CEphemeron.InvalidKey -> None, None in
- let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in
- sl
+ if is_nth_suffix how_many mb curmb
+ then Some (n + how_many, mb)
+ else None
+ with CEphemeron.InvalidKey -> None in
+ let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in
+ match sl with
+ | None -> 0
+ | Some (n, _) -> n
let skip_trusted_seff sl b e =
let rec aux sl b e acc =
let open Context.Rel.Declaration in
- match sl, kind b with
- | (None|Some 0), _ -> b, e, acc
- | Some sl, LetIn (n,c,ty,bo) ->
- aux (Some (sl-1)) bo
+ if Int.equal sl 0 then b, e, acc
+ else match kind b with
+ | LetIn (n,c,ty,bo) ->
+ aux (sl - 1) bo
(Environ.push_rel (LocalDef (n,c,ty)) e) (`Let(n,c,ty)::acc)
- | Some sl, App(hd,arg) ->
+ | App(hd,arg) ->
begin match kind hd with
| Lambda (n,ty,bo) ->
- aux (Some (sl-1)) bo
+ aux (sl - 1) bo
(Environ.push_rel (LocalAssum (n,ty)) e) (`Cut(n,ty,arg)::acc)
| _ -> assert false
end
@@ -250,7 +250,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = Undef nl;
cook_type = t;
- cook_proj = false;
cook_universes = univs;
cook_inline = false;
cook_context = ctx;
@@ -291,7 +290,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = def;
cook_type = typ;
- cook_proj = false;
cook_universes = Monomorphic_const univs;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
@@ -343,39 +341,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = def;
cook_type = typ;
- cook_proj = false;
cook_universes = univs;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
}
- | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} ->
- let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
- let kn, pb =
- match mib.mind_record with
- | Some (Some (id, kns, pbs)) ->
- if i < Array.length pbs then
- kns.(i), pbs.(i)
- else assert false
- | _ -> assert false
- in
- let univs =
- match mib.mind_universes with
- | Monomorphic_ind ctx -> Monomorphic_const ctx
- | Polymorphic_ind auctx -> Polymorphic_const auctx
- | Cumulative_ind acumi ->
- Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi)
- in
- let term, typ = pb.proj_eta in
- {
- Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term));
- cook_type = typ;
- cook_proj = true;
- cook_universes = univs;
- cook_inline = false;
- cook_context = None;
- }
-
let record_aux env s_ty s_bo =
let in_ty = keep_hyps env s_ty in
let v =
@@ -464,7 +434,6 @@ let build_constant_declaration kn env result =
{ const_hyps = hyps;
const_body = def;
const_type = typ;
- const_proj = result.cook_proj;
const_body_code = tps;
const_universes = univs;
const_inline_code = result.cook_inline;
@@ -553,23 +522,24 @@ let export_side_effects mb env c =
end
in
let rec translate_seff sl seff acc env =
- match sl, seff with
- | _, [] -> List.rev acc, ce
- | (None | Some 0), cbs :: rest ->
+ match seff with
+ | [] -> List.rev acc, ce
+ | cbs :: rest ->
+ if Int.equal sl 0 then
let env, cbs =
List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
let ce = constant_entry_of_side_effect ocb u in
let cb = translate_constant Pure env kn ce in
(push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs))
(env,[]) cbs in
- translate_seff sl rest (cbs @ acc) env
- | Some sl, cbs :: rest ->
+ translate_seff 0 rest (cbs @ acc) env
+ else
let cbs_len = List.length cbs in
let cbs = List.map turn_direct cbs in
let env = List.fold_left push_seff env cbs in
let ecbs = List.map (fun (kn,cb,u,r) ->
kn, cb, r) cbs in
- translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env
+ translate_seff (sl - cbs_len) rest (ecbs @ acc) env
in
translate_seff trusted seff [] env
;;
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-15 04:40:08 +0000