Module `Redexpr`

Interpretation layer of redexprs such as hnf, cbv, etc.

type red_expr = (EConstr.constr, Tacred.evaluable_global_reference, Pattern.constr_pattern) Genredexpr.red_expr_gen
type red_expr_val

val out_with_occurrences : 'a Locus.with_occurrences -> Locus.occurrences * 'a
val eval_red_expr : Environ.env -> red_expr -> red_expr_val
val reduction_of_red_expr_val : ?⁠occs:(Locus.occurrences_expr * int) -> red_expr_val -> Reductionops.e_reduction_function * Constr.cast_kind
val reduction_of_red_expr : Environ.env -> red_expr -> Reductionops.e_reduction_function * Constr.cast_kind: Composition of reduction_of_red_expr_val with eval_red_expr

val declare_reduction : string -> Reductionops.reduction_function -> unit: Adding a custom reduction (function to be use at the ML level) NB: the effect is permanent.

val declare_red_expr : bool -> string -> red_expr -> unit: Adding a custom reduction (function to be called a vernac command). The boolean flag is the locality.

val set_strategy : bool -> (Conv_oracle.level * Tacred.evaluable_global_reference list) list -> unit: Sets the expansion strategy of a constant. When the boolean is true, the effect is non-synchronous (i.e. it does not survive section and module closure).

val cbv_vm : Reductionops.reduction_function: call by value normalisation function using the virtual machine

val wit_red_expr : ((Constrexpr.constr_expr, Libnames.qualid Constrexpr.or_by_notation, Constrexpr.constr_expr) Genredexpr.red_expr_gen, (Genintern.glob_constr_and_expr, Tacred.evaluable_global_reference Genredexpr.and_short_name Locus.or_var, Genintern.glob_constr_pattern_and_expr) Genredexpr.red_expr_gen, (EConstr.t, Tacred.evaluable_global_reference, Pattern.constr_pattern) Genredexpr.red_expr_gen) Genarg.genarg_type