X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReduction.ml;h=56e98775f31caf7276303a091dbeb22612128046;hb=7be6aeb94aa8da17732511a4844bd108976f947f;hp=fe0c09aaeff029c860c1d8abb07c4ab9cc0d2a41;hpb=a93a94942ad58d8645af1fd94bef8fa31d9541a4;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index fe0c09aae..56e98775f 100644
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -23,9 +23,10 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 (* TODO unify exceptions *)
 
-exception CicReductionInternalError;;
 exception WrongUriToInductiveDefinition;;
 exception Impossible of int;;
 exception ReferenceToConstant;;
@@ -33,7 +34,9 @@ exception ReferenceToVariable;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
-let debug_print = fun _ -> ()
+let debug = false
+let profile = false
+let debug_print s = if debug then prerr_endline (Lazy.force s)
 
 let fdebug = ref 1;;
 let debug t env s =
@@ -51,64 +54,73 @@ module type Strategy =
   type stack_term
   type env_term
   type ens_term
-  val to_stack : Cic.term -> stack_term
-  val to_stack_list : Cic.term list -> stack_term list
-  val to_env : Cic.term -> env_term
-  val to_ens : Cic.term -> ens_term
-  val from_stack :
-   unwind:
-    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
-      Cic.term -> Cic.term) ->
-   stack_term -> Cic.term
-  val from_stack_list :
-   unwind:
-    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
-      Cic.term -> Cic.term) ->
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
+  val to_env : config -> env_term
+  val to_ens : config -> ens_term
+  val from_stack : stack_term -> config
+  val from_stack_list_for_unwind :
+   unwind: (config -> Cic.term) ->
    stack_term list -> Cic.term list
-  val from_env : env_term -> Cic.term
-  val from_ens : ens_term -> Cic.term
+  val from_env : env_term -> config
+  val from_env_for_unwind :
+   unwind: (config -> Cic.term) ->
+   env_term -> Cic.term
+  val from_ens : ens_term -> config
+  val from_ens_for_unwind :
+   unwind: (config -> Cic.term) ->
+   ens_term -> Cic.term
   val stack_to_env :
-   reduce:
-    (int * env_term list * ens_term Cic.explicit_named_substitution *
-      Cic.term * stack_term list -> Cic.term) ->
-   unwind:
-    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
-      Cic.term -> Cic.term) ->
+   reduce: (config -> config) ->
+   unwind: (config -> Cic.term) ->
    stack_term -> env_term
   val compute_to_env :
-   reduce:
-    (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
-      stack_term list -> Cic.term) ->
-   unwind:
-    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
-      Cic.term -> Cic.term) ->
+   reduce: (config -> config) ->
+   unwind: (config -> Cic.term) ->
    int -> env_term list -> ens_term Cic.explicit_named_substitution ->
     Cic.term -> env_term
   val compute_to_stack :
-   reduce:
-    (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
-      stack_term list -> Cic.term) ->
-   unwind:
-    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
-      Cic.term -> Cic.term) ->
-   int -> env_term list -> ens_term Cic.explicit_named_substitution ->
-    Cic.term -> stack_term
+   reduce: (config -> config) ->
+   unwind: (config -> Cic.term) ->
+   config -> stack_term
  end
 ;;
 
+module CallByValueByNameForUnwind =
+ struct
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
+  and stack_term = config
+  and env_term = config * config (* cbv, cbn *)
+  and ens_term = config * config (* cbv, cbn *)
+
+  let to_env c = c,c
+  let to_ens c = c,c
+  let from_stack config = config
+  let from_stack_list_for_unwind ~unwind l = List.map unwind l
+  let from_env (c,_) = c
+  let from_ens (c,_) = c
+  let from_env_for_unwind ~unwind (_,c) = unwind c
+  let from_ens_for_unwind ~unwind (_,c) = unwind c
+  let stack_to_env ~reduce ~unwind config = reduce config, (0,[],[],unwind config,[])
+  let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[]), (k,e,ens,t,[])
+  let compute_to_stack ~reduce ~unwind config = config
+ end
+;;
+
+
 module CallByNameStrategy =
  struct
   type stack_term = Cic.term
   type env_term = Cic.term
   type ens_term = Cic.term
-  let to_stack v = v
-  let to_stack_list l = l
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
   let to_env v = v
   let to_ens v = v
   let from_stack ~unwind v = v
   let from_stack_list ~unwind l = l
   let from_env v = v
   let from_ens v = v
+  let from_env_for_unwind ~unwind v = v
+  let from_ens_for_unwind ~unwind v = v
   let stack_to_env ~reduce ~unwind v = v
   let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
   let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
@@ -120,14 +132,15 @@ module CallByValueStrategy =
   type stack_term = Cic.term
   type env_term = Cic.term
   type ens_term = Cic.term
-  let to_stack v = v
-  let to_stack_list l = l
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
   let to_env v = v
   let to_ens v = v
   let from_stack ~unwind v = v
   let from_stack_list ~unwind l = l
   let from_env v = v
   let from_ens v = v
+  let from_env_for_unwind ~unwind v = v
+  let from_ens_for_unwind ~unwind v = v
   let stack_to_env ~reduce ~unwind v = v
   let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
   let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
@@ -139,14 +152,15 @@ module CallByValueStrategyByNameOnConstants =
   type stack_term = Cic.term
   type env_term = Cic.term
   type ens_term = Cic.term
-  let to_stack v = v
-  let to_stack_list l = l
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
   let to_env v = v
   let to_ens v = v
   let from_stack ~unwind v = v
   let from_stack_list ~unwind l = l
   let from_env v = v
   let from_ens v = v
+  let from_env_for_unwind ~unwind v = v
+  let from_ens_for_unwind ~unwind v = v
   let stack_to_env ~reduce ~unwind v = v
   let compute_to_stack ~reduce ~unwind k e ens =
    function
@@ -164,14 +178,15 @@ module LazyCallByValueStrategy =
   type stack_term = Cic.term lazy_t
   type env_term = Cic.term lazy_t
   type ens_term = Cic.term lazy_t
-  let to_stack v = lazy v
-  let to_stack_list l = List.map to_stack l
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
   let to_env v = lazy v
   let to_ens v = lazy v
   let from_stack ~unwind v = Lazy.force v
   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
   let from_env v = Lazy.force v
   let from_ens v = Lazy.force v
+  let from_env_for_unwind ~unwind v = Lazy.force v
+  let from_ens_for_unwind ~unwind v = Lazy.force v
   let stack_to_env ~reduce ~unwind v = v
   let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
   let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
@@ -183,14 +198,15 @@ module LazyCallByValueStrategyByNameOnConstants =
   type stack_term = Cic.term lazy_t
   type env_term = Cic.term lazy_t
   type ens_term = Cic.term lazy_t
-  let to_stack v = lazy v
-  let to_stack_list l = List.map to_stack l
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
   let to_env v = lazy v
   let to_ens v = lazy v
   let from_stack ~unwind v = Lazy.force v
   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
   let from_env v = Lazy.force v
   let from_ens v = Lazy.force v
+  let from_env_for_unwind ~unwind v = Lazy.force v
+  let from_ens_for_unwind ~unwind v = Lazy.force v
   let stack_to_env ~reduce ~unwind v = v
   let compute_to_stack ~reduce ~unwind k e ens t =
    lazy (
@@ -210,14 +226,15 @@ module LazyCallByNameStrategy =
   type stack_term = Cic.term lazy_t
   type env_term = Cic.term lazy_t
   type ens_term = Cic.term lazy_t
-  let to_stack v = lazy v
-  let to_stack_list l = List.map to_stack l
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
   let to_env v = lazy v
   let to_ens v = lazy v
   let from_stack ~unwind v = Lazy.force v
   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
   let from_env v = Lazy.force v
   let from_ens v = Lazy.force v
+  let from_env_for_unwind ~unwind v = Lazy.force v
+  let from_ens_for_unwind ~unwind v = Lazy.force v
   let stack_to_env ~reduce ~unwind v = v
   let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
   let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
@@ -231,10 +248,7 @@ module
   type stack_term = reduce:bool -> Cic.term
   type env_term = reduce:bool -> Cic.term
   type ens_term = reduce:bool -> Cic.term
-  let to_stack v =
-   let value = lazy v in
-    fun ~reduce -> Lazy.force value
-  let to_stack_list l = List.map to_stack l
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
   let to_env v =
    let value = lazy v in
     fun ~reduce -> Lazy.force value
@@ -245,6 +259,8 @@ module
   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
   let from_env v = (v ~reduce:true)
   let from_ens v = (v ~reduce:true)
+  let from_env_for_unwind ~unwind v = (v ~reduce:true)
+  let from_ens_for_unwind ~unwind v = (v ~reduce:true)
   let stack_to_env ~reduce ~unwind v = v
   let compute_to_stack ~reduce ~unwind k e ens t =
    let svalue =
@@ -275,22 +291,22 @@ module
 
 module ClosuresOnStackByValueFromEnvOrEnsStrategy =
  struct
-  type stack_term =
-   int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
-  type env_term = Cic.term
-  type ens_term = Cic.term
-  let to_stack v = (0,[],[],v)
-  let to_stack_list l = List.map to_stack l
-  let to_env v = v
-  let to_ens v = v
-  let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
-  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
+  and stack_term = config
+  and env_term = config
+  and ens_term = config
+
+  let to_env config = config
+  let to_ens config = config
+  let from_stack config = config
+  let from_stack_list_for_unwind ~unwind l = List.map unwind l
   let from_env v = v
   let from_ens v = v
-  let stack_to_env ~reduce ~unwind (k,e,ens,t) = reduce (k,e,ens,t,[])
-  let compute_to_env ~reduce ~unwind k e ens t =
-   unwind k e ens t
-  let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
+  let from_env_for_unwind ~unwind config = unwind config
+  let from_ens_for_unwind ~unwind config = unwind config
+  let stack_to_env ~reduce ~unwind config = reduce config
+  let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[])
+  let compute_to_stack ~reduce ~unwind config = config
  end
 ;;
 
@@ -300,14 +316,15 @@ module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
    int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
   type env_term = Cic.term
   type ens_term = Cic.term
-  let to_stack v = (0,[],[],v)
-  let to_stack_list l = List.map to_stack l
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
   let to_env v = v
   let to_ens v = v
   let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
   let from_env v = v
   let from_ens v = v
+  let from_env_for_unwind ~unwind v = v
+  let from_ens_for_unwind ~unwind v = v
   let stack_to_env ~reduce ~unwind (k,e,ens,t) =
    match t with
       Cic.Const _ as t -> unwind k e ens t    
@@ -327,7 +344,7 @@ module Reduction(RS : Strategy) =
 
   (* k is the length of the environment e *)
   (* m is the current depth inside the term *)
-  let unwind' m k e ens t = 
+  let rec unwind' m k e ens t = 
    let module C = Cic in
    let module S = CicSubstitution in
     if k = 0 && ens = [] then
@@ -339,7 +356,7 @@ module Reduction(RS : Strategy) =
           if n <= m then t else
            let d =
             try
-             Some (RS.from_env (List.nth e (n-m-1)))
+             Some (RS.from_env_for_unwind ~unwind (List.nth e (n-m-1)))
             with _ -> None
            in
             (match d with 
@@ -352,7 +369,7 @@ module Reduction(RS : Strategy) =
 debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens))) ;
 *)
          if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
-          CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
+          CicSubstitution.lift m (RS.from_ens_for_unwind ~unwind (List.assq uri ens))
          else
           let params =
             let o,_ = 
@@ -490,7 +507,7 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,
             &&
              List.mem uri params
            ->
-            (uri,CicSubstitution.lift m (RS.from_ens t)) ::
+            (uri,CicSubstitution.lift m (RS.from_ens_for_unwind ~unwind t)) ::
              (filter_and_lift (uri::already_instantiated) tl)
         | _::tl -> filter_and_lift already_instantiated tl
 (*
@@ -507,43 +524,48 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
         (filter_and_lift [] (List.rev ens))
      in
       unwind_aux m t          
-  ;;
   
+  and unwind (k,e,ens,t,s) =
+   let t' = unwind' 0 k e ens t in
+    if s = [] then t' else Cic.Appl (t'::(RS.from_stack_list_for_unwind ~unwind s))
+  ;;
+
+(*
   let unwind =
-   unwind' 0 
+   let profiler_unwind = HExtlib.profile ~enable:profile "are_convertible.unwind" in
+    fun k e ens t ->
+     profiler_unwind.HExtlib.profile (unwind k e ens) t
   ;;
+*)
   
-  let reduce ~delta ?(subst = []) context : config -> Cic.term = 
+  let reduce ~delta ?(subst = []) context : config -> config = 
    let module C = Cic in
    let module S = CicSubstitution in 
    let rec reduce =
     function
-       (k, e, _, (C.Rel n as t), s) ->
-        let d =
+       (k, e, _, C.Rel n, s) as config ->
+        let config' =
          try
           Some (RS.from_env (List.nth e (n-1)))
          with
-          _ ->
+          Failure _ ->
            try
             begin
              match List.nth context (n - 1 - k) with
                 None -> assert false
               | Some (_,C.Decl _) -> None
-              | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x)
+              | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[])
             end
            with
-            _ -> None
+            Failure _ -> None
         in
-         (match d with 
-             Some t' -> reduce (0,[],[],t',s)
-           | None ->
-              if s = [] then
-               C.Rel (n-k)
-              else C.Appl (C.Rel (n-k)::(RS.from_stack_list ~unwind s))
-         )
-     | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) -> 
+         (match config' with 
+             Some (k',e',ens',t',s') -> reduce (k',e',ens',t',s'@s)
+           | None -> config)
+     | (k, e, ens, C.Var (uri,exp_named_subst), s) as config -> 
          if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
-          reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
+          let (k',e',ens',t',s') = RS.from_ens (List.assq uri ens) in
+           reduce (k',e',ens',t',s'@s)
          else
           ( let o,_ = 
               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
@@ -552,60 +574,36 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
               C.Constant _ -> raise ReferenceToConstant
             | C.CurrentProof _ -> raise ReferenceToCurrentProof
             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-            | C.Variable (_,None,_,_,_) ->
-               let t' = unwind k e ens t in
-                if s = [] then t' else
-                 C.Appl (t'::(RS.from_stack_list ~unwind s))
+            | C.Variable (_,None,_,_,_) -> config
             | C.Variable (_,Some body,_,_,_) ->
                let ens' = push_exp_named_subst k e ens exp_named_subst in
                 reduce (0, [], ens', body, s)
           )
-     | (k, e, ens, (C.Meta (n,l) as t), s) ->
+     | (k, e, ens, C.Meta (n,l), s) as config ->
         (try 
            let (_, term,_) = CicUtil.lookup_subst n subst in
            reduce (k, e, ens,CicSubstitution.subst_meta l term,s)
-         with  CicUtil.Subst_not_found _ ->
-           let t' = unwind k e ens t in
-           if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
-     | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
-     | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
-     | (k, e, ens, (C.Cast (te,ty) as t), s) ->
-        reduce (k, e, ens, te, s) (* s should be empty *)
-     | (k, e, ens, (C.Prod _ as t), s) ->
-         unwind k e ens t (* s should be empty *)
-     | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t' 
+         with  CicUtil.Subst_not_found _ -> config)
+     | (_, _, _, C.Sort _, _)
+     | (_, _, _, C.Implicit _, _) as config -> config
+     | (k, e, ens, C.Cast (te,ty), s) ->
+        reduce (k, e, ens, te, s)
+     | (_, _, _, C.Prod _, _) as config -> config
+     | (_, _, _, C.Lambda _, []) as config -> config
      | (k, e, ens, C.Lambda (_,_,t), p::s) ->
          reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
-     | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
+     | (k, e, ens, C.LetIn (_,m,t), s) ->
         let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
          reduce (k+1, m'::e, ens, t, s)
      | (_, _, _, C.Appl [], _) -> assert false
      | (k, e, ens, C.Appl (he::tl), s) ->
         let tl' =
          List.map
-          (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl
+          (function t -> RS.compute_to_stack ~reduce ~unwind (k,e,ens,t,[])) tl
         in
          reduce (k, e, ens, he, (List.append tl') s)
-  (* CSC: Old Dead Code 
-     | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s) 
-     | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)  
-     | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s) 
-     | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
-  (* strict evaluation, but constants are NOT unfolded *)
-        let red =
-         function
-            C.Const _ as t -> unwind k e ens t
-          | t -> reduce (k,e,ens,t,[])
-        in
-         let tl' = List.map red tl in
-          reduce (k, e, ens, he , List.append tl' s)
-     | (k, e, ens, C.Appl l, s) ->
-         C.Appl (List.append (List.map (unwind k e ens) l) s)
-  *)
-     | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) when delta=false->
-           let t' = unwind k e ens t in
-           if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
-     | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
+     | (_, _, _, C.Const _, _) as config when delta=false-> config
+     | (k, e, ens, C.Const (uri,exp_named_subst), s) as config ->
         (let o,_ = 
            CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
          in
@@ -614,9 +612,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
              let ens' = push_exp_named_subst k e ens exp_named_subst in
               (* constants are closed *)
               reduce (0, [], ens', body, s) 
-          | C.Constant (_,None,_,_,_) ->
-             let t' = unwind k e ens t in
-              if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+          | C.Constant (_,None,_,_,_) -> config
           | C.Variable _ -> raise ReferenceToVariable
           | C.CurrentProof (_,_,body,_,_,_) ->
              let ens' = push_exp_named_subst k e ens exp_named_subst in
@@ -624,16 +620,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
               reduce (0, [], ens', body, s)
           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
         )
-     | (k, e, ens, (C.MutInd _ as t),s) ->
-        let t' = unwind k e ens t in 
-         if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
-     | (k, e, ens, (C.MutConstruct _ as t),s) -> 
-         let t' = unwind k e ens t in
-          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
-     | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
+     | (_, _, _, C.MutInd _, _)
+     | (_, _, _, C.MutConstruct _, _) as config -> config 
+     | (k, e, ens, C.MutCase (mutind,i,outty,term,pl),s) as config ->
         let decofix =
          function
-            C.CoFix (i,fl) as t ->
+            (k, e, ens, C.CoFix (i,fl), s) ->
              let (_,_,body) = List.nth fl i in
               let body' =
                let counter = ref (List.length fl) in
@@ -642,34 +634,20 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
                  fl
                  body
               in
-               (* the term is the result of a reduction; *)
-               (* so it is already unwinded.             *)
-               reduce (0,[],[],body',[])
-          | C.Appl (C.CoFix (i,fl) :: tl) ->
-             let (_,_,body) = List.nth fl i in
-              let body' =
-               let counter = ref (List.length fl) in
-                List.fold_right
-                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
-                 fl
-                 body
-              in
-               (* the term is the result of a reduction; *)
-               (* so it is already unwinded.             *)
-               reduce (0,[],[],body',RS.to_stack_list tl)
-          | t -> t
+               reduce (k,e,ens,body',s)
+          | config -> config
         in
          (match decofix (reduce (k,e,ens,term,[])) with
-             C.MutConstruct (_,_,j,_) ->
-              reduce (k, e, ens, (List.nth pl (j-1)), s)
-           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
+             (k', e', ens', C.MutConstruct (_,_,j,_), []) ->
+              reduce (k, e, ens, (List.nth pl (j-1)), [])
+           | (k', e', ens', C.MutConstruct (_,_,j,_), s') ->
               let (arity, r) =
                 let o,_ = 
                   CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind 
                 in
                   match o with
-                      C.InductiveDefinition (tl,ingredients,r,_) ->
-                        let (_,_,arity,_) = List.nth tl i in
+                      C.InductiveDefinition (s,ingredients,r,_) ->
+                        let (_,_,arity,_) = List.nth s i in
                           (arity,r)
                     | _ -> raise WrongUriToInductiveDefinition
               in
@@ -678,146 +656,116 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
                  let rec eat_first =
                   function
                      (0,l) -> l
-                   | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
+                   | (n,he::s) when n > 0 -> eat_first (n - 1, s)
                    | _ -> raise (Impossible 5)
                  in
-                  eat_first (num_to_eat,tl)
+                  eat_first (num_to_eat,s')
                in
-                (* ts are already unwinded because they are a sublist of tl *)
-                reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
-           | C.Cast _ | C.Implicit _ ->
+                reduce (k, e, ens, (List.nth pl (j-1)), ts@s)
+           | (_, _, _, C.Cast _, _)
+           | (_, _, _, C.Implicit _, _) ->
               raise (Impossible 2) (* we don't trust our whd ;-) *)
-           | _ ->
-             let t' = unwind k e ens t in
-              if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
-         )
-     | (k, e, ens, (C.Fix (i,fl) as t), s) ->
+           | config' ->
+              (*CSC: here I am unwinding the configuration and for sure I
+                will do it twice; to avoid this unwinding I should push the
+                "match [] with _" continuation on the stack;
+                another possibility is to just return the original configuration,
+                partially undoing the weak-head computation *)
+              (*this code is uncorrect since term' lives in e' <> e
+              let term' = unwind config' in
+               (k, e, ens, C.MutCase (mutind,i,outty,term',pl),s)
+              *)
+              config)
+     | (k, e, ens, C.Fix (i,fl), s) as config ->
         let (_,recindex,_,body) = List.nth fl i in
          let recparam =
           try
-           Some (RS.from_stack ~unwind (List.nth s recindex))
+           Some (RS.from_stack (List.nth s recindex))
           with
            _ -> None
          in
           (match recparam with
               Some recparam ->
-               (match reduce (0,[],[],recparam,[]) with
-                   (* match recparam with *) 
-                   C.MutConstruct _
-                 | C.Appl ((C.MutConstruct _)::_) ->
-                    (* OLD 
-                    let body' =
-                     let counter = ref (List.length fl) in
-                      List.fold_right
-                       (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
-                       fl
-                       body
-                    in 
-                     reduce (k, e, ens, body', s) *)
-                    (* NEW *)
+               (match reduce recparam with
+                   (_,_,_,C.MutConstruct _,_) as config ->
                     let leng = List.length fl in
-                    let fl' = 
-                     let unwind_fl (name,recindex,typ,body) = 
-                      (name,recindex,unwind k e ens typ,
-                        unwind' leng k e ens body)
+                    let new_env =
+                     let counter = ref 0 in
+                     let rec build_env e =
+                      if !counter = leng then e
+                      else
+                       (incr counter ;
+                        build_env
+                         ((RS.to_env (k,e,ens,C.Fix (!counter -1, fl),[]))::e))
                      in
-                      List.map unwind_fl fl
+                      build_env e
                     in
-                     let new_env =
-                      let counter = ref 0 in
-                      let rec build_env e =
-                       if !counter = leng then e
-                       else
-                        (incr counter ;
-                         build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e))
-                      in
-                       build_env e
-                     in
-                      reduce (k+leng, new_env, ens, body, s)  
-                 | _ ->
-                   let t' = unwind k e ens t in 
-                    if s = [] then t' else
-                     C.Appl (t'::(RS.from_stack_list ~unwind s))
-               )
-            | None ->
-               let t' = unwind k e ens t in 
-                if s = [] then t' else
-                 C.Appl (t'::(RS.from_stack_list ~unwind s))
+                    let rec replace i s t =
+                     match i,s with
+                        0,_::tl -> t::tl
+                      | n,he::tl -> he::(replace (n - 1) tl t)
+                      | _,_ -> assert false in
+                    let new_s =
+                     replace recindex s (RS.compute_to_stack ~reduce ~unwind config)
+                    in
+                     reduce (k+leng, new_env, ens, body, new_s)
+                 | _ -> config)
+            | None -> config
           )
-     | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
-        let t' = unwind k e ens t in 
-         if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+     | (_,_,_,C.CoFix _,_) as config -> config
    and push_exp_named_subst k e ens =
     function
        [] -> ens
      | (uri,t)::tl ->
-         push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
+         push_exp_named_subst k e ((uri,RS.to_ens (k,e,ens,t,[]))::ens) tl
    in
-     reduce 
-  ;;
-  (*
-  let rec whd context t = 
-    try 
-      reduce context (0, [], [], t, [])
-    with Not_found -> 
-      debug_print (lazy (CicPp.ppterm t)) ; 
-      raise Not_found
+    reduce
   ;;
-  *)
 
-  let rec whd ?(delta=true) ?(subst=[]) context t = 
-    reduce ~delta ~subst context (0, [], [], t, [])
+  let whd ?(delta=true) ?(subst=[]) context t = 
+   unwind (reduce ~delta ~subst context (0, [], [], t, []))
   ;;
 
-  
-(* DEBUGGING ONLY
-let whd context t =
- let res = whd context t in
- let rescsc = CicReductionNaif.whd context t in
-  if not (CicReductionNaif.are_convertible context res rescsc) then
-   begin
-    debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
-    flush stderr ;
-    debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
-    flush stderr ;
-    debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
-    flush stderr ;
-CicReductionNaif.fdebug := 0 ;
-let _ =  CicReductionNaif.are_convertible context res rescsc in
-    assert false ;
-   end
-  else 
-   res
-;;
-*)
  end
 ;;
 
 
-(*
-module R = Reduction CallByNameStrategy;;
-module R = Reduction CallByValueStrategy;;
-module R = Reduction CallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByValueStrategy;;
-module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByNameStrategy;;
+(* ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
+           senza ridurre la testa
+module R = Reduction CallByNameStrategy;; OK 56.368s
+module R = Reduction CallByValueStrategy;; ROTTO
+module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
+module R = Reduction LazyCallByValueStrategy;; ROTTO
+module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
+module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
 module R = Reduction
  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
-module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
+ OK 59.058s
+module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
 module R = Reduction
- ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
+ ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
+module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 *)
-module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
+module R = Reduction(CallByValueByNameForUnwind);;
+(*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*)
 module U = UriManager;;
 
-let whd = R.whd;;
+let whd = R.whd
+
+(*
+let whd =
+ let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
+  fun ?(delta=true) ?(subst=[]) context t ->
+   profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
+*)
 
   (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
     * fallbacks to structural equality *)
-let (===) x y = (Pervasives.compare x y = 0)
+let (===) x y =
+  Pervasives.compare x y = 0
 
 (* t1, t2 must be well-typed *)
-let are_convertible ?(subst=[]) ?(metasenv=[])  =
+let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
  let rec aux test_equality_only context t1 t2 ugraph =
   let aux2 test_equality_only t1 t2 ugraph =
 
@@ -1016,37 +964,58 @@ let are_convertible ?(subst=[]) ?(metasenv=[])  =
             else
               false,ugraph
         | (C.Cast _, _) | (_, C.Cast _)
-        | (C.Implicit _, _) | (_, C.Implicit _) ->
-            assert false
+        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
         | (_,_) -> false,ugraph
     end
   in
-     begin
-     debug t1 [t2] "PREWHD";
-     (* 
-     (match t1 with 
-         Cic.Meta _ -> 
-           debug_print (lazy (CicPp.ppterm t1));
-           debug_print (lazy (CicPp.ppterm (whd ~subst context t1)));
-           debug_print (lazy (CicPp.ppterm t2));
-           debug_print (lazy (CicPp.ppterm (whd ~subst context t2)))
-       | _ -> ()); *)
-     let t1' = whd ~subst context t1 in
-     let t2' = whd ~subst context t2 in
-      debug t1' [t2'] "POSTWHD";
-      aux2 test_equality_only t1' t2' ugraph
-    end
+   debug t1 [t2] "PREWHD";
+   let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
+   let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
+    debug t1' [t2'] "POSTWHD";
+    aux2 test_equality_only t1' t2' ugraph
  in
   aux false (*c t1 t2 ugraph *)
 ;;
 
+(* DEBUGGING ONLY
+let whd ?(delta=true) ?(subst=[]) context t = 
+ let res = whd ~delta ~subst context t in
+ let rescsc = CicReductionNaif.whd ~delta ~subst context t in
+  if not (fst (are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph)) then
+   begin
+    debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
+    flush stderr ;
+    debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
+    flush stderr ;
+    debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
+    flush stderr ;
+fdebug := 0 ;
+let _ =  are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph in
+    assert false ;
+   end
+  else 
+   res
+;;
+*)
+
+let are_convertible = are_convertible whd
+
+let whd = R.whd
+
+(*
+let profiler_other_whd = HExtlib.profile ~enable:profile "~are_convertible.whd"
+let whd ?(delta=true) ?(subst=[]) context t = 
+ let foo () =
+  whd ~delta ~subst context t
+ in
+  profiler_other_whd.HExtlib.profile foo ()
+*)
 
 let rec normalize ?(delta=true) ?(subst=[]) ctx term =
   let module C = Cic in
   let t = whd ~delta ~subst ctx term in
   let aux = normalize ~delta ~subst in
   let decl name t = Some (name, C.Decl t) in
-  let def  name t = Some (name, C.Def (t,None)) in
   match t with
   | C.Rel n -> t
   | C.Var (uri,exp_named_subst) ->