Turn the kernel reduction sharing flag into an argument passed in the cache.

We move the global declaration of that argument to the environment, and reuse
the Global module to handle this flag.

Note that the checker was not using this flag before this patch, and still
doesn't use it. This should probably be fixed in a later patch.

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