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.ml19
-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/esubst.ml23
-rw-r--r--kernel/esubst.mli7
-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.ml6
-rw-r--r--kernel/subtyping.ml5
-rw-r--r--kernel/term_typing.ml53
-rw-r--r--kernel/typeops.ml2
17 files changed, 225 insertions, 154 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 68057b389..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
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/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 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..244e5e0dd 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -432,7 +432,6 @@ module Renv =
r
end
-(* What about pattern matching ?*)
let is_lazy prefix t =
match kind t with
| App (f,args) ->
@@ -448,7 +447,7 @@ let is_lazy prefix t =
with Not_found -> true)
| _ -> true
end
- | LetIn _ -> true
+ | LetIn _ | Case _ | Proj _ -> true
| _ -> false
let evar_value sigma ev = sigma.evars_val ev
@@ -520,8 +519,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 2e9a33a91..1e58f5c24 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -194,8 +194,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 37bf679c5..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
@@ -522,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-05-21 20:15:54 +0000