aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/cic.mli1
-rw-r--r--checker/values.ml4
-rw-r--r--kernel/cClosure.ml47
-rw-r--r--kernel/cClosure.mli10
-rw-r--r--kernel/declarations.ml1
-rw-r--r--kernel/declareops.ml1
-rw-r--r--library/global.ml7
-rw-r--r--library/global.mli3
-rw-r--r--pretyping/cbv.ml3
-rw-r--r--vernac/vernacentries.ml4
10 files changed, 54 insertions, 27 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index df747692a4..17259bb438 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -220,6 +220,7 @@ type typing_flags = {
points are assumed to be total. *)
check_universes : bool; (** If [false] universe constraints are not checked *)
conv_oracle : oracle; (** Unfolding strategies for conversion *)
+ share_reduction : bool; (** Use by-need reduction algorithm *)
}
type constant_body = {
diff --git a/checker/values.ml b/checker/values.ml
index e68cd18b87..e1b5a949ac 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 064cd8d9651d37aebf77fb638b889cad checker/cic.mli
+MD5 f7b267579138eabf86a74d6f2a7ed794 checker/cic.mli
*)
@@ -226,7 +226,7 @@ let v_cst_def =
[|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
let v_typing_flags =
- v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
+ v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool|]
let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index ac4c6c52c6..fd9394025a 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -31,7 +31,6 @@ open Environ
open Esubst
let stats = ref false
-let share = ref true
(* Profiling *)
let beta = ref 0
@@ -266,6 +265,7 @@ type 'a infos_cache = {
i_env : env;
i_sigma : existential -> constr option;
i_rels : (Constr.rel_declaration * lazy_val) Range.t;
+ i_share : bool;
}
and 'a infos = {
@@ -313,12 +313,13 @@ let ref_value_cache ({i_cache = cache} as infos) tab ref =
let evar_value cache ev =
cache.i_sigma ev
-let create mk_cl flgs env evars =
+let create ~repr ~share flgs env evars =
let cache =
- { i_repr = mk_cl;
+ { i_repr = repr;
i_env = env;
i_sigma = evars;
i_rels = env.env_rel_context.env_rel_map;
+ i_share = share;
}
in { i_flags = flgs; i_cache = cache }
@@ -384,8 +385,8 @@ let mk_red f = {norm=Red;term=f}
(* Could issue a warning if no is still Red, pointing out that we loose
sharing. *)
-let update v1 no t =
- if !share then
+let update ~share v1 no t =
+ if share then
(v1.norm <- no;
v1.term <- t;
v1)
@@ -498,14 +499,16 @@ let compact_stack head stk =
(* Be sure to create a new cell otherwise sharing would be
lost by the update operation *)
let h' = lft_fconstr depth head in
- let _ = update m h'.norm h'.term in
+ (** The stack contains [Zupdate] marks only if in sharing mode *)
+ let _ = update ~share:true m h'.norm h'.term in
strip_rec depth s
| stk -> zshift depth stk in
strip_rec 0 stk
(* Put an update mark in the stack, only if needed *)
-let zupdate m s =
- if !share && begin match m.norm with Red -> true | _ -> false end
+let zupdate info m s =
+ let share = info.i_cache.i_share in
+ if share && begin match m.norm with Red -> true | _ -> false end
then
let s' = compact_stack m s in
let _ = m.term <- FLOCKED in
@@ -698,7 +701,8 @@ let rec zip m stk =
| Zshift(n)::s ->
zip (lift_fconstr n m) s
| Zupdate(rf)::s ->
- zip (update rf m.norm m.term) s
+ (** The stack contains [Zupdate] marks only if in sharing mode *)
+ zip (update ~share:true rf m.norm m.term) s
let fapp_stack (m,stk) = zip m stk
@@ -718,7 +722,8 @@ let strip_update_shift_app_red head stk =
strip_rec (Zapp args :: rstk)
{norm=h.norm;term=FApp(h,args)} depth s
| Zupdate(m)::s ->
- strip_rec rstk (update m h.norm h.term) depth s
+ (** The stack contains [Zupdate] marks only if in sharing mode *)
+ strip_rec rstk (update ~share:true m h.norm h.term) depth s
| stk -> (depth,List.rev rstk, stk) in
strip_rec [] head 0 stk
@@ -743,7 +748,8 @@ let get_nth_arg head n stk =
List.rev (if Int.equal n 0 then rstk else (Zapp bef :: rstk)) in
(Some (stk', args.(n)), append_stack aft s')
| Zupdate(m)::s ->
- strip_rec rstk (update m h.norm h.term) n s
+ (** The stack contains [Zupdate] mark only if in sharing mode *)
+ strip_rec rstk (update ~share:true m h.norm h.term) n s
| s -> (None, List.rev rstk @ s) in
strip_rec [] head n stk
@@ -752,7 +758,8 @@ let get_nth_arg head n stk =
let rec get_args n tys f e stk =
match stk with
Zupdate r :: s ->
- let _hd = update r Cstr (FLambda(n,tys,f,e)) in
+ (** The stack contains [Zupdate] mark only if in sharing mode *)
+ let _hd = update ~share:true r Cstr (FLambda(n,tys,f,e)) in
get_args n tys f e s
| Zshift k :: s ->
get_args n tys f (subs_shft (k,e)) s
@@ -889,10 +896,10 @@ let unfold_projection info p =
let rec knh info m stk =
match m.term with
| FLIFT(k,a) -> knh info a (zshift k stk)
- | FCLOS(t,e) -> knht info e t (zupdate m stk)
+ | FCLOS(t,e) -> knht info e t (zupdate info m stk)
| FLOCKED -> assert false
- | FApp(a,b) -> knh info a (append_stack b (zupdate m stk))
- | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate m stk)
+ | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk))
+ | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk)
| FFix(((ri,n),(_,_,_)),_) ->
(match get_nth_arg m ri.(n) stk with
(Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
@@ -901,7 +908,7 @@ let rec knh info m stk =
| FProj (p,c) ->
(match unfold_projection info p with
| None -> (m, stk)
- | Some s -> knh info c (s :: zupdate m stk))
+ | Some s -> knh info c (s :: zupdate info m stk))
(* cases where knh stops *)
| (FFlex _|FLetIn _|FConstruct _|FEvar _|
@@ -1019,10 +1026,11 @@ let rec zip_term zfun m stk =
2- tries to rebuild the term. If a closure still has to be computed,
calls itself recursively. *)
let rec kl info tab m =
+ let share = info.i_cache.i_share in
if is_val m then (incr prune; term_of_fconstr m)
else
let (nm,s) = kni info tab m [] in
- let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *)
+ let () = if share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *)
zip_term (kl info tab) (norm_head info tab nm) s
(* no redex: go up for atoms and already normalized terms, go down
@@ -1078,14 +1086,15 @@ let whd_stack infos tab m stk = match m.norm with
knh infos m stk
| Red | Cstr ->
let k = kni infos tab m stk in
- let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
+ let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
k
(* cache of constants: the body is computed only when needed. *)
type clos_infos = fconstr infos
let create_clos_infos ?(evars=fun _ -> None) flgs env =
- create (fun _ _ c -> inject c) flgs env evars
+ let share = (Environ.typing_flags env).Declarations.share_reduction in
+ create ~share ~repr:(fun _ _ c -> inject c) flgs env evars
let create_tab () = KeyTable.create 17
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 1e3e7b48ac..6121b3a1ec 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -15,7 +15,6 @@ open Esubst
(** Flags for profiling reductions. *)
val stats : bool ref
-val share : bool ref
val with_stats: 'a Lazy.t -> 'a
@@ -106,8 +105,13 @@ type 'a infos = {
i_cache : 'a infos_cache }
val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option
-val create: ('a infos -> 'a infos_tab -> constr -> 'a) -> reds -> env ->
- (existential -> constr option) -> 'a infos
+val create:
+ repr:('a infos -> 'a infos_tab -> constr -> 'a) ->
+ share:bool ->
+ reds ->
+ env ->
+ (existential -> constr option) ->
+ 'a infos
val create_tab : unit -> 'a infos_tab
val evar_value : 'a infos_cache -> existential -> constr option
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 0811eb72fd..1d49550442 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -65,6 +65,7 @@ type typing_flags = {
points are assumed to be total. *)
check_universes : bool; (** If [false] universe constraints are not checked *)
conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
+ share_reduction : bool; (** Use by-need reduction algorithm *)
}
(* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index bbe4bc0dcb..b0d8410873 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -21,6 +21,7 @@ let safe_flags oracle = {
check_guarded = true;
check_universes = true;
conv_oracle = oracle;
+ share_reduction = true;
}
(** {6 Arities } *)
diff --git a/library/global.ml b/library/global.ml
index dcb20a280e..e833f71142 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -90,6 +90,7 @@ let push_context b c = globalize0 (Safe_typing.push_context b c)
let set_engagement c = globalize0 (Safe_typing.set_engagement c)
let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
+let typing_flags () = Environ.typing_flags (env ())
let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
@@ -278,3 +279,9 @@ let register_inline c = globalize0 (Safe_typing.register_inline c)
let set_strategy k l =
GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l)
+let set_reduction_sharing b =
+ let env = safe_env () in
+ let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in
+ let flags = { flags with Declarations.share_reduction = b } in
+ let env = Safe_typing.set_typing_flags flags env in
+ GlobalSafeEnv.set_safe_env env
diff --git a/library/global.mli b/library/global.mli
index b2a191ceeb..2819c187ed 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -30,6 +30,7 @@ val named_context : unit -> Constr.named_context
(** Changing the (im)predicativity of the system *)
val set_engagement : Declarations.engagement -> unit
val set_typing_flags : Declarations.typing_flags -> unit
+val typing_flags : unit -> Declarations.typing_flags
(** Variables, Local definitions, constants, inductive types *)
@@ -155,6 +156,8 @@ val register_inline : Constant.t -> unit
val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
+val set_reduction_sharing : bool -> unit
+
(* Modifies the global state, registering new universes *)
val current_modpath : unit -> ModPath.t
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index da6e26cc4b..fc24e9b3a9 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -455,7 +455,8 @@ let cbv_norm infos constr =
(* constant bodies are normalized at the first expansion *)
let create_cbv_infos flgs env sigma =
let infos = create
- (fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c)
+ ~share:true (** Not used by cbv *)
+ ~repr:(fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c)
flgs
env
(Reductionops.safe_evar_value sigma) in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 653f8b26e0..d33c278e31 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1501,8 +1501,8 @@ let _ =
{ optdepr = false;
optname = "kernel term sharing";
optkey = ["Kernel"; "Term"; "Sharing"];
- optread = (fun () -> !CClosure.share);
- optwrite = (fun b -> CClosure.share := b) }
+ optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction);
+ optwrite = (fun b -> Global.set_reduction_sharing b) }
let _ =
declare_bool_option
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:36:57 +0000