Reductionops.Stack.strip* are ready to deal with Shift

5 files changed, 99 insertions, 99 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 43e8a11df..c3453a385 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -90,20 +90,19 @@ let position_problem l2r = function
    projection would have been reduced) *)
 
 let check_conv_record (t1,sk1) (t2,sk2) =
-  try
     let proji = global_of_constr t1 in
     let canon_s,sk2_effective =
       try
 	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.append_app_list [a;pop b] Stack.empty)
-	  | Sort s ->
-	      lookup_canonical_conversion
-		(proji, Sort_cs (family_of_sort s)),[]
-	  | _ ->
-	      let c2 = global_of_constr t2 in
-		lookup_canonical_conversion (proji, Const_cs c2),sk2
+	  Prod (_,a,b) -> (* assert (l2=[]); *)
+      	  if dependent (mkRel 1) b then raise Not_found
+	  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)),[]
+	| _ ->
+	   let c2 = global_of_constr t2 in
+	   lookup_canonical_conversion (proji, Const_cs c2),sk2
       with Not_found ->
 	lookup_canonical_conversion (proji,Default_cs),[]
     in
@@ -111,16 +110,16 @@ let check_conv_record (t1,sk1) (t2,sk2) =
           o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in
     let params1, c1, extra_args1 =
       match Stack.strip_n_app nparams sk1 with
-	| Some (params1, c1,extra_args1) -> params1, c1, extra_args1
-	| _ -> raise Not_found in
+      | Some (params1, c1,extra_args1) -> params1, c1, extra_args1
+      | _ -> raise Not_found in
     let us2,extra_args2 =
-      let l',s' = Stack.strip_app sk2_effective in
-      let bef,aft = List.chop (List.length us) l' in
-      (bef, Stack.append_app_list aft s') in
-    c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1,
-    (n,Stack.zip(t2,sk2))
-  with Failure _ | Not_found ->
-    raise Not_found
+      let l_us = List.length us in
+      if Int.equal l_us 0 then Stack.empty,sk2_effective
+      else match (Stack.strip_n_app (l_us-1) sk2_effective) with
+	   | None -> raise Not_found
+	   | Some (l',el,s') -> (l'@Stack.append_app_list [el] Stack.empty,s') in
+    (c,bs,(Stack.append_app_list params Stack.empty,params1),(Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
+    (n,Stack.zip(t2,sk2)))
 
 (* Precondition: one of the terms of the pb is an uninstantiated evar,
  * possibly applied to arguments. *)
@@ -156,18 +155,6 @@ let ise_exact ise x1 x2 =
   | _, (UnifFailure _ as out) -> out
   | Some _, Success i -> UnifFailure (i,NotSameArgSize)
 
-let ise_list2 i f l1 l2 =
-  let rec aux i l1 l2 =
-    match l1,l2 with
-    | [], [] -> Success i
-    | l, [] -> UnifFailure (i,NotSameArgSize)
-    | [], l -> UnifFailure (i,NotSameArgSize)
-    | x::l1, y::l2 ->
-        (match aux i l1 l2 with
-        | Success i' -> f i' x y
-        | (UnifFailure _ as x) -> x)
-  in aux i (List.rev l1) (List.rev l2)
-
 let ise_array2 evd f v1 v2 =
   let rec allrec i = function
     | -1 -> Success i
@@ -403,7 +390,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
             match eval_flexible_term ts env term2 with
             | None -> false
             | Some v2 ->
-	      let applicative_stack = Stack.append_app_list (fst (Stack.strip_app sk2)) Stack.empty in
+	      let applicative_stack = fst (Stack.strip_app sk2) in
 	      is_unnamed
 		(fst (whd_betaiota_deltazeta_for_iota_state
 			ts env i Cst_stack.empty (v2, applicative_stack))) in
@@ -597,12 +584,12 @@ and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2))
     let app = mkApp (c, Array.rev_of_list ks) in
     ise_and evd'
       [(fun i ->
-	ise_list2 i
-          (fun i' x1 x -> evar_conv_x trs env i' CONV x1 (substl ks x))
+	exact_ise_stack2 env i
+          (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (substl ks x))
           params1 params);
        (fun i ->
-	 ise_list2 i
-           (fun i' u1 u -> evar_conv_x trs env i' CONV u1 (substl ks u))
+	 exact_ise_stack2 env i
+           (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (substl ks u))
            us2 us);
        (fun i -> evar_conv_x trs env i CONV c1 app);
        (fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1)]
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 65eae6560..89993189f 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -45,8 +45,8 @@ val check_problems_are_solved : evar_map -> unit
 (** Check if a canonical structure is applicable *)
 
 val check_conv_record : constr * types Stack.t -> constr * types Stack.t ->
-  constr * constr list * (constr list * constr list) *
-    (constr list * types list) *
+  constr * constr list * (constr Stack.t * constr Stack.t) *
+    (constr Stack.t * types Stack.t) *
     (constr Stack.t * types Stack.t) * constr *
     (int * constr)
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index afd48bd0b..a7fd54a73 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -142,30 +142,43 @@ module Stack = struct
     | 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
+  let strip_app s =
+    let rec aux out = function
+      | ( App _ | Shift _ as e) :: s -> aux (e :: out) s
+      | s -> List.rev out,s
+    in aux [] s
   let strip_n_app n s =
-    let apps,s' = strip_app s in
-    try
-      let bef,aft = List.chop n apps in
-      match aft with
-      |h::[] -> Some (bef,h,s')
-      |h::t -> Some (bef,h,append_app_list t s')
-      |[] -> None
-    with
-    |Failure _ -> None
-  let nfirsts_app n s =
-    let (args, _) = strip_app s in List.firstn n args
+    let rec aux n out = function
+      | Shift k as e :: s -> aux n (e :: out) s
+      | App args as e :: s ->
+	 let k = List.length args in
+	 if k < n then aux (n - k) (e::out) s else
+	   let bef,aft = List.chop n args in
+	   let pre = CList.rev
+		       (if CList.is_empty bef then out else App bef :: out) in
+	   begin
+             match aft with
+             |h::[] -> Some (pre,h,s)
+             |h::t -> Some (pre,h,append_app_list t s)
+             |[] -> None
+	   end
+      | s -> None
+    in aux n [] s
 
   let not_purely_applicative args =
     List.exists (function (Fix _ | Case _) -> true | _ -> false) args
   let list_of_app_stack s =
-    let (out,s') = strip_app s in
-    let init = match s' with [] -> true | _ -> false in
+    let rec aux = function
+      | App args :: s ->
+	 let (k,(args',s')) = aux s in
+	 let largs = CList.rev_map (Vars.lift k) args in
+	 k,(CList.rev_append largs args', s')
+      | Shift n :: s ->
+	 let (k,(args',s')) = aux s in (k+n,(args', s'))
+      | s -> (0,([],s)) in
+    let (lft,(out,s')) = aux s in
+    let init = match s' with [] when Int.equal lft 0 -> true | _ -> false in
     Option.init init out
-  let array_of_app_stack s =
-    Option.map Array.of_list (list_of_app_stack s)
 
   let rec assign s p c = match s with
     | App args :: s ->
@@ -177,14 +190,18 @@ module Stack = struct
           (bef, _::aft) -> App (bef@c::aft) :: s
         | _ -> assert false)
     | _ -> s
-  let rec tail p s =
-    if Int.equal p 0 then s else
-      match s with
-      | App args :: s ->
-	let q = List.length args in
-	if p >= q then tail (p-q) s
-	else App (List.skipn p args) :: s
-      | _ -> failwith "Reductionops.Stack.tail"
+  let tail p s0 =
+    let rec aux lft p s =
+      let out s = if Int.equal lft 0 then s else Shift lft :: s in
+      if Int.equal p 0 then out s else
+	match s with
+	| App args :: s' ->
+	   let q = List.length args in
+	   if p >= q then aux lft (p-q) s'
+	   else App (List.skipn p args) :: out s'
+	| Shift k :: s' -> aux (lft+k) p s'
+	| _ -> raise (Invalid_argument "Reductionops.Stack.tail")
+    in aux 0 p s0
   let rec nth s p = match s with
     | App args :: s ->
       let q = List.length args in
@@ -425,10 +442,9 @@ let rec whd_state_gen ?csts refold flags env sigma =
   let noth = [] in
   let rec whrec cst_l (x, stack as s) =
     let best_state def (cst,params,nb_skip) =
-      let apps,s' = Stack.strip_app stack in
       try
-	let _,aft = List.chop nb_skip apps in
-	(cst, Stack.append_app_list (List.rev params) (Stack.append_app_list aft s'))
+	let s' = Stack.tail nb_skip stack in
+	(cst, Stack.append_app_list (List.rev params) s')
       with Failure _ -> def in
     let fold () =
       if refold then (List.fold_left best_state s cst_l,noth) else (s,cst_l)
@@ -490,15 +506,15 @@ 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.append_app_list bef Stack.empty,Cst_stack.best_cst cst_l)::s'))
+	whrec noth (arg, Stack.Fix(f,bef,Cst_stack.best_cst cst_l)::s'))
 
     | Construct (ind,c) ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
 	|args, (Stack.Case(ci, _, lf,_)::s') ->
-	  whrec noth (lf.(c-1), Stack.append_app_list (List.skipn ci.ci_npar args) s')
+	  whrec noth (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
 	|args, (Stack.Fix (f,s',cst)::s'') ->
-	  let x' = applist(x,args) in
+	  let x' = Stack.zip(x,args) in
 	  whrec noth ((if refold then contract_fix ~env f else contract_fix f) cst,
 		      s' @ (Stack.append_app_list [x'] s''))
 	|_ -> fold ()
@@ -553,7 +569,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.append_app_list bef Stack.empty,None)::s'))
+      |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,bef,None)::s'))
 
     | Evar ev ->
       (match safe_evar_value sigma ev with
@@ -569,9 +585,9 @@ let local_whd_state_gen flags sigma =
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
 	|args, (Stack.Case(ci, _, lf,_)::s') ->
-	  whrec (lf.(c-1), Stack.append_app_list (List.skipn ci.ci_npar args) s')
+	  whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
 	|args, (Stack.Fix (f,s',cst)::s'') ->
-	  let x' = applist(x,args) in
+	  let x' = Stack.zip(x,args) in
 	  whrec (contract_fix f cst, s' @ (Stack.append_app_list [x'] s''))
 	|_ -> s
       else s
@@ -761,9 +777,9 @@ let whd_betaiota_preserving_vm_cast env sigma t =
        | Construct (ind,c) -> begin
 	 match Stack.strip_app stack with
 	   |args, (Stack.Case(ci, _, lf,_)::s') ->
-	     whrec (lf.(c-1), Stack.append_app_list (List.skipn ci.ci_npar args) s')
+	     whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
 	   |args, (Stack.Fix (f,s',cst)::s'') ->
-	     let x' = applist(x,args) in
+	     let x' = Stack.zip(x,args) in
 	     whrec (contract_fix f cst,s' @ (Stack.append_app_list [x'] s''))
 	   |_ -> s
        end
@@ -1017,14 +1033,12 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
     let (t, stack as s),csts' = whd_state_gen ~csts false betaiota env sigma s in
     match Stack.strip_app stack with
       |args, (Stack.Case _ :: _ as stack') ->
-	let seq = (t,Stack.append_app_list args Stack.empty) in
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
-	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma seq in
+	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in
 	if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
       |args, (Stack.Fix _ :: _ as stack') ->
-	let seq = (t,Stack.append_app_list args Stack.empty) in
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
-	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma seq in
+	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in
 	if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
       |_ -> s,csts'
   in whrec csts s
@@ -1061,13 +1075,13 @@ 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.append_app_list bef Stack.empty,None)::s'))
+	  |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,bef,None)::s'))
       | Construct (ind,c) -> begin
 	match Stack.strip_app stack with
 	  |args, (Stack.Case(ci, _, lf,_)::s') ->
-	    whrec (lf.(c-1), Stack.append_app_list (List.skipn ci.ci_npar args) s')
+	    whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
 	  |args, (Stack.Fix (f,s',cst)::s'') ->
-	    let x' = applist(x,args) in
+	    let x' = Stack.zip(x,args) in
 	    whrec (contract_fix f cst,s' @ (Stack.append_app_list [x'] s''))
 	  |_ -> s
       end
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 52ee728ea..11cfe9553 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -46,16 +46,14 @@ module Stack : sig
     Term.constr t -> Term.constr t -> 'a * int * int
   val append_app_list : 'a list -> 'a t -> 'a t
 
-  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. *)
-  val nfirsts_app : int -> 'a t -> 'a list
+  (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not
+      start by App or Shift *)
+  val strip_app : 'a t -> 'a t * 'a t
   (** @return (the nth first elements, the (n+1)th element, the remaining stack)  *)
-  val strip_n_app : int -> 'a t -> ('a list * 'a * 'a t) option
+  val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
 
   val not_purely_applicative : 'a t -> bool
-  val list_of_app_stack : 'a t -> 'a list option
-  val array_of_app_stack : 'a t -> 'a array option
+  val list_of_app_stack : constr t -> constr list option
 
   val assign : 'a t -> int -> 'a -> 'a t
   val args_size : 'a t -> int
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 49f12438b..fbb7de7af 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -637,17 +637,18 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	      (evd', mkMeta mv :: ks, m - 1))
 	  (sigma,[],List.length bs - 1) bs
       in
-      let unilist2 f substn l l' =
-	try List.fold_left2 f substn l l'
-	with Invalid_argument "List.fold_left2" -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
-      in
-      let substn = unilist2 (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u))
-	(evd,ms,es) us2 us in
-      let substn = unilist2 (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u))
-	substn params1 params in
-	let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb b false) substn ts ts1 in
-        let app = mkApp (c, Array.rev_of_list ks) in
+      try
+      let (substn,_,_) = Reductionops.Stack.fold2
+			   (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u))
+			   (evd,ms,es) us2 us in
+      let (substn,_,_) = Reductionops.Stack.fold2
+			   (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u))
+			   substn params1 params in
+      let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb b false) substn ts ts1 in
+      let app = mkApp (c, Array.rev_of_list ks) in
 	unirec_rec curenvnb pb b false substn c1 app
+      with Invalid_argument "Reductionops.Stack.fold2" ->
+	error_cannot_unify (fst curenvnb) sigma (cM,cN)
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
       in
   let evd = sigma in