Module Reductionops.Stack

type 'a app_node
val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
type cst_member =
| Cst_const of Constr.pconstant
| Cst_proj of Names.Projection.t
type 'a member =
| App of 'a app_node
| Case of Constr.case_info * 'a * 'a array * Cst_stack.t
| Proj of Names.Projection.t * Cst_stack.t
| Fix of ('a, 'a) Constr.pfixpoint * 'a t * Cst_stack.t
| Primitive of CPrimitives.t * Names.Constant.t * EConstr.EInstance.t * 'a t * CPrimitives.args_red * Cst_stack.t
| Cst of cst_member * int * int list * 'a t * Cst_stack.t
and 'a t = 'a member list
val pr : ('a -> Pp.t) -> 'a t -> Pp.t
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
val compare_shape : 'a t -> 'a t -> bool
exception IncompatibleFold2
val fold2 : ('a -> EConstr.constr -> EConstr.constr -> 'a) -> 'a -> EConstr.constr t -> EConstr.constr t -> 'a

fold2 f x sk1 sk2 folds f on any pair of term in (sk1,sk2).

returns

the result and the lifts to apply on the terms

raises IncompatibleFold2

when sk1 and sk2 have incompatible shapes

val map : ('a -> 'a) -> 'a t -> 'a t
val append_app_list : 'a list -> 'a t -> 'a t
val strip_app : 'a t -> 'a t * 'a t

if strip_app s = (a,b), then s = a @ b and b does not start by App

val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
returns

(the nth first elements, the (n+1)th element, the remaining stack)

val not_purely_applicative : 'a t -> bool
val list_of_app_stack : EConstr.constr t -> EConstr.constr list option
val assign : 'a t -> int -> 'a -> 'a t
val args_size : 'a t -> int
val tail : int -> 'a t -> 'a t
val nth : 'a t -> int -> 'a
val best_state : Evd.evar_map -> (EConstr.constr * EConstr.constr t) -> Cst_stack.t -> EConstr.constr * EConstr.constr t
val zip : ?⁠refold:bool -> Evd.evar_map -> (EConstr.constr * EConstr.constr t) -> EConstr.constr