X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=5f75fb3aa8b24b828a554455df0e0e04fbd4aa02;hb=bd3680d6b90f6c8bdda4eb4a915a86a0e806de63;hp=b32a5b1be43bdeb5b13444903d9573f88aadeff8;hpb=c091ca7a030a85a529543de98e45c54284028b63;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index b32a5b1be..5f75fb3aa 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -4,6 +4,7 @@ let debug s =
 
 let nparamod rdb metasenv subst context t table =
   let nb_iter = ref 200 in
+  let amount_of_time = 20.0 in
   let module C = struct
     let metasenv = metasenv
     let subst = subst
@@ -29,6 +30,7 @@ let nparamod rdb metasenv subst context t table =
   let add_passive_clause passives cl =
     PassiveSet.add (Utils.mk_passive_clause cl) passives
   in
+  let timeout = Unix.gettimeofday () +. amount_of_time in 
     (* TODO : fairness condition *)
   let select passives =
     if PassiveSet.is_empty passives then None
@@ -43,7 +45,9 @@ let nparamod rdb metasenv subst context t table =
       prerr_endline "Active table :"; 
        (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
 	  (fst actives));*)
-    raise (Failure "Timeout !");
+      raise (Failure "No iterations left !");
+    if Unix.gettimeofday () > timeout then
+      raise (Failure "Timeout !");
 
 
       
@@ -90,8 +94,8 @@ let nparamod rdb metasenv subst context t table =
 	  | None -> assert false
 	  | Some (current, passives) -> 
 	      debug ("Selected fact : " ^ Pp.pp_unit_clause current);
-              match Sup.keep_simplified current actives bag maxvar with
-	      (* match Sup.one_pass_simplification current actives bag with *)
+(*               match Sup.keep_simplified current actives bag maxvar with *)
+               match Sup.one_pass_simplification current actives bag maxvar with 
 		| None -> aux_simplify passives
 		| Some x -> x,passives
       in
@@ -188,18 +192,27 @@ let nparamod rdb metasenv subst context t table =
         let gsteps = List.rev gsteps in
         esteps@(i::gsteps)
       in
-      debug "YES!";
-      debug ("Meeting point : " ^ (string_of_int i));
-      debug "Proof:"; 
-      (*List.iter (fun x -> prerr_endline (string_of_int x);
-              prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l; *)
+(*
+      prerr_endline "Proof:"; 
+      List.iter (fun x -> prerr_endline (string_of_int x);
+              prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;
+*)
       let proofterm = B.mk_proof bag i l in
-	prerr_endline (NCicPp.ppterm ~metasenv:C.metasenv
-			 ~subst:C.subst ~context:C.context proofterm);
+      let metasenv, proofterm = 
+        let rec aux k metasenv = function
+          | NCic.Meta _ as t -> metasenv, t
+          | NCic.Implicit _ -> 
+              let metasenv,i,_,_=NCicMetaSubst.mk_meta metasenv context `Term in
+              metasenv, NCic.Meta (i,(k,NCic.Irl (List.length context)))
+          | t -> NCicUntrusted.map_term_fold_a 
+                  (fun _ k -> k+1) k aux metasenv t                 
+        in
+         aux 0 metasenv proofterm
+      in
       let metasenv, subst, proofterm, _prooftype = 
         NCicRefiner.typeof 
           (rdb#set_coerc_db NCicCoercion.empty_db) 
-          C.metasenv C.subst C.context proofterm None
+          metasenv subst context proofterm None
       in
       proofterm, metasenv, subst
   | Failure _ -> prerr_endline "FAILURE"; assert false