Module Reductionops.Stack
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
val fold2 : ('a -> EConstr.constr -> EConstr.constr -> 'a) -> 'a -> EConstr.constr t -> EConstr.constr t -> 'a
fold2 f x sk1 sk2
foldsf
on any pair of term in(sk1,sk2)
.- returns
the result and the lifts to apply on the terms
- raises IncompatibleFold2
when
sk1
andsk2
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)
, thens = a @ b
andb
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