diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-14 07:14:42 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-14 07:14:42 +0000 |
| commit | 2e224a5d535f761a194ba27f026c3b6c26c1c7c1 (patch) | |
| tree | 137be3072b6bc9c4553012c12b1f191a379f8097 /kernel/reduction.mli | |
| parent | 972616f79a627d97788caaab992497cfb7a86a17 (diff) | |
Nouvelle version de frterm; ajout des contextes dans l'enviornnement de réduction de Closure
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@602 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 21 |
1 files changed, 3 insertions, 18 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index bc004aec6..d1a092ae7 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -13,7 +13,6 @@ open Closure (* Reduction Functions. *) -exception Redelimination exception Elimconst (*s A [stack] is a context of arguments, arguments are pushed by @@ -58,22 +57,15 @@ val stack_reduction_of_reduction : i*) val stacklam : (state -> 'a) -> constr list -> constr -> stack -> 'a -(*s Generic Optimized Reduction Functions using Closures *) +(*s Generic Optimized Reduction Function using Closures *) -(* 1. lazy strategy *) val clos_norm_flags : Closure.flags -> 'a reduction_function (* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) val nf_beta : 'a reduction_function val nf_betaiota : 'a reduction_function val nf_betadeltaiota : 'a reduction_function -(* 2. call by value strategy *) -val cbv_norm_flags : flags -> 'a reduction_function -val cbv_beta : 'a reduction_function -val cbv_betaiota : 'a reduction_function -val cbv_betadeltaiota : 'a reduction_function - -(* 3. lazy strategy, weak head reduction *) +(* Lazy strategy, weak head reduction *) val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function val whd_betadeltaiota : 'a contextual_reduction_function @@ -147,13 +139,6 @@ val poly_args : env -> 'a evar_map -> constr -> int list val whd_programs : 'a reduction_function -val unfoldn : - (int list * section_path) list -> 'a reduction_function -val fold_one_com : constr -> 'a reduction_function -val fold_commands : constr list -> 'a reduction_function -val pattern_occs : (int list * constr * constr) list -> 'a reduction_function -val compute : 'a reduction_function - (* [reduce_fix] contracts a fix redex if it is actually reducible *) type fix_reduction_result = NotReducible | Reduced of state @@ -231,4 +216,4 @@ val whd_ise1_metas : 'a evar_map -> constr -> constr val hnf : env -> 'a evar_map -> constr -> constr * constr list i*) val apprec : 'a state_reduction_function -val red_product : 'a reduction_function + |