aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorherbelin2000-05-22 17:21:17 +0000
committerherbelin2000-05-22 17:21:17 +0000
commit08f5f4b1268624de1f8733ce30b51a62080f6ba6 (patch)
treea9cebdf444e0b1fdcd77e00d725a7905cafe6ff0 /kernel
parentabcf77362c7744ade443307d62dcb30e9025541a (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.ml4
-rw-r--r--kernel/inductive.mli13
-rw-r--r--kernel/reduction.ml36
-rw-r--r--kernel/reduction.mli23
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 *)