aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/cic.mli2
-rw-r--r--checker/environ.ml20
-rw-r--r--checker/environ.mli1
-rw-r--r--checker/mod_checking.ml9
-rw-r--r--checker/values.ml4
-rw-r--r--kernel/clambda.ml6
-rw-r--r--kernel/cooking.ml22
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/declareops.ml5
-rw-r--r--kernel/environ.ml21
-rw-r--r--kernel/environ.mli1
-rw-r--r--kernel/inductive.ml4
-rw-r--r--kernel/nativecode.ml14
-rw-r--r--kernel/term_typing.ml34
-rw-r--r--kernel/typeops.ml10
-rw-r--r--kernel/typeops.mli2
-rw-r--r--library/heads.ml2
-rw-r--r--plugins/extraction/extraction.ml12
-rw-r--r--pretyping/inductiveops.ml6
-rw-r--r--tactics/hints.ml18
21 files changed, 80 insertions, 117 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index c4b00d0dc..27e2a479f 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -241,7 +241,7 @@ type constant_body = {
const_type : constr;
const_body_code : to_patch_substituted;
const_universes : constant_universes;
- const_proj : projection_body option;
+ const_proj : bool;
const_inline_code : bool;
const_typing_flags : typing_flags;
}
diff --git a/checker/environ.ml b/checker/environ.ml
index bbd043c8e..809150cea 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -7,6 +7,7 @@ open Declarations
type globals = {
env_constants : constant_body Cmap_env.t;
+ env_projections : projection_body Cmap_env.t;
env_inductives : mutual_inductive_body Mindmap_env.t;
env_inductives_eq : KerName.t KNmap.t;
env_modules : module_body MPmap.t;
@@ -34,6 +35,7 @@ let empty_oracle = {
let empty_env = {
env_globals =
{ env_constants = Cmap_env.empty;
+ env_projections = Cmap_env.empty;
env_inductives = Mindmap_env.empty;
env_inductives_eq = KNmap.empty;
env_modules = MPmap.empty;
@@ -165,12 +167,10 @@ let evaluable_constant cst env =
with Not_found | NotEvaluableConst _ -> false
let is_projection cst env =
- not (Option.is_empty (lookup_constant cst env).const_proj)
+ (lookup_constant cst env).const_proj
let lookup_projection p env =
- match (lookup_constant (Projection.constant p) env).const_proj with
- | Some pb -> pb
- | None -> anomaly ("lookup_projection: constant is not a projection.")
+ Cmap_env.find (Projection.constant p) env.env_globals.env_projections
(* Mutual Inductives *)
let scrape_mind env kn=
@@ -194,6 +194,13 @@ let add_mind kn mib env =
Printf.ksprintf anomaly ("Inductive %s is already defined.")
(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
+ in
let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in
let new_inds_eq = if KerName.equal kn1 kn2 then
env.env_globals.env_inductives_eq
@@ -201,8 +208,9 @@ let add_mind kn mib env =
KNmap.add kn1 kn2 env.env_globals.env_inductives_eq in
let new_globals =
{ env.env_globals with
- env_inductives = new_inds;
- env_inductives_eq = new_inds_eq} in
+ env_inductives = new_inds;
+ env_projections = new_projections;
+ env_inductives_eq = new_inds_eq} in
{ env with env_globals = new_globals }
diff --git a/checker/environ.mli b/checker/environ.mli
index 81da83875..4a7597249 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -5,6 +5,7 @@ open Cic
type globals = {
env_constants : constant_body Cmap_env.t;
+ env_projections : projection_body Cmap_env.t;
env_inductives : mutual_inductive_body Mindmap_env.t;
env_inductives_eq : KerName.t KNmap.t;
env_modules : module_body MPmap.t;
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 7685863ea..ca9581167 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -47,13 +47,8 @@ let check_constant_declaration env kn cb =
let () =
match body_of_constant cb with
| Some bd ->
- (match cb.const_proj with
- | None -> let j = infer envty bd in
- conv_leq envty j ty
- | Some pb ->
- let env' = add_constant kn cb env' in
- let j = infer env' bd in
- conv_leq envty j ty)
+ let j = infer envty bd in
+ conv_leq envty j ty
| None -> ()
in
let env =
diff --git a/checker/values.ml b/checker/values.ml
index 1ac8d7cef..f7ab95fe2 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 c4fdf8a846aed45c27b5acb1add7d1c6 checker/cic.mli
+MD5 92de14d7bf9134532e8a0cff5618bd50 checker/cic.mli
*)
@@ -240,7 +240,7 @@ let v_cb = v_tuple "constant_body"
v_constr;
Any;
v_const_univs;
- Opt v_projbody;
+ v_bool;
v_bool;
v_typing_flags|]
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 8389dd326..b722e4200 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -708,12 +708,10 @@ let rec lambda_of_constr env c =
Lcofix(init, (names, ltypes, lbodies))
| Proj (p,c) ->
- let kn = Projection.constant p in
- let cb = lookup_constant kn env.global_env in
- let pb = Option.get cb.const_proj in
+ let pb = lookup_projection p env.global_env in
let n = pb.proj_arg in
let lc = lambda_of_constr env c in
- Lproj (n,kn,lc)
+ Lproj (n,Projection.constant p,lc)
and lambda_of_app env f args =
match Constr.kind f with
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 6f4541e95..5783453e6 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -156,7 +156,7 @@ type inline = bool
type result = {
cook_body : constant_def;
cook_type : types;
- cook_proj : projection_body option;
+ cook_proj : bool;
cook_universes : constant_universes;
cook_inline : inline;
cook_context : Context.Named.t option;
@@ -227,28 +227,10 @@ let cook_constant ~hcons env { from = cb; info } =
hyps)
hyps ~init:cb.const_hyps in
let typ = abstract_constant_type (expmod cb.const_type) hyps in
- let projection pb =
- let c' = abstract_constant_body (expmod pb.proj_body) hyps in
- let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in
- let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in
- let ((mind, _), _), n' =
- try
- let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in
- match kind c' with
- | App (f,l) -> (destInd f, Array.length l)
- | Ind ind -> ind, 0
- | _ -> assert false
- with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0)
- in
- let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in
- { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg;
- proj_eta = etab, etat;
- proj_type = ty'; proj_body = c' }
- in
{
cook_body = body;
cook_type = typ;
- cook_proj = Option.map projection cb.const_proj;
+ 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 7bd0ae566..0d907f3de 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,7 +21,7 @@ type inline = bool
type result = {
cook_body : constant_def;
cook_type : types;
- cook_proj : projection_body option;
+ 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 b7427d20a..913c13173 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -87,7 +87,7 @@ type constant_body = {
const_type : types;
const_body_code : Cemitcodes.to_patch_substituted option;
const_universes : constant_universes;
- const_proj : projection_body option;
+ const_proj : bool;
const_inline_code : bool;
const_typing_flags : typing_flags; (** The typing options which
were used for
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 832d478b3..75c0e5b4c 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -94,14 +94,13 @@ let subst_const_body sub cb =
else
let body' = subst_const_def sub cb.const_body in
let type' = subst_const_type sub cb.const_type in
- let proj' = Option.Smart.map (subst_const_proj sub) cb.const_proj in
if body' == cb.const_body && type' == cb.const_type
- && proj' == cb.const_proj then cb
+ then cb
else
{ const_hyps = [];
const_body = body';
const_type = type';
- const_proj = proj';
+ 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;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index c3e7cec75..fb89576dd 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -52,6 +52,7 @@ type mind_key = mutual_inductive_body * link_info ref
type globals = {
env_constants : constant_key Cmap_env.t;
+ env_projections : projection_body Cmap_env.t;
env_inductives : mind_key Mindmap_env.t;
env_modules : module_body MPmap.t;
env_modtypes : module_type_body MPmap.t}
@@ -108,6 +109,7 @@ let empty_rel_context_val = {
let empty_env = {
env_globals = {
env_constants = Cmap_env.empty;
+ env_projections = Cmap_env.empty;
env_inductives = Mindmap_env.empty;
env_modules = MPmap.empty;
env_modtypes = MPmap.empty};
@@ -485,14 +487,10 @@ let type_in_type_constant cst env =
not (lookup_constant cst env).const_typing_flags.check_universes
let lookup_projection cst env =
- match (lookup_constant (Projection.constant cst) env).const_proj with
- | Some pb -> pb
- | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.")
+ Cmap_env.find (Projection.constant cst) env.env_globals.env_projections
let is_projection cst env =
- match (lookup_constant cst env).const_proj with
- | Some _ -> true
- | None -> false
+ (lookup_constant cst env).const_proj
(* Mutual Inductives *)
let polymorphic_ind (mind,i) env =
@@ -514,11 +512,18 @@ let template_polymorphic_pind (ind,u) env =
if not (Univ.Instance.is_empty u) then false
else template_polymorphic_ind ind env
-let add_mind_key kn mind_key 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
+ in
let new_globals =
{ env.env_globals with
- env_inductives = new_inds } in
+ env_inductives = new_inds; env_projections = new_projections; } in
{ env with env_globals = new_globals }
let add_mind kn mib env =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index fc45ce0e3..8928b32f1 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -48,6 +48,7 @@ type mind_key = mutual_inductive_body * link_info ref
type globals = {
env_constants : constant_key Cmap_env.t;
+ env_projections : projection_body Cmap_env.t;
env_inductives : mind_key Mindmap_env.t;
env_modules : module_body MPmap.t;
env_modtypes : module_type_body MPmap.t
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9bed598bb..090acdf16 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -803,9 +803,7 @@ let rec subterm_specif renv stack t =
(* We take the subterm specs of the constructor of the record *)
let wf_args = (dest_subterms wf).(0) in
(* We extract the tree of the projected argument *)
- let kn = Projection.constant p in
- let cb = lookup_constant kn renv.env in
- let pb = Option.get cb.const_proj in
+ let pb = lookup_projection p renv.env in
let n = pb.proj_arg in
spec_of_tree (List.nth wf_args n)
| Dead_code -> Dead_code
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 0cd0ad46c..036cd4847 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1859,7 +1859,7 @@ and compile_named env sigma univ auxdefs id =
let compile_constant env sigma prefix ~interactive con cb =
match cb.const_proj with
- | None ->
+ | false ->
let no_univs =
match cb.const_universes with
| Monomorphic_const _ -> true
@@ -1903,7 +1903,8 @@ let compile_constant env sigma prefix ~interactive con cb =
if interactive then LinkedInteractive prefix
else Linked prefix
end
- | Some pb ->
+ | true ->
+ let pb = lookup_projection (Projection.make con false) env in
let mind = pb.proj_ind in
let ind = (mind,0) in
let mib = lookup_mind mind env in
@@ -2029,11 +2030,12 @@ let rec compile_deps env sigma prefix ~interactive init t =
else
let comp_stack, (mind_updates, const_updates) =
match cb.const_proj, cb.const_body with
- | None, Def t ->
+ | false, Def t ->
compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
- | Some pb, _ ->
- let mind = pb.proj_ind in
- compile_mind_deps env prefix ~interactive init mind
+ | true, _ ->
+ let pb = lookup_projection (Projection.make c false) env in
+ let mind = pb.proj_ind in
+ compile_mind_deps env prefix ~interactive init mind
| _ -> init
in
let code, name =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 7352c1882..db1109e75 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -250,7 +250,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = Undef nl;
cook_type = t;
- cook_proj = None;
+ cook_proj = false;
cook_universes = univs;
cook_inline = false;
cook_context = ctx;
@@ -291,7 +291,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = def;
cook_type = typ;
- cook_proj = None;
+ cook_proj = false;
cook_universes = Monomorphic_const univs;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
@@ -343,7 +343,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = def;
cook_type = typ;
- cook_proj = None;
+ cook_proj = false;
cook_universes = univs;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
@@ -370,7 +370,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term));
cook_type = typ;
- cook_proj = Some pb;
+ cook_proj = true;
cook_universes = univs;
cook_inline = false;
cook_context = None;
@@ -458,30 +458,8 @@ let build_constant_declaration kn env result =
check declared inferred) lc) in
let univs = result.cook_universes in
let tps =
- let res =
- match result.cook_proj with
- | None -> Cbytegen.compile_constant_body ~fail_on_error:false env univs def
- | Some pb ->
- (* The compilation of primitive projections is a bit tricky, because
- they refer to themselves (the body of p looks like fun c =>
- Proj(p,c)). We break the cycle by building an ad-hoc compilation
- environment. A cleaner solution would be that kernel projections are
- simply Proj(i,c) with i an int and c a constr, but we would have to
- get rid of the compatibility layer. *)
- let cb =
- { const_hyps = hyps;
- const_body = def;
- const_type = typ;
- const_proj = result.cook_proj;
- const_body_code = None;
- const_universes = univs;
- const_inline_code = result.cook_inline;
- const_typing_flags = Environ.typing_flags env;
- }
- in
- let env = add_constant kn cb env in
- Cbytegen.compile_constant_body ~fail_on_error:false env univs def
- in Option.map Cemitcodes.from_val res
+ let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
+ Option.map Cemitcodes.from_val res
in
{ const_hyps = hyps;
const_body = def;
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index fd9cefb2c..325d5cecd 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -528,13 +528,3 @@ let judge_of_case env ci pj cj lfj =
let lf, lft = dest_judgev lfj in
make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft))
(type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft)
-
-let type_of_projection_constant env (p,u) =
- let cst = Projection.constant p in
- let cb = lookup_constant cst env in
- match cb.const_proj with
- | Some pb ->
- if Declareops.constant_is_polymorphic cb then
- Vars.subst_instance_constr u pb.proj_type
- else pb.proj_type
- | None -> raise (Invalid_argument "type_of_projection: not a projection")
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 85b2cfffd..546f2d2b4 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -100,8 +100,6 @@ val judge_of_case : env -> case_info
-> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
-> unsafe_judgment
-val type_of_projection_constant : env -> Projection.t puniverses -> types
-
val type_of_constant_in : env -> pconstant -> types
(** Check that hyps are included in env and fails with error otherwise *)
diff --git a/library/heads.ml b/library/heads.ml
index 198672a0a..3d5f6a6ff 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -129,7 +129,7 @@ let compute_head = function
let cb = Environ.lookup_constant cst env in
let is_Def = function Declarations.Def _ -> true | _ -> false in
let body =
- if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body
+ if not cb.Declarations.const_proj && is_Def cb.Declarations.const_body
then Global.body_of_constant cst else None
in
(match body with
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index cdd698304..5aee70194 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1066,8 +1066,10 @@ let extract_constant env kn cb =
| Undef _ -> warn_info (); mk_typ_ax ()
| Def c ->
(match cb.const_proj with
- | None -> mk_typ (get_body c)
- | Some pb -> mk_typ (EConstr.of_constr pb.proj_body))
+ | false -> mk_typ (get_body c)
+ | true ->
+ let pb = lookup_projection (Projection.make kn false) env in
+ mk_typ (EConstr.of_constr pb.proj_body))
| OpaqueDef c ->
add_opaque r;
if access_opaque () then mk_typ (get_opaque env c)
@@ -1077,8 +1079,10 @@ let extract_constant env kn cb =
| Undef _ -> warn_info (); mk_ax ()
| Def c ->
(match cb.const_proj with
- | None -> mk_def (get_body c)
- | Some pb -> mk_def (EConstr.of_constr pb.proj_body))
+ | false -> mk_def (get_body c)
+ | true ->
+ let pb = lookup_projection (Projection.make kn false) env in
+ mk_def (EConstr.of_constr pb.proj_body))
| OpaqueDef c ->
add_opaque r;
if access_opaque () then mk_def (get_opaque env c)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 8e3c33ff7..b1ab2d2b7 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -629,6 +629,10 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
env evdref scl ar.template_level (ctx,ar.template_param_levels) in
!evdref, EConstr.of_constr (mkArity (List.rev ctx,scl))
+let type_of_projection_constant env (p,u) =
+ let pb = lookup_projection p env in
+ Vars.subst_instance_constr u pb.proj_type
+
let type_of_projection_knowing_arg env sigma p c ty =
let c = EConstr.Unsafe.to_constr c in
let IndType(pars,realargs) =
@@ -637,7 +641,7 @@ let type_of_projection_knowing_arg env sigma p c ty =
raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type")
in
let (_,u), pars = dest_ind_family pars in
- substl (c :: List.rev pars) (Typeops.type_of_projection_constant env (p,u))
+ substl (c :: List.rev pars) (type_of_projection_constant env (p,u))
(***********************************************)
(* Guard condition *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 7b5be4c1c..29744e406 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -293,15 +293,15 @@ let strip_params env sigma c =
| App (f, args) ->
(match EConstr.kind sigma f with
| Const (p,_) ->
- let cb = lookup_constant p env in
- (match cb.Declarations.const_proj with
- | Some pb ->
- let n = pb.Declarations.proj_npars in
- if Array.length args > n then
- mkApp (mkProj (Projection.make p false, args.(n)),
- Array.sub args (n+1) (Array.length args - (n + 1)))
- else c
- | None -> c)
+ let p = Projection.make p false in
+ (match lookup_projection p env with
+ | pb ->
+ let n = pb.Declarations.proj_npars in
+ if Array.length args > n then
+ mkApp (mkProj (p, args.(n)),
+ Array.sub args (n+1) (Array.length args - (n + 1)))
+ else c
+ | exception Not_found -> c)
| _ -> c)
| _ -> c
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 08:36:01 +0000