From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 18 Jun 2009 16:58:39 +0000 (+0000)
Subject: proof patching!
X-Git-Tag: make_still_working~3845
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=59eba9406321e2eeb1e4471dc490aa72ebf4ec47;p=helm.git

proof patching!
---

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index 1e5e67979..46710db21 100644
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -197,7 +197,7 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
           let amount = List.length seen in
           let lit,vl,proof = get_literal id in
           if not ongoal && id = mp then
-            ((*prerr_endline ("Reached meeting point, id=" ^ (string_of_int id));*)
+            ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
 	     assert (vl = []);  
              NCic.LetIn ("clause_" ^ string_of_int id, 
                 extract amount vl lit, 
diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index b32a5b1be..b80bfc500 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,19 +192,32 @@ 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 "YES!";
+      prerr_endline ("Meeting point : " ^ (string_of_int i));
+      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
+      prerr_endline
+        ("prova generata: " ^ NCicPp.ppterm 
+           ~metasenv ~subst ~context proofterm);
       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
+      prerr_endline "prova raffinata";
       proofterm, metasenv, subst
   | Failure _ -> prerr_endline "FAILURE"; assert false
 ;;