From 35ff578d093b3616af1280dd768e2afc96a8e09e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 3 Oct 2020 16:34:37 +0200
Subject: Deduce Stack.decomp from Stack.strip_n_app.

---
 pretyping/evarconv.ml      | 19 +++++++++----------
 pretyping/reductionops.ml  | 16 ++++++++++------
 pretyping/reductionops.mli |  4 ++++
 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
 
-- 
cgit v1.2.3


From a20d7312897cc9b4f580b68d1d6cefdfd0c5ead3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 3 Oct 2020 16:40:57 +0200
Subject: Unification: documenting eta for pi-types and record types.

We also align their type on (more) standard invariants.
---
 pretyping/evarconv.ml | 26 ++++++++++++++------------
 1 file changed, 14 insertions(+), 12 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4637017517..f02d96563b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -542,11 +542,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
       |None, Success i' -> switch (evar_conv_x flags env i' pbty) termF termO
       |_, (UnifFailure _ as x) -> x
       |Some _, _ -> UnifFailure (evd,NotSameArgSize) in
-  let eta env evd onleft sk term sk' term' =
-    assert (match sk with [] -> true | _ -> false);
+  let eta_lambda env evd onleft term (term',sk') =
+    (* Reduces an equation [env |- <(fun na:c1 => c'1)|empty> = <term'|sk'>] to
+       [env, na:c1 |- c'1 = sk'[term'] (with some additional reduction) *)
     let (na,c1,c'1) = destLambda evd term in
-    let c = nf_evar evd c1 in
-    let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
+    let env' = push_rel (RelDecl.LocalAssum (na,c1)) env in
     let out1 = whd_betaiota_deltazeta_for_iota_state
       flags.open_ts env' evd (c'1, Stack.empty) in
     let out2 = whd_nored_state env' evd
@@ -675,8 +675,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     let eta evd =
       match EConstr.kind evd termR with
       | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR ->
-         eta env evd false skR termR skF termF
-      | Construct u -> eta_constructor flags env evd skR u skF termF
+         eta_lambda env evd false termR apprF
+      | Construct u -> eta_constructor flags env evd u skR apprF
       | _ -> UnifFailure (evd,NotSameHead)
     in
     match Stack.list_of_app_stack skF with
@@ -762,7 +762,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
          else
            (* We could instead try Miller unification, then
               postpone to see if other equations help, as in:
-              [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *)
+              [Check fun a b c : unit => (eq_refl : _ a b = _ c a b)] *)
            UnifFailure (i,NotSameArgSize)
     | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.")
   in
@@ -974,10 +974,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
 
     (* Eta-expansion *)
     | Rigid, _ when isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 ->
-        eta env evd true sk1 term1 sk2 term2
+        eta_lambda env evd true term1 (term2,sk2)
 
     | _, Rigid when isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 ->
-        eta env evd false sk2 term2 sk1 term1
+        eta_lambda env evd false term2 (term1,sk1)
 
     | Rigid, Rigid -> begin
         match EConstr.kind evd term1, EConstr.kind evd term2 with
@@ -1031,10 +1031,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           else UnifFailure (evd,NotSameHead)
 
         | Construct u, _ ->
-          eta_constructor flags env evd sk1 u sk2 term2
+          eta_constructor flags env evd u sk1 (term2,sk2)
 
         | _, Construct u ->
-          eta_constructor flags env evd sk2 u sk1 term1
+          eta_constructor flags env evd u sk2 (term1,sk1)
 
         | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *)
           if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
@@ -1129,7 +1129,9 @@ and conv_record flags env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk
          (fst (decompose_app_vect i (substl ks h))))]
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
-and eta_constructor flags env evd sk1 ((ind, i), u) sk2 term2 =
+and eta_constructor flags env evd ((ind, i), u) sk1 (term2,sk2) =
+  (* reduces an equation <Construct(ind,i)|sk1> == <term2|sk2> to the
+     equations [arg_i = Proj_i (sk2[term2])] where [sk1] is [params args] *)
   let open Declarations in
   let mib = lookup_mind (fst ind) env in
     match get_projections env ind with
-- 
cgit v1.2.3


From 82fffac9b316f3ff31a5dd297e79f948b8749250 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 3 Oct 2020 16:42:40 +0200
Subject: Documenting module Reductionops.Stack.

Also includes minor layout or code changes.
---
 pretyping/reductionops.ml  | 32 ++++++++++++++++----------------
 pretyping/reductionops.mli | 33 ++++++++++++++++++++++++++++-----
 2 files changed, 44 insertions(+), 21 deletions(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2a5de7ba74..cf5d4de40c 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -215,13 +215,13 @@ end =
 struct
   open EConstr
   type 'a app_node = int * 'a array * int
-  (* first releavnt position, arguments, last relevant position *)
+  (* first relevant position, arguments, last relevant position *)
 
   (*
-     Invariant that this module must ensure :
-     (behare of direct access to app_node by the rest of Reductionops)
+     Invariant that this module must ensure:
+     (beware of direct access to app_node by the rest of Reductionops)
      - in app_node (i,_,j) i <= j
-     - There is no array realocation (outside of debug printing)
+     - There is no array reallocation (outside of debug printing)
    *)
 
   let pr_app_node pr (i,a,j) =
@@ -292,7 +292,7 @@ struct
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
       | (Primitive(_,_,a1,_)::s1, Primitive(_,_,a2,_)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
-      | ((Case _|Proj _|Fix _|Primitive _) :: _ | []) ,_ -> false in
+      | ((Case _ | Proj _ | Fix _ | Primitive _) :: _ | []) ,_ -> false in
     compare_rec 0 stk1 stk2
 
   exception IncompatibleFold2
@@ -333,26 +333,27 @@ struct
     append_app a s
 
   let rec args_size = function
-    | App (i,_,j)::s -> j + 1 - i + args_size s
-    | (Case _|Fix _|Proj _|Primitive _)::_ | [] -> 0
+    | App (i,_,j) :: s -> j + 1 - i + args_size s
+    | (Case _ | Fix _ | Proj _ | Primitive _) :: _ | [] -> 0
 
   let strip_app s =
     let rec aux out = function
       | ( App _ as e) :: s -> aux (e :: out) s
       | s -> List.rev out,s
     in aux [] s
+
   let strip_n_app n s =
     let rec aux n out = function
       | App (i,a,j) as e :: s ->
-         let nb = j  - i + 1 in
+         let nb = j - i + 1 in
          if n >= nb then
-           aux (n - nb) (e::out) s
+           aux (n - nb) (e :: out) s
          else
-           let p = i+n in
+           let p = i + n in
            Some (CList.rev
               (if Int.equal n 0 then out else App (i,a,p-1) :: out),
             a.(p),
-            if j > p then App(succ p,a,j)::s else s)
+            if j > p then App (succ p,a,j) :: s else s)
       | s -> None
     in aux n [] s
 
@@ -373,12 +374,11 @@ struct
         (Array.fold_right (fun x y -> x::y) a' args', s')
       | s -> ([],s) in
     let (out,s') = aux s in
-    let init = match s' with [] -> true | _ -> false in
-    Option.init init out
+    match s' with [] -> Some out | _ -> None
 
   let assign s p c =
     match strip_n_app p s with
-    | Some (pre,_,sk) -> pre @ (App (0,[|c|],0)::sk)
+    | Some (pre,_,sk) -> pre @ (App (0,[|c|],0) :: sk)
     | None -> assert false
 
   let tail n0 s0 =
@@ -386,12 +386,12 @@ struct
       if Int.equal n 0 then s else
         match s with
       | App (i,a,j) :: s ->
-         let nb = j  - i + 1 in
+         let nb = j - i + 1 in
          if n >= nb then
            aux (n - nb) s
          else
            let p = i+n in
-           if j >= p then App(p,a,j)::s else s
+           if j >= p then App (p,a,j) :: s else s
         | _ -> raise (Invalid_argument "Reductionops.Stack.tail")
     in aux n0 s0
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 7a840c5731..29b698f9d6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -69,8 +69,6 @@ module Stack : sig
 
   val empty : 'a t
   val is_empty : 'a t -> bool
-  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)
   [@@ocaml.deprecated "Use decomp_rev"]
@@ -85,26 +83,51 @@ module Stack : sig
   val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
     constr t -> constr t -> 'a
   val map : ('a -> 'a) -> 'a t -> 'a t
+
+  (** [append_app args sk] pushes array of arguments [args] on [sk] *)
+  val append_app : 'a array -> 'a t -> 'a t
+
+  (** [append_app_list args sk] pushes list of arguments [args] on [sk] *)
   val append_app_list : 'a list -> 'a t -> 'a t
 
-  (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not
-      start by App *)
+  (** if [strip_app sk] = [(sk1,sk2)], then [sk = sk1 @ sk2] with
+      [sk1] purely applicative and [sk2] does not start with an argument *)
   val strip_app : 'a t -> 'a t * 'a t
 
-  (** @return (the nth first elements, the (n+1)th element, the remaining stack)  *)
+  (** @return (the nth first elements, the (n+1)th element, the remaining stack)
+      if there enough of those *)
   val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
 
+  (** [decomp sk] extracts the first argument of [sk] is there is some *)
+  val decomp : '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
 
+  (** [not_purely_applicative sk] *)
   val not_purely_applicative : 'a t -> bool
+
+  (** [list_of_app_stack sk] either returns [Some sk] turned into a list of
+      arguments if [sk] is purely applicative and [None] otherwise *)
   val list_of_app_stack : constr t -> constr list option
 
+  (** [assign sk n a] changes the [n]th argument of [sk] with [a], counting from 0
+      @raise an anomaly if there is less that [n] arguments available *)
   val assign : 'a t -> int -> 'a -> 'a t
+
+  (** [args_size sk] returns the number of arguments available at the
+      head of [sk] *)
   val args_size : 'a t -> int
+
+  (** [tail n sk] drops the [n] first arguments of [sk]
+      @raise [Invalid_argument] if there are not enough arguments *)
   val tail : int -> 'a t -> 'a t
+
+  (** [nth sk n] returns the [n]-th argument of [sk], counting from 0
+      @raise [Not_found] if there is no [n]th argument *)
   val nth : 'a t -> int -> 'a
 
+  (** [zip sigma t sk] *)
   val zip : evar_map -> constr * constr t -> constr
 end
 
-- 
cgit v1.2.3


From e9da1fe4fe614f8fb34891c2580cfb5e94de50f9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 3 Oct 2020 16:45:20 +0200
Subject: Short documentation of solve_simple_eqn.

---
 pretyping/evarsolve.mli | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 094dae4828..d347f46637 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -136,6 +136,24 @@ val solve_evar_evar : ?force:bool ->
   (** The two evars are expected to be in inferably convertible types;
       if not, an exception IllTypedInstance is raised *)
 
+(* [solve_simple_eqn unifier flags env evd (direction,?ev[inst],t)]
+   makes progresses on problems of the form [?ev[inst] := t] (or
+   [?ev[inst] :<= t], or [?ev[inst] :>= t]). It uses imitation and a
+   limited form of projection. At the time of writing this comment,
+   only rels/vars (possibly indirectly via a chain of evars) and
+   constructors are used for projection. For instance
+   [?e[x,S 0] := x + S 0] will be solved by imitating [+] and
+   projecting [x] and [S 0] (so that [?e[a,b]:=a+b]) but in
+   [?e[0+0] := 0+0], the possible imitation will not be seen.
+
+   [choose] tells to make an irreversible choice when two valid
+   projections are competing. It is to be used when no more reversible
+   progress can be done. It is [false] by default.
+
+   [imitate_defs] tells to expand local definitions if they cannot be
+   projected. It is [true] by default.
+*)
+
 val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env ->  evar_map ->
   bool option * existential * constr -> unification_result
 
-- 
cgit v1.2.3


From dc5a992e226b74b59d7a246c761576f098395f99 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 7 Apr 2016 00:31:39 +0200
Subject: Some partial documentation of evar_conv_x.

---
 pretyping/evarconv.ml | 119 +++++++++++++++++++++++++++++++++++---------------
 1 file changed, 83 insertions(+), 36 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f02d96563b..f2bae2cf09 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -127,9 +127,10 @@ let flex_kind_of_term flags env evd c sk =
        else Rigid
     | Evar ev ->
        if is_evar_allowed flags (fst ev) then Flexible ev else Rigid
-    | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Rigid
+    | Lambda _ | Prod _ | Sort _ | Ind _ | Int _ | Float _ | Array _ -> Rigid
+    | Construct _ | CoFix _ (* Incorrect: should check only app in sk *) -> Rigid
     | Meta _ -> Rigid
-    | Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
+    | Fix _ -> Rigid (* happens when the fixpoint is partially applied (should check it?) *)
     | Cast _ | App _ | Case _ -> assert false
 
 let apprec_nohdbeta flags env evd c =
@@ -368,12 +369,23 @@ let rec ise_app_rev_stack2 env f evd sk1 sk2 =
 (* This function tries to unify 2 stacks element by element. It works
    from the end to the beginning. If it unifies a non empty suffix of
    stacks but not the entire stacks, the first part of the answer is
-   Some(the remaining prefixes to tackle)) *)
+   Some(the remaining prefixes to tackle)
+   If [no_app] is set, situations like [match head u1 u2 with ... end]
+   will not try to match [u1] and [u2] (why?); but situations like
+   [match head u1 u2 with ... end v] will try to match [v] (??) *)
+(* Input: E1[] =? E2[] where the E1, E2 are concatenations of
+     n-ary-app/case/fix/proj elimination rules
+   Output:
+   - either None if E1 = E2 is solved,
+   - or Some (E1'',E2'') such that there is a decomposition of
+     E1[] = E1'[E1''[]] and E2[] = E2'[E2''[]] s.t.  E1' = E2' and
+     E1'' cannot be unified with E2''
+   - UnifFailure if no such non-empty E1' = E2' exists *)
 let ise_stack2 no_app env evd f sk1 sk2 =
-  let rec ise_stack2 deep i sk1 sk2 =
-    let fail x = if deep then Some (List.rev sk1, List.rev sk2), Success i
+  let rec ise_stack2 deep i revsk1 revsk2 =
+    let fail x = if deep then Some (List.rev revsk1, List.rev revsk2), Success i
       else None, x in
-    match sk1, sk2 with
+    match revsk1, revsk2 with
     | [], [] -> None, Success i
     | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
       (match f env i CONV t1 t2 with
@@ -398,7 +410,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_rev_stack2 env f i sk1 sk2 with
+         begin match ise_app_rev_stack2 env f i revsk1 revsk2 with
                |_,(UnifFailure _ as x) -> fail x
                |(l1, l2), Success i' -> ise_stack2 true i' l1 l2
          end
@@ -407,8 +419,8 @@ let ise_stack2 no_app env evd f sk1 sk2 =
 
 (* Make sure that the matching suffix is the all stack *)
 let exact_ise_stack2 env evd f sk1 sk2 =
-  let rec ise_stack2 i sk1 sk2 =
-    match sk1, sk2 with
+  let rec ise_stack2 i revsk1 revsk2 =
+    match revsk1, revsk2 with
     | [], [] -> Success i
     | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
       ise_and i [
@@ -429,7 +441,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_rev_stack2 env f i sk1 sk2 with
+         begin match ise_app_rev_stack2 env f i revsk1 revsk2 with
                |_,(UnifFailure _ as x) -> x
                |(l1, l2), Success i' -> ise_stack2 i' l1 l2
          end
@@ -522,26 +534,30 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
   let quick_fail i = (* not costly, loses info *)
     UnifFailure (i, NotSameHead)
   in
-  let miller_pfenning on_left fallback ev lF tM evd =
+  let miller_pfenning l2r fallback ev lF tM evd =
     match is_unification_pattern_evar env evd ev lF tM with
       | None -> fallback ()
       | Some l1' -> (* Miller-Pfenning's patterns unification *)
         let t2 = tM in
         let t2 = solve_pattern_eqn env evd l1' t2 in
           solve_simple_eqn (conv_fun evar_conv_x) flags env evd
-            (position_problem on_left pbty,ev,t2)
+            (position_problem l2r pbty,ev,t2)
   in
-  let consume_stack on_left (termF,skF) (termO,skO) evd =
-    let switch f a b = if on_left then f a b else f b a in
+  let consume_stack l2r (termF,skF) (termO,skO) evd =
+    let switch f a b = if l2r then f a b else f b a in
     let not_only_app = Stack.not_purely_applicative skO in
     match switch (ise_stack2 not_only_app env evd (evar_conv_x flags)) skF skO with
-      |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) ->
+    | Some (l,r), Success i' when l2r && (not_only_app || List.is_empty l) ->
+        (* E[?n]=E'[redex] reduces to either l[?n]=r[redex] with
+           case/fix/proj in E' (why?) or ?n=r[redex] *)
         switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r))
-      |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) ->
+    | Some (r,l), Success i' when not l2r && (not_only_app || List.is_empty l) ->
+        (* E'[redex]=E[?n] reduces to either r[redex]=l[?n] with
+           case/fix/proj in E' (why?) or r[redex]=?n *)
         switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r))
-      |None, Success i' -> switch (evar_conv_x flags env i' pbty) termF termO
-      |_, (UnifFailure _ as x) -> x
-      |Some _, _ -> UnifFailure (evd,NotSameArgSize) in
+    | None, Success i' -> switch (evar_conv_x flags env i' pbty) termF termO
+    | _, (UnifFailure _ as x) -> x
+    | Some _, _ -> UnifFailure (evd,NotSameArgSize) in
   let eta_lambda env evd onleft term (term',sk') =
     (* Reduces an equation [env |- <(fun na:c1 => c'1)|empty> = <term'|sk'>] to
        [env, na:c1 |- c'1 = sk'[term'] (with some additional reduction) *)
@@ -615,32 +631,39 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                 with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
                  (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')]
   in
-  let consume on_left (_, skF as apprF) (_,skM as apprM) i =
+  let consume l2r (_, skF as apprF) (_,skM as apprM) i =
     if not (Stack.is_empty skF && Stack.is_empty skM) then
-      consume_stack on_left apprF apprM i
+      consume_stack l2r apprF apprM i
     else quick_fail i
   in
-  let miller on_left ev (termF,skF as apprF) (termM, skM as apprM) i =
-    let switch f a b = if on_left then f a b else f b a in
+  let miller l2r ev (termF,skF as apprF) (termM, skM as apprM) i =
+    let switch f a b = if l2r then f a b else f b a in
     let not_only_app = Stack.not_purely_applicative skM in
       match Stack.list_of_app_stack skF with
       | None -> quick_fail evd
       | Some lF ->
         let tM = Stack.zip evd apprM in
-          miller_pfenning on_left
+          miller_pfenning l2r
             (fun () -> if not_only_app then (* Postpone the use of an heuristic *)
               switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM
             else quick_fail i)
             ev lF tM i
   in
-  let flex_maybeflex on_left ev (termF,skF as apprF) (termM, skM as apprM) vM =
-    let switch f a b = if on_left then f a b else f b a in
+  let flex_maybeflex l2r ev (termF,skF as apprF) (termM, skM as apprM) vM =
+    (* Problem: E[?n[inst]] = E'[redex]
+       Strategy, as far as I understand:
+       1.  if E[]=[]u1..un and ?n[inst] u1..un = E'[redex] is a Miller pattern: solve it now
+       2a. if E'=E'1[E'2] and E=E'1 unifiable, recursively solve ?n[inst] = E'2[redex]
+       2b. if E'=E'1[E'2] and E=E1[E2] and E=E'1 unifiable and E' contient app/fix/proj,
+           recursively solve E2[?n[inst]] = E'2[redex]
+       3.  reduce the redex into M and recursively solve E[?n[inst]] =? E'[M] *)
+    let switch f a b = if l2r then f a b else f b a in
     let delta i =
       switch (evar_eqappr_x flags env i pbty) apprF
         (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (vM,skM))
     in
-    let default i = ise_try i [miller on_left ev apprF apprM;
-                               consume on_left apprF apprM;
+    let default i = ise_try i [miller l2r ev apprF apprM;
+                               consume l2r apprF apprM;
                                delta]
     in
       match EConstr.kind evd termM with
@@ -661,8 +684,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                   let delta' i =
                     switch (evar_eqappr_x flags env i pbty) apprF apprM'
                   in
-                  fun i -> ise_try i [miller on_left ev apprF apprM';
-                                   consume on_left apprF apprM'; delta']
+                  fun i -> ise_try i [miller l2r ev apprF apprM';
+                                   consume l2r apprF apprM'; delta']
                 with Retyping.RetypeError _ ->
                 (* Happens thanks to w_unify building ill-typed terms *)
                   default
@@ -670,8 +693,19 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           end
       | _ -> default evd
   in
-  let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) =
-    let switch f a b = if on_left then f a b else f b a in
+  let flex_rigid l2r ev (termF, skF as apprF) (termR, skR as apprR) =
+    (* Problem: E[?n[inst]] = E'[M] with M blocking computation (in theory)
+       Strategy, as far as I understand:
+       1.  if E[]=[]u1..un and ?n[inst] u1..un = E'[M] is a Miller pattern: solve it now
+       2a. if E'=E'1[E'2] and E=E'1 unifiable and E' contient app/fix/proj,
+           recursively solve ?n[inst] = E'2[M]
+       2b. if E'=E'1[E'2] and E=E1[E2] and E=E'1 unifiable and E' contient app/fix/proj,
+           recursively solve E2[?n[inst]] = E'2[M]
+       3a. if M a lambda or a constructor: eta-expand and recursively solve
+       3b. if M a constructor C ..ui..: eta-expand and recursively solve proji[E[?n[inst]]]=ui
+       4.  fail if E purely applicative and ?n occurs rigidly in E'[M]
+       5.  absorb arguments if purely applicative and postpone *)
+    let switch f a b = if l2r then f a b else f b a in
     let eta evd =
       match EConstr.kind evd termR with
       | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR ->
@@ -681,10 +715,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     in
     match Stack.list_of_app_stack skF with
     | None ->
-        ise_try evd [consume_stack on_left apprF apprR; eta]
+        ise_try evd [consume_stack l2r apprF apprR; eta]
     | Some lF ->
         let tR = Stack.zip evd apprR in
-          miller_pfenning on_left
+          miller_pfenning l2r
             (fun () ->
               ise_try evd
                 [eta;(* Postpone the use of an heuristic *)
@@ -714,6 +748,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
          solve_simple_eqn (conv_fun evar_conv_x) flags env i'
                           (position_problem true pbty,destEvar i' ev1',term2)
        else
+         (* HH: Why not to drop sk1 and sk2 since they unified *)
          evar_eqappr_x flags env evd pbty
                        (ev1', sk1) (term2, sk2)
     | Some (r,[]), Success i' ->
@@ -734,7 +769,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
        if isEvar i' ev1' then
          solve_simple_eqn (conv_fun evar_conv_x) flags env i'
                           (position_problem true pbty,destEvar i' ev1',Stack.zip i' (term2,r))
-       else evar_eqappr_x flags env evd pbty
+       else
+         (* HH: Why not to drop sk1 and sk2 since they unified *)
+         evar_eqappr_x flags env evd pbty
                           (ev1', sk1) (term2, sk2)
     | None, (UnifFailure _ as x) ->
        (* sk1 and sk2 have no common outer part *)
@@ -774,7 +811,17 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
   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) ->
-        (* sk1[?ev1] =? sk2[?ev2] *)
+      (* Notations:
+         - "sk" is a stack (or, more abstractly, an evaluation context, written E)
+         - "ev" is an evar "?ev", more precisely an evar ?n with an instance inst
+         - "al" is an evar instance
+         Problem: E₁[?n₁[inst₁]] = E₂[?n₂[inst₂]] (i.e. sk1[?ev1] =? sk2[?ev2]
+         Strategy is first-order unification
+           1a. if E₁=E₂ unifiable, solve ?n₁[inst₁] = ?n₂[inst₂]
+           1b. if E₂=E₂'[E₂''] and E₁=E₂' unifiable, recursively solve ?n₁[inst₁] = E₂''[?n₂[inst₂]]
+           1b'. if E₁=E₁'[E₁''] and E₁'=E₂ unifiable, recursively solve E₁''[?n₁[inst₁]] = ?n₂[inst₂]
+             recursively solve E2[?n[inst]] = E'2[redex]
+           2. fails if neither E₁ nor E₂ is a prefix of the other *)
         let f1 i = first_order env i term1 term2 sk1 sk2
         and f2 i =
           if Evar.equal sp1 sp2 then
-- 
cgit v1.2.3


From 3e78772edb175bf0473acb70136c640365678594 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 3 Oct 2020 18:55:12 +0200
Subject: Unification: renamings in ise_stack2 to get a more explicit idea of
 its semantic.

---
 pretyping/evarconv.ml | 60 ++++++++++++++++++++++++---------------------------
 1 file changed, 28 insertions(+), 32 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f2bae2cf09..b770ae53bd 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -329,12 +329,6 @@ let ise_and evd l =
         | UnifFailure _ as x -> x in
   ise_and evd l
 
-let ise_exact ise x1 x2 =
-  match ise x1 x2 with
-  | None, out -> out
-  | _, (UnifFailure _ as out) -> out
-  | Some _, Success i -> UnifFailure (i,NotSameArgSize)
-
 let ise_array2 evd f v1 v2 =
   let rec allrec i = function
     | -1 -> Success i
@@ -356,15 +350,15 @@ 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_rev_stack2 env f evd sk1 sk2 =
-  match Stack.decomp_rev sk1, Stack.decomp_rev sk2 with
-  | Some (t1,l1), Some (t2,l2) ->
+let rec ise_app_rev_stack2 env f evd revsk1 revsk2 =
+  match Stack.decomp_rev revsk1, Stack.decomp_rev revsk2 with
+  | Some (t1,revsk1), Some (t2,revsk2) ->
      begin
-       match ise_app_rev_stack2 env f evd l1 l2 with
+       match ise_app_rev_stack2 env f evd revsk1 revsk2 with
        | (_, UnifFailure _) as x -> x
        | x, Success i' -> x, f env i' CONV t1 t2
      end
-  | _, _ -> (sk1,sk2), Success evd
+  | _, _ -> (revsk1,revsk2), Success evd
 
 (* This function tries to unify 2 stacks element by element. It works
    from the end to the beginning. If it unifies a non empty suffix of
@@ -381,22 +375,24 @@ let rec ise_app_rev_stack2 env f evd sk1 sk2 =
      E1[] = E1'[E1''[]] and E2[] = E2'[E2''[]] s.t.  E1' = E2' and
      E1'' cannot be unified with E2''
    - UnifFailure if no such non-empty E1' = E2' exists *)
-let ise_stack2 no_app env evd f sk1 sk2 =
-  let rec ise_stack2 deep i revsk1 revsk2 =
+let rec ise_stack2 no_app env evd f sk1 sk2 =
+  let rec ise_rev_stack2 deep i revsk1 revsk2 =
     let fail x = if deep then Some (List.rev revsk1, List.rev revsk2), Success i
       else None, x in
     match revsk1, revsk2 with
     | [], [] -> None, Success i
     | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
-      (match f env i CONV t1 t2 with
-      | Success i' ->
-        (match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with
-        | Success i'' -> ise_stack2 true i'' q1 q2
-        | UnifFailure _ as x -> fail x)
-      | UnifFailure _ as x -> fail x)
+      begin
+        match ise_and i [
+          (fun i -> f env i CONV t1 t2);
+          (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2)]
+        with
+        | Success i' -> ise_rev_stack2 true i' q1 q2
+        | UnifFailure _ as x -> fail x
+      end
     | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 ->
        if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2)
-       then ise_stack2 true i q1 q2
+       then ise_rev_stack2 true i q1 q2
        else fail (UnifFailure (i, NotSameHead))
     | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1,
       Stack.Fix (((li2, i2),(_,tys2,bds2)),a2)::q2 ->
@@ -404,51 +400,51 @@ let ise_stack2 no_app env evd f sk1 sk2 =
         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 -> ise_exact (ise_stack2 false i) a1 a2)] with
-        | Success i' -> ise_stack2 true i' q1 q2
+          (fun i -> snd (ise_stack2 no_app env i f a1 a2))] with
+        | Success i' -> ise_rev_stack2 true i' q1 q2
         | UnifFailure _ as x -> fail x
       else fail (UnifFailure (i,NotSameHead))
     | Stack.App _ :: _, Stack.App _ :: _ ->
        if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else
          begin match ise_app_rev_stack2 env f i revsk1 revsk2 with
                |_,(UnifFailure _ as x) -> fail x
-               |(l1, l2), Success i' -> ise_stack2 true i' l1 l2
+               |(l1, l2), Success i' -> ise_rev_stack2 true i' l1 l2
          end
     |_, _ -> fail (UnifFailure (i,(* Maybe improve: *) NotSameHead))
-  in ise_stack2 false evd (List.rev sk1) (List.rev sk2)
+  in ise_rev_stack2 false evd (List.rev sk1) (List.rev sk2)
 
 (* Make sure that the matching suffix is the all stack *)
-let exact_ise_stack2 env evd f sk1 sk2 =
-  let rec ise_stack2 i revsk1 revsk2 =
+let rec exact_ise_stack2 env evd f sk1 sk2 =
+  let rec ise_rev_stack2 i revsk1 revsk2 =
     match revsk1, revsk2 with
     | [], [] -> Success i
     | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
       ise_and i [
-      (fun i -> ise_stack2 i q1 q2);
+      (fun i -> ise_rev_stack2 i q1 q2);
       (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2);
       (fun i -> f env i CONV t1 t2)]
     | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1,
       Stack.Fix (((li2, i2),(_,tys2,bds2)),a2)::q2 ->
       if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
         ise_and i [
-          (fun i -> ise_stack2 i q1 q2);
+          (fun i -> ise_rev_stack2 i q1 q2);
           (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 -> ise_stack2 i a1 a2)]
+          (fun i -> exact_ise_stack2 env i f a1 a2)]
       else UnifFailure (i,NotSameHead)
     | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 ->
        if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2)
-       then ise_stack2 i q1 q2
+       then ise_rev_stack2 i q1 q2
        else (UnifFailure (i, NotSameHead))
     | Stack.App _ :: _, Stack.App _ :: _ ->
          begin match ise_app_rev_stack2 env f i revsk1 revsk2 with
                |_,(UnifFailure _ as x) -> x
-               |(l1, l2), Success i' -> ise_stack2 i' l1 l2
+               |(l1, l2), Success i' -> ise_rev_stack2 i' l1 l2
          end
     |_, _ -> UnifFailure (i,(* Maybe improve: *) NotSameHead)
   in
   if Reductionops.Stack.compare_shape sk1 sk2 then
-    ise_stack2 evd (List.rev sk1) (List.rev sk2)
+    ise_rev_stack2 evd (List.rev sk1) (List.rev sk2)
   else UnifFailure (evd, (* Dummy *) NotSameHead)
 
 (* Add equality constraints for covariant/invariant positions. For
-- 
cgit v1.2.3


From c213d571f7628078c087b845d0142e2e88aac9d6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Oct 2020 16:27:41 +0200
Subject: More documentation about the situation ?ev := C[?ev'] in
 solve_simple_eqn.

---
 pretyping/evarsolve.ml | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 44414aa6a0..f9f6f74a66 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1585,7 +1585,16 @@ let rec invert_definition unify flags choose imitate_defs
         imitate envk (subst1 b c)
     | Evar (evk',args' as ev') ->
         if Evar.equal evk evk' then raise (OccurCheckIn (evd,rhs));
-        (* Evar/Evar problem (but left evar is virtual) *)
+        (* At this point, we imitated a context say, C[ ], and virtually
+           instantiated ?evk@{x₁..xn} with C[?evk''@{x₁..xn,y₁..yk}]
+           for y₁..yk the spine of variables of C[ ], now facing the
+           equation env, y₁...yk |- ?evk'@{args'} =?= ?evk''@{args,y1:=y1..yk:=yk} *)
+        (* Assume evk' is defined in context x₁'..xk'.
+           As a first step, we try to find a restriction ?evk'''@{xᵢ₁'..xᵢⱼ} of
+           ?evk' and an instance args''' in the environment of ?evk such that
+           env, y₁..yk |- args'''[args] = args' and thus such that
+           env, y₁..yk |- ?evk'''@{args'''[args]} = ?evk''@{args,y1:=y1..yk:=yk} *)
+        (* Note that we don't need to declare ?evk'' yet: it may remain virtual *)
         let aliases = lift_aliases k aliases in
         (try
           let ev = (evk,List.map (lift k) argsv) in
@@ -1597,14 +1606,14 @@ let rec invert_definition unify flags choose imitate_defs
         | CannotProject (evd,ev') ->
           if not !progress then
             raise (NotEnoughInformationEvarEvar t);
-          (* Make the virtual left evar real *)
+          (* We could not invert args' in terms of args, so we now make ?evk'' real *)
           let ty = get_type_of env' evd t in
           let (evd,evar'',ev'') =
              materialize_evar (evar_define unify flags ~choose) env' evd k ev ty in
           (* materialize_evar may instantiate ev' by another evar; adjust it *)
           let (evk',args' as ev') = normalize_evar evd ev' in
           let evd =
-             (* Try to project (a restriction of) the left evar ... *)
+             (* Try now to invert args in terms of args' *)
             try
               let evd,body = project_evar_on_evar false unify flags env' evd aliases 0 None ev'' ev' in
               let evd = Evd.define evk' body evd in
-- 
cgit v1.2.3