From 9c21f4a9a35415878189aca003847cbd42c1a9fc Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 21 Dec 2009 08:56:01 +0000
Subject: [PATCH] Trying to be faster

---
 .../ng_paramodulation/nCicParamod.ml          | 22 ++++++++++---------
 .../ng_paramodulation/nCicParamod.mli         |  4 ++--
 .../components/ng_paramodulation/nCicProof.ml |  6 ++++-
 .../ng_paramodulation/nCicProof.mli           |  2 +-
 4 files changed, 20 insertions(+), 14 deletions(-)

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index fb60d3142..3b9bfce04 100644
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -31,10 +31,10 @@ let readback rdb metasenv subst context (bag,i,fo_subst,l) =
      print_endline (Pp.pp_unit_clause ~margin:max_int
      (fst(Terms.M.find x bag)))) l; 
 *)
-  let stamp = Unix.gettimeofday () in
-  let proofterm = NCicProof.mk_proof bag i fo_subst l in
-    print (lazy (Printf.sprintf "Got proof term in %fs"
-		     (Unix.gettimeofday() -. stamp)));
+  (* let stamp = Unix.gettimeofday () in *)
+  let proofterm,prooftype = NCicProof.mk_proof bag i fo_subst l in
+  (* debug (lazy (Printf.sprintf "Got proof term in %fs"
+		     (Unix.gettimeofday() -. stamp))); *)
   let metasenv, proofterm = 
     let rec aux k metasenv = function
       | NCic.Meta _ as t -> metasenv, t
@@ -47,8 +47,9 @@ let readback rdb metasenv subst context (bag,i,fo_subst,l) =
           (fun _ k -> k+1) k aux metasenv t
     in
       aux 0 metasenv proofterm
-  in
-  print (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm));
+  in 
+  debug (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm));
+(*
   let stamp = Unix.gettimeofday () in
   let metasenv, subst, proofterm, _prooftype = 
     NCicRefiner.typeof 
@@ -57,7 +58,8 @@ let readback rdb metasenv subst context (bag,i,fo_subst,l) =
   in
     print (lazy (Printf.sprintf "Refined in %fs"
 		     (Unix.gettimeofday() -. stamp)));
-    proofterm, metasenv, subst
+*)
+    proofterm, prooftype, metasenv, subst
 
 let nparamod rdb metasenv subst context t table =
   let module C =
@@ -115,12 +117,12 @@ let index_obj s uri =
 ;;
 
 let fast_eq_check rdb metasenv subst context s goal =
-  let stamp = Unix.gettimeofday () in
+  (* let stamp = Unix.gettimeofday () in *)
   match P.fast_eq_check s goal with
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
   | P.Unsatisfiable solutions -> 
-      print (lazy (Printf.sprintf "Got solutions in %fs"
-		     (Unix.gettimeofday() -. stamp)));
+      (* print (lazy (Printf.sprintf "Got solutions in %fs"
+		     (Unix.gettimeofday() -. stamp))); *)
       List.map (readback rdb metasenv subst context) solutions
 ;;
 
diff --git a/helm/software/components/ng_paramodulation/nCicParamod.mli b/helm/software/components/ng_paramodulation/nCicParamod.mli
index 0572f8c64..a0f5265ee 100644
--- a/helm/software/components/ng_paramodulation/nCicParamod.mli
+++ b/helm/software/components/ng_paramodulation/nCicParamod.mli
@@ -15,7 +15,7 @@ val nparamod :
   #NRstatus.status ->
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
     (NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
-     (NCic.term * NCic.metasenv * NCic.substitution) list
+     (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
 
 type state 
 val empty_state: state
@@ -26,4 +26,4 @@ val fast_eq_check :
   NCic.metasenv -> NCic.substitution -> NCic.context ->
   state -> 
   (NCic.term * NCic.term) -> 
-  (NCic.term * NCic.metasenv * NCic.substitution) list
+  (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index 65c0b1613..f13f35fbf 100644
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -160,6 +160,10 @@ let debug c _ = c;;
 	  -> NCic.Appl [eq_refl();ty;l]
       | _ -> assert false
     in  
+    let proof_type =
+      let lit,_,_ = get_literal mp in
+      let lit = Subst.apply_subst subst lit in
+	extract 0 [] lit in
     let rec aux ongoal seen = function
       | [] -> NCic.Rel 1
       | id :: tl ->
@@ -239,6 +243,6 @@ let debug c _ = c;;
                  aux ongoal 
                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
     in 
-      aux false [] steps
+      aux false [] steps, proof_type
   ;;
 
diff --git a/helm/software/components/ng_paramodulation/nCicProof.mli b/helm/software/components/ng_paramodulation/nCicProof.mli
index 4383b2928..1ba93353b 100644
--- a/helm/software/components/ng_paramodulation/nCicProof.mli
+++ b/helm/software/components/ng_paramodulation/nCicProof.mli
@@ -22,4 +22,4 @@ val mk_proof:
   -> Terms.M.key 
   -> NCic.term Terms.substitution
   -> Terms.M.key list 
-  -> NCic.term
+  -> NCic.term * NCic.term (* proof, type *)
-- 
2.39.2