nouvel algo de conversion plus uniforme

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

9 files changed, 298 insertions, 263 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 3b2655af6..56ef7cafb 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -167,11 +167,11 @@ end : RedFlagsSig)
 
 open RedFlags
 
-let betadeltaiota_red = mkflags [fBETA;fDELTA;fZETA;fIOTA]
-let betadeltaiotanolet_red = mkflags [fBETA;fDELTA;fIOTA]
-let betaiota_red = mkflags [fBETA;fIOTA]
-let beta_red = mkflags [fBETA]
-let betaiotazeta_red = mkflags [fBETA;fIOTA;fZETA]
+let betadeltaiota = mkflags [fBETA;fDELTA;fZETA;fIOTA]
+let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA]
+let betaiota = mkflags [fBETA;fIOTA]
+let beta = mkflags [fBETA]
+let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
 let unfold_red sp = 
   let flag = match sp with
     | EvalVarRef id -> fVAR id
@@ -309,48 +309,6 @@ let red_get_const red =
 fin obsolète **************)
 (* specification of the reduction function *)
 
-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
- *)
-
-(* Examples *)
-let no_flag = (UNIFORM,no_red)
-let beta = (UNIFORM,beta_red)
-let betaiota = (UNIFORM,betaiota_red)
-let betadeltaiota = (UNIFORM,betadeltaiota_red)
-let betadeltaiotanolet = (UNIFORM,betadeltaiotanolet_red)
-
-let hnf_flags = (SIMPL,betaiotazeta_red)
-let unfold_flags sp = (UNIFORM, unfold_red sp)
-
-let flags_under = function
-  | (SIMPL,r) -> (WITHBACK,r)
-  | fl -> fl
-
-
-(* Reductions allowed in "normal" circumstances: reduce only what is
- * specified by r *)
-
-let red_top (_,r) rk = red_set r rk
-
-(* Sometimes, we may want to perform a bdi reduction, to generate new redexes.
- * Typically: in the Simpl reduction, terms in recursive position of a fixpoint
- * are bdi-reduced, even if r is weaker.
- *
- * It is important to keep in mind that when we talk of "normal" or
- * "head normal" forms, it always refer to the reduction specified by r,
- * whatever the term context. *)
-
-let red_under (md,r) rk =
-  match md with
-    | WITHBACK -> true
-    | _ -> red_set r rk
 
 (* Flags of reduction and cache of constants: 'a is a type that may be
  * mapped to constr. 'a infos implements a cache for constants and
@@ -379,7 +337,7 @@ type table_key =
    (* FarRel: index in the rel_context part of _initial_ environment *)
 
 type 'a infos = {
-  i_flags : flags;
+  i_flags : reds;
   i_repr : 'a infos -> constr -> 'a;
   i_env : env;
   i_rels : int * (int * constr) list;
@@ -437,9 +395,6 @@ let create mk_cl flgs env =
     i_tab = Hashtbl.create 17 }
 
 
-let infos_under infos = { infos with i_flags = flags_under infos.i_flags }
-
-
 (**********************************************************************)
 (* The type of (machine) stacks (= lambda-bar-calculus' contexts)     *) 
 
@@ -472,14 +427,6 @@ let rec stack_args_size = function
   | Zupdate(_)::s -> stack_args_size s
   | _ -> 0
 
-(* Parameterization: check the a given reduction is allowed in the
-   context of the stack *)
-let can_red info stk r =
-  red_top info.i_flags r ||
-  (fst info.i_flags = SIMPL &&
-    List.exists (function (Zcase _|Zfix _) -> true | _ -> false) stk)
-
-
 (* When used as an argument stack (only Zapp can appear) *)
 let rec decomp_stack = function
   | Zapp[v]::s -> Some (v, s)
@@ -953,23 +900,23 @@ and knht e t stk =
 (* Computes a normal form from the result of knh. *)
 let rec knr info m stk =
   match m.term with
-  | FLambda(_,_,_,f,e) when can_red info stk fBETA ->
+  | FLambda(_,_,_,f,e) when red_set info.i_flags fBETA ->
       (match get_arg m stk with
           (Some(depth,arg),s) -> knit info (subs_shift_cons(depth,e,arg)) f s
         | (None,s) -> (m,s))
-  | FFlex(ConstKey sp) when can_red info stk (fCONST sp) ->
+  | FFlex(ConstKey sp) when red_set info.i_flags (fCONST sp) ->
       (match ref_value_cache info (ConstKey sp) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
-  | FFlex(VarKey id) when can_red info stk (fVAR id) ->
+  | FFlex(VarKey id) when red_set info.i_flags (fVAR id) ->
       (match ref_value_cache info (VarKey id) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
-  | FFlex(FarRelKey k) when can_red info stk fDELTA ->
+  | FFlex(FarRelKey k) when red_set info.i_flags fDELTA ->
       (match ref_value_cache info (FarRelKey k) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
-  | FConstruct(ind,c) when can_red info stk fIOTA ->
+  | FConstruct(ind,c) when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
           (depth, args, Zcase(ci,_,br)::s) ->
             assert (ci.ci_npar>=0);
@@ -981,13 +928,13 @@ let rec knr info m stk =
             let efx = contract_fix_vect fx.term in
             kni info efx stk'
         | (_,args,s) -> (m,args@s))
-  | FCoFix _ when can_red info stk fIOTA ->
+  | FCoFix _ when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
           (_, args, ((Zcase _::_) as stk')) ->
             let efx = contract_fix_vect m.term in
             kni info efx (args@stk')
         | (_,args,s) -> (m,args@s))
-  | FLetIn (_,v,_,_,bd,e) when can_red info stk fZETA ->
+  | FLetIn (_,v,_,_,bd,e) when red_set info.i_flags fZETA ->
       knit info (subs_cons(v,e)) bd stk
   | _ -> (m,stk)
 
@@ -1048,6 +995,8 @@ let norm_val info v =
 
 let inject = mk_clos (ESID 0)
 
+let whd_stack = kni
+
 (* cache of constants: the body is computed only when needed. *)
 type clos_infos = fconstr infos
 
@@ -1055,24 +1004,3 @@ let create_clos_infos flgs env =
   create (fun _ -> inject) flgs env
 
 let unfold_reference = ref_value_cache
-
-(* Head normal form. *)
-
-(* TODO: optimise *)
-let rec strip_applstack k acc m =
-  match m.term with
-      FApp(a,b) ->
-        strip_applstack k (append_stack (lift_fconstr_vect k b) acc) a
-    | FLIFT(n,a) ->
-        strip_applstack (k+n) acc a
-    | FCLOS _ -> assert false
-    | _ -> (k,m,acc)
-
-
-let fhnf info v =
-  strip_applstack 0 [] (kh info v [])
-
-
-let fhnf_apply info k head appl =
-  let stk = zshift k appl in
-  strip_applstack 0 [] (kh info head stk)
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 96c86b05f..54c1328b4 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*)
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
new file mode 100644
index 000000000..350e1a5a0
--- /dev/null
+++ b/kernel/conv_oracle.ml
@@ -0,0 +1,47 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Names
+open Closure
+
+(* Opaque constants *)
+let cst_transp = ref Sppred.full
+
+let set_opaque_const sp = cst_transp := Sppred.remove sp !cst_transp
+let set_transparent_const sp = cst_transp := Sppred.add sp !cst_transp
+
+let is_opaque_cst sp = not (Sppred.mem sp !cst_transp)
+
+(* Unfold the first only if it is not opaque and the second is
+   opaque *)
+let const_order sp1 sp2 = is_opaque_cst sp2 & not (is_opaque_cst sp1)
+
+(* Opaque variables *)
+let var_transp = ref Idpred.full
+
+let set_opaque_var sp = var_transp := Idpred.remove sp !var_transp
+let set_transparent_var sp = var_transp := Idpred.add sp !var_transp
+
+let is_opaque_var sp = not (Idpred.mem sp !var_transp)
+
+let var_order id1 id2 = is_opaque_var id2 & not (is_opaque_var id1)
+
+(* *)
+let oracle_order k1 k2 =
+  match (k1,k2) with
+      (ConstKey sp1, ConstKey sp2) -> const_order sp1 sp2
+    | (VarKey id1, VarKey id2) -> var_order id1 id2
+    | _ -> false
+
+(* summary operations *)
+
+let init() = (cst_transp := Sppred.full; var_transp := Idpred.full)
+let freeze () = (!var_transp, !cst_transp)
+let unfreeze (vo,co) = (cst_transp := co; var_transp := vo)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
new file mode 100644
index 000000000..94da48d4d
--- /dev/null
+++ b/kernel/conv_oracle.mli
@@ -0,0 +1,32 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Names
+open Closure
+
+(* Order on section paths for unfolding.
+   If oracle_order sp1 sp2 is true, then unfold sp1 first.
+   Note: the oracle does not introduce incompleteness, it only
+   tries to postpone unfolding of "opaque" constants. *)
+val oracle_order : table_key -> table_key -> bool
+
+(* Changing the oracle *)
+val set_opaque_const      : section_path -> unit
+val set_transparent_const : section_path -> unit
+
+val set_opaque_var      : identifier -> unit
+val set_transparent_var : identifier -> unit
+
+(*****************************)
+
+(* transparent state summary operations *)
+val init     : unit -> unit
+val freeze   : unit -> transparent_state
+val unfreeze : transparent_state -> unit
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index c9399925b..7a01a6dc3 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -321,24 +321,6 @@ let check_case_info env indsp ci =
 
 (* A powerful notion of subterm *)
 
-let find_sorted_assoc p = 
-  let rec findrec = function 
-    | (a,ta)::l -> 
-	if a < p then findrec l else if a = p then ta else raise Not_found
-    | _ -> raise Not_found
-  in 
-  findrec
-
-let map_lift_fst_n m = List.map (function (n,t)->(n+m,t))
-let map_lift_fst = map_lift_fst_n 1
-
-let rec instantiate_recarg sp lrc ra = 
-  match ra with 
-    | Mrec(j)        -> Imbr((sp,j),lrc)
-    | Imbr(ind_sp,l) -> Imbr(ind_sp, List.map (instantiate_recarg sp lrc) l)
-    | Norec          -> Norec
-    | Param(k)       -> List.nth lrc k
-
 (* To each inductive definition corresponds an array describing the
    structure of recursive arguments for each constructor, we call it
    the recursive spec of the type (it has type recargs vect).  For
@@ -350,6 +332,16 @@ let rec instantiate_recarg sp lrc ra =
    first argument.
 *)
 
+let map_lift_fst_n m = List.map (function (n,t)->(n+m,t))
+let map_lift_fst = map_lift_fst_n 1
+
+let rec instantiate_recarg sp lrc ra = 
+  match ra with 
+    | Mrec(j)        -> Imbr((sp,j),lrc)
+    | Imbr(ind_sp,l) -> Imbr(ind_sp, List.map (instantiate_recarg sp lrc) l)
+    | Norec          -> Norec
+    | Param(k)       -> List.nth lrc k
+
 (*
    f is a function of type
      env -> int -> (int * recargs) list -> constr -> 'a 
@@ -390,6 +382,14 @@ let is_inst_var k c =
     | Rel n -> n=k
     | _ -> false
 
+let find_sorted_assoc p = 
+  let rec findrec = function 
+    | (a,ta)::l -> 
+	if a < p then findrec l else if a = p then ta else raise Not_found
+    | _ -> raise Not_found
+  in 
+  findrec
+
 (* 
    is_subterm_specif env lcx mind_recvec n lst c 
 
@@ -514,7 +514,8 @@ let rec check_subterm_rec_meta env vectn k def =
      (* n gives the index of the recursive variable *)
      (noccur_with_meta (n+k+1) nfi t) or 
      (* no recursive call in the term *)
-     (let f,l = hnf_stack env t in
+     (* Rq: why not try and expand some definitions ? *)
+     (let f,l = decompose_app (whd_betaiotazeta env t) in
       match kind_of_term f with
 	| Rel p -> 
 	    if n+k+1 <= p & p < n+k+nfi+1 then
diff --git a/kernel/names.ml b/kernel/names.ml
index b91c6b08c..7e9d9ecf3 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -40,31 +40,13 @@ module Idset = Set.Make(IdOrdered)
 module Idmap = Map.Make(IdOrdered)
 module Idpred = Predicate.Make(IdOrdered)
 
-let pr_id id = [< 'sTR (string_of_id id) >]
-
-let wildcard = id_of_string "_"
-
 (* Names *)
 
 type name = Name of identifier | Anonymous
 
-(*s Directory paths = section names paths *)
-let parse_fields s =
-  let len = String.length s in
-  let rec decoupe_dirs n =
-    try
-      let pos = String.index_from s n '.' in
-      let dir = String.sub s n (pos-n) in
-      let dirs,n' = decoupe_dirs (succ pos) in
-      (id_of_string dir)::dirs,n'
-    with
-      | Not_found -> [],n
-  in
-  if len = 0 then invalid_arg "parse_section_path";
-  let dirs,n = decoupe_dirs 0 in
-  let id = String.sub s n (len-n) in
-  dirs, (id_of_string id)
-
+(* Dirpaths are lists of module identifiers. The actual representation
+   is reversed to optimise sharing: Coq.A.B is ["B";"A";"Coq"] *)
+ 
 type module_ident = identifier
 type dir_path = module_ident list
 
@@ -84,8 +66,6 @@ let string_of_dirpath = function
   | sl ->
       String.concat "." (List.map string_of_id (List.rev sl))
 
-let pr_dirpath sl = [< 'sTR (string_of_dirpath sl) >]
-
 (*s Section paths are absolute names *)
 
 type section_path = {
diff --git a/kernel/names.mli b/kernel/names.mli
index 5a01c2d86..7f410149c 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -15,7 +15,6 @@ type name = Name of identifier | Anonymous
 (* Parsing and printing of identifiers *)
 val string_of_id : identifier -> string
 val id_of_string : string -> identifier
-val pr_id : identifier -> Pp.std_ppcmds
 
 (* Identifiers sets and maps *)
 module Idset  : Set.S with type elt = identifier
@@ -24,17 +23,17 @@ module Idmap  : Map.S with type key = identifier
 
 (*s Directory paths = section names paths *)
 type module_ident = identifier
-type dir_path
-
 module ModIdmap : Map.S with type key = module_ident
 
-(* Inner modules idents on top of list *)
+type dir_path
+
+(* Inner modules idents on top of list (to improve sharing).
+   For instance: A.B.C is ["C";"B";"A"] *)
 val make_dirpath : module_ident list -> dir_path
 val repr_dirpath : dir_path -> module_ident list
 
 (* Printing of directory paths as ["coq_root.module.submodule"] *)
 val string_of_dirpath : dir_path -> string
-val pr_dirpath : dir_path -> Pp.std_ppcmds
 
 
 (*s Section paths are {\em absolute} names *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4e99446b6..a5b773c24 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -17,6 +17,58 @@ open Environ
 open Closure
 open Esubst
 
+let rec is_empty_stack = function
+    [] -> true
+  | Zupdate _::s -> is_empty_stack s
+  | Zshift _::s -> is_empty_stack s
+  | _ -> false
+
+(* Compute the lift to be performed on a term placed in a given stack *)
+let el_stack el stk =
+  let n =
+    List.fold_left
+      (fun i z ->
+        match z with
+            Zshift n -> i+n
+          | _ -> i)
+      0
+      stk in
+  el_shft n el
+
+let compare_stack_shape stk1 stk2 =
+  let rec compare_rec bal stk1 stk2 =
+  match (stk1,stk2) with
+      ([],[]) -> bal=0
+    | ((Zupdate _|Zshift _)::s1, _) -> compare_rec bal s1 stk2
+    | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
+    | (Zapp l1::s1, _) -> compare_rec (bal+List.length l1) s1 stk2
+    | (_, Zapp l2::s2) -> compare_rec (bal-List.length l2) stk1 s2
+    | (Zcase(c1,_,_)::s1, Zcase(c2,_,_)::s2) ->
+        bal=0 && c1.ci_ind = c2.ci_ind && compare_rec 0 s1 s2
+    | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
+        bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
+    | (_,_) -> false in
+  compare_rec 0 stk1 stk2
+
+let pure_stack lfts stk =
+  let rec pure_rec lfts stk =
+    match stk with
+        [] -> (lfts,[])
+      | zi::s ->
+          (match (zi,pure_rec lfts s) with
+              (Zupdate _,lpstk)  -> lpstk
+            | (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
+            | (Zapp a1,(l,Zapp a2::pstk)) ->
+                (l,Zapp (List.map (fun t -> (l,t)) a1 @ a2)::pstk)
+            | (Zapp a, (l,pstk)) ->
+                (l,Zapp (List.map (fun t -> (l,t)) a)::pstk)
+            | (Zfix(fx,a),(l,pstk)) ->
+                let (lfx,pa) = pure_rec l a in
+                (l, Zfix((lfx,fx),pa)::pstk)
+            | (Zcase(ci,p,br),(l,pstk)) ->
+                (l,Zcase(ci,(l,p),Array.map (fun t -> (l,t)) br)::pstk)) in
+  snd (pure_rec lfts stk)
+
 (****************************************************************************)
 (*                   Reduction Functions                                    *)
 (****************************************************************************)
@@ -24,9 +76,8 @@ open Esubst
 let nf_betaiota t =
   norm_val (create_clos_infos betaiota empty_env) (inject t)
 
-let hnf_stack env x =
-  decompose_app
-    (norm_val (create_clos_infos hnf_flags env) (inject x))
+let whd_betaiotazeta env x =
+  whd_val (create_clos_infos betaiotazeta env) (inject x)
 
 let whd_betadeltaiota env t = 
   whd_val (create_clos_infos betadeltaiota env) (inject t)
@@ -43,30 +94,35 @@ let beta_appvect c v =
       | _ -> app_stack (substl env t, stack) in
   stacklam [] c (append_stack v empty_stack)
 
-(* pseudo-reduction rule:
- * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
- * with an HNF on the first argument to produce a product.
- * if this does not work, then we use the string S as part of our
- * error message. *)
-
-let hnf_prod_app env t n =
-  match kind_of_term (whd_betadeltaiota env t) with
-    | Prod (_,_,b) -> subst1 n b
-    | _ -> anomaly "hnf_prod_app: Need a product"
-
-let hnf_prod_applist env t nl = 
-  List.fold_left (hnf_prod_app env) t nl
-
 (********************************************************************)
 (*                         Conversion                               *)
 (********************************************************************)
 
 (* Conversion utility functions *)
-type 'a conversion_function = env -> 'a -> 'a -> constraints
+type 'a conversion_function = env -> 'a -> 'a -> Univ.constraints
 
 exception NotConvertible
 exception NotConvertibleVect of int
 
+let compare_stacks f lft1 stk1 lft2 stk2 cuniv =
+  let rec cmp_rec pstk1 pstk2 cuniv =
+    match (pstk1,pstk2) with
+      | (z1::s1, z2::s2) ->
+          let c1 = cmp_rec s1 s2 cuniv in
+          (match (z1,z2) with
+            | (Zapp a1,Zapp a2) -> List.fold_right2 f a1 a2 c1
+            | (Zfix(fx1,a1),Zfix(fx2,a2)) ->
+                let c2 = f fx1 fx2 c1 in
+                cmp_rec a1 a2 c2
+            | (Zcase(ci1,p1,br1),Zcase(ci2,p2,br2)) ->
+                let c2 = f p1 p2 c1 in
+                array_fold_right2 f br1 br2 c2
+            | _ -> assert false)
+      | _ -> cuniv in
+  if compare_stack_shape stk1 stk2 then
+    cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv
+  else raise NotConvertible
+
 (* Convertibility of sorts *)
 
 type conv_pb = 
@@ -86,24 +142,27 @@ let sort_cmp pb s0 s1 cuniv =
 	   | CUMUL -> enforce_geq u2 u1 cuniv)
     | (_, _) -> raise NotConvertible
 
+
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv = 
-  eqappr cv_pb infos (lft1, fhnf infos term1) (lft2, fhnf infos term2) cuniv
+  eqappr cv_pb infos
+    (lft1, whd_stack infos term1 [])
+    (lft2, whd_stack infos term2 [])
+    cuniv
 
-(* Conversion between [lft1]([^n1]hd1 v1) and [lft2]([^n2]hd2 v2) *)
+(* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
 and eqappr cv_pb infos appr1 appr2 cuniv =
-  let (lft1,(n1,hd1,v1)) = appr1
-  and (lft2,(n2,hd2,v2)) = appr2 in
-  let el1 = el_shft n1 lft1
-  and el2 = el_shft n2 lft2 in
+  let (lft1,(hd1,v1)) = appr1 in
+  let (lft2,(hd2,v2)) = appr2 in
+  let el1 = el_stack lft1 v1 in
+  let el2 = el_stack lft2 v2 in
   match (fterm_of hd1, fterm_of hd2) with
     (* case of leaves *)
     | (FAtom a1, FAtom a2) ->
 	(match kind_of_term a1, kind_of_term a2 with
 	   | (Sort s1, Sort s2) -> 
-	       if stack_args_size v1 = 0 && stack_args_size v2 = 0
-	       then sort_cmp cv_pb s1 s2 cuniv
-               else raise NotConvertible
+	       assert (is_empty_stack v1 && is_empty_stack v2);
+	       sort_cmp cv_pb s1 s2 cuniv
 	   | (Meta n, Meta m) ->
                if n=m
 	       then convert_stacks infos lft1 lft2 v1 v2 cuniv
@@ -111,8 +170,8 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
 	   | _ -> raise NotConvertible)
     | (FEvar (ev1,args1), FEvar (ev2,args2)) ->
         if ev1=ev2 then
-          let u1 = convert_vect infos el1 el2 args1 args2 cuniv in
-	  convert_stacks infos lft1 lft2 v1 v2 u1
+          let u1 = convert_stacks infos lft1 lft2 v1 v2 cuniv in
+          convert_vect infos el1 el2 args1 args2 u1
         else raise NotConvertible
 
     (* 2 index known to be bound to no constant *)
@@ -121,70 +180,65 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
         then convert_stacks infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
-    (* 2 constants, 2 existentials or 2 local defined vars or 2 defined rels *)
+    (* 2 constants, 2 local defined vars or 2 defined rels *)
     | (FFlex fl1, FFlex fl2) ->
 	(try (* try first intensional equality *)
 	  if fl1 = fl2
-          then
-	    convert_stacks infos lft1 lft2 v1 v2 cuniv
+          then convert_stacks infos lft1 lft2 v1 v2 cuniv
           else raise NotConvertible
         with NotConvertible ->
-          (* else expand the second occurrence (arbitrary heuristic) *)
-	  match unfold_reference infos fl2 with
-            | Some def2 -> 
-		eqappr cv_pb infos appr1
-                  (lft2, fhnf_apply infos n2 def2 v2) cuniv
-             | None ->
-                 (match unfold_reference infos fl1 with
-                   | Some def1 ->
-                       eqappr cv_pb infos
-			 (lft1, fhnf_apply infos n1 def1 v1) appr2 cuniv
-		   | None -> raise NotConvertible))
-
-    (* only one constant, existential, defined var or defined rel *)
+          (* else the oracle tells which constant is to be expanded *)
+          let (app1,app2) =
+            if Conv_oracle.oracle_order fl1 fl2 then
+              match unfold_reference infos fl1 with
+                | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
+                | None ->
+                    (match unfold_reference infos fl2 with
+                      | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
+		      | None -> raise NotConvertible)
+            else
+	      match unfold_reference infos fl2 with
+                | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
+                | None ->
+                    (match unfold_reference infos fl1 with
+                    | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
+		    | None -> raise NotConvertible) in
+          eqappr cv_pb infos app1 app2 cuniv)
+
+    (* only one constant, defined var or defined rel *)
     | (FFlex fl1, _)      ->
         (match unfold_reference infos fl1 with
            | Some def1 -> 
-	       eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1)
-                 appr2 cuniv
+	       eqappr cv_pb infos (lft1, whd_stack infos def1 v1) appr2 cuniv
            | None -> raise NotConvertible)
     | (_, FFlex fl2)      ->
         (match unfold_reference infos fl2 with
            | Some def2 -> 
-	       eqappr cv_pb infos appr1
-                 (lft2, fhnf_apply infos n2 def2 v2)
-                 cuniv
+	       eqappr cv_pb infos appr1 (lft2, whd_stack infos def2 v2) cuniv
            | None -> raise NotConvertible)
 	
     (* other constructors *)
     | (FLambda (_,c1,c2,_,_), FLambda (_,c'1,c'2,_,_)) ->
-        if stack_args_size v1 = 0 && stack_args_size v2 = 0
-        then
-          let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in
-          ccnv CONV infos
-            (el_lift el1) (el_lift el2) c2 c'2 u1
-        else raise NotConvertible
-
-    | (FLetIn _, _) | (_, FLetIn _) ->
-        anomaly "LetIn normally removed by fhnf"
+        assert (is_empty_stack v1 && is_empty_stack v2);
+        let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in
+        ccnv CONV infos (el_lift el1) (el_lift el2) c2 c'2 u1
 
     | (FProd (_,c1,c2,_,_), FProd (_,c'1,c'2,_,_)) ->
-	if stack_args_size v1 = 0 && stack_args_size v2 = 0
-	then (* Luo's system *)
-          let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in
-          ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 u1
-        else raise NotConvertible
+        assert (is_empty_stack v1 && is_empty_stack v2);
+	(* Luo's system *)
+        let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in
+        ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 u1
 
     (* Inductive types:  MutInd MutConstruct MutCase Fix Cofix *)
 
       (* Les annotations du MutCase ne servent qu'à l'affichage *)
-
+(*
     | (FCases (_,p1,c1,cl1), FCases (_,p2,c2,cl2)) ->
         let u1 = ccnv CONV infos el1 el2 p1 p2 cuniv in
         let u2 = ccnv CONV infos el1 el2 c1 c2 u1 in
         let u3 = convert_vect infos el1 el2 cl1 cl2 u2 in
 	convert_stacks infos lft1 lft2 v1 v2 u3
-
+*)
      | (FInd op1, FInd op2) ->
          if op1 = op2 then
            convert_stacks infos lft1 lft2 v1 v2 cuniv
@@ -218,15 +272,17 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
            convert_stacks infos lft1 lft2 v1 v2 u2
          else raise NotConvertible
 
+    | ( (FLetIn _, _) | (_, FLetIn _) | (FCases _,_) | (_,FCases _)
+      | (FApp _,_) | (_,FApp _) | (FCLOS _, _) | (_,FCLOS _)
+      | (FLIFT _, _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED)) ->
+        anomaly "Unexpected term returned by fhnf"
+
      | _ -> raise NotConvertible
 
 and convert_stacks infos lft1 lft2 stk1 stk2 cuniv =
-  match (decomp_stack stk1, decomp_stack stk2) with
-      (Some(a1,s1), Some(a2,s2)) ->
-        let u1 = ccnv CONV infos lft1 lft2 a1 a2 cuniv in
-        convert_stacks infos lft1 lft2 s1 s2 u1
-    | (None, None) -> cuniv
-    | _ -> raise NotConvertible
+  compare_stacks
+    (fun (l1,t1) (l2,t2) c -> ccnv CONV infos l1 l2 t1 t2 c)
+    lft1 stk1 lft2 stk2 cuniv
 
 and convert_vect infos lft1 lft2 v1 v2 cuniv =
   let lv1 = Array.length v1 in
@@ -247,12 +303,12 @@ let fconv cv_pb env t1 t2 =
   if eq_constr t1 t2 then 
     Constraint.empty
   else
-    let infos = create_clos_infos hnf_flags env in
+    let infos = create_clos_infos betaiotazeta env in
     ccnv cv_pb infos ELID ELID (inject t1) (inject t2)
       Constraint.empty
 
-let conv env = fconv CONV env
-let conv_leq env = fconv CUMUL env
+let conv = fconv CONV
+let conv_leq = fconv CUMUL
 
 let conv_leq_vecti env v1 v2 =
   array_fold_left2_i 
@@ -279,6 +335,20 @@ let conv env t1 t2 =
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
 
+(* pseudo-reduction rule:
+ * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
+ * with an HNF on the first argument to produce a product.
+ * if this does not work, then we use the string S as part of our
+ * error message. *)
+
+let hnf_prod_app env t n =
+  match kind_of_term (whd_betadeltaiota env t) with
+    | Prod (_,_,b) -> subst1 n b
+    | _ -> anomaly "hnf_prod_app: Need a product"
+
+let hnf_prod_applist env t nl = 
+  List.fold_left (hnf_prod_app env) t nl
+
 (* Dealing with arities *)
 
 let dest_prod env = 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 9ac3d8042..50371e85f 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -16,15 +16,11 @@ open Environ
 (***********************************************************************)
 (*s Reduction functions *)
 
+val whd_betaiotazeta        : env -> constr -> constr
 val whd_betadeltaiota       : env -> constr -> constr
 val whd_betadeltaiota_nolet : env -> constr -> constr
 
 val nf_betaiota      : constr -> constr
-val hnf_stack        : env -> constr -> constr * constr list
-val hnf_prod_applist : env -> types -> constr list -> types
-
-(* Builds an application node, reducing beta redexes it may produce. *) 
-val beta_appvect : constr -> constr array -> constr
 
 (***********************************************************************)
 (*s conversion functions *)
@@ -38,6 +34,15 @@ val conv_leq       : types conversion_function
 val conv_leq_vecti : types array conversion_function
 
 (***********************************************************************)
+
+(* Builds an application node, reducing beta redexes it may produce. *) 
+val beta_appvect : constr -> constr array -> constr
+
+(* Pseudo-reduction rule  Prod(x,A,B) a --> B[x\a] *)
+val hnf_prod_applist : env -> types -> constr list -> types
+
+
+(***********************************************************************)
 (*s Recognizing products and arities modulo reduction *)
 
 val dest_prod       : env -> types -> Sign.rel_context * types