From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 22 May 2006 15:06:42 +0000 (+0000)
Subject: - code cleanup, especialli in Indexing where all the goal related functions have
X-Git-Tag: make_still_working~7342
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=942023d1f147318b7869f40fb1556c2d69f3d731;p=helm.git

- code cleanup, especialli in Indexing where all the goal related functions have
  been revised
- proofs are now factorized with LetIn
- support for profiling
---

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 521c7635c..c31538bda 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -228,10 +228,13 @@ let canonical t =
                   remove_refl p1
               | _ -> Cic.Appl (List.map remove_refl args))
     | Cic.Appl l -> Cic.Appl (List.map remove_refl l)
+    | Cic.LetIn (name,bo,rest) ->
+        Cic.LetIn (name,remove_refl bo,remove_refl rest)
     | _ -> t
   in
   let rec canonical t =
     match t with
+      | Cic.LetIn(name,bo,rest) -> Cic.LetIn(name,canonical bo,canonical rest)
       | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
           when LibraryObjects.is_sym_eq_URI uri_sym ->
           (match p_of_sym ens tl with
@@ -315,6 +318,9 @@ let contextualize uri ty left right t =
    * ctx is a term with an open (Rel 1). (Rel 1) is the empty context
    *)
     let rec aux uri ty left right ctx_d = function
+      | Cic.LetIn (name,body,rest) ->
+          (* we should go in body *)
+          Cic.LetIn (name,body,aux uri ty left right ctx_d rest)
       | Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
         when LibraryObjects.is_eq_ind_URI uri_ind || 
              LibraryObjects.is_eq_ind_r_URI uri_ind ->
@@ -392,12 +398,15 @@ let contextualize_rewrites t ty =
   contextualize eq ty l r t
 ;;
   
-let build_proof_step subst p1 p2 pos l r pred =
-  let p1 = Subst.apply_subst subst p1 in
-  let p2 = Subst.apply_subst subst p2 in
-  let l  = Subst.apply_subst subst l in
-  let r  = Subst.apply_subst subst r in
-  let pred = Subst.apply_subst subst pred in
+let build_proof_step lift subst p1 p2 pos l r pred =
+  let p1 = Subst.apply_subst_lift lift subst p1 in
+  let p2 = Subst.apply_subst_lift lift subst p2 in
+  let l  = CicSubstitution.lift lift l in
+  let l = Subst.apply_subst_lift lift subst l in
+  let r  = CicSubstitution.lift lift r in
+  let r = Subst.apply_subst_lift lift subst r in
+  let pred = CicSubstitution.lift lift pred in
+  let pred = Subst.apply_subst_lift lift subst pred in
   let ty,body = 
     match pred with
       | Cic.Lambda (_,ty,body) -> ty,body 
@@ -413,17 +422,38 @@ let build_proof_step subst p1 p2 pos l r pred =
         mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
 ;;
 
-let build_proof_term proof =
-  let rec aux = function
-     | Exact term -> term
-     | Step (subst,(_, id1, (pos,id2), pred)) ->
-         let p,_,_ = proof_of_id id1 in
-         let p1 = aux p in
-         let p,l,r = proof_of_id id2 in
-         let p2 = aux p in
-           build_proof_step subst p1 p2 pos l r pred
+let parametrize_proof p ty = 
+  let parameters = CicUtil.metas_of_term p in (* ?if they are under a lambda? *)
+  let parameters = 
+    HExtlib.list_uniq (List.sort Pervasives.compare parameters) 
   in
-   aux proof
+  let what = List.map (fun (i,l) -> Cic.Meta (i,l)) parameters in 
+  let with_what, lift_no = 
+    List.fold_right (fun _ (acc,n) -> ((Cic.Rel n)::acc),n+1) what ([],1) 
+  in
+  let p = CicSubstitution.lift (lift_no-1) p in
+  let p = 
+    ProofEngineReduction.replace_lifting
+    ~equality:(=) ~what ~with_what ~where:p
+  in
+  let ty_of_m _ = ty (*function 
+    | Cic.Meta (i,_) -> List.assoc i menv 
+    | _ -> assert false *)
+  in
+  let args, proof,_ = 
+    List.fold_left 
+      (fun (instance,p,n) m -> 
+        (instance@[m],
+        Cic.Lambda 
+          (Cic.Name ("x"^string_of_int n),
+          CicSubstitution.lift (lift_no - n - 1) (ty_of_m m),
+          p),
+        n+1)) 
+      ([Cic.Rel 1],p,1) 
+      what
+  in
+  let instance = match args with | [x] -> x | _ -> Cic.Appl args in
+  proof, instance
 ;;
 
 let wfo goalproof proof =
@@ -465,23 +495,104 @@ let pp_proof names goalproof proof =
       ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
 ;;
 
+(* returns the list of ids that should be factorized *)
+let get_duplicate_step_in_wfo l p =
+  let ol = List.rev l in
+  let h = Hashtbl.create 13 in
+  let add i n = 
+    let p,_,_ = proof_of_id i in 
+    match p with 
+    | Exact _ -> ()
+    | _ -> 
+        try let (pos,no) = Hashtbl.find h i in Hashtbl.replace h i (pos,no+1)
+        with Not_found -> Hashtbl.add h i (n,1)
+  in
+  let rec aux n = function
+    | Exact _ -> n
+    | Step (_,(_,i1,(_,i2),_)) -> 
+        add i1 n;add i2 n;
+        max (aux (n+1) (let p,_,_ = proof_of_id i1 in p))
+          (aux (n+1) (let p,_,_ = proof_of_id i2 in p))
+  in
+  let i = aux 0 p in 
+  let _ = 
+    List.fold_left 
+      (fun acc (_,id,_,_) -> aux acc (let p,_,_ = proof_of_id id in p))
+      i ol
+  in
+  (* now h is complete *)
+  let proofs = Hashtbl.fold (fun k (pos,count) acc->(k,pos,count)::acc) h [] in
+  let proofs = List.filter (fun (_,_,c) -> c > 1) proofs in
+  let proofs = 
+    List.sort (fun (_,c1,_) (_,c2,_) -> Pervasives.compare c2 c1) proofs 
+  in
+  List.map (fun (i,_,_) -> i) proofs
+;;
+
+let build_proof_term h lift proof =
+  let proof_of_id aux id =
+    let p,l,r = proof_of_id id in
+    try List.assoc id h,l,r with Not_found -> aux p, l, r
+  in
+  let rec aux = function
+     | Exact term -> CicSubstitution.lift lift term
+     | Step (subst,(_, id1, (pos,id2), pred)) ->
+         if Subst.is_in_subst 9 subst then
+           prerr_endline (Printf.sprintf "ID %d-%d has: %s\n" id1 id2 (Subst.ppsubst
+           subst));
+         let p1,_,_ = proof_of_id aux id1 in
+         let p2,l,r = proof_of_id aux id2 in
+           build_proof_step lift subst p1 p2 pos l r pred
+  in
+   aux proof
+;;
+
 let build_goal_proof l initial ty se =
   let se = List.map (fun i -> Cic.Meta (i,[])) se in 
+  let lets = get_duplicate_step_in_wfo l initial in
+  let letsno = List.length lets in
+  let _,mty,_,_ = open_eq ty in
+  let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l 
+  in
+  let lets,_,h = 
+    List.fold_left
+      (fun (acc,n,h) id -> 
+        let p,_,_ = proof_of_id id in
+        let cic = build_proof_term h n p in
+        let real_cic,instance = 
+          parametrize_proof cic (CicSubstitution.lift n mty)
+        in
+        let h = (id, instance)::lift_list h in
+        acc@[id,real_cic],n+1,h) 
+      ([],0,[]) lets
+  in
   let proof,se = 
     let rec aux se current_proof = function
       | [] -> current_proof,se
       | (pos,id,subst,pred)::tl ->
            let p,l,r = proof_of_id id in
-           let p = build_proof_term p in
+           let p = build_proof_term h letsno p in
            let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
-           let proof = build_proof_step subst current_proof p pos l r pred in
+           let proof = 
+             build_proof_step letsno subst current_proof p pos l r pred 
+           in
            let proof,se = aux se proof tl in
-           Subst.apply_subst subst proof,
-           List.map (fun x -> Subst.apply_subst subst x) se
+           Subst.apply_subst_lift letsno subst proof,
+           List.map (fun x -> Subst.apply_subst_lift letsno subst x) se
     in
-    aux se initial l
+    aux se (build_proof_term h letsno initial) l
+  in
+  let n,proof = 
+    let initial = proof in
+    List.fold_right
+      (fun (id,cic) (n,p) -> 
+        n-1,
+        Cic.LetIn (
+          Cic.Name ("H"^string_of_int id),
+          cic, p))
+    lets (letsno-1,initial)
   in
-  canonical (contextualize_rewrites proof ty), se
+  canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), se
 ;;
 
 let refl_proof ty term = 
@@ -492,7 +603,7 @@ let refl_proof ty term =
 ;;
 
 let metas_of_proof p =
-  let p = build_proof_term p in
+  let p = build_proof_term [] 0 p in
   Utils.metas_of_term p
 ;;
 
@@ -515,10 +626,6 @@ let relocate newmeta menv =
 
 let fix_metas newmeta eq = 
   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
-  (* debug 
-  let _ , eq = 
-    fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
-  prerr_endline (string_of_equality eq); *)
   let subst, metasenv, newmeta = relocate newmeta menv in
   let ty = Subst.apply_subst subst ty in
   let left = Subst.apply_subst subst left in
@@ -530,7 +637,6 @@ let fix_metas newmeta eq =
   in
   let p = fix_proof p in
   let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in
-  (* debug prerr_endline (string_of_equality eq); *)
   newmeta+1, eq  
 
 exception NotMetaConvertible;;
diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli
index c86cbdeac..6b5e34af9 100644
--- a/helm/software/components/tactics/paramodulation/equality.mli
+++ b/helm/software/components/tactics/paramodulation/equality.mli
@@ -57,14 +57,12 @@ val compare : equality -> equality -> int
 val string_of_equality : ?env:Utils.environment -> equality -> string
 val string_of_proof : 
   ?names:(Cic.name option)list -> proof -> goal_proof -> string
-val build_proof_term: 
-  proof -> Cic.term
 (* given a proof and a list of meta indexes we are interested in the
  * instantiation gives back the cic proof and the list of instantiations *)  
 (* build_goal_proof [goal_proof] [initial_proof] [ty] 
  *  [ty] is the type of the goal *)
 val build_goal_proof: 
-  goal_proof -> Cic.term -> Cic.term-> int list -> Cic.term * Cic.term list
+  goal_proof -> proof -> Cic.term-> int list -> Cic.term * Cic.term list
 val refl_proof: Cic.term -> Cic.term -> Cic.term 
 (** ensures that metavariables in equality are unique *)
 val fix_metas: int -> equality -> int * equality
diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index d35fbff34..a2e6eda07 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let _profiler = <:profiler<_profiler>>;;
+
 (* $Id$ *)
 
 type goal = Equality.goal_proof * Cic.metasenv * Cic.term
@@ -32,8 +34,6 @@ module Index = Equality_indexing.DT (* discrimination tree based indexing *)
 module Index = Equality_indexing.DT (* path tree based indexing *)
 *)
 
-let beta_expand_time = ref 0.;;
-
 let debug_print = Utils.debug_print;;
 
 (* 
@@ -92,9 +92,6 @@ let print_candidates ?env mode term res =
 ;;
 
 
-let indexing_retrieval_time = ref 0.;;
-
-
 let apply_subst = Subst.apply_subst
 
 let index = Index.index
@@ -182,32 +179,14 @@ let check_target context target msg =
 *)
 
 let get_candidates ?env mode tree term =
-  let t1 = Unix.gettimeofday () in
-  let res =
-    let s = 
-      match mode with
-      | Matching -> Index.retrieve_generalizations tree term
-      | Unification -> Index.retrieve_unifiables tree term
-    in
-    Index.PosEqSet.elements s
+  let s = 
+    match mode with
+    | Matching -> Index.retrieve_generalizations tree term
+    | Unification -> Index.retrieve_unifiables tree term
   in
-(*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
-(*   print_newline (); *)
-  let t2 = Unix.gettimeofday () in
-  indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1); 
- (* make fresh instances *)
-  res 
+  Index.PosEqSet.elements s
 ;;
 
-let profiler = HExtlib.profile "P/Indexing.get_candidates"
-
-let get_candidates ?env mode tree term =
-  profiler.HExtlib.profile (get_candidates ?env mode tree) term
-
-let match_unif_time_ok = ref 0.;;
-let match_unif_time_no = ref 0.;;
-
-
 (*
   finds the first equality in the index that matches "term", of type "termty"
   termty can be Implicit if it is not needed. The result (one of the sides of
@@ -252,11 +231,13 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
             let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
             let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
             let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
+(*
             let p="proof = "^
               (CicPp.ppterm(Equality.build_proof_term proof))^"\n" 
             in
+*)
               check_for_duplicates metas "gia nella metas";
-              check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
+              check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*))
           end;
         if check && not (fst (CicReduction.are_convertible
                                 ~metasenv context termty ty ugraph)) then (
@@ -264,21 +245,8 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
         ) else
           let do_match c eq_URI =
             let subst', metasenv', ugraph' =
-              let t1 = Unix.gettimeofday () in
-              try
-                let r =
-                  ( Inference.matching metasenv metas context 
-                    term (S.lift lift_amount c)) ugraph
-                in
-                let t2 = Unix.gettimeofday () in
-                match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
-                r
-              with 
-                | Inference.MatchingFailure as e ->
-                let t2 = Unix.gettimeofday () in
-                match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
-                  raise e
-                | CicUtil.Meta_not_found _ as exn -> raise exn
+              Inference.matching 
+                metasenv metas context term (S.lift lift_amount c) ugraph
             in
             Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph',
                   (candidate, eq_URI))
@@ -318,6 +286,10 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
                 find_matches metasenv context ugraph lift_amount term termty tl
 ;;
 
+let find_matches metasenv context ugraph lift_amount term termty =
+  find_matches metasenv context ugraph lift_amount term termty
+;;
+
 (*
   as above, but finds all the matching equalities, and the matching condition
   can be either Inference.matching or Inference.unification
@@ -337,36 +309,9 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
         let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
         let do_match c eq_URI =
           let subst', metasenv', ugraph' =
-            let t1 = Unix.gettimeofday () in
-            try
-                let term = 
-                  match c,term with
-                  | Cic.Meta _, Cic.Appl[Cic.MutInd(u,0,_);_;l;r] 
-                    when  LibraryObjects.is_eq_URI u -> l
-(*
-                      if Utils.compare_weights (Utils.weight_of_term l)
-                         (Utils.weight_of_term r) = Utils.Gt 
-                      then l else r
-*)
-                  | _ -> term
-                in
-              
-              let r = 
-                unif_fun metasenv metas context
-                  term (S.lift lift_amount c) ugraph in
-              let t2 = Unix.gettimeofday () in
-              match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
-              r
-            with
-            | Inference.MatchingFailure
-            | CicUnification.UnificationFailure _
-            | CicUnification.Uncertain _ as e ->
-                let t2 = Unix.gettimeofday () in
-                match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
-                raise e
+            unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
           in
-          (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
-           (candidate, eq_URI))
+          (C.Rel (1+lift_amount),subst',metasenv',ugraph',(candidate, eq_URI))
         in
         let c, other, eq_URI =
           if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
@@ -408,24 +353,22 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
 let find_all_matches 
   ?unif_fun metasenv context ugraph lift_amount term termty l 
 =
-  let rc = 
     find_all_matches 
       ?unif_fun metasenv context ugraph lift_amount term termty l 
-  in
   (*prerr_endline "CANDIDATES:";
   List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
   prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
   (List.length rc));*)
-  rc
-
+;;
 (*
   returns true if target is subsumed by some equality in table
 *)
+let print_res l =
+  prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
+    ((pos,equation),_)) -> Equality.string_of_equality equation)l))
+;;
+
 let subsumption_aux use_unification env table target = 
-(*  let print_res l =*)
-(*    prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,*)
-(*    ((pos,equation),_)) -> Equality.string_of_equality equation)l))*)
-(*  in*)
   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
   let metasenv, context, ugraph = env in
   let metasenv = tmetas in
@@ -443,7 +386,6 @@ let subsumption_aux use_unification env table target =
         find_all_matches ~unif_fun
           metasenv context ugraph 0 left ty leftc
   in
-(*  print_res leftr;*)
   let rec ok what = function
     | [] -> None
     | (_, subst, menv, ug, ((pos,equation),_))::tl ->
@@ -472,17 +414,16 @@ let subsumption_aux use_unification env table target =
                 find_all_matches ~unif_fun
                   metasenv context ugraph 0 right ty rightc
       in
-(*        print_res rightr;*)
         ok left rightr
-(*     (if r then  *)
-(*        debug_print  *)
-(*          (lazy *)
-(*             (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
-(*                (Inference.string_of_equality target) (Utils.print_subst s)))); *)
 ;;
 
-let subsumption = subsumption_aux false;;
-let unification = subsumption_aux true;;
+let subsumption x y z =
+  subsumption_aux false x y z
+;;
+
+let unification x y z = 
+  subsumption_aux true x y z
+;;
 
 let rec demodulation_aux ?from ?(typecheck=false) 
   metasenv context ugraph table lift_amount term =
@@ -583,16 +524,8 @@ let rec demodulation_aux ?from ?(typecheck=false)
   res
 ;;
 
-
-let build_newtarget_time = ref 0.;;
-
-
-let demod_counter = ref 1;;
-
 exception Foo
 
-let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
-
 (** demodulation, when target is an equality *)
 let rec demodulation_equality ?from newmeta env table sign target =
   let module C = Cic in
@@ -617,7 +550,6 @@ let rec demodulation_equality ?from newmeta env table sign target =
   let maxmeta = ref newmeta in
   
   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
-    let time1 = Unix.gettimeofday () in
     
     if Utils.debug_metas then
       begin
@@ -639,7 +571,6 @@ let rec demodulation_equality ?from newmeta env table sign target =
         Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 (*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
       let name = C.Name "x" in
-      incr demod_counter;
       let bo' =
         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
           C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
@@ -707,6 +638,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
 *)
     in
     let newmenv = (* Inference.filter subst *) menv in
+(*
     let _ = 
       if Utils.debug_metas then 
         try ignore(CicTypeChecker.type_of_aux'
@@ -727,22 +659,18 @@ let rec demodulation_equality ?from newmeta env table sign target =
           raise exc;
       else () 
     in
+*)
     let left, right = if is_left then newterm, right else left, newterm in
     let ordering = !Utils.compare_terms left right in
     let stat = (eq_ty, left, right, ordering) in
-    let time2 = Unix.gettimeofday () in
-    build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
     let res =
       let w = Utils.compute_equality_weight stat in
-      Equality.mk_equality (w, newproof, stat,newmenv) 
+          (Equality.mk_equality (w, newproof, stat,newmenv))
     in
     if Utils.debug_metas then 
       ignore(check_target context res "buildnew_target output");
     !maxmeta, res 
   in
-  let build_newtarget is_left x =
-    profiler.HExtlib.profile (build_newtarget is_left) x
-  in
 
   let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
   if Utils.debug_res then check_res res "demod result";
@@ -779,12 +707,13 @@ let rec demodulation_equality ?from newmeta env table sign target =
    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
    in table.
 *)
-let rec betaexpand_term metasenv context ugraph table lift_amount term =
+let rec betaexpand_term 
+  ?(subterms_only=false) metasenv context ugraph table lift_amount term 
+=
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
-  let candidates = get_candidates Unification table term in
   
   let res, lifted_term = 
     match term with
@@ -892,88 +821,17 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term =
         C.Implicit None, ugraph
 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
       in
+      let candidates = get_candidates Unification table term in
       let r = 
-        find_all_matches
-          metasenv context ugraph lift_amount term termty candidates
+        if subterms_only then 
+          [] 
+        else 
+          find_all_matches
+            metasenv context ugraph lift_amount term termty candidates
       in
       r @ res, lifted_term
 ;;
 
-let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
-
-let betaexpand_term metasenv context ugraph table lift_amount term =
-  profiler.HExtlib.profile 
-    (betaexpand_term metasenv context ugraph table lift_amount) term
-
-
-let sup_l_counter = ref 1;;
-
-(**
-   superposition_left 
-   returns a list of new clauses inferred with a left superposition step
-   the negative equation "target" and one of the positive equations in "table"
-*)
-let fix_expansion (eq,ty,unchanged,posu) (t, subst, menv, ug, eq_f) = 
-  let unchanged = CicSubstitution.lift 1 unchanged in
-  let ty = CicSubstitution.lift 1 ty in
-  let pred = 
-    match posu with
-    | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
-    | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
-  in
-  (pred, subst, menv, ug, eq_f)
-;;
-  
-let build_newgoal context goalproof goal_info expansion =
-  let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal_info expansion in
-  let pos, equality = eq_found in
-  let (_, proof', (ty, what, other, _), menv',id) = 
-    Equality.open_equality equality in
-  let what, other = if pos = Utils.Left then what, other else other, what in
-  let newterm, newgoalproof =
-    let bo = 
-      Utils.guarded_simpl context 
-        (apply_subst subst (CicSubstitution.subst other t)) 
-    in
-    let bo' = (*apply_subst subst*) t in 
-    let name = Cic.Name "x" in
-    let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
-    bo, (newgoalproofstep::goalproof)
-  in
-  let newmetasenv = (* Inference.filter subst *) menv in
-  (newgoalproof, newmetasenv, newterm)
-;;
-
-let superposition_left 
-  (metasenv, context, ugraph) table (proof,menv,ty)
-= 
-  let module C = Cic in
-  let module S = CicSubstitution in
-  let module M = CicMetaSubst in
-  let module HL = HelmLibraryObjects in
-  let module CR = CicReduction in
-  let module U = Utils in
-  let big,small,pos,eq,ty = 
-    match ty with
-    | Cic.Appl [eq;ty;l;r] ->
-       let c = 
-         Utils.compare_weights ~normalize:true
-           (Utils.weight_of_term l) (Utils.weight_of_term r)
-       in
-       (match c with 
-       | Utils.Gt -> l,r,Utils.Right,eq,ty
-       | _ -> r,l,Utils.Left,eq,ty)
-    | _ -> 
-        let names = Utils.names_of_context context in 
-        prerr_endline ("NON TROVO UN EQ: " ^ CicPp.pp ty names);
-        assert false
-  in
-  let expansions, _ = betaexpand_term menv context ugraph table 0 big in
-  List.map (build_newgoal context proof (eq,ty,small,pos)) expansions
-;;
-
-let sup_r_counter = ref 1;;
-
 (**
    superposition_right
    returns a list of new clauses inferred with a right superposition step
@@ -981,7 +839,9 @@ let sup_r_counter = ref 1;;
    the first free meta index, i.e. the first number above the highest meta
    index: its updated value is also returned
 *)
-let superposition_right newmeta (metasenv, context, ugraph) table target =
+let superposition_right 
+  ?(subterms_only=false) newmeta (metasenv, context, ugraph) table target 
+=
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -996,18 +856,11 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
   let metasenv' = newmetas in
   let maxmeta = ref newmeta in
   let res1, res2 =
-    let betaexpand_term metasenv context ugraph table d term =
-      let t1 = Unix.gettimeofday () in
-      let res = betaexpand_term metasenv context ugraph table d term in
-      let t2 = Unix.gettimeofday () in
-        beta_expand_time := !beta_expand_time  +. (t2 -. t1);
-        res
-    in
     match ordering with
     | U.Gt -> 
-        fst (betaexpand_term metasenv' context ugraph table 0 left), []
+        fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
     | U.Lt -> 
-        [], fst (betaexpand_term metasenv' context ugraph table 0 right)
+        [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
     | _ ->
         let res l r =
           List.filter
@@ -1015,14 +868,13 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
                let subst = apply_subst subst in
                let o = !Utils.compare_terms (subst l) (subst r) in
                o <> U.Lt && o <> U.Le)
-            (fst (betaexpand_term metasenv' context ugraph table 0 l))
+            (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
         in
         (res left right), (res right left)
   in
   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
     if Utils.debug_metas then 
       ignore (check_target context (snd eq_found) "buildnew1" );
-    let time1 = Unix.gettimeofday () in
     
     let pos, equality =  eq_found in
     let (_, proof', (ty, what, other, _), menv',id') = 
@@ -1035,7 +887,6 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
         Utils.guarded_simpl context (apply_subst s (S.subst other bo)) 
       in
       let name = C.Name "x" in
-      incr sup_r_counter;
       let bo'' =
         let l, r =
           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
@@ -1065,8 +916,6 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       newm, eq'
     in
     maxmeta := newmeta;
-    let time2 = Unix.gettimeofday () in
-    build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
     if Utils.debug_metas then 
       ignore(check_target context newequality "buildnew2"); 
     newequality
@@ -1078,47 +927,6 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
    (List.filter ok (new1 @ new2)))
 ;;
 
-(** demodulation, when the target is a goal *)
-let goal_metaconvertibility_eq (_,_,g1) (_,_,g2) = 
-  Equality.meta_convertibility g1 g2
-;;
-
-let rec demodulation_goal env table goal =
-  let metasenv, context, ugraph = env in
-  let goalproof, metas, term = goal in
-  let term = Utils.guarded_simpl (~debug:true) context term in
-  let goal = goalproof, metas, term in
-  let metasenv' = metas in
-
-  let left,right,eq,ty = 
-    match term with
-    | Cic.Appl [eq;ty;l;r] -> l,r,eq,ty
-    | _ -> assert false
-  in
-  let do_right () = 
-      let resright = demodulation_aux metasenv' context ugraph table 0 right in
-      match resright with
-      | Some t ->
-          let newg=build_newgoal context goalproof (eq,ty,left,Utils.Left) t in
-          if goal_metaconvertibility_eq goal newg then
-            false, goal
-          else
-            true, snd (demodulation_goal env table newg)
-      | None -> false, goal
-  in
-  let resleft =
-    demodulation_aux (*~typecheck:true*) metasenv' context ugraph table 0 left
-  in
-  match resleft with
-  | Some t ->
-      let newg = build_newgoal context goalproof (eq,ty,right,Utils.Right) t in
-      if goal_metaconvertibility_eq goal newg then
-        do_right ()
-      else
-        true, snd (demodulation_goal env table newg)
-  | None -> do_right ()
-;;
-
 (** demodulation, when the target is a theorem *)
 let rec demodulation_theorem newmeta env table theorem =
   let module C = Cic in
@@ -1139,7 +947,6 @@ let rec demodulation_theorem newmeta env table theorem =
       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 (*      let bo' = apply_subst subst t in *)
 (*      let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
-      incr demod_counter;
 (*
       let newproofold =
         Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
@@ -1167,3 +974,111 @@ let rec demodulation_theorem newmeta env table theorem =
       newmeta, theorem
 ;;
 
+(*****************************************************************************)
+(**                         OPERATIONS ON GOALS                             **)
+(**                                                                         **)
+(**                DEMODULATION_GOAL & SUPERPOSITION_LEFT                   **)
+(*****************************************************************************)
+
+let open_goal g =
+  match g with
+  | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) -> 
+      assert (LibraryObjects.is_eq_URI uri);
+      proof,menv,eq,ty,l,r
+  | _ -> assert false
+;;
+
+let ty_of_goal (_,_,ty) = ty ;;
+
+(* checks if two goals are metaconvertible *)
+let goal_metaconvertibility_eq g1 g2 = 
+  Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
+;;
+
+(* when the betaexpand_term function is called on the left/right side of the
+ * goal, the predicate has to be fixed
+ * C[x] ---> (eq ty unchanged C[x])
+ * [posu] is the side of the [unchanged] term in the original goal
+ *)
+let fix_expansion goal posu (t, subst, menv, ug, eq_f) = 
+  let _,_,eq,ty,l,r = open_goal goal in
+  let unchanged = if posu = Utils.Left then l else r in
+  let unchanged = CicSubstitution.lift 1 unchanged in
+  let ty = CicSubstitution.lift 1 ty in
+  let pred = 
+    match posu with
+    | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
+    | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
+  in
+  (pred, subst, menv, ug, eq_f)
+;;
+
+(* ginve the old [goal], the side that has not changed [posu] and the 
+ * expansion builds a new goal *)
+let build_newgoal context goal posu expansion =
+  let goalproof,_,_,_,_,_ = open_goal goal in
+  let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion in
+  let pos, equality = eq_found in
+  let (_, proof', (ty, what, other, _), menv',id) = 
+    Equality.open_equality equality in
+  let what, other = if pos = Utils.Left then what, other else other, what in
+  let newterm, newgoalproof =
+    let bo = 
+      Utils.guarded_simpl context 
+        (apply_subst subst (CicSubstitution.subst other t)) 
+    in
+    let bo' = (*apply_subst subst*) t in 
+    let name = Cic.Name "x" in
+    let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+    bo, (newgoalproofstep::goalproof)
+  in
+  let newmetasenv = (* Inference.filter subst *) menv in
+  (newgoalproof, newmetasenv, newterm)
+;;
+
+(**
+   superposition_left 
+   returns a list of new clauses inferred with a left superposition step
+   the negative equation "target" and one of the positive equations in "table"
+*)
+let superposition_left (metasenv, context, ugraph) table goal = 
+  let proof,menv,eq,ty,l,r = open_goal goal in
+  let c = 
+    Utils.compare_weights ~normalize:true
+      (Utils.weight_of_term l) (Utils.weight_of_term r)
+  in
+  let big,small,possmall = 
+    match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
+  in
+  let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+  List.map (build_newgoal context goal possmall) expansions
+;;
+
+(** demodulation, when the target is a goal *)
+let rec demodulation_goal env table goal =
+  let goalproof,menv,_,_,left,right = open_goal goal in
+  let metasenv, context, ugraph = env in
+(*  let term = Utils.guarded_simpl (~debug:true) context term in*)
+  let do_right () = 
+      let resright = demodulation_aux menv context ugraph table 0 right in
+      match resright with
+      | Some t ->
+          let newg = build_newgoal context goal Utils.Left t in
+          if goal_metaconvertibility_eq goal newg then
+            false, goal
+          else
+            true, snd (demodulation_goal env table newg)
+      | None -> false, goal
+  in
+  let resleft = demodulation_aux menv context ugraph table 0 left in
+  match resleft with
+  | Some t ->
+      let newg = build_newgoal context goal Utils.Right t in
+      if goal_metaconvertibility_eq goal newg then
+        do_right ()
+      else
+        true, snd (demodulation_goal env table newg)
+  | None -> do_right ()
+;;
+
+let get_stats () = <:show<Indexing.>> ;;
diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli
index 27ac1680a..fe8582e92 100644
--- a/helm/software/components/tactics/paramodulation/indexing.mli
+++ b/helm/software/components/tactics/paramodulation/indexing.mli
@@ -40,11 +40,7 @@ val index : Index.t -> Equality.equality -> Index.t
 val remove_index : Index.t -> Equality.equality -> Index.t
 val in_index : Index.t -> Equality.equality -> bool
 val empty : Index.t
-val match_unif_time_ok : float ref
-val match_unif_time_no : float ref
-val indexing_retrieval_time : float ref
 val init_index : unit -> unit
-val build_newtarget_time : float ref
 val unification :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
@@ -62,6 +58,7 @@ val superposition_left :
    goal list
 
 val superposition_right :
+  ?subterms_only:bool ->
   int ->
   'a * Cic.context * CicUniv.universe_graph ->
   Index.t ->
@@ -89,3 +86,5 @@ val check_target:
   Cic.context ->
     Equality.equality -> string -> unit
 
+    (** profiling *)
+val get_stats: unit -> string
diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index 272a81003..ccc73c351 100644
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/components/tactics/paramodulation/inference.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let _profiler = <:profiler<_profiler>>;;
+
 (* $Id$ *)
 
 open Utils;;
@@ -144,7 +146,7 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
         (lazy
            (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
               (CicPp.ppterm t1) (CicPp.ppterm t2)));
-      raise (CicUnification .UnificationFailure (lazy "Inference.unification.unif"))
+      raise (CicUnification.UnificationFailure (lazy "Inference.unification.unif"))
     ) else
       if b then
         (* full unification *)
@@ -170,22 +172,24 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
 
 exception MatchingFailure;;
 
-let matching1 metasenv1 metasenv2 context t1 t2 ugraph = 
+(** matching takes in input the _disjoint_ metasenv of t1 and  t2;
+it perform unification in the union metasenv, then check that
+the first metasenv has not changed *)
+let matching metasenv1 metasenv2 context t1 t2 ugraph = 
   try 
     unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
   with
-    CicUnification .UnificationFailure _ ->
+    CicUnification.UnificationFailure _ -> 
       raise MatchingFailure
 ;;
 
-let unification = unification_aux true 
+let unification m1 m2 c t1 t2 ug = 
+  try 
+    unification_aux true m1 m2 c t1 t2 ug
+  with exn -> 
+    raise exn
 ;;
 
-(** matching takes in input the _disjoint_ metasenv of t1 and  t2;
-it perform unification in the union metasenv, then check that
-the first metasenv has not changed *)
-
-let matching = matching1;;
 
 let check_eq context msg eq =
   let w, proof, (eq_ty, left, right, order), metas = eq in
@@ -484,4 +488,4 @@ let find_context_hypotheses env equalities_indexes =
   in
   res
 ;;
-
+let get_stats () = <:show<Inference.>> ;;
diff --git a/helm/software/components/tactics/paramodulation/inference.mli b/helm/software/components/tactics/paramodulation/inference.mli
index 9bfb84cb2..0de5e8433 100644
--- a/helm/software/components/tactics/paramodulation/inference.mli
+++ b/helm/software/components/tactics/paramodulation/inference.mli
@@ -75,3 +75,4 @@ val find_library_theorems:
 val find_context_hypotheses:
   Utils.environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list
 
+val get_stats: unit -> string
diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 5eb62666f..b5b727b4d 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -23,9 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(* $Id$ *)
+let _profiler = <:profiler<_profiler>>;;
 
-(* <:profiler<"saturation">> *)
+(* $Id$ *)
 
 open Inference;;
 open Utils;;
@@ -106,7 +106,7 @@ module OrderedEquality = struct
   let compare eq1 eq2 =
     match Equality.meta_convertibility_eq eq1 eq2 with
     | true -> 0
-    | false ->
+    | false -> 
         let w1, _, (ty,left, right, _), m1,_ = Equality.open_equality eq1 in
         let w2, _, (ty',left', right', _), m2,_ = Equality.open_equality eq2 in
         match Pervasives.compare w1 w2 with
@@ -342,8 +342,14 @@ let infer env current (active_list, active_table) =
     (ignore(Indexing.check_target c current "infer1");
      ignore(List.map (function current -> Indexing.check_target c current "infer2") active_list)); 
   let new_pos = 
-    let maxm, res =
-      Indexing.superposition_right !maxmeta env active_table current in
+      let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
+        maxmeta := maxm;
+      let active_table =  Indexing.index active_table copy_of_current in
+      let _ = <:start<current contro active>> in
+      let maxm, res =
+        Indexing.superposition_right !maxmeta env active_table current 
+      in
+      let _ = <:stop<current contro active>> in
       if Utils.debug_metas then
         ignore(List.map 
                  (function current -> 
@@ -353,7 +359,8 @@ let infer env current (active_list, active_table) =
         | [] -> []
         | equality::tl ->
             let maxm, res =
-              Indexing.superposition_right !maxmeta env table equality in
+              Indexing.superposition_right ~subterms_only:true !maxmeta env table equality 
+            in
               maxmeta := maxm;
               if Utils.debug_metas then
                 ignore
@@ -363,16 +370,19 @@ let infer env current (active_list, active_table) =
               let pos = infer_positive table tl in
               res @ pos
       in
+(*
       let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
         maxmeta := maxm;
+*)
       let curr_table = Indexing.index Indexing.empty current in
-      let pos = infer_positive curr_table (copy_of_current::active_list) 
-      in 
+      let _ = <:start<active contro current>> in
+      let pos = infer_positive curr_table ((*copy_of_current::*)active_list) in
+      let _ = <:stop<active contro current>> in
       if Utils.debug_metas then 
         ignore(List.map 
                  (function current -> 
                     Indexing.check_target c current "sup3") pos);
-        res @ pos
+      res @ pos
   in
   derived_clauses := !derived_clauses + (List.length new_pos);
   match !maximal_retained_equality with
@@ -389,8 +399,6 @@ let infer env current (active_list, active_table) =
 
 let check_for_deep_subsumption env active_table eq =
   let _,_,(eq_ty, left, right, order),metas,id = Equality.open_equality eq in
-  if id = 14242 then assert false;
-  
   let check_subsumed deep l r = 
     let eqtmp = 
       Equality.mk_tmp_equality(0,(eq_ty,l,r,Utils.Incomparable),metas)in
@@ -561,37 +569,28 @@ let forward_simplify_new env new_pos ?passive active =
         (fun current -> Indexing.check_target c current "forward new pos") 
       new_pos;)
     end;
-  let t1 = Unix.gettimeofday () in
-
   let active_list, active_table = active in
   let passive_table =
     match passive with
     | None -> None
     | Some ((_, _), pt) -> Some pt
   in
-  let t2 = Unix.gettimeofday () in
-  fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
-  
   let demodulate sign table target =
     let newmeta, newtarget =
       Indexing.demodulation_equality !maxmeta env table sign target in
     maxmeta := newmeta;
     newtarget
   in
-  let t1 = Unix.gettimeofday () in
   (* we could also demodulate using passive. Currently we don't *)
   let new_pos =
     List.map (demodulate Positive active_table) new_pos 
   in
-  let t2 = Unix.gettimeofday () in
-  fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
-
   let new_pos_set =
     List.fold_left
       (fun s e ->
          if not (Equality.is_identity env e) then
-           if EqualitySet.mem e s then s
-           else EqualitySet.add e s
+(*            if EqualitySet.mem e s then s *)
+           (*else*) EqualitySet.add e s
          else s)
       EqualitySet.empty new_pos
   in
@@ -617,7 +616,7 @@ let forward_simplify_new env new_pos ?passive active =
            not ((Indexing.in_index active_table e) ||
                   (Indexing.in_index passive_table e)))
   in
-  List.filter subs (List.filter is_duplicate new_pos)
+    List.filter subs (List.filter is_duplicate new_pos)
 ;;
 
 
@@ -1309,8 +1308,6 @@ let infer_goal_set env active goals =
         let selected = hd in
         let passive_goals = tl in
         let new' = Indexing.superposition_left env (snd active) selected in
-        let metasenv, context, ugraph = env in
-        let names = names_of_context context in
         selected::active_goals, passive_goals @ new'
     | _::tl -> aux tl
   in 
@@ -1355,11 +1352,14 @@ let given_clause
     else if Unix.gettimeofday () > max_time then
       (ParamodulationFailure "No more time to spend")
     else
+      let _ = prerr_endline "simpl goal with active" in
       let goals = simplify_goal_set env goals passive active in  
       match check_if_goals_set_is_solved env active goals with
       | Some p -> 
-          Printf.eprintf "Found a proof in: %f\n" 
-            (Unix.gettimeofday() -. initial_time);
+          prerr_endline 
+            (Printf.sprintf "Found a proof in: %f\n" 
+              (Unix.gettimeofday() -. initial_time));
+(*          assert false;*)
           ParamodulationSuccess p
       | None -> 
           prerr_endline 
@@ -1381,13 +1381,13 @@ let given_clause
           kept_clauses := (size_of_passive passive) + (size_of_active active);
           (* SELECTION *)
           if passive_is_empty passive then
-            ParamodulationFailure "No more passive" (* maybe this is a success! *)
+            ParamodulationFailure "No more passive"(*maybe this is a success! *)
           else
             begin
               let goals = infer_goal_set env active goals in
               let current, passive = select env goals passive in
-              Printf.eprintf  "Selected = %s\n"
-                (Equality.string_of_equality ~env current);
+              prerr_endline (Printf.sprintf  "Selected = %s\n"
+                (Equality.string_of_equality ~env current));
               (* SIMPLIFICATION OF CURRENT *)
               let res = 
                 forward_simplify env (Positive, current) ~passive active 
@@ -1396,23 +1396,24 @@ let given_clause
               | None -> step goals theorems passive active (iterno+1)
               | Some current ->
                   (* GENERATION OF NEW EQUATIONS *)
+                  prerr_endline "infer";
                   let new' = infer env current active in
+                  prerr_endline "infer goal";
                   let goals = infer_goal_set_with_current env current goals in
                   let active = 
-                    if Equality.is_identity env current then 
-                      assert false 
-                      (* nonsense code, check to se if it can be removed *)
-                    else
                       let al, tbl = active in
                       al @ [current], Indexing.index tbl current
                   in
                   (* FORWARD AND BACKWARD SIMPLIFICATION *)
+                  prerr_endline "fwd/back simpl";
                   let rec simplify new' active passive =
                     let new' = forward_simplify_new env new' ~passive active in
                     let active, passive, newa, retained, pruned =
                       backward_simplify env new' ~passive  active 
                     in
-                    let passive = List.fold_left filter_dependent passive pruned in
+                    let passive = 
+                      List.fold_left filter_dependent passive pruned 
+                    in
                     match newa, retained with
                     | None, None -> active, passive, new'
                     | Some p, None 
@@ -1420,6 +1421,7 @@ let given_clause
                     | Some p, Some rp -> simplify (new' @ p @ rp) active passive
                   in
                   let active, passive, new' = simplify new' active passive in
+                  prerr_endline "simpl goal with new";
                   let goals = 
                     let a,b,_ = build_table new' in
                     simplify_goal_set env goals passive (a,b)
@@ -1745,7 +1747,7 @@ let saturate
 *)
       let goals = make_goal_set goal in
       let max_iterations = 1000 in
-      let max_time = Unix.gettimeofday () +.  600. (* minutes *) in
+      let max_time = Unix.gettimeofday () +.  120. (* minutes *) in
       given_clause env goals theorems passive active max_iterations max_time 
     in
     let finish = Unix.gettimeofday () in
@@ -1766,7 +1768,7 @@ let saturate
             ~newmetasenv:metasenv ~oldmetasenv:proof_menv)
       in
       let goal_proof, side_effects_t = 
-        let initial = Equality.build_proof_term newproof in
+        let initial = newproof in
         Equality.build_goal_proof goalproof initial type_of_goal side_effects
       in
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
@@ -2037,7 +2039,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
   in
   if changed then
     begin
-      let opengoal = Cic.Meta(maxm,irl) in
+      let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
       let proofterm,_ = 
         Equality.build_goal_proof newproof opengoal ty [] in
         let extended_metasenv = (maxm,context,newty)::metasenv in
@@ -2059,3 +2061,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
 let demodulate_tac ~dbd ~pattern = 
   ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
 ;;
+
+let get_stats () = 
+  <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats ();;
+
diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli
index 95f258124..7a16895a7 100644
--- a/helm/software/components/tactics/paramodulation/saturation.mli
+++ b/helm/software/components/tactics/paramodulation/saturation.mli
@@ -51,3 +51,5 @@ val main: HMysql.dbd ->
 val demodulate_tac: 
   dbd:HMysql.dbd ->  
   pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+
+val get_stats: unit -> string
diff --git a/helm/software/components/tactics/paramodulation/subst.ml b/helm/software/components/tactics/paramodulation/subst.ml
index 819472a15..7e8ab8b18 100644
--- a/helm/software/components/tactics/paramodulation/subst.ml
+++ b/helm/software/components/tactics/paramodulation/subst.ml
@@ -76,7 +76,7 @@ let cic_merge_subst_if_possible s1 s2 =
 
 type naif_substitution = (int * Cic.term) list 
 
-let naif_apply_subst subst term =
+let naif_apply_subst lift subst term =
  let rec aux k t =
    match t with
        Cic.Rel _ -> t
@@ -87,7 +87,7 @@ let naif_apply_subst subst term =
            Cic.Var (uri, exp_named_subst')
     | Cic.Meta (i, l) -> 
         (try
-          aux k (CicSubstitution.lift k (List.assoc i subst)) 
+          aux k (CicSubstitution.lift (k+lift) (List.assoc i subst)) 
          with Not_found -> t)
     | Cic.Sort _
     | Cic.Implicit _ -> t
@@ -141,7 +141,7 @@ substitution to the context *)
 let naif_apply_subst_metasenv subst metasenv =
   List.map
     (fun (n, context, ty) ->
-      (n, context, naif_apply_subst subst ty))
+      (n, context, naif_apply_subst 0 subst ty))
     (List.filter
       (fun (i, _, _) -> not (List.mem_assoc i subst))
       metasenv)
@@ -157,7 +157,7 @@ let naif_ppsubst names subst =
 let naif_buildsubst n context t ty tail = (n,t) :: tail ;;
 
 let naif_flatten_subst subst = 
-  List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst
+  List.map (fun (i,t) -> i, naif_apply_subst 0 subst t ) subst
 ;;
 
 let rec naif_lookup_subst meta subst =
@@ -189,7 +189,8 @@ let naif_merge_subst_if_possible s1 s2 =
 (********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************)
 
 type substitution = naif_substitution
-let apply_subst = naif_apply_subst
+let apply_subst = naif_apply_subst 0
+let apply_subst_lift = naif_apply_subst
 let apply_subst_metasenv = naif_apply_subst_metasenv
 let ppsubst ?(names=[]) l = naif_ppsubst names l
 let buildsubst = naif_buildsubst
diff --git a/helm/software/components/tactics/paramodulation/subst.mli b/helm/software/components/tactics/paramodulation/subst.mli
index 9c124d963..6627bf067 100644
--- a/helm/software/components/tactics/paramodulation/subst.mli
+++ b/helm/software/components/tactics/paramodulation/subst.mli
@@ -27,6 +27,7 @@ type substitution
 
 val empty_subst : substitution
 val apply_subst : substitution -> Cic.term -> Cic.term
+val apply_subst_lift : int -> substitution -> Cic.term -> Cic.term
 val apply_subst_metasenv : substitution -> Cic.metasenv -> Cic.metasenv
 val ppsubst : ?names:(Cic.name option list) -> substitution -> string
 val buildsubst :