diff options
Diffstat (limited to 'kernel')
| -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 ec4dc3cc30..235adffb4a 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 25adf3b889..c772ede665 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 |