Cst_stack before stack (abstraction leak in whd_gen)

3 files changed, 82 insertions, 82 deletions

diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 500bb54306..19175f930c 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -65,6 +65,6 @@ val evar_conv_x : transparent_state ->
   env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
 val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state ->
   env -> evar_map ->
-    conv_pb -> state * Cst_stack.t -> state * Cst_stack.t ->
+    conv_pb -> state * constr Cst_stack.t -> state * constr Cst_stack.t ->
       Evarsolve.unification_result
 (**/**)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 19fb98b6bd..a3eaba68b7 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -134,6 +134,56 @@ module ReductionBehaviour = struct
 		 | _ -> str "unfold " ++ pr_global ref ++ pp_nomatch )
 end
 
+(** Machinery about stack of unfolded constants *)
+module Cst_stack = struct
+(** constant * params * args
+
+- constant applied to params = term in head applied to args
+- there is at most one arguments with an empty list of args, it must be the first.
+- in args, the int represents the indice of the first arg to consider *)
+  type 'a t = ('a * 'a list * (int * 'a array) list)  list
+
+  let empty = []
+
+  let sanity x y =
+    assert (Constr.equal x y)
+
+  let drop_useless = function
+    | _ :: ((_,_,[])::_ as q) -> q
+    | l -> l
+
+  let add_param h cst_l =
+    let append2cst = function
+      | (c,params,[]) -> (c, h::params, [])
+      | (c,params,((i,t)::q)) when i = pred (Array.length t) ->
+	 let () = sanity h t.(i) in (c, params, q)
+      | (c,params,(i,t)::q) ->
+	 let () = sanity h t.(i) in (c, params, (succ i,t)::q)
+ in
+    drop_useless (List.map append2cst cst_l)
+
+  let add_args cl =
+    List.map (fun (a,b,args) -> (a,b,(0,cl)::args))
+
+  let add_cst cst = function
+    | (_,_,[]) :: q as l -> l
+    | l -> (cst,[],[])::l
+
+  let best_cst = function
+    | (cst,params,[])::_ -> Some(cst,params)
+    | _ -> None
+
+  let pr l =
+    let open Pp in
+    let p_c = Termops.print_constr in
+    prlist_with_sep pr_semicolon
+      (fun (c,params,args) ->
+	hov 1 (p_c c ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++
+		 pr_sequence (fun (i,el) -> prvect_with_sep spc p_c (Array.sub el i (Array.length el - i))) args ++
+		 str ")")) l
+end
+
+
 (** The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
 module Stack :
 sig
@@ -478,67 +528,6 @@ let betadeltaiota = Closure.RedFlags.red_add betadelta Closure.RedFlags.fIOTA
 let betadeltaiota_nolet = Closure.betadeltaiotanolet
 let betadeltaiotaeta = Closure.RedFlags.red_add betadeltaiota Closure.RedFlags.fETA
 
-(** Machinery about stack of unfolded constants *)
-module Cst_stack = struct
-(** constant * params * args
-
-- constant applied to params = term in head applied to args
-- there is at most one arguments with an empty list of args, it must be the first.
-- in args, the int represents the indice of the first arg to consider *)
-  type t = (Term.constr * Term.constr list * (int * Term.constr array) list)  list
-
-  let empty = []
-
-  let sanity x y =
-    assert (Constr.equal x y)
-
-  let drop_useless = function
-    | _ :: ((_,_,[])::_ as q) -> q
-    | l -> l
-
-  let add_param h cst_l =
-    let append2cst = function
-      | (c,params,[]) -> (c, h::params, [])
-      | (c,params,((i,t)::q)) when i = pred (Array.length t) ->
-	 let () = sanity h t.(i) in (c, params, q)
-      | (c,params,(i,t)::q) ->
-	 let () = sanity h t.(i) in (c, params, (succ i,t)::q)
- in
-    drop_useless (List.map append2cst cst_l)
-
-  let add_args cl =
-    List.map (fun (a,b,args) -> (a,b,(0,cl)::args))
-
-  let add_cst cst = function
-    | (_,_,[]) :: q as l -> l
-    | l -> (cst,[],[])::l
-
-  let best_cst = function
-    | (cst,params,[])::_ -> Some(cst,params)
-    | _ -> None
-
-  let best_state (_,sk as s) l =
-    let rec aux sk def = function
-    |(cst, params, []) -> (cst, Stack.append_app_list (List.rev params) sk)
-    |(cst, params, (i,t)::q) -> match Stack.decomp sk with
-				| None -> def
-				| Some (el,sk') ->
-				   let () = sanity el t.(i) in
-				   if i = pred (Array.length t)
-				   then aux sk' def (cst, params, q)
-				   else aux sk' def (cst, params, (succ i,t)::q)
-    in List.fold_left (aux sk) s l
-
-  let pr l =
-    let open Pp in
-    let p_c = Termops.print_constr in
-    prlist_with_sep pr_semicolon
-		    (fun (c,params,args) ->
-		     hov 1 (p_c c ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++
-			      pr_sequence (fun (i,el) -> prvect_with_sep spc p_c (Array.sub el i (Array.length el - i))) args ++
-			      str ")")) l
-end
-
 (* Beta Reduction tools *)
 
 let apply_subst recfun env cst_l t stack =
@@ -668,8 +657,19 @@ type 'a reduced_state =
 *)
 let rec whd_state_gen ?csts tactic_mode flags env sigma =
   let rec whrec cst_l (x, stack as s) =
+    let best_state (_,sk as s) l =
+      let rec aux sk def = function
+	|(cst, params, []) -> (cst, Stack.append_app_list (List.rev params) sk)
+	|(cst, params, (i,t)::q) -> match Stack.decomp sk with
+	  | None -> def
+	  | Some (el,sk') ->
+	    let () = Cst_stack.sanity el t.(i) in
+	    if i = pred (Array.length t)
+	    then aux sk' def (cst, params, q)
+	    else aux sk' def (cst, params, (succ i,t)::q)
+      in List.fold_left (aux sk) s l in
     let fold () =
-      if tactic_mode then (Cst_stack.best_state s cst_l,Cst_stack.empty) else (s,cst_l)
+      if tactic_mode then (best_state s cst_l,Cst_stack.empty) else (s,cst_l)
     in
     match kind_of_term x with
     | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b4eaf27d50..091eb7c81b 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -29,6 +29,21 @@ module ReductionBehaviour : sig
   val print : Globnames.global_reference -> Pp.std_ppcmds
 end
 
+(** {6 Machinery about a stack of unfolded constant }
+
+    cst applied to params must convertible to term of the state applied to args
+*)
+module Cst_stack : sig
+  type 'a t
+  val empty : 'a t
+  val add_param : constr -> constr t -> constr t
+  val add_args : 'a array -> 'a t -> 'a t
+  val add_cst : 'a -> 'a t -> 'a t
+  val best_cst : 'a t -> ('a * 'a list) option
+  val pr : constr t -> Pp.std_ppcmds
+end
+
+
 module Stack : sig
   type 'a app_node
 
@@ -100,21 +115,6 @@ type local_state_reduction_function = evar_map -> state -> state
 
 val pr_state : state -> Pp.std_ppcmds
 
-(** {6 Machinery about a stack of unfolded constant }
-
-    cst applied to params must convertible to term of the state applied to args
-*)
-module Cst_stack : sig
-  type t
-  val empty : t
-  val add_param : constr -> t -> t
-  val add_args : constr array -> t -> t
-  val add_cst : constr -> t -> t
-  val best_cst : t -> (constr * constr list) option
-  val best_state : state -> t -> state
-  val pr : t -> Pp.std_ppcmds
-end
-
 (** {6 Reduction Function Operators } *)
 
 val strong : reduction_function -> reduction_function
@@ -126,8 +126,8 @@ val stack_reduction_of_reduction :
 i*)
 val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a
 
-val whd_state_gen : ?csts:Cst_stack.t -> bool -> Closure.RedFlags.reds ->
-  Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
+val whd_state_gen : ?csts:constr Cst_stack.t -> bool -> Closure.RedFlags.reds ->
+  Environ.env -> Evd.evar_map -> state -> state * constr Cst_stack.t
 
 val iterate_whd_gen : bool -> Closure.RedFlags.reds ->
   Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
@@ -274,8 +274,8 @@ val head_unfold_under_prod : transparent_state -> reduction_function
 (** {6 Heuristic for Conversion with Evar } *)
 
 val whd_betaiota_deltazeta_for_iota_state :
-  transparent_state -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state ->
-  state * Cst_stack.t
+  transparent_state -> Environ.env -> Evd.evar_map -> constr Cst_stack.t -> state ->
+  state * constr Cst_stack.t
 
 (** {6 Meta-related reduction functions } *)
 val meta_instance : evar_map -> constr freelisted -> constr