diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 121 |
1 files changed, 68 insertions, 53 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 4cd7a2a8..b8ac085a 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -1,13 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names -open Term +open Constr +open EConstr open Univ open Evd open Environ @@ -25,13 +28,24 @@ module ReductionBehaviour : sig bool -> Globnames.global_reference -> (int list * int * flag list) -> unit val get : Globnames.global_reference -> (int list * int * flag list) option - val print : Globnames.global_reference -> Pp.std_ppcmds + val print : Globnames.global_reference -> Pp.t end -(** Option telling if reduction should use the refolding machinery of cbn - (off by default) *) -val get_refolding_in_reduction : unit -> bool -val set_refolding_in_reduction : bool -> unit +(** {6 Support for reduction effects } *) + +type effect_name = string + +(* [declare_reduction_effect name f] declares [f] under key [name]; + [name] must be a unique in "world". *) +val declare_reduction_effect : effect_name -> + (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit + +(* [set_reduction_effect cst name] declares effect [name] to be called when [cst] is found *) +val set_reduction_effect : Globnames.global_reference -> effect_name -> unit + +(* [effect_hook env sigma key term] apply effect associated to [key] on [term] *) +val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constr.constr -> + Constr.constr Lazy.t -> unit (** {6 Machinery about a stack of unfolded constant } @@ -44,33 +58,30 @@ module Cst_stack : sig val add_args : constr array -> t -> t val add_cst : constr -> t -> t val best_cst : t -> (constr * constr list) option - val best_replace : constr -> t -> constr -> constr - val reference : t -> Constant.t option - val pr : t -> Pp.std_ppcmds + val best_replace : Evd.evar_map -> constr -> t -> constr -> constr + val reference : Evd.evar_map -> t -> Constant.t option + val pr : t -> Pp.t end - module Stack : sig type 'a app_node - val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds + val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t type cst_member = | Cst_const of pconstant - | Cst_proj of projection + | Cst_proj of Projection.t type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * projection * Cst_stack.t - | Fix of fixpoint * 'a t * Cst_stack.t + | Proj of int * int * Projection.t * Cst_stack.t + | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *) * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list - val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val pr : ('a -> Pp.t) -> 'a t -> Pp.t val empty : 'a t val is_empty : 'a t -> bool @@ -80,15 +91,18 @@ module Stack : sig val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) val compare_shape : 'a t -> 'a t -> bool + + exception IncompatibleFold2 (** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)]. - @return the result and the lifts to apply on the terms *) - val fold2 : ('a -> Term.constr -> Term.constr -> 'a) -> 'a -> - Term.constr t -> Term.constr t -> 'a * int * int - val map : (Term.constr -> Term.constr) -> Term.constr t -> Term.constr t + @return the result and the lifts to apply on the terms + @raise IncompatibleFold2 when [sk1] and [sk2] have incompatible shapes *) + val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> + constr t -> constr t -> 'a + val map : ('a -> 'a) -> 'a t -> 'a t val append_app_list : 'a list -> 'a t -> 'a t (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not - start by App or Shift *) + start by App *) val strip_app : 'a t -> 'a t * 'a t (** @return (the nth first elements, the (n+1)th element, the remaining stack) *) val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option @@ -101,8 +115,8 @@ module Stack : sig val tail : int -> 'a t -> 'a t val nth : 'a t -> int -> 'a - val best_state : constr * constr t -> Cst_stack.t -> constr * constr t - val zip : ?refold:bool -> constr * constr t -> constr + val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t + val zip : ?refold:bool -> evar_map -> constr * constr t -> constr end (************************************************************************) @@ -113,7 +127,7 @@ type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function type local_reduction_function = evar_map -> constr -> constr -type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma } +type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type contextual_stack_reduction_function = env -> evar_map -> constr -> constr * constr list @@ -126,7 +140,7 @@ type contextual_state_reduction_function = type state_reduction_function = contextual_state_reduction_function type local_state_reduction_function = evar_map -> state -> state -val pr_state : state -> Pp.std_ppcmds +val pr_state : state -> Pp.t (** {6 Reduction Function Operators } *) @@ -137,22 +151,23 @@ val strong_prodspine : local_reduction_function -> local_reduction_function val stack_reduction_of_reduction : 'a reduction_function -> 'a state_reduction_function i*) -val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a +val stacklam : (state -> 'a) -> constr list -> evar_map -> constr -> constr Stack.t -> 'a val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool -> CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t val iterate_whd_gen : bool -> CClosure.RedFlags.reds -> - Environ.env -> Evd.evar_map -> Term.constr -> Term.constr + Environ.env -> Evd.evar_map -> constr -> constr (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function +val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function (** Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) -val nf_beta : local_reduction_function -val nf_betaiota : local_reduction_function -val nf_betaiotazeta : local_reduction_function +val nf_beta : reduction_function +val nf_betaiota : reduction_function +val nf_betaiotazeta : reduction_function val nf_all : reduction_function val nf_evar : evar_map -> constr -> constr @@ -200,9 +215,9 @@ val shrink_eta : constr -> constr (** Various reduction functions *) -val safe_evar_value : evar_map -> existential -> constr option +val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option -val beta_applist : constr * constr list -> constr +val beta_applist : evar_map -> constr * constr list -> constr val hnf_prod_app : env -> evar_map -> constr -> constr -> constr val hnf_prod_appvect : env -> evar_map -> constr -> constr array -> constr @@ -213,12 +228,12 @@ val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr -val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * sorts -val sort_of_arity : env -> evar_map -> constr -> sorts -val splay_prod_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr -val splay_lam_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr +val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * ESorts.t +val sort_of_arity : env -> evar_map -> constr -> ESorts.t +val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr +val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_prod_assum : - env -> evar_map -> constr -> Context.Rel.t * constr + env -> evar_map -> constr -> rel_context * constr type 'a miota_args = { mP : constr; (** the result type *) @@ -227,22 +242,22 @@ type 'a miota_args = { mcargs : 'a list; (** the constructor's arguments *) mlf : 'a array } (** the branch code vector *) -val reducible_mind_case : constr -> bool -val reduce_mind_case : constr miota_args -> constr +val reducible_mind_case : evar_map -> constr -> bool +val reduce_mind_case : evar_map -> constr miota_args -> constr -val find_conclusion : env -> evar_map -> constr -> (constr,constr) kind_of_term +val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, EInstance.t) kind_of_term val is_arity : env -> evar_map -> constr -> bool val is_sort : env -> evar_map -> types -> bool -val contract_fix : ?env:Environ.env -> ?reference:Constant.t -> fixpoint -> constr -val fix_recarg : fixpoint -> constr Stack.t -> (int * constr) option +val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> fixpoint -> constr +val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) -val is_transparent : Environ.env -> constant tableKey -> bool +val is_transparent : Environ.env -> Constant.t tableKey -> bool (** {6 Conversion Functions (uses closures, lazy strategy) } *) -type conversion_test = constraints -> constraints +type conversion_test = Constraint.t -> Constraint.t val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb @@ -258,7 +273,7 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con (** [infer_conv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. - @raises UniverseInconsistency iff catch_incon is set to false, + @raise UniverseInconsistency iff catch_incon is set to false, otherwise returns false in that case. *) val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> @@ -274,14 +289,14 @@ val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a conversion function. Used to pretype vm and native casts. *) val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> - (constr, evar_map) Reduction.generic_conversion_function) -> + (Constr.constr, evar_map) Reduction.generic_conversion_function) -> ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> evar_map * bool (** {6 Special-Purpose Reduction Functions } *) -val whd_meta : evar_map -> constr -> constr -val plain_instance : constr Metamap.t -> constr -> constr +val whd_meta : local_reduction_function +val plain_instance : evar_map -> constr Metamap.t -> constr -> constr val instance : evar_map -> constr Metamap.t -> constr -> constr val head_unfold_under_prod : transparent_state -> reduction_function val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr |