diff options
| author | herbelin | 2000-05-22 17:21:17 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-22 17:21:17 +0000 |
| commit | 08f5f4b1268624de1f8733ce30b51a62080f6ba6 (patch) | |
| tree | a9cebdf444e0b1fdcd77e00d725a7905cafe6ff0 /kernel | |
| parent | abcf77362c7744ade443307d62dcb30e9025541a (diff) | |
suppression de l'env/sigma dans les fonctions de reduction beta et iota seuls
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@464 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 4 | ||||
| -rw-r--r-- | kernel/inductive.mli | 13 | ||||
| -rw-r--r-- | kernel/reduction.ml | 36 | ||||
| -rw-r--r-- | kernel/reduction.mli | 23 |
4 files changed, 44 insertions, 32 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 4a7649a79c..c096008db2 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -171,8 +171,8 @@ let ith_constructor_of_inductive (ind_sp,args) i = ((ind_sp,i),args) exception Induc -let extract_mrectype env sigma t = - let (t,l) = whd_stack env sigma t [] in +let extract_mrectype t = + let (t,l) = whd_stack t [] in match t with | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l) | _ -> raise Induc diff --git a/kernel/inductive.mli b/kernel/inductive.mli index b7501dd642..b603fbf1ee 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -128,17 +128,24 @@ val make_arity : env -> 'a evar_map -> bool -> inductive_family -> val build_branch_type : env -> bool -> constr -> constructor_summary -> constr -(*s [find_m*type env sigma c] coerce [c] to an recursive type (I args). +(*s Extracting an inductive type from a constructions *) + +exception Induc + +(* [extract_mrectype c] assumes [c] is syntactically an inductive type + applied to arguments then it returns its components; if not an + inductive type, it raises [Induc] *) +val extract_mrectype : constr -> inductive * constr list + +(* [find_m*type env sigma c] coerce [c] to an recursive type (I args). [find_mrectype], [find_minductype] and [find_mcoinductype] respectively accepts any recursive type, only an inductive type and only a coinductive type. They raise [Induc] if not convertible to a recursive type. *) -exception Induc val find_mrectype : env -> 'a evar_map -> constr -> inductive * constr list val find_minductype : env -> 'a evar_map -> constr -> inductive * constr list val find_mcoinductype : env -> 'a evar_map -> constr -> inductive * constr list -val extract_mrectype : env -> 'a evar_map -> constr -> inductive * constr list val lookup_mind_specif : inductive -> env -> inductive_instance diff --git a/kernel/reduction.ml b/kernel/reduction.ml index de61b72e97..4361a1bf39 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -20,8 +20,11 @@ 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 = +type 'a contextual_stack_reduction_function = env -> 'a evar_map -> constr -> constr list -> constr * constr list +type 'a stack_reduction_function = 'a contextual_stack_reduction_function +type local_stack_reduction_function = + constr -> constr list -> constr * constr list (*************************************) (*** Reduction Functions Operators ***) @@ -31,15 +34,19 @@ let rec under_casts f env sigma = function | DOP2(Cast,c,t) -> DOP2(Cast,under_casts f env sigma c, t) | c -> f env sigma c -let rec whd_stack env sigma x stack = +let rec local_under_casts f = function + | DOP2(Cast,c,t) -> DOP2(Cast,local_under_casts f c, t) + | c -> f c + +let rec whd_stack x stack = match x with - | DOPN(AppL,cl) -> whd_stack env sigma cl.(0) (array_app_tl cl stack) - | DOP2(Cast,c,_) -> whd_stack env sigma c stack + | DOPN(AppL,cl) -> whd_stack cl.(0) (array_app_tl cl stack) + | DOP2(Cast,c,_) -> whd_stack c stack | _ -> (x,stack) let stack_reduction_of_reduction red_fun env sigma x stack = let t = red_fun env sigma (applistc x stack) in - whd_stack env sigma t [] + whd_stack t [] let strong whdfun env sigma = let rec strongrec t = match whdfun env sigma t with @@ -291,7 +298,7 @@ let rec stacklam recfun env t stack = let beta_applist (c,l) = stacklam (fun c l -> applist(c,l)) [] c l -let whd_beta_stack_gen = +let whd_beta_stack = let rec whrec x stack = match x with | DOP2(Lambda,c1,DLAM(name,c2)) -> (match stack with @@ -304,10 +311,7 @@ let whd_beta_stack_gen = in whrec -let whd_beta_gen x = applist (whd_beta_stack_gen x []) - -let whd_beta_stack env sigma = whd_beta_stack_gen -let whd_beta env sigma = whd_beta_gen +let whd_beta x = applist (whd_beta_stack x []) (* 2. Delta Reduction *) @@ -542,7 +546,7 @@ let reduce_fix whfun fix stack = -------------------- qui coute cher dans whd_betadeltaiota *) -let whd_betaiota_stack_gen = +let whd_betaiota_stack = let rec whrec x stack = match x with | DOP2(Cast,c,_) -> whrec c stack @@ -567,11 +571,7 @@ let whd_betaiota_stack_gen = in whrec -let whd_betaiota_gen x = applist (whd_betaiota_stack_gen x []) - -let whd_betaiota_stack env sigma = whd_betaiota_stack_gen -let whd_betaiota env sigma = whd_betaiota_gen - +let whd_betaiota x = applist (whd_betaiota_stack x []) let whd_betaiotaevar_stack env sigma = let rec whrec x stack = @@ -970,7 +970,7 @@ let plain_instance s c = (* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *) let instance s c = - if s = [] then c else strong whd_betaiota () () (plain_instance s c) + if s = [] then c else local_strong whd_betaiota (plain_instance s c) (* pseudo-reduction rule: @@ -1080,7 +1080,7 @@ let compute_consteval env sigma c = (* One step of approximation *) let rec apprec env sigma c stack = - let (t,stack) = whd_betaiota_stack env sigma c stack in + let (t,stack) = whd_betaiota_stack c stack in match t with | DOPN(MutCase _,_) -> let (ci,p,d,lf) = destCase t in diff --git a/kernel/reduction.mli b/kernel/reduction.mli index a1c5421998..9be27fb7cc 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -20,14 +20,19 @@ 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 = +type 'a contextual_stack_reduction_function = env -> 'a evar_map -> constr -> constr list -> constr * constr list +type 'a stack_reduction_function = 'a contextual_stack_reduction_function +type local_stack_reduction_function = + constr -> constr list -> constr * constr list -val whd_stack : 'a stack_reduction_function +val whd_stack : local_stack_reduction_function (*s Reduction Function Operators *) -val under_casts : 'a reduction_function -> 'a reduction_function +val local_under_casts : local_reduction_function -> local_reduction_function +val under_casts : + 'a contextual_reduction_function -> 'a contextual_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 @@ -52,13 +57,13 @@ val cbv_betaiota : 'a reduction_function val cbv_betadeltaiota : 'a reduction_function (* 3. lazy strategy, weak head reduction *) -val whd_beta : 'a reduction_function -val whd_betaiota : 'a reduction_function -val whd_betadeltaiota : 'a reduction_function +val whd_beta : local_reduction_function +val whd_betaiota : local_reduction_function +val whd_betadeltaiota : 'a contextual_reduction_function -val whd_beta_stack : 'a stack_reduction_function -val whd_betaiota_stack : 'a stack_reduction_function -val whd_betadeltaiota_stack : 'a stack_reduction_function +val whd_beta_stack : local_stack_reduction_function +val whd_betaiota_stack : local_stack_reduction_function +val whd_betadeltaiota_stack : 'a contextual_stack_reduction_function (*s Head normal forms *) |
