diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
commit | 39efc41237ec906226a3a53d7396d51173495204 (patch) | |
tree | 87cd58d72d43469d2a2a0a127c1060d7c9e0206b /pretyping/reductionops.mli | |
parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'pretyping/reductionops.mli')
-rw-r--r-- | pretyping/reductionops.mli | 57 |
1 files changed, 28 insertions, 29 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 95032bde..3ffc587e 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -1,28 +1,24 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: reductionops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Term open Univ open Evd open Environ open Closure -(*i*) -(* Reduction Functions. *) +(** Reduction Functions. *) exception Elimconst -(************************************************************************) -(*s A [stack] is a context of arguments, arguments are pushed by +(*********************************************************************** + s A [stack] is a context of arguments, arguments are pushed by [append_stack] one array at a time but popped with [decomp_stack] one by one *) @@ -67,13 +63,13 @@ type contextual_state_reduction_function = type state_reduction_function = contextual_state_reduction_function type local_state_reduction_function = evar_map -> state -> state -(* Removes cast and put into applicative form *) +(** Removes cast and put into applicative form *) val whd_stack : local_stack_reduction_function -(* For compatibility: alias for whd\_stack *) +(** For compatibility: alias for whd\_stack *) val whd_castapp_stack : local_stack_reduction_function -(*s Reduction Function Operators *) +(** {6 Reduction Function Operators } *) val strong : reduction_function -> reduction_function val local_strong : local_reduction_function -> local_reduction_function @@ -84,17 +80,19 @@ val stack_reduction_of_reduction : i*) val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a -(*s Generic Optimized Reduction Function using Closures *) +(** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : Closure.RedFlags.reds -> reduction_function -(* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) + +(** 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_betadeltaiota : reduction_function val nf_evar : evar_map -> constr -> constr val nf_betaiota_preserving_vm_cast : reduction_function -(* Lazy strategy, weak head reduction *) + +(** Lazy strategy, weak head reduction *) val whd_evar : evar_map -> constr -> constr val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function @@ -120,7 +118,7 @@ val whd_betadeltaiota_nolet_state : contextual_state_reduction_function val whd_betaetalet_state : local_state_reduction_function val whd_betalet_state : local_state_reduction_function -(*s Head normal forms *) +(** {6 Head normal forms } *) val whd_delta_stack : stack_reduction_function val whd_delta_state : state_reduction_function @@ -138,7 +136,7 @@ val whd_betadeltaiotaeta : reduction_function val whd_eta : constr -> constr val whd_zeta : constr -> constr -(* Various reduction functions *) +(** Various reduction functions *) val safe_evar_value : evar_map -> existential -> constr option @@ -154,7 +152,7 @@ val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr val splay_prod : env -> evar_map -> constr -> (name * constr) list * constr val splay_lam : env -> evar_map -> constr -> (name * constr) list * constr val splay_arity : env -> evar_map -> constr -> (name * constr) list * sorts -val sort_of_arity : env -> constr -> sorts +val sort_of_arity : env -> evar_map -> constr -> sorts 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 : @@ -163,11 +161,11 @@ val decomp_sort : env -> evar_map -> types -> sorts val is_sort : env -> evar_map -> types -> bool 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 *) + 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 : constr -> bool val reduce_mind_case : constr miota_args -> constr @@ -177,7 +175,7 @@ val is_arity : env -> evar_map -> constr -> bool val whd_programs : reduction_function -(* [reduce_fix redfun fix stk] contracts [fix stk] if it is actually +(** [reduce_fix redfun fix stk] contracts [fix stk] if it is actually reducible; the structural argument is reduced by [redfun] *) type fix_reduction_result = NotReducible | Reduced of state @@ -186,10 +184,10 @@ val fix_recarg : fixpoint -> constr stack -> (int * constr) option val reduce_fix : local_state_reduction_function -> evar_map -> fixpoint -> constr stack -> fix_reduction_result -(*s Querying the kernel conversion oracle: opaque/transparent constants *) +(** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) val is_transparent : 'a tableKey -> bool -(*s Conversion Functions (uses closures, lazy strategy) *) +(** {6 Conversion Functions (uses closures, lazy strategy) } *) type conversion_test = constraints -> constraints @@ -206,18 +204,19 @@ val is_trans_conv : transparent_state -> env -> evar_map -> constr -> constr -> val is_trans_conv_leq : transparent_state -> env -> evar_map -> constr -> constr -> bool val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr -> constr -> bool -(*s Special-Purpose Reduction Functions *) +(** {6 Special-Purpose Reduction Functions } *) val whd_meta : evar_map -> constr -> constr val plain_instance : (metavariable * constr) list -> constr -> constr val instance :evar_map -> (metavariable * constr) list -> constr -> constr val head_unfold_under_prod : transparent_state -> reduction_function -(*s Heuristic for Conversion with Evar *) +(** {6 Heuristic for Conversion with Evar } *) -val whd_betaiota_deltazeta_for_iota_state : state_reduction_function +val whd_betaiota_deltazeta_for_iota_state : + transparent_state -> state_reduction_function -(*s Meta-related reduction functions *) +(** {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 |