Merge PR #13630: Cleanup reductionops

Reviewed-by: gares

5 files changed, 32 insertions, 48 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index b6e44265ae..aa862a912e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -323,23 +323,32 @@ let check_and_decompose_canonical_structure env sigma ref =
 let lookup_canonical_conversion env (proj,pat) =
   assoc_pat env pat (GlobRef.Map.find proj !object_table)
 
-let decompose_projection sigma c args =
+let rec get_nth n = function
+| [] -> raise Not_found
+| arg :: args ->
+  let len = Array.length arg in
+  if n < len then arg.(n)
+  else get_nth (n - len) args
+
+let rec decompose_projection sigma c args =
   match EConstr.kind sigma c with
+  | Meta mv -> decompose_projection sigma (Evd.meta_value sigma mv) args
+  | Cast (c, _, _) -> decompose_projection sigma c args
+  | App (c, arg) -> decompose_projection sigma c (arg :: args)
   | Const (c, u) ->
      let n = find_projection_nparams (GlobRef.ConstRef c) in
      (* Check if there is some canonical projection attached to this structure *)
      let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in
-     let arg = Stack.nth args n in
-     arg
+     get_nth n args
   | Proj (p, c) ->
      let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in
      c
   | _ -> raise Not_found
 
-let is_open_canonical_projection env sigma (c,args) =
+let is_open_canonical_projection env sigma c =
   let open EConstr in
   try
-    let arg = decompose_projection sigma c args in
+    let arg = decompose_projection sigma c [] in
     try
       let arg = whd_all env sigma arg in
       let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 5b8dc8184a..83927085e9 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -94,7 +94,7 @@ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
   cs -> unit
 val subst_canonical_structure : Mod_subst.substitution -> cs -> cs
 val is_open_canonical_projection :
-  Environ.env -> Evd.evar_map -> Reductionops.state -> bool
+  Environ.env -> Evd.evar_map -> EConstr.t -> bool
 val canonical_projections : unit ->
   ((GlobRef.t * cs_pattern) * obj_typ) list
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3352bfce38..7a5d0897b5 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -930,14 +930,6 @@ let stack_red_of_state_red f =
   let f env sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f env sigma (x, Stack.empty))) in
   f
 
-(* Drops the Cst_stack *)
-let iterate_whd_gen flags env sigma s =
-  let rec aux t =
-  let (hd,sk) = whd_state_gen flags env sigma (t,Stack.empty) in
-  let whd_sk = Stack.map aux sk in
-  Stack.zip sigma (hd,whd_sk)
-  in aux s
-
 let red_of_state_red f env sigma x =
   Stack.zip sigma (f env sigma (x,Stack.empty))
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index d404a7e414..04dfc5ffe6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -106,8 +106,6 @@ end
 
 (************************************************************************)
 
-type state = constr * constr Stack.t
-
 type reduction_function = env -> evar_map -> constr -> constr
 
 type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
@@ -115,11 +113,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
 type stack_reduction_function =
     env -> evar_map -> constr -> constr * constr list
 
-type state_reduction_function =
-    env -> evar_map -> state -> state
-
-val pr_state : env -> evar_map -> state -> Pp.t
-
 (** {6 Reduction Function Operators } *)
 
 val strong_with_flags :
@@ -127,12 +120,6 @@ val strong_with_flags :
   (CClosure.RedFlags.reds -> reduction_function)
 val strong : reduction_function -> reduction_function
 
-val whd_state_gen :
-  CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state
-
-val iterate_whd_gen : CClosure.RedFlags.reds ->
-  Environ.env -> Evd.evar_map -> constr -> constr
-
 (** {6 Generic Optimized Reduction Function using Closures } *)
 
 val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function
@@ -166,24 +153,13 @@ val whd_all_stack : stack_reduction_function
 val whd_allnolet_stack : stack_reduction_function
 val whd_betalet_stack : stack_reduction_function
 
-val whd_nored_state : state_reduction_function
-val whd_beta_state : state_reduction_function
-val whd_betaiota_state : state_reduction_function
-val whd_betaiotazeta_state : state_reduction_function
-val whd_all_state : state_reduction_function
-val whd_allnolet_state : state_reduction_function
-val whd_betalet_state : state_reduction_function
-
 (** {6 Head normal forms } *)
 
 val whd_delta_stack :  stack_reduction_function
-val whd_delta_state :  state_reduction_function
 val whd_delta :  reduction_function
 val whd_betadeltazeta_stack :  stack_reduction_function
-val whd_betadeltazeta_state :  state_reduction_function
 val whd_betadeltazeta :  reduction_function
 val whd_zeta_stack : stack_reduction_function
-val whd_zeta_state : state_reduction_function
 val whd_zeta : reduction_function
 
 val shrink_eta : Environ.env -> constr -> constr
@@ -269,8 +245,17 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t ->
 
 (** {6 Heuristic for Conversion with Evar } *)
 
+type state = constr * constr Stack.t
+
+type state_reduction_function =
+    env -> evar_map -> state -> state
+
+val pr_state : env -> evar_map -> state -> Pp.t
+
+val whd_nored_state : state_reduction_function
+
 val whd_betaiota_deltazeta_for_iota_state :
-  TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state
+  TransparentState.t -> state_reduction_function
 
 (** {6 Meta-related reduction functions } *)
 val meta_instance : env -> evar_map -> constr freelisted -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1c24578a1c..3d3010d1a4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1070,10 +1070,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
   and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
     let f1 () =
       if isApp_or_Proj sigma cM then
-        let f1l1 = whd_nored_state curenv sigma (cM,Stack.empty) in
-          if is_open_canonical_projection curenv sigma f1l1 then
-            let f2l2 = whd_nored_state curenv sigma (cN,Stack.empty) in
-              solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn
+          if is_open_canonical_projection curenv sigma cM then
+            solve_canonical_projection curenvnb pb opt cM cN substn
           else error_cannot_unify (fst curenvnb) sigma (cM,cN)
       else error_cannot_unify (fst curenvnb) sigma (cM,cN)
     in
@@ -1086,14 +1084,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       else
         try f1 () with e when precatchable_exception e ->
           if isApp_or_Proj sigma cN then
-            let f2l2 = whd_nored_state curenv sigma (cN, Stack.empty) in
-              if is_open_canonical_projection curenv sigma f2l2 then
-                let f1l1 = whd_nored_state curenv sigma (cM, Stack.empty) in
-                  solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn
+              if is_open_canonical_projection curenv sigma cN then
+                solve_canonical_projection curenvnb pb opt cN cM substn
               else error_cannot_unify (fst curenvnb) sigma (cM,cN)
           else error_cannot_unify (fst curenvnb) sigma (cM,cN)
 
-  and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) =
+  and solve_canonical_projection curenvnb pb opt cM cN (sigma,ms,es) =
+    let f1l1 = whd_nored_state (fst curenvnb) sigma (cM,Stack.empty) in
+    let f2l2 = whd_nored_state (fst curenvnb) sigma (cN,Stack.empty) in
     let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
       try Evarconv.check_conv_record (fst curenvnb) sigma f1l1 f2l2
       with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)