Module `Reductionops.Stack`

type 'a app_node

val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t

type 'a member = | App of 'a app_node | Case of Constr.case_info * 'a * ('a, EConstr.EInstance.t) Constr.case_invert * 'a array | Proj of Names.Projection.t | Fix of ('a, 'a) Constr.pfixpoint * 'a t | Primitive of CPrimitives.t * Names.Constant.t * EConstr.EInstance.t * 'a t * CPrimitives.args_red
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 zip : Evd.evar_map -> (EConstr.constr * EConstr.constr t) -> EConstr.constr