diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-05 13:29:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-05 13:29:20 +0000 |
| commit | 47bf3b7fee031096013b29ad496949de063f010a (patch) | |
| tree | e81a6604979d02840c7e6250d2da46a61dd58739 | |
| parent | 40be348f4502976adc0a7612e9dcf489cfd19330 (diff) | |
Ajout d'un strong 'light'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@426 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | kernel/reduction.ml | 19 | ||||
| -rw-r--r-- | kernel/reduction.mli | 5 |
2 files changed, 22 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index ec4dc3cc3..235adffb4 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -17,7 +17,9 @@ open Closure exception Redelimination exception Elimconst -type 'a reduction_function = env -> 'a evar_map -> constr -> constr +type 'a contextual_reduction_function = env -> 'a evar_map -> constr -> constr +type 'a reduction_function = 'a contextual_reduction_function +type local_reduction_function = constr -> constr type 'a stack_reduction_function = env -> 'a evar_map -> constr -> constr list -> constr * constr list @@ -55,6 +57,21 @@ let strong whdfun env sigma = in strongrec +let local_strong whdfun = + let rec strongrec t = match whdfun t with + | DOP0 _ as t -> t + (* Cas ad hoc *) + | DOP1(oper,c) -> DOP1(oper,strongrec c) + | DOP2(oper,c1,c2) -> DOP2(oper,strongrec c1,strongrec c2) + | DOPN(oper,cl) -> DOPN(oper,Array.map strongrec cl) + | DOPL(oper,cl) -> DOPL(oper,List.map strongrec cl) + | DLAM(na,c) -> DLAM(na,strongrec c) + | DLAMV(na,c) -> DLAMV(na,Array.map strongrec c) + | VAR _ as t -> t + | Rel _ as t -> t + in + strongrec + let rec strong_prodspine redfun env sigma c = match redfun env sigma c with | DOP2(Prod,a,DLAM(na,b)) -> diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 25adf3b88..c772ede66 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -16,7 +16,9 @@ open Closure exception Redelimination exception Elimconst -type 'a reduction_function = env -> 'a evar_map -> constr -> constr +type 'a contextual_reduction_function = env -> 'a evar_map -> constr -> constr +type 'a reduction_function = 'a contextual_reduction_function +type local_reduction_function = constr -> constr type 'a stack_reduction_function = env -> 'a evar_map -> constr -> constr list -> constr * constr list @@ -27,6 +29,7 @@ val whd_stack : 'a stack_reduction_function val under_casts : 'a reduction_function -> 'a reduction_function val strong : 'a reduction_function -> 'a reduction_function +val local_strong : local_reduction_function -> local_reduction_function val strong_prodspine : 'a reduction_function -> 'a reduction_function val stack_reduction_of_reduction : 'a reduction_function -> 'a stack_reduction_function |