nouvel algo de conversion plus uniforme

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 22 insertions, 49 deletions

diff --git a/kernel/closure.mli b/kernel/closure.mli
index 96c86b05fd..54c1328b48 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -78,36 +78,13 @@ end
 module RedFlags : RedFlagsSig
 open RedFlags
 
-val beta_red : reds
-val betaiota_red : reds
-val betadeltaiota_red : reds
-val betaiotazeta_red : reds
-val betadeltaiotanolet_red : reds
+val beta               : reds
+val betaiota           : reds
+val betadeltaiota      : reds
+val betaiotazeta       : reds
+val betadeltaiotanolet : reds
 
-(*s Reduction function specification. *)
-
-type red_mode = UNIFORM | SIMPL | WITHBACK
-
-type flags = red_mode * reds
-
-(* [(UNIFORM,r)]  == [r]-reduce in any context.
-   [(SIMPL,r)]    == bdi-reduce under cases or fix, [r] otherwise 
-   (like hnf does).
-   [(WITHBACK,r)] == internal use: means we are under a case 
-   or in rec. arg. of fix. *)
-
-val flags_under : flags -> flags
-val red_top : flags -> red_kind -> bool
-val red_under : flags -> red_kind -> bool
-
-val no_flag : flags
-val beta : flags
-val betaiota : flags
-val betadeltaiota : flags
-val betadeltaiotanolet : flags
-
-val hnf_flags : flags
-val unfold_flags : evaluable_global_reference -> flags
+val unfold_red : evaluable_global_reference -> reds
 
 (***********************************************************************)
 
@@ -119,9 +96,8 @@ type table_key =
 
 type 'a infos
 val ref_value_cache: 'a infos -> table_key -> 'a option
-val info_flags: 'a infos -> flags
-val infos_under: 'a infos -> 'a infos
-val create: ('a infos -> constr -> 'a) -> flags -> env -> 'a infos
+val info_flags: 'a infos -> reds
+val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
 
 (***********************************************************************)
 (*s A [stack] is a context of arguments, arguments are pushed by
@@ -181,8 +157,8 @@ type fterm =
   | FLOCKED
 
 
-(* To lazy reduce a constr, create a ['a clos_infos] with
-   [create_cbv_infos], inject the term to reduce with [inject]; then use
+(* To lazy reduce a constr, create a [clos_infos] with
+   [create_clos_infos], inject the term to reduce with [inject]; then use
    a reduction function *)
 
 val inject : constr -> fconstr
@@ -191,7 +167,7 @@ val term_of_fconstr : fconstr -> constr
 
 (* Global and local constant cache *)
 type clos_infos
-val create_clos_infos : flags -> env -> clos_infos
+val create_clos_infos : reds -> env -> clos_infos
 
 (* Reduction function *)
 
@@ -201,14 +177,12 @@ val norm_val : clos_infos -> fconstr -> constr
 (* [whd_val] is for weak head normalization *)
 val whd_val : clos_infos -> fconstr -> constr
 
-(* Conversion auxiliary functions to do step by step normalisation *)
-
-(* [fhnf] and [fnf_apply] are for weak head normalization but staying
-   in [fconstr] world to perform step by step weak head normalization *)
+(* [whd_stack] performs weak head normalization in a given stack. It
+   stops whenever a reduction is blocked. *)
+val whd_stack :
+  clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
 
-val fhnf: clos_infos -> fconstr -> int * fconstr * fconstr stack
-val fhnf_apply : clos_infos ->
-  int -> fconstr -> fconstr stack -> int * fconstr * fconstr stack
+(* Conversion auxiliary functions to do step by step normalisation *)
 
 (* [unfold_reference] unfolds references in a [fconstr] *)
 val unfold_reference : clos_infos -> table_key -> fconstr option
@@ -216,20 +190,19 @@ val unfold_reference : clos_infos -> table_key -> fconstr option
 (***********************************************************************)
 (*i This is for lazy debug *)
 
-val lift_fconstr : int -> fconstr -> fconstr
+val lift_fconstr      : int -> fconstr -> fconstr
 val lift_fconstr_vect : int -> fconstr array -> fconstr array
 
-val mk_clos : fconstr subs -> constr -> fconstr
+val mk_clos      : fconstr subs -> constr -> fconstr
 val mk_clos_vect : fconstr subs -> constr array -> fconstr array
 val mk_clos_deep :
   (fconstr subs -> constr -> fconstr) ->
    fconstr subs -> constr -> fconstr
 
-val knr: clos_infos -> fconstr -> fconstr stack ->
-  fconstr * fconstr stack
-val kl: clos_infos -> fconstr -> fconstr
+val kni: clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
+val knr: clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
+val kl : clos_infos -> fconstr -> fconstr
 
-val to_constr :
-  (lift -> fconstr -> constr) -> lift -> fconstr -> constr
+val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
 
 (* End of cbn debug section i*)