optimize non-applicative stack nodes

When unifying terms that both have a Case, Fix or Proj node in their arguments stack, unify and remove the longest suffix of the stack containing applicative nodes or the last nodes if none exists.

Author: Tragicus

pretyping/evarconv.ml

@@ -609,6 +609,56 @@ let rec exact_ise_stack2 env evd f sk1 sk2 =
     ise_rev_stack2 evd (List.rev sk1) (List.rev sk2)
   else UnifFailure (evd, (* Dummy *) NotSameHead)
 
+(* Removes the last group of applicative stack nodes or one node if the last node is not applicative. *)
+let ise_stack2_once env evd f sk1 sk2 =
+  let ise_rev_stack2 i revsk1 revsk2 =
+    let stop app revsk1 revsk2 i = Some (app, List.rev revsk1, List.rev revsk2, i) in
+    match revsk1, revsk2 with
+    | [], [] -> (* We want to see a non-applicative node*) None
+    | Stack.Case cse1 :: q1, Stack.Case cse2 :: q2 ->
+      let () = debug_unification (fun () -> Pp.(v 0 (str "ise_stack2_once : case" ++ cut ()))) in
+      let (ci1, u1, pms1, (t1,_), br1) = Stack.expand_case env evd cse1 in
+      let (ci2, u2, pms2, (t2,_), br2) = Stack.expand_case env evd cse2 in
+      let hd1 = mkIndU (ci1.ci_ind, u1) in
+      let hd2 = mkIndU (ci2.ci_ind, u2) in
+      let fctx i (ctx1, t1) (_ctx2, t2) = f (push_rel_context ctx1 env) i CONV t1 t2 in
+      begin match (ise_and i [
+          (fun i -> compare_heads CONV env i ~nargs:FullyApplied hd1 hd2);
+          (fun i -> ise_array2 i (fun ii -> f env ii CONV) pms1 pms2);
+          (fun i -> fctx i t1 t2);
+          (fun i -> ise_array2 i fctx br1 br2);
+        ]) with
+        | Success i -> stop false q1 q2 i
+        | _ -> None
+      end
+    | Stack.Proj (p1,_)::q1, Stack.Proj (p2,_)::q2 ->
+      let () = debug_unification (fun () -> Pp.(v 0 (str "ise_stack2_once : proj" ++ cut ()))) in
+       if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2)
+         then stop false q1 q2 i
+         else None
+    | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1,
+      Stack.Fix (((li2, i2),(_,tys2,bds2)),a2)::q2 ->
+      let () = debug_unification (fun () -> Pp.(v 0 (str "ise_stack2_once : fix" ++ cut ()))) in
+      if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
+        match ise_and i [
+          (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2);
+          (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2);
+          (fun i -> exact_ise_stack2 env i f a1 a2)] with
+          | Success i ->
+              let () = debug_unification (fun () -> Pp.(v 0 (str "ise_stack2_once : fix succeeds" ++ cut ()))) in
+              stop false q1 q2 i
+          | _ -> None
+        else None
+    | Stack.App a1 :: _, Stack.App a2 :: _ ->
+      let () = debug_unification (fun () -> Pp.(v 0 (str "ise_stack2_once : app: " ++ cut () ++ Stack.pr_app_node (Termops.Internal.print_constr_env env i) a1 ++ cut () ++ Stack.pr_app_node (Termops.Internal.print_constr_env env i) a2 ++ cut ()))) in
+       begin match ise_app_rev_stack2 env f i revsk1 revsk2 with
+       |_,(UnifFailure _) -> None
+       |(l1, l2), Success i' -> stop true l1 l2 i'
+       end
+    |_, _ -> None
+  in ise_rev_stack2 evd (List.rev sk1) (List.rev sk2)
+
+
 let compare_heads pbty env evd ~nargs term term' =
   compare_heads pbty env evd ~nargs:(NumArgs nargs) term term'
 
@@ -993,7 +1043,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
       match x with | Some x -> Inl x | _ -> Inr false
     with _ -> Inr false in
   let () = debug_unification (fun () -> Pp.(v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ()))) in
-  match (flex_kind_of_term flags env evd term1 sk1,
+  if (List.exists (function (Stack.Fix _ | Stack.Case _  | Stack.Proj _) -> true | _ -> false) sk1) && (List.exists (function (Stack.Fix _ | Stack.Case _  | Stack.Proj _) -> true | _ -> false) sk2) then
+    let () = debug_unification (fun () -> Pp.(v 0 (str "both sides have non applicative stacks" ++ cut ()))) in
+    match ise_stack2_once env evd (evar_conv_x flags) sk1 sk2 with
+    | None -> quick_fail evd
+    | Some (app, sk1, sk2, evd) ->
+        if app then
+          evar_eqappr_x flags env evd pbty keys None
+            (whd_betaiota_deltazeta_for_iota_state
+               flags.open_ts env evd (term1, sk1))
+            (whd_betaiota_deltazeta_for_iota_state
+               flags.open_ts env evd (term2, sk2))
+        else
+          evar_eqappr_x flags env evd pbty keys None (term1, sk1) (term2, sk2)
+  else match (flex_kind_of_term flags env evd term1 sk1,
          flex_kind_of_term flags env evd term2 sk2) with
     | Flexible (sp1,al1), Flexible (sp2,al2) ->
       (* Notations:
@@ -1154,7 +1217,6 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                       flags.open_ts env i (v2', applicative_stack)) in
           let rhs_is_already_stuck =
             rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
-
           let b = EConstr.isLambda i term1 || rhs_is_already_stuck
             && (not (Stack.not_purely_applicative sk1')) in
           ise_try i [