Merge PR #13905: Inline the refold and tactic_mode flags for the cbn tactic.

Reviewed-by: SkySkimmer

1 files changed, 33 insertions, 53 deletions

diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 167f7d4026..99d579f5c6 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -402,11 +402,11 @@ let safe_meta_value sigma ev =
 
 (* Beta Reduction tools *)
 
-let apply_subst recfun env sigma refold cst_l t stack =
+let apply_subst recfun env sigma cst_l t stack =
   let rec aux env cst_l t stack =
     match (Stack.decomp stack, EConstr.kind sigma t) with
     | Some (h,stacktl), Lambda (_,_,c) ->
-       let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in
+       let cst_l' = Cst_stack.add_param h cst_l in
        aux (h::env) cst_l' c stacktl
     | _ -> recfun sigma cst_l (substl env t, stack)
   in aux env cst_l t stack
@@ -453,50 +453,42 @@ let magically_constant_of_fixbody env sigma reference bd = function
           | None -> bd
         end
 
-let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
+let contract_cofix ~env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
   let make_Fi j =
     let ind = nbodies-j-1 in
     if Int.equal bodynum ind then mkCoFix (ind,typedbodies)
     else
       let bd = mkCoFix (ind,typedbodies) in
-      match env with
+      match reference with
       | None -> bd
-      | Some e ->
-        match reference with
-        | None -> bd
-        | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+      | Some r -> magically_constant_of_fixbody env sigma r bd names.(ind).binder_name in
   let closure = List.init nbodies make_Fi in
   substl closure bodies.(bodynum)
 
 (** Similar to the "fix" case below *)
-let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk =
+let reduce_and_refold_cofix recfun env sigma cst_l cofix sk =
   let raw_answer =
-    let env = if refold then Some env else None in
-    contract_cofix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in
+    contract_cofix ~env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in
   apply_subst
     (fun sigma x (t,sk') ->
-      let t' =
-        if refold then Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t else t in
+      let t' = Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t in
       recfun x (t',sk'))
-    [] sigma refold Cst_stack.empty raw_answer sk
+    [] sigma Cst_stack.empty raw_answer sk
 
 (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
    Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
 
-let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) =
+let contract_fix ~env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) =
     let nbodies = Array.length recindices in
     let make_Fi j =
       let ind = nbodies-j-1 in
       if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies)
       else
         let bd = mkFix ((recindices,ind),typedbodies) in
-        match env with
+        match reference with
         | None -> bd
-        | Some e ->
-          match reference with
-          | None -> bd
-          | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+        | Some r -> magically_constant_of_fixbody env sigma r bd names.(ind).binder_name in
     let closure = List.init nbodies make_Fi in
     substl closure bodies.(bodynum)
 
@@ -504,18 +496,14 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies
     replace the fixpoint by the best constant from [cst_l]
     Other rels are directly substituted by constants "magically found from the
     context" in contract_fix *)
-let reduce_and_refold_fix recfun env sigma refold cst_l fix sk =
+let reduce_and_refold_fix recfun env sigma cst_l fix sk =
   let raw_answer =
-    let env = if refold then Some env else None in
-    contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in
+    contract_fix ~env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in
   apply_subst
     (fun sigma x (t,sk') ->
-      let t' =
-        if refold then
-          Cst_stack.best_replace sigma (mkFix fix) cst_l t
-        else t
-      in recfun x (t',sk'))
-    [] sigma refold Cst_stack.empty raw_answer sk
+      let t' = Cst_stack.best_replace sigma (mkFix fix) cst_l t in
+      recfun x (t',sk'))
+    [] sigma Cst_stack.empty raw_answer sk
 
 module CredNative = Reductionops.CredNative
 
@@ -524,7 +512,7 @@ module CredNative = Reductionops.CredNative
     Here is where unfolded constant are stored in order to be
     eventually refolded.
 
-    If tactic_mode is true, it uses ReductionBehaviour, prefers
+    It uses ReductionBehaviour, prefers
     refold constant instead of value and tries to infer constants
     fix and cofix came from.
 
@@ -558,7 +546,7 @@ let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
   in
   Vars.substl subst (snd br)
 
-let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
+let rec whd_state_gen ?csts flags env sigma =
   let open Context.Named.Declaration in
   let open ReductionBehaviour in
   let rec whrec cst_l (x, stack) =
@@ -584,7 +572,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) ->
       (match lookup_named id env with
       | LocalDef (_,body,_) ->
-        whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack)
+        whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack)
       | _ -> fold ())
     | Evar ev -> fold ()
     | Meta ev ->
@@ -600,10 +588,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
        | body ->
          begin
           let body = EConstr.of_constr body in
-          if not tactic_mode
-          then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
-              (body, stack)
-          else (* Looks for ReductionBehaviour *)
+          (* Looks for ReductionBehaviour *)
             match ReductionBehaviour.get (GlobRef.ConstRef c) with
             | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
             | Some behavior ->
@@ -652,10 +637,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       else fold ()
     | Proj (p, c) when CClosure.RedFlags.red_projection flags p ->
       (let npars = Projection.npars p in
-       if not tactic_mode then
-         let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in
-         whrec Cst_stack.empty stack'
-       else match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with
+       match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with
          | None ->
            let stack' = (c, Stack.Proj (p, cst_l) :: stack) in
            let stack'', csts = whrec Cst_stack.empty stack' in
@@ -693,24 +675,24 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
            end)
 
     | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
-      apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack
+      apply_subst (fun _ -> whrec) [b] sigma cst_l c stack
     | Cast (c,_,_) -> whrec cst_l (c, stack)
     | App (f,cl)  ->
       whrec
-        (if refold then Cst_stack.add_args cl cst_l else cst_l)
+        (Cst_stack.add_args cl cst_l)
         (f, Stack.append_app cl stack)
     | Lambda (na,t,c) ->
       (match Stack.decomp stack with
       | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
-        apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack
+        apply_subst (fun _ -> whrec) [] sigma cst_l x stack
       | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
         let env' = push_rel (LocalAssum (na, t)) env in
-        let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in
-        (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with
+        let whrec' = whd_state_gen flags env' sigma in
+        (match EConstr.kind sigma (Stack.zip ~refold:true sigma (whrec' (c, Stack.empty))) with
         | App (f,cl) ->
           let napp = Array.length cl in
           if napp > 0 then
-            let (x', l'),_ = whrec' (Array.last cl, Stack.empty) in
+            let (x', l') = whrec' (Array.last cl, Stack.empty) in
             match EConstr.kind sigma x', l' with
             | Rel 1, [] ->
               let lc = Array.sub cl 0 (napp-1) in
@@ -743,7 +725,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
         |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
           let x' = Stack.zip sigma (x, args) in
           let out_sk = s' @ (Stack.append_app [|x'|] s'') in
-          reduce_and_refold_fix whrec env sigma refold cst_l f out_sk
+          reduce_and_refold_fix whrec env sigma cst_l f out_sk
         |args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') ->
           let x' = Stack.zip sigma (x, args) in
           begin match remains with
@@ -755,7 +737,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
               | Some body ->
                 let const = (fst const, EInstance.make (snd const)) in
                 let body = EConstr.of_constr body in
-                whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
+                whrec (Cst_stack.add_cst (mkConstU const) cst_l)
                   (body, s' @ (Stack.append_app [|x'|] s'')))
             | Stack.Cst_proj p ->
               let stack = s' @ (Stack.append_app [|x'|] s'') in
@@ -778,7 +760,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then
         match Stack.strip_app stack with
         |args, ((Stack.Case _ |Stack.Proj _)::s') ->
-          reduce_and_refold_cofix whrec env sigma refold cst_l cofix stack
+          reduce_and_refold_cofix whrec env sigma cst_l cofix stack
         |_ -> fold ()
       else fold ()
 
@@ -812,12 +794,10 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   in
   fun xs ->
   let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in
-  if tactic_mode then (Stack.best_state sigma s cst_l,Cst_stack.empty) else res
+  (Stack.best_state sigma s cst_l)
 
 let whd_cbn flags env sigma t =
-  let (state,_) =
-    (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t, Stack.empty))
-  in
+  let state = whd_state_gen flags env sigma (t, Stack.empty) in
   Stack.zip ~refold:true sigma state
 
 let norm_cbn flags env sigma t =