X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=40d07e414b644090362d3da6dabf2daf7ab6f785;hb=61f3a8a688132be943b81befa5805e27148f2038;hp=b5026d32079bcb435d6301da675e9f9b9969234a;hpb=9795c5698b48a9ce63fcf681fa63cb8f69cd1724;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index b5026d320..40d07e414 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -116,6 +116,10 @@ type result =
   | ParamodulationFailure of string * active_table * passive_table
   | ParamodulationSuccess of new_proof * active_table * passive_table
 ;;
+
+let list_of_passive (l,s) = l
+;;
+
 let make_passive eq_list =
   let set =
     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list
@@ -838,6 +842,29 @@ let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) =
   | _ -> None
 ;;
 
+let find_all_subsumed bag env table (goalproof,menv,ty) =
+  match ty with
+  | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
+    when LibraryObjects.is_eq_URI uri ->
+      let goal_equation = 
+        Equality.mk_equality bag
+          (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) 
+      in
+	List.map
+	  (fun (subst, equality, swapped ) ->
+	     let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
+             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
+             let p =
+	       if swapped then
+                 Equality.symmetric bag eq_ty l id uri m
+	       else
+                 p
+             in (goalproof, p, id, subst, cicmenv))
+	  (Indexing.unification_all env table goal_equation)
+  | _ -> assert false
+;;
+
+
 let check_if_goal_is_identity env = function
   | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) 
     when left = right && LibraryObjects.is_eq_URI uri ->
@@ -1367,146 +1394,71 @@ let build_proof
       final_subst, proof, open_goals
 ;;
 
-let find_equalities dbd status smart_flag ?auto cache =
-  let proof, goalno = status in
-  let _, metasenv,_,_ = proof in
-  let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
-  let eq_uri = eq_of_goal type_of_goal in 
-  let env = (metasenv, context, CicUniv.empty_ugraph) in 
-  let bag = Equality.mk_equality_bag () in
-  let eq_indexes, equalities, maxm, cache = 
-    Equality_retrieval.find_context_equalities 0 bag ?auto context proof cache
-  in
-  prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>";
-  List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
-  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
-  let lib_eq_uris, library_equalities, maxm, cache =
-    Equality_retrieval.find_library_equalities bag
-      ?auto smart_flag dbd context (proof, goalno) (maxm+2)
-      cache
-  in
-  prerr_endline (">>>>>>>>>>  gained from the library >>>>>>>>>>>>" ^
-    string_of_int maxm);
-  List.iter
-    (fun (_,e) -> prerr_endline (Equality.string_of_equality e)) 
-    library_equalities;
-  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
-  let equalities = List.map snd library_equalities @ equalities in
-  let equalities = 
-    simplify_equalities bag eq_uri env equalities
+
+(* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *)
+
+(* exported functions  *)
+
+let pump_actives context bag maxm active passive saturation_steps max_time =
+  reset_refs();
+  maxmeta := maxm;
+  let max_l l = 
+    List.fold_left 
+     (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in
+      List.fold_left (fun acc (i,_,_) -> max i acc) acc menv)
+     0 l in
+  let active_l = fst active in
+  let passive_l = fst passive in
+  let ma = max_l active_l in
+  let mp = max_l passive_l in
+  assert (maxm > max ma mp);  
+  let eq_uri = 
+    match LibraryObjects.eq_URI () with
+      | None -> assert false
+      | Some uri -> uri
   in 
-  prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
-  List.iter
-    (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
-  prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
-  bag, equalities, cache, maxm
+  let env = [],context,CicUniv.empty_ugraph in
+  match 
+    given_clause bag eq_uri env ([],[]) passive active 0 saturation_steps max_time
+  with
+  | ParamodulationFailure (_,a,p) ->
+      a, p, !maxmeta
+  | ParamodulationSuccess _ ->
+      assert false
 ;;
 
-let saturate_more bag active maxmeta status smart_flag ?auto cache =
-  let proof, goalno = status in
-  let _, metasenv,_,_ = proof in
-  let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
-  let eq_uri = eq_of_goal type_of_goal in 
-  let env = (metasenv, context, CicUniv.empty_ugraph) in 
-  let eq_indexes, equalities, maxm, cache = 
-    Equality_retrieval.find_context_equalities maxmeta bag ?auto context proof cache
-  in
-  prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
-    string_of_int maxm);
-  List.iter
-    (fun e -> prerr_endline (Equality.string_of_equality ~env e)) 
-    equalities;
-  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
-  let equalities = 
-    HExtlib.filter_map 
-      (fun e -> forward_simplify bag eq_uri env e active)
-    equalities
-  in
-  prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
-  List.iter
-    (fun e -> prerr_endline (Equality.string_of_equality ~env e)) equalities;
-  prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
-  bag, equalities, cache, maxm
-
-let saturate 
-    smart_flag 
-    dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) 
-    ?(timeout=600.) ?auto status = 
-  let module C = Cic in
-  reset_refs ();
-  maxdepth := depth;
-  maxwidth := width;
-(*  CicUnification.unif_ty := false;*)
+let all_subsumed bag maxm status active passive =
+  maxmeta := maxm;
   let proof, goalno = status in
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
-  let eq_uri = eq_of_goal type_of_goal in 
+  let env = metasenv,context,CicUniv.empty_ugraph in
   let cleaned_goal = Utils.remove_local_context type_of_goal in
-  Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
-  let ugraph = CicUniv.empty_ugraph in
-  let env = (metasenv, context, ugraph) in 
   let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
-  let bag, equalities, cache, maxm = 
-    find_equalities dbd status smart_flag ?auto AutoCache.cache_empty 
-  in
-  let res, time =
-    maxmeta := maxm+2;
-    let t1 = Unix.gettimeofday () in
-    let theorems =
-      let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in
-      let t = CicUtil.term_of_uri refl_equal in
-      let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
-      [(t, ty, [])], []
-    in
-    let t2 = Unix.gettimeofday () in
-    let _ =
-      Utils.debug_print
-        (lazy
-           (Printf.sprintf
-              "Theorems:\n-------------------------------------\n%s\n"
-              (String.concat "\n"
-                 (List.map
-                    (fun (t, ty, _) ->
-                       Printf.sprintf
-                         "Term: %s, type: %s"
-                         (CicPp.ppterm t) (CicPp.ppterm ty))
-                    (fst theorems)))));
-      Utils.debug_print
-        (lazy
-           (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
-    in
-    let active = make_empty_active () in
-    let passive = make_passive equalities in
-    let start = Unix.gettimeofday () in
-    let res =
-(*
-      let goals = make_goals goal in
-      given_clause_fullred dbd env goals theorems passive active
-*)
-      let goals = make_goal_set goal in
-      let max_iterations = 10000 in
-      let max_time = Unix.gettimeofday () +.  timeout (* minutes *) in
-      given_clause bag
-        eq_uri env goals passive active max_iterations max_iterations max_time 
-    in
-    let finish = Unix.gettimeofday () in
-    (res, finish -. start)
-  in
-  match res with
-  | ParamodulationFailure (s,_,_) ->
-      raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s)))
-  | ParamodulationSuccess 
-    ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),_,_) ->
-      prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
-    let _,p,gl = 
-      build_proof bag
-        status goalproof newproof subsumption_id subsumption_subst proof_menv
-    in
-    p,gl
-;;
-(* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *)
+  prerr_endline (string_of_int (List.length (fst active)));
+   (* we simplify using both actives passives *)
+  let table = 
+    List.fold_left 
+      (fun (l,tbl) eq -> eq::l,(Indexing.index tbl eq))
+      active (list_of_passive passive) in
+  let _,goal = simplify_goal bag env goal table in
+  let (_,_,ty) = goal in
+  prerr_endline (CicPp.ppterm ty);
+  let subsumed = find_all_subsumed bag env (snd table) goal in
+  let subsumed_or_id =
+    match (check_if_goal_is_identity env goal) with
+	None -> subsumed
+      | Some id -> id::subsumed in
+  let res =
+    List.map 
+      (fun 
+	 (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
+	     build_proof bag
+               status goalproof newproof subsumption_id subsumption_subst proof_menv)
+      subsumed_or_id in
+  res, !maxmeta
+
 
-(* exported version of given_clause *)
 let given_clause 
   bag maxm status active passive goal_steps saturation_steps max_time 
 =
@@ -1537,6 +1489,7 @@ let given_clause
   prerr_endline ">>>>>>>>>>>>>>"; 
   let goals = make_goal_set goal in
   match 
+(* given_caluse non prende in input maxm ????? *)
     given_clause bag eq_uri env goals passive active 
       goal_steps saturation_steps max_time
   with
@@ -1551,360 +1504,8 @@ let given_clause
     Some (subst, proof,gl),a,p, !maxmeta
 ;;
 
-let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = 
-  let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let eq_uri = eq_of_goal ty in
-  let bag = Equality.mk_equality_bag () in
-  let eq_indexes, equalities, maxm, cache = 
-    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty
-  in
-  let lib_eq_uris, library_equalities, maxm, cache =
-    Equality_retrieval.find_library_equalities bag 
-      false dbd context (proof, goal) (maxm+2)  cache 
-  in
-  if library_equalities = [] then prerr_endline "VUOTA!!!";
-  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-  let library_equalities = List.map snd library_equalities in
-  let initgoal = [], [], ty in
-  let env = (metasenv, context, CicUniv.empty_ugraph) in
-  let equalities = 
-    simplify_equalities bag eq_uri env (equalities@library_equalities) 
-  in   
-  let table = 
-    List.fold_left 
-      (fun tbl eq -> Indexing.index tbl eq) 
-      Indexing.empty equalities 
-  in
-  let changed,(newproof,newmetasenv, newty) = 
-    Indexing.demodulation_goal bag
-      (metasenv,context,CicUniv.empty_ugraph) table initgoal 
-  in
-  if changed then
-    begin
-      let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
-      let proofterm,_ = 
-        Equality.build_goal_proof bag
-          eq_uri newproof opengoal ty [] context metasenv
-      in
-        let extended_metasenv = (maxm,context,newty)::metasenv in
-        let extended_status = 
-          (curi,extended_metasenv,pbo,pty),goal in
-        let (status,newgoals) = 
-          ProofEngineTypes.apply_tactic 
-            (PrimitiveTactics.apply_tac ~term:proofterm)
-            extended_status in
-        (status,maxm::newgoals)
-    end
-  else (* if newty = ty then *)
-    raise (ProofEngineTypes.Fail (lazy "no progress"))
-  (*else ProofEngineTypes.apply_tactic 
-    (ReductionTactics.simpl_tac
-      ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
-;;
-
-let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);;
-
-let rec find_in_ctx i name = function
-  | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
-  | Some (Cic.Name name', _)::tl when name = name' -> i
-  | _::tl -> find_in_ctx (i+1) name tl
-;;
-
-let rec position_of i x = function
-  | [] -> assert false
-  | j::tl when j <> x -> position_of (i+1) x tl
-  | _ -> i
-;;
-
-(* Syntax: 
- *   auto superposition target = NAME 
- *     [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
- *
- *  - if table is omitted no superposition will be performed
- *  - if demod_table is omitted no demodulation will be prformed
- *  - subterms_only is passed to Indexing.superposition_right
- *
- *  lists are coded using _ (example: H_H1_H2)
- *)
-
-let superposition_tac ~target ~table ~subterms_only ~demod_table status = 
-  reset_refs();
-  let proof,goalno = status in 
-  let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
-  let eq_uri,tty = eq_and_ty_of_goal ty in
-  let env = (metasenv, context, CicUniv.empty_ugraph) in
-  let names = Utils.names_of_context context in
-  let bag = Equality.mk_equality_bag () in
-  let eq_index, equalities, maxm,cache  = 
-    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty 
-  in
-  let eq_what = 
-    let what = find_in_ctx 1 target context in
-    List.nth equalities (position_of 0 what eq_index)
-  in
-  let eq_other = 
-    if table <> "" then
-      let other = 
-        let others = Str.split (Str.regexp "_") table in 
-        List.map (fun other -> find_in_ctx 1 other context) others 
-      in
-      List.map 
-        (fun other -> List.nth equalities (position_of 0 other eq_index)) 
-        other 
-    else
-      []
-  in
-  let index = List.fold_left Indexing.index Indexing.empty eq_other in
-  let maxm, eql = 
-    if table = "" then maxm,[eq_what] else 
-    Indexing.superposition_right bag
-      ~subterms_only eq_uri maxm env index eq_what
-  in
-  prerr_endline ("Superposition right:");
-  prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env);
-  prerr_endline ("\n table: ");
-  List.iter (fun e -> prerr_endline ("  " ^ Equality.string_of_equality e ~env)) eq_other;
-  prerr_endline ("\n result: ");
-  List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
-  prerr_endline ("\n result (cut&paste): ");
-  List.iter 
-    (fun e -> 
-      let t = Equality.term_of_equality eq_uri e in
-      prerr_endline (CicPp.pp t names)) 
-  eql;
-  prerr_endline ("\n result proofs: ");
-  List.iter (fun e -> 
-    prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
-    let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
-    Subst.ppsubst s ^ "\n" ^ 
-    CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names)) eql;
-  if demod_table <> "" then
-    begin
-      let eql = 
-        if eql = [] then [eq_what] else eql
-      in
-      let demod = 
-        let demod = Str.split (Str.regexp "_") demod_table in 
-        List.map (fun other -> find_in_ctx 1 other context) demod 
-      in
-      let eq_demod = 
-        List.map 
-          (fun demod -> List.nth equalities (position_of 0 demod eq_index)) 
-          demod 
-      in
-      let table = List.fold_left Indexing.index Indexing.empty eq_demod in
-      let maxm,eql = 
-        List.fold_left 
-          (fun (maxm,acc) e -> 
-            let maxm,eq = 
-              Indexing.demodulation_equality bag eq_uri maxm env table e
-            in
-            maxm,eq::acc) 
-          (maxm,[]) eql
-      in
-      let eql = List.rev eql in
-      prerr_endline ("\n result [demod]: ");
-      List.iter 
-        (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
-      prerr_endline ("\n result [demod] (cut&paste): ");
-      List.iter 
-        (fun e -> 
-          let t = Equality.term_of_equality eq_uri e in
-          prerr_endline (CicPp.pp t names)) 
-      eql;
-    end;
-  proof,[goalno]
-;;
-
-let get_stats () = "" 
-(*
-  <:show<Saturation.>> ^ Indexing.get_stats () ^ Founif.get_stats () ^
-  Equality.get_stats ()
-;;
-*)
-
-(* THINGS USED ONLY BY saturate_main.ml *)
-
-let main _ _ _ _ _ = () ;;
-
-let retrieve_and_print dbd term metasenv ugraph = 
-  let module C = Cic in
-  let module T = CicTypeChecker in
-  let module PET = ProofEngineTypes in
-  let module PP = CicPp in
-  let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
-  let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
-  let proof, goals = status in
-  let goal' = List.nth goals 0 in
-  let uri, metasenv, meta_proof, term_to_prove = proof in
-  let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in
-  let eq_uri = eq_of_goal type_of_goal in
-  let bag = Equality.mk_equality_bag () in
-  let eq_indexes, equalities, maxm,cache = 
-    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in
-  let ugraph = CicUniv.empty_ugraph in
-  let env = (metasenv, context, ugraph) in
-  let t1 = Unix.gettimeofday () in
-  let lib_eq_uris, library_equalities, maxm, cache =
-    Equality_retrieval.find_library_equalities bag
-      false dbd context (proof, goal') (maxm+2)  cache
-  in 
-  let t2 = Unix.gettimeofday () in
-  maxmeta := maxm+2;
-  let equalities = (* equalities @ *) library_equalities in
-  Utils.debug_print
-     (lazy
-        (Printf.sprintf "\n\nequalities:\n%s\n"
-           (String.concat "\n"
-              (List.map 
-          (fun (u, e) ->
-(*                  Printf.sprintf "%s: %s" *)
-                   (UriManager.string_of_uri u)
-(*                    (string_of_equality e) *)
-                     )
-          equalities))));
-  Utils.debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
-  let rec simpl e others others_simpl =
-    let (u, e) = e in
-    let active = (others @ others_simpl) in
-    let tbl =
-      List.fold_left
-        (fun t (_, e) -> Indexing.index t e)
-        Indexing.empty active
-    in
-    let res = forward_simplify bag eq_uri env e (active, tbl) in
-    match others with
-        | hd::tl -> (
-            match res with
-              | None -> simpl hd tl others_simpl
-              | Some e -> simpl hd tl ((u, e)::others_simpl)
-          )
-        | [] -> (
-            match res with
-              | None -> others_simpl
-              | Some e -> (u, e)::others_simpl
-          ) 
-  in
-  let _equalities =
-    match equalities with
-      | [] -> []
-      | hd::tl ->
-          let others = tl in (* List.map (fun e -> (Utils.Positive, e)) tl in *)
-          let res =
-            List.rev (simpl (*(Positive,*) hd others [])
-          in
-            Utils.debug_print
-              (lazy
-                 (Printf.sprintf "\nequalities AFTER:\n%s\n"
-                    (String.concat "\n"
-                       (List.map
-                          (fun (u, e) ->
-                             Printf.sprintf "%s: %s"
-                               (UriManager.string_of_uri u)
-                               (Equality.string_of_equality e)
-                          )
-                          res))));
-            res in
-    Utils.debug_print
-      (lazy
-         (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
-;;
-
-
-let main_demod_equalities dbd term metasenv ugraph =
-  let module C = Cic in
-  let module T = CicTypeChecker in
-  let module PET = ProofEngineTypes in
-  let module PP = CicPp in
-  let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
-  let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
-  let proof, goals = status in
-  let goal' = List.nth goals 0 in
-  let _, metasenv, meta_proof, _ = proof in
-  let _, context, goal = CicUtil.lookup_meta goal' metasenv in
-  let eq_uri = eq_of_goal goal in 
-  let bag = Equality.mk_equality_bag () in
-  let eq_indexes, equalities, maxm,  cache = 
-    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in
-  let lib_eq_uris, library_equalities, maxm,cache =
-    Equality_retrieval.find_library_equalities bag
-      false dbd context (proof, goal') (maxm+2)  cache
-  in
-  let library_equalities = List.map snd library_equalities in
-  maxmeta := maxm+2; (* TODO ugly!! *)
-  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-  let new_meta_goal, metasenv, type_of_goal =
-    let _, context, ty = CicUtil.lookup_meta goal' metasenv in
-    Utils.debug_print
-      (lazy
-         (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
-            (CicPp.ppterm ty)));
-    Cic.Meta (maxm+1, irl),
-    (maxm+1, context, ty)::metasenv,
-    ty
-  in
-  let env = (metasenv, context, ugraph) in
-  (*try*)
-    let goal = [], [], goal 
-    in
-    let equalities = 
-      simplify_equalities bag eq_uri env (equalities@library_equalities) 
-    in
-    let active = make_empty_active () in
-    let passive = make_passive equalities in
-    Printf.eprintf "\ncontext:\n%s\n" (PP.ppcontext context);
-    Printf.eprintf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
-    Printf.eprintf "\nequalities:\n%s\n"
-      (String.concat "\n"
-         (List.map
-            (Equality.string_of_equality ~env) equalities));
-    prerr_endline "--------------------------------------------------";
-    prerr_endline "GO!";
-    start_time := Unix.gettimeofday ();
-    if !time_limit < 1. then time_limit := 60.;    
-    let ra, rp =
-      saturate_equations bag eq_uri env goal (fun e -> true) passive active
-    in
-
-    let initial =
-      List.fold_left (fun s e -> EqualitySet.add e s)
-        EqualitySet.empty equalities
-    in
-    let addfun s e = 
-      if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
-    in
-
-    let passive =
-      match rp with
-      | p, _ ->
-          EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
-    in
-    let active =
-      let l = fst ra in
-      EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
-    in
-    Printf.eprintf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
-       (String.concat "\n" (List.map (Equality.string_of_equality ~env) active)) 
-     (*  (String.concat "\n"
-         (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)
-(*       (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
-      (String.concat "\n"
-         (List.map 
-           (fun e -> CicPp.ppterm (Equality.term_of_equality eq_uri e)) 
-          passive));
-    print_newline ();
-(*
-  with e ->
-    Utils.debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
-*)
-;;
-let saturate_equations eq_uri env goal accept_fun passive active =
-  let bag = Equality.mk_equality_bag () in
-  saturate_equations bag eq_uri env goal accept_fun passive active
-;;
-
 let add_to_passive eql passives = 
   add_to_passive passives eql eql
 ;;
+
+