more profiling and fixes for paramod

[helm.git] / components / tactics / paramodulation / inference.ml

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index f5508c8c146cc72bc2c418b5ae80770febf6fd4c..e2f21b25cfe823d004c5579238d5f3562586f3dd 100644 (file)
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -37,8 +37,7 @@ type equality =
      Cic.term *          (* left side *)
      Cic.term *          (* right side *)
      Utils.comparison) * (* ordering *)  
-    Cic.metasenv *       (* environment for metas *)
-    Cic.term list        (* arguments *)
+    Cic.metasenv        (* environment for metas *)
 
 and proof =
   | NoProof (* term is the goal missing a proof *)
@@ -55,14 +54,14 @@ let string_of_equality ?env =
   match env with
   | None -> (
       function
-        | w, _, (ty, left, right, o), _, _ ->
+        | w, _, (ty, left, right, o), _ ->
             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
               (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
     )
   | Some (_, context, _) -> (
       let names = names_of_context context in
       function
-        | w, _, (ty, left, right, o), _, _ ->
+        | w, _, (ty, left, right, o), _ ->
             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
               (CicPp.pp left names) (string_of_comparison o)
               (CicPp.pp right names)
@@ -139,11 +138,11 @@ let build_proof_term ?(noproof=Cic.Implicit None) proof =
     | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
         let t' = Cic.Lambda (name, ty, bo) in
         let proof' =
-          let _, proof', _, _, _ = eq in
+          let _, proof', _, _ = eq in
           do_build_proof proof'
         in
         let eqproof = do_build_proof eqproof in
-        let _, _, (ty, what, other, _), menv', args' = eq in
+        let _, _, (ty, what, other, _), menv' = eq in
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
@@ -311,8 +310,8 @@ let meta_convertibility_aux table t1 t2 =
 
 
 let meta_convertibility_eq eq1 eq2 =
-  let _, _, (ty, left, right, _), _, _ = eq1
-  and _, _, (ty', left', right', _), _, _ = eq2 in
+  let _, _, (ty, left, right, _), _ = eq1
+  and _, _, (ty', left', right', _), _ = eq2 in
   if ty <> ty' then
     false
   else if (left = left') && (right = right') then
@@ -451,7 +450,10 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
   List.rev subst, menv, ugraph
 ;;
 
-let profiler = HExtlib.profile "flatten"
+let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]"
+let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]"
+let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
+let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
 
 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
   let metasenv = metasenv1 @ metasenv2 in
@@ -480,8 +482,25 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
         let ty = CicMetaSubst.apply_subst subst ty in  
           (i, (context, term, ty))) subst 
   in
-  let flatten subst = profiler.HExtlib.profile flatten subst in
-  let subst = flatten subst in
+  let flatten_fast subst = 
+    let resolve_meta (i, (context, term, ty)) subst = 
+           let term = CicMetaSubst.apply_subst subst term in
+           let ty = CicMetaSubst.apply_subst subst ty in  
+            (i, (context, term, ty))
+    in
+    let resolve_meta t s = profiler3.HExtlib.profile (resolve_meta t) s in
+    let filter j (i,_) = i <> j in
+    let filter a b = profiler4.HExtlib.profile (filter a) b in
+    List.fold_left 
+      (fun subst (j,(c,t,ty)) as s ->  
+        let s = resolve_meta s subst in 
+        s::(List.filter (filter j) subst)) 
+      subst subst
+  in
+  (*let flatten subst = profiler.HExtlib.profile flatten subst in*)
+  let flatten_fast subst = profiler2.HExtlib.profile flatten_fast subst in
+  (*let subst = flatten subst in*)
+(*  let subst = flatten_fast subst in*)
     subst, menv, ug
 ;;
 
@@ -726,7 +745,7 @@ let matching metasenv1 metasenv2 context t1 t2 ugraph =
 let matching = matching1;;
 
 let check_eq context msg eq =
-  let w, proof, (eq_ty, left, right, order), metas, args = eq in
+  let w, proof, (eq_ty, left, right, order), metas = eq in
   if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty
    (fst (CicTypeChecker.type_of_aux' metas context  left CicUniv.empty_ugraph))
    CicUniv.empty_ugraph))
@@ -773,7 +792,7 @@ let find_equalities context proof =
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
                     let proof = BasicProof p in
-                    let e = (w, proof, stat, newmetas, args) in
+                    let e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -785,7 +804,7 @@ let find_equalities context proof =
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
-              let e = (w, BasicProof (C.Rel index), stat, [], []) in
+              let e = (w, BasicProof (C.Rel index), stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in (
@@ -923,7 +942,7 @@ let find_library_equalities dbd context status maxmeta =
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
                     let proof = BasicProof p in
-                    let e = (w, proof, stat, newmetas, args) in
+                    let e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -932,7 +951,7 @@ let find_library_equalities dbd context status maxmeta =
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
-              let e = (w, BasicProof term, stat, [], []) in
+              let e = (w, BasicProof term, stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in
@@ -1135,7 +1154,7 @@ let relocate newmeta menv =
   subst, metasenv, newmeta
 
 
-let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
+let fix_metas newmeta (w, p, (ty, left, right, o), menv) =
   (*
   let metas = (metas_of_term left)@(metas_of_term right)
     @(metas_of_term ty)@(metas_of_proof p) in
@@ -1149,7 +1168,6 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
   let ty = CicMetaSubst.apply_subst subst ty in
   let left = CicMetaSubst.apply_subst subst left in
   let right = CicMetaSubst.apply_subst subst right in
-  let args = List.map (CicMetaSubst.apply_subst subst) args in
   let rec fix_proof = function
     | NoProof -> NoProof 
     | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term)
@@ -1171,7 +1189,7 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
     @(metas_of_term ty)@(metas_of_proof p) in
   let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
   *)
-  let eq = (w, p, (ty, left, right, o), metasenv, args) in
+  let eq = (w, p, (ty, left, right, o), metasenv) in
   (* debug prerr_endline (string_of_equality eq); *)
   newmeta+1, eq  
 
@@ -1193,7 +1211,7 @@ let equality_of_term proof term =
       let o = !Utils.compare_terms t1 t2 in
       let stat = (ty,t1,t2,o) in
       let w = compute_equality_weight stat in
-      let e = (w, BasicProof proof, stat, [], []) in
+      let e = (w, BasicProof proof, stat, []) in
       e
   | _ ->
       raise TermIsNotAnEquality
@@ -1203,7 +1221,7 @@ let equality_of_term proof term =
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 
 let is_weak_identity (metasenv, context, ugraph) = function
-  | (_, _, (ty, left, right, _), menv, _) -> 
+  | (_, _, (ty, left, right, _), menv) -> 
        (left = right ||
           (meta_convertibility left right)) 
           (* the test below is not a good idea since it stops
@@ -1213,7 +1231,7 @@ let is_weak_identity (metasenv, context, ugraph) = function
 ;;
 
 let is_identity (metasenv, context, ugraph) = function
-  | (_, _, (ty, left, right, _), menv, _) ->
+  | (_, _, (ty, left, right, _), menv) ->
        (left = right ||
           (* (meta_convertibility left right)) *)
            (fst (CicReduction.are_convertible 
@@ -1222,7 +1240,7 @@ let is_identity (metasenv, context, ugraph) = function
 
 
 let term_of_equality equality =
-  let _, _, (ty, left, right, _), menv, _ = equality in
+  let _, _, (ty, left, right, _), menv = equality in
   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
   let argsno = List.length menv in
   let t =