Merge PR #11922: No more local reduction functions in Reductionops.

Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares

1 files changed, 28 insertions, 45 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f7456ef35e..15bf9667b3 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -603,9 +603,7 @@ end
 (** The type of (machine) states (= lambda-bar-calculus' cuts) *)
 type state = constr * constr Stack.t
 
-type contextual_reduction_function = env -> evar_map -> constr -> constr
-type reduction_function = contextual_reduction_function
-type local_reduction_function = evar_map -> constr -> constr
+type reduction_function = env -> evar_map -> constr -> constr
 type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
 
 type contextual_stack_reduction_function =
@@ -650,16 +648,6 @@ let strong whdfun env sigma t =
     map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in
   strongrec env t
 
-let local_strong whdfun sigma =
-  let rec strongrec t = EConstr.map sigma strongrec (whdfun sigma t) in
-  strongrec
-
-let rec strong_prodspine redfun sigma c =
-  let x = redfun sigma c in
-  match EConstr.kind sigma x with
-    | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b)
-    | _ -> x
-
 (*************************************)
 (*** Reduction using bindingss ***)
 (*************************************)
@@ -1225,7 +1213,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   if tactic_mode then (Stack.best_state sigma s cst_l,Cst_stack.empty) else res
 
 (** reduction machine without global env and refold machinery *)
-let local_whd_state_gen flags sigma =
+let local_whd_state_gen flags _env sigma =
   let rec whrec (x, stack) =
     let c0 = EConstr.kind sigma x in
     let s = (EConstr.of_kind c0, stack) in
@@ -1308,7 +1296,7 @@ let raw_whd_state_gen flags env =
   f
 
 let stack_red_of_state_red f =
-  let f sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f sigma (x, Stack.empty))) in
+  let f env sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f env sigma (x, Stack.empty))) in
   f
 
 (* Drops the Cst_stack *)
@@ -1319,8 +1307,8 @@ let iterate_whd_gen refold flags env sigma s =
   Stack.zip sigma ~refold (hd,whd_sk)
   in aux s
 
-let red_of_state_red f sigma x =
-  Stack.zip sigma (f sigma (x,Stack.empty))
+let red_of_state_red f env sigma x =
+  Stack.zip sigma (f env sigma (x,Stack.empty))
 
 (* 0. No Reduction Functions *)
 
@@ -1341,15 +1329,12 @@ let whd_betalet = red_of_state_red whd_betalet_state
 (* 2. Delta Reduction Functions *)
 
 let whd_delta_state e = raw_whd_state_gen CClosure.delta e
-let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env)
-let whd_delta env = red_of_state_red  (whd_delta_state env)
-
-let whd_betadeltazeta_state e = raw_whd_state_gen CClosure.betadeltazeta e
-let whd_betadeltazeta_stack env =
-  stack_red_of_state_red (whd_betadeltazeta_state env)
-let whd_betadeltazeta env =
-  red_of_state_red (whd_betadeltazeta_state env)
+let whd_delta_stack = stack_red_of_state_red whd_delta_state
+let whd_delta = red_of_state_red whd_delta_state
 
+let whd_betadeltazeta_state = raw_whd_state_gen CClosure.betadeltazeta
+let whd_betadeltazeta_stack = stack_red_of_state_red whd_betadeltazeta_state
+let whd_betadeltazeta = red_of_state_red whd_betadeltazeta_state
 
 (* 3. Iota reduction Functions *)
 
@@ -1361,21 +1346,19 @@ let whd_betaiotazeta_state = local_whd_state_gen CClosure.betaiotazeta
 let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state
 let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state
 
-let whd_all_state env = raw_whd_state_gen CClosure.all env
-let whd_all_stack env =
-  stack_red_of_state_red (whd_all_state env)
-let whd_all env =
-  red_of_state_red (whd_all_state env)
+let whd_all_state = raw_whd_state_gen CClosure.all
+let whd_all_stack = stack_red_of_state_red whd_all_state
+let whd_all = red_of_state_red whd_all_state
 
-let whd_allnolet_state env = raw_whd_state_gen CClosure.allnolet env
-let whd_allnolet_stack env =
-  stack_red_of_state_red (whd_allnolet_state env)
-let whd_allnolet env =
-  red_of_state_red (whd_allnolet_state env)
+let whd_allnolet_state = raw_whd_state_gen CClosure.allnolet
+let whd_allnolet_stack = stack_red_of_state_red whd_allnolet_state
+let whd_allnolet = red_of_state_red whd_allnolet_state
 
 (* 4. Ad-hoc eta reduction, does not substitute evars *)
 
-let shrink_eta c = Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty))
+let shrink_eta env c =
+  let evd = Evd.from_env env in
+  Stack.zip evd (local_whd_state_gen eta env evd (c,Stack.empty))
 
 (* 5. Zeta Reduction Functions *)
 
@@ -1627,9 +1610,9 @@ let plain_instance sigma s c =
      empty map).
  *)
 
-let instance sigma s c =
+let instance env sigma s c =
   (* if s = [] then c else *)
-  local_strong whd_betaiota sigma (plain_instance sigma s c)
+  strong whd_betaiota env sigma (plain_instance sigma s c)
 
 (* pseudo-reduction rule:
  * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
@@ -1795,23 +1778,23 @@ let is_arity env sigma c =
 (*************************************)
 (* Metas *)
 
-let meta_value evd mv =
+let meta_value env evd mv =
   let rec valrec mv =
     match meta_opt_fvalue evd mv with
     | Some (b,_) ->
       let metas = Metamap.bind valrec b.freemetas in
-      instance evd metas b.rebus
+      instance env evd metas b.rebus
     | None -> mkMeta mv
   in
   valrec mv
 
-let meta_instance sigma b =
+let meta_instance env sigma b =
   let fm = b.freemetas in
   if Metaset.is_empty fm then b.rebus
   else
-    let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in
-    instance sigma c_sigma b.rebus
+    let c_sigma = Metamap.bind (fun mv -> meta_value env sigma mv) fm in
+    instance env sigma c_sigma b.rebus
 
-let nf_meta sigma c =
+let nf_meta env sigma c =
   let cl = mk_freelisted c in
-  meta_instance sigma { cl with rebus = cl.rebus }
+  meta_instance env sigma { cl with rebus = cl.rebus }