Trying to be faster

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index fb60d3142ccb526b5520bff439263d576512fae2..3b9bfce045a4ca2496f9fa1c6b74b030a5d36100 100644 (file)
--- 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 0572f8c64ea74ddf6bf15b7813e901f5e6648d32..a0f5265eea85c4798bdbefb1f9f1a5dc17da4b7d 100644 (file)
--- 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 65c0b16138f3d5880006cb848e3f77a45b85f73d..f13f35fbfb9c6552a621aada1db5aee60e40b1a9 100644 (file)
--- 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 4383b2928956ada851ae6de53b87a68454ccf915..1ba93353b4f646abe3069aff5deac5c661c219c2 100644 (file)
--- 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 *)