Reductionops.Stack.app_node is secret

4 files changed, 56 insertions, 37 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 899b64984e..43e8a11dfe 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -97,7 +97,7 @@ let check_conv_record (t1,sk1) (t2,sk2) =
 	match kind_of_term t2 with
 	    Prod (_,a,b) -> (* assert (l2=[]); *)
       	      if dependent (mkRel 1) b then raise Not_found
-	      else lookup_canonical_conversion (proji, Prod_cs),[Stack.App [a;pop b]]
+	      else lookup_canonical_conversion (proji, Prod_cs),(Stack.append_app_list [a;pop b] Stack.empty)
 	  | Sort s ->
 	      lookup_canonical_conversion
 		(proji, Sort_cs (family_of_sort s)),[]
@@ -156,22 +156,18 @@ let ise_exact ise x1 x2 =
   | _, (UnifFailure _ as out) -> out
   | Some _, Success i -> UnifFailure (i,NotSameArgSize)
 
-let generic_ise_list2 i f l1 l2 =
+let ise_list2 i f l1 l2 =
   let rec aux i l1 l2 =
     match l1,l2 with
-    | [], [] -> (None, Success i)
-    | l, [] -> (Some (Inl (List.rev l)), Success i)
-    | [], l -> (Some (Inr (List.rev l)), Success i)
+    | [], [] -> Success i
+    | l, [] -> UnifFailure (i,NotSameArgSize)
+    | [], l -> UnifFailure (i,NotSameArgSize)
     | x::l1, y::l2 ->
         (match aux i l1 l2 with
-        | aa, Success i' -> (aa, f i' x y)
-        | _, (UnifFailure _ as x) -> None, x)
+        | Success i' -> f i' x y
+        | (UnifFailure _ as x) -> x)
   in aux i (List.rev l1) (List.rev l2)
 
-(* Same but the 2 lists must have the same length *)
-let ise_list2 evd f l1 l2 =
-  ise_exact (generic_ise_list2 evd f) l1 l2
-
 let ise_array2 evd f v1 v2 =
   let rec allrec i = function
     | -1 -> Success i
@@ -183,6 +179,19 @@ let ise_array2 evd f v1 v2 =
   if Int.equal lv1 (Array.length v2) then allrec evd (pred lv1)
   else UnifFailure (evd,NotSameArgSize)
 
+(* 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
+     end
+  | _, _ -> (sk1,sk2), 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
    stacks but not the entire stacks, the first part of the answer is
@@ -212,19 +221,12 @@ let ise_stack2 no_app env evd f sk1 sk2 =
       else fail (UnifFailure (i,NotSameHead))
     | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _
     | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false
-    | Stack.App l1 :: q1, Stack.App l2 :: q2 ->
-      if no_app&&deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else begin
-      (* Is requiring to match on all the shorter list a restriction
-	 here ? we could imagine a generalization of
-	 generic_ise_list2 that succeed when it matches only a strict
-	 non empty suffix of both lists and returns in this case the 2
-	 prefixes *)
-      match generic_ise_list2 i (fun ii -> f env ii CONV) l1 l2 with
-      |_,(UnifFailure _ as x) -> fail x
-      |None,Success i' -> ise_stack2 true i' q1 q2
-      |Some (Inl r),Success i' -> ise_stack2 true i' (Stack.App r :: q1) q2
-      |Some (Inr r),Success i' -> ise_stack2 true i' q1 (Stack.App r :: q2)
-    end
+    | 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
+	       |_,(UnifFailure _ as x) -> fail x
+	       |(l1, l2), Success i' -> ise_stack2 true i' l1 l2
+	 end
     |_, _ -> fail (UnifFailure (i,(* Maybe improve: *) NotSameHead))
   in ise_stack2 false evd (List.rev sk1) (List.rev sk2)
 
@@ -316,7 +318,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let out1 = whd_betaiota_deltazeta_for_iota_state
       ts env' evd Cst_stack.empty (c'1, Stack.empty) in
     let out2 = whd_nored_state evd
-      (Stack.zip (term', sk' @ [Stack.Shift 1]), [Stack.App [mkRel 1]]), Cst_stack.empty in
+      (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app_list [mkRel 1] Stack.empty), Cst_stack.empty in
     if onleft then evar_eqappr_x ts env' evd CONV out1 out2
     else evar_eqappr_x ts env' evd CONV out2 out1
   in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a9ab641909..afd48bd0b5 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -29,12 +29,18 @@ exception Elimconst
 
 (** The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
 module Stack = struct
+  type 'a app_node = 'a list
+  (*
+     Invariant that this module must ensure :
+     (behare of direct access to app_node by the rest of Reductionops)
+     - app_node list is never empty
+   *)
   let pr_app_node pr node =
     let open Pp in surround (prlist_with_sep pr_comma pr node)
 
   type 'a member =
-  | App of 'a list
-  | Case of case_info * 'a * 'a array * ('a * 'a list) option
+  | App of 'a app_node
+  | Case of Term.case_info * 'a * 'a array * ('a * 'a list) option
   | Fix of fixpoint * 'a t * ('a * 'a list) option
   | Shift of int
   | Update of 'a
@@ -130,6 +136,12 @@ module Stack = struct
     | App(v::l)::s -> Some (v, (App l :: s))
     | App [] :: s -> decomp s
     | _ -> None
+
+  let decomp_node_last node sk =
+    match List.sep_last node with
+    | v, [] -> (v, sk)
+    | v, l -> (v, App l :: sk)
+
   let rec strip_app = function
     | App args :: s -> let (args',s') = strip_app s in args @ args', s'
     | s -> [],s
@@ -478,7 +490,7 @@ let rec whd_state_gen ?csts refold flags env sigma =
       (match Stack.strip_n_app ri.(n) stack with
       |None -> fold ()
       |Some (bef,arg,s') ->
-	whrec noth (arg, Stack.Fix(f,[Stack.App bef],Cst_stack.best_cst cst_l)::s'))
+	whrec noth (arg, Stack.Fix(f,Stack.append_app_list bef Stack.empty,Cst_stack.best_cst cst_l)::s'))
 
     | Construct (ind,c) ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
@@ -541,7 +553,7 @@ let local_whd_state_gen flags sigma =
     | Fix ((ri,n),_ as f) ->
       (match Stack.strip_n_app ri.(n) stack with
       |None -> s
-      |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,[Stack.App bef],None)::s'))
+      |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,Stack.append_app_list bef Stack.empty,None)::s'))
 
     | Evar ev ->
       (match safe_evar_value sigma ev with
@@ -1049,7 +1061,7 @@ let whd_programs_stack env sigma =
       | Fix ((ri,n),_ as f) ->
 	(match Stack.strip_n_app ri.(n) stack with
 	  |None -> s
-	  |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,[Stack.App bef],None)::s'))
+	  |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,Stack.append_app_list bef Stack.empty,None)::s'))
       | Construct (ind,c) -> begin
 	match Stack.strip_app stack with
 	  |args, (Stack.Case(ci, _, lf,_)::s') ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 6c5d9e485e..52ee728eaf 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -19,10 +19,12 @@ open Closure
 exception Elimconst
 
 module Stack : sig
-  (** 90% copy-paste of kernel/closure.ml but polymorphic and with extra
-      arguments for storing refold *)
+  type 'a app_node
+
+  val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds
+
   type 'a member =
-  | App of 'a list
+  | App of 'a app_node
   | Case of case_info * 'a * 'a array * ('a * 'a list) option
   | Fix of fixpoint * 'a t * ('a * 'a list) option
   | Shift of int
@@ -32,15 +34,18 @@ module Stack : sig
   val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
 
   val empty : 'a t
+  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 compare_shape : 'a t -> 'a t -> bool
   (** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)].
       @return the result and the lifts to apply on the terms *)
   val fold2 : ('a -> Term.constr -> Term.constr -> 'a) -> 'a ->
     Term.constr t -> Term.constr t -> 'a * int * int
-  val append_app : 'a array -> 'a t -> 'a t
   val append_app_list : 'a list -> 'a t -> 'a t
 
-  val decomp : 'a t -> ('a * 'a t) option
   val strip_app : 'a t -> 'a list * 'a t
   (** Takes the n first arguments of application put on the stack. Fails is the
       stack does not start by n arguments of application. *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 456693a968..e252f0a7ef 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -425,7 +425,7 @@ let substl_checking_arity env subst sigma c =
 type fix_reduction_result = NotReducible | Reduced of (constr*constr list)
 
 let reduce_fix whdfun sigma fix stack =
-  match fix_recarg fix [Stack.App stack] with
+  match fix_recarg fix (Stack.append_app_list stack Stack.empty) with
     | None -> NotReducible
     | Some (recargnum,recarg) ->
         let (recarg'hd,_ as recarg') = whdfun sigma recarg in
@@ -442,7 +442,7 @@ let contract_fix_use_function env sigma f
   substl_checking_arity env (List.rev lbodies) sigma (nf_beta sigma bodies.(bodynum))
 
 let reduce_fix_use_function env sigma f whfun fix stack =
-  match fix_recarg fix [Stack.App stack] with
+  match fix_recarg fix (Stack.append_app_list stack Stack.empty) with
     | None -> NotReducible
     | Some (recargnum,recarg) ->
         let (recarg'hd,_ as recarg') =