1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316
|
(************************************************************************)
(* * 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 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
open Constr
open EConstr
open Univ
open Evd
open Environ
(** Reduction Functions. *)
exception Elimconst
(** Machinery to customize the behavior of the reduction *)
module ReductionBehaviour : sig
type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ]
(** [set is_local ref (recargs, nargs, flags)] *)
val set :
bool -> GlobRef.t -> (int list * int * flag list) -> unit
val get :
GlobRef.t -> (int list * int * flag list) option
val print : GlobRef.t -> Pp.t
end
(** {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 : Constant.t -> 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 -> Constant.t ->
Constr.constr Lazy.t -> unit
(** {6 Machinery about a stack of unfolded constant }
cst applied to params must convertible to term of the state applied to args
*)
module Cst_stack : sig
type t
val empty : t
val add_param : constr -> t -> t
val add_args : constr array -> t -> t
val add_cst : constr -> t -> t
val best_cst : t -> (constr * constr list) option
val best_replace : Evd.evar_map -> constr -> t -> constr -> constr
val reference : Evd.evar_map -> t -> Constant.t option
val pr : env -> Evd.evar_map -> t -> Pp.t
end
module Stack : sig
type 'a app_node
val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
type cst_member =
| Cst_const of pconstant
| 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 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
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
(** [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
@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 *)
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
val not_purely_applicative : 'a t -> bool
val list_of_app_stack : constr t -> 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 : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t
val zip : ?refold:bool -> evar_map -> constr * constr t -> constr
end
(************************************************************************)
type state = constr * constr Stack.t
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 = env -> evar_map -> constr -> evar_map * constr
type contextual_stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
type stack_reduction_function = contextual_stack_reduction_function
type local_stack_reduction_function =
evar_map -> constr -> constr * constr list
type contextual_state_reduction_function =
env -> evar_map -> state -> state
type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = evar_map -> state -> state
val pr_state : env -> evar_map -> state -> Pp.t
(** {6 Reduction Function Operators } *)
val strong_with_flags :
(CClosure.RedFlags.reds -> reduction_function) ->
(CClosure.RedFlags.reds -> reduction_function)
val strong : reduction_function -> reduction_function
val local_strong : local_reduction_function -> local_reduction_function
val strong_prodspine : local_reduction_function -> local_reduction_function
(*i
val stack_reduction_of_reduction :
'a reduction_function -> 'a state_reduction_function
i*)
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 -> 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 : reduction_function
val nf_betaiota : reduction_function
val nf_betaiotazeta : reduction_function
val nf_all : reduction_function
val nf_evar : evar_map -> constr -> constr
(** Lazy strategy, weak head reduction *)
val whd_evar : evar_map -> constr -> constr
val whd_nored : local_reduction_function
val whd_beta : local_reduction_function
val whd_betaiota : local_reduction_function
val whd_betaiotazeta : local_reduction_function
val whd_all : contextual_reduction_function
val whd_allnolet : contextual_reduction_function
val whd_betalet : local_reduction_function
(** Removes cast and put into applicative form *)
val whd_nored_stack : local_stack_reduction_function
val whd_beta_stack : local_stack_reduction_function
val whd_betaiota_stack : local_stack_reduction_function
val whd_betaiotazeta_stack : local_stack_reduction_function
val whd_all_stack : contextual_stack_reduction_function
val whd_allnolet_stack : contextual_stack_reduction_function
val whd_betalet_stack : local_stack_reduction_function
val whd_nored_state : local_state_reduction_function
val whd_beta_state : local_state_reduction_function
val whd_betaiota_state : local_state_reduction_function
val whd_betaiotazeta_state : local_state_reduction_function
val whd_all_state : contextual_state_reduction_function
val whd_allnolet_state : contextual_state_reduction_function
val whd_betalet_state : local_state_reduction_function
(** {6 Head normal forms } *)
val whd_delta_stack : stack_reduction_function
val whd_delta_state : state_reduction_function
val whd_delta : reduction_function
val whd_betadeltazeta_stack : stack_reduction_function
val whd_betadeltazeta_state : state_reduction_function
val whd_betadeltazeta : reduction_function
val whd_zeta_stack : local_stack_reduction_function
val whd_zeta_state : local_state_reduction_function
val whd_zeta : local_reduction_function
val shrink_eta : constr -> constr
(** Various reduction functions *)
val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option
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
val hnf_prod_applist : env -> evar_map -> constr -> constr list -> constr
val hnf_lam_app : env -> evar_map -> constr -> constr -> constr
val hnf_lam_appvect : env -> evar_map -> constr -> constr array -> constr
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 * 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 -> rel_context * constr
type 'a miota_args = {
mP : constr; (** the result type *)
mconstr : constr; (** the constructor *)
mci : case_info; (** special info to re-build pattern *)
mcargs : 'a list; (** the constructor's arguments *)
mlf : 'a array } (** the branch code vector *)
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, 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 -> 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.t tableKey -> bool
(** {6 Conversion Functions (uses closures, lazy strategy) } *)
type conversion_test = Constraint.t -> Constraint.t
val pb_is_equal : conv_pb -> bool
val pb_equal : conv_pb -> conv_pb
val is_conv : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool
val is_conv_leq : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool
val is_fconv : ?reds:transparent_state -> conv_pb -> env -> evar_map -> constr -> constr -> bool
(** [check_conv] Checks universe constraints only.
pb defaults to CUMUL and ts to a full transparent state.
*)
val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> bool
(** [infer_conv] Adds necessary universe constraints to the evar map.
pb defaults to CUMUL and ts to a full transparent state.
@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 ->
env -> evar_map -> constr -> constr -> evar_map option
(** Conversion with inference of universe constraints *)
val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr ->
evar_map option) -> unit
val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
evar_map option
(** [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.constr, evar_map) Reduction.generic_conversion_function) ->
?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env ->
evar_map -> constr -> constr -> evar_map option
(** {6 Special-Purpose Reduction Functions } *)
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
(** {6 Heuristic for Conversion with Evar } *)
val whd_betaiota_deltazeta_for_iota_state :
transparent_state -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state ->
state * Cst_stack.t
(** {6 Meta-related reduction functions } *)
val meta_instance : evar_map -> constr freelisted -> constr
val nf_meta : evar_map -> constr -> constr
val meta_reducible_instance : evar_map -> constr freelisted -> constr
|