From de20a45db5d45154819f2ed4359effdbb8bf0292 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 27 Mar 2018 16:16:40 +0200
Subject: 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.
---
 kernel/cClosure.ml     | 47 ++++++++++++++++++++++++++++-------------------
 kernel/cClosure.mli    | 10 +++++++---
 kernel/declarations.ml |  1 +
 kernel/declareops.ml   |  1 +
 4 files changed, 37 insertions(+), 22 deletions(-)

(limited to 'kernel')

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 } *)
-- 
cgit v1.2.3