Deduce Stack.decomp from Stack.strip_n_app.

3 files changed, 23 insertions, 16 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index cdf2922516..4637017517 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -355,14 +355,13 @@ let rec ise_inst2 evd f l1 l2 = match l1, l2 with
 
 (* Applicative node of stack are read from the outermost to the innermost
    but are unified the other way. *)
-let rec ise_app_stack2 env f evd sk1 sk2 =
-  match sk1,sk2 with
-  | Stack.App node1 :: q1, Stack.App node2 :: q2 ->
-     let (t1,l1) = Stack.decomp_node_last node1 q1 in
-     let (t2,l2) = Stack.decomp_node_last node2 q2 in
-     begin match ise_app_stack2 env f evd l1 l2 with
-           |(_,UnifFailure _) as x -> x
-           |x,Success i' -> x,f env i' CONV t1 t2
+let rec ise_app_rev_stack2 env f evd sk1 sk2 =
+  match Stack.decomp_rev sk1, Stack.decomp_rev sk2 with
+  | Some (t1,l1), Some (t2,l2) ->
+     begin
+       match ise_app_rev_stack2 env f evd l1 l2 with
+       | (_, UnifFailure _) as x -> x
+       | x, Success i' -> x, f env i' CONV t1 t2
      end
   | _, _ -> (sk1,sk2), Success evd
 
@@ -399,7 +398,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
       else fail (UnifFailure (i,NotSameHead))
     | Stack.App _ :: _, Stack.App _ :: _ ->
        if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else
-         begin match ise_app_stack2 env f i sk1 sk2 with
+         begin match ise_app_rev_stack2 env f i sk1 sk2 with
                |_,(UnifFailure _ as x) -> fail x
                |(l1, l2), Success i' -> ise_stack2 true i' l1 l2
          end
@@ -430,7 +429,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
        then ise_stack2 i q1 q2
        else (UnifFailure (i, NotSameHead))
     | Stack.App _ :: _, Stack.App _ :: _ ->
-         begin match ise_app_stack2 env f i sk1 sk2 with
+         begin match ise_app_rev_stack2 env f i sk1 sk2 with
                |_,(UnifFailure _ as x) -> x
                |(l1, l2), Success i' -> ise_stack2 i' l1 l2
          end
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3352bfce38..2a5de7ba74 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -194,6 +194,7 @@ sig
   val append_app : 'a array -> 'a t -> 'a t
   val decomp : 'a t -> ('a * 'a t) option
   val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t)
+  val decomp_rev : 'a t -> ('a * 'a t) option
   val compare_shape : 'a t -> 'a t -> bool
   val map : ('a -> 'a) -> 'a t -> 'a t
   val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
@@ -267,12 +268,10 @@ struct
     let le = Array.length v in
     if Int.equal le 0 then s else App (0,v,pred le) :: s
 
-  let decomp_node (i,l,j) sk =
-    if i < j then (l.(i), App (succ i,l,j) :: sk)
-    else (l.(i), sk)
-
-  let decomp = function
-    | App node::s -> Some (decomp_node node s)
+  let decomp_rev = function
+    | App (i,l,j) :: sk ->
+      if i < j then Some (l.(j), App (i,l,pred j) :: sk)
+      else Some (l.(j), sk)
     | _ -> None
 
   let decomp_node_last (i,l,j) sk =
@@ -357,6 +356,11 @@ struct
       | s -> None
     in aux n [] s
 
+  let decomp s =
+    match strip_n_app 0 s with
+    | Some (_,a,s) -> Some (a,s)
+    | None -> None
+
   let not_purely_applicative args =
     List.exists (function (Fix _ | Case _ | Proj _ ) -> true
                           | App _ | Primitive _ -> false) args
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index d404a7e414..7a840c5731 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -73,6 +73,7 @@ module Stack : sig
   val decomp : 'a t -> ('a * 'a t) option
 
   val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t)
+  [@@ocaml.deprecated "Use decomp_rev"]
 
   val compare_shape : 'a t -> 'a t -> bool
 
@@ -93,6 +94,9 @@ module Stack : sig
   (** @return (the nth first elements, the (n+1)th element, the remaining stack)  *)
   val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
 
+  (** [decomp sk] extracts the first argument of reversed stack [sk] is there is some *)
+  val decomp_rev : 'a t -> ('a * 'a t) option
+
   val not_purely_applicative : 'a t -> bool
   val list_of_app_stack : constr t -> constr list option