- patch to consider the symbols of the goal when computing the weight of an

[helm.git] / helm / software / components / tactics / paramodulation / equality.ml

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 1e9e97ec58f3147733356cfde501a72bdf83da74..91ed61cd5ea9426b7e111029a1e68cf84625f784 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let _profiler = <:profiler<_profiler>>;;
+
 (* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
 
 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
@@ -44,6 +46,8 @@ and proof =
 and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
 ;;
 
+type goal = goal_proof * Cic.metasenv * Cic.term
+
 (* globals *)
 let maxid = ref 0;;
 let id_to_eq = Hashtbl.create 1024;;
@@ -430,7 +434,7 @@ let add_subst subst =
   function
     | Exact t -> Exact (Subst.apply_subst subst t)
     | Step (s,(rule, id1, (pos,id2), pred)) -> 
-       Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
+        Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
 ;;
        
 let build_proof_step eq lift subst p1 p2 pos l r pred =
@@ -461,9 +465,10 @@ let build_proof_step eq lift subst p1 p2 pos l r pred =
 ;;
 
 let parametrize_proof p l r ty = 
-  let parameters = 
-    CicUtil.metas_of_term p @ CicUtil.metas_of_term l @ CicUtil.metas_of_term r
-  in (* ?if they are under a lambda? *)
+  let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in
+  let mot = CicUtil.metas_of_term_set in
+  let parameters = uniq (mot p @ mot l @ mot r) in 
+  (* ?if they are under a lambda? *)
   let parameters = 
     HExtlib.list_uniq (List.sort Pervasives.compare parameters) 
   in
@@ -576,9 +581,12 @@ let rec find_deps m i =
 
 let topological_sort l = 
   (* build the partial order relation *)
-  let m = 
-    List.fold_left (fun m i -> find_deps m i)
-    M.empty l
+  let m = List.fold_left (fun m i -> find_deps m i) M.empty l in
+  let m = (* keep only deps inside l *) 
+    List.fold_left 
+      (fun m' i ->
+        M.add i (List.filter (fun x -> List.mem x l) (M.find i m)) m') 
+      M.empty l 
   in
   let m = M.map (fun x -> Some x) m in
   (* utils *)
@@ -599,7 +607,8 @@ let topological_sort l =
       let res = ok @ res in
       if ok = [] then res else aux m res
   in
-  aux m []
+  let rc = List.rev (aux m []) in
+  rc
 ;;
   
 
@@ -646,7 +655,8 @@ let build_proof_term eq h lift proof =
     try List.assoc id h,l,r with Not_found -> aux p, l, r
   in
   let rec aux = function
-     | Exact term -> CicSubstitution.lift lift term
+     | Exact term -> 
+         CicSubstitution.lift lift term
      | Step (subst,(rule, id1, (pos,id2), pred)) ->
          let p1,_,_ = proof_of_id aux id1 in
          let p2,l,r = proof_of_id aux id2 in
@@ -661,7 +671,7 @@ let build_proof_term eq h lift proof =
            | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
            | _ -> assert false
          in
-         let p =   build_proof_step eq lift subst p1 p2 pos l r pred in
+         let p = build_proof_step eq lift subst p1 p2 pos l r pred in
 (*         let cond =  (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in
            if not cond then
              prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2);
@@ -747,6 +757,15 @@ let metas_of_proof p =
   Utils.metas_of_term p
 ;;
 
+let remove_local_context eq =
+   let w, p, (ty, left, right, o), menv,id = open_equality eq in
+   let p = Utils.remove_local_context p in
+   let ty = Utils.remove_local_context ty in
+   let left = Utils.remove_local_context left in
+   let right = Utils.remove_local_context right in
+   w, p, (ty, left, right, o), menv, id
+;;
+
 let relocate newmeta menv to_be_relocated =
   let subst, newmetasenv, newmeta = 
     List.fold_right 
@@ -761,6 +780,20 @@ let relocate newmeta menv to_be_relocated =
   let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in
   subst, menv, newmeta
 
+let fix_metas_goal newmeta goal =
+  let (proof, menv, ty) = goal in
+  let to_be_relocated = 
+    HExtlib.list_uniq (List.sort Pervasives.compare (Utils.metas_of_term ty))
+  in
+  let subst, menv, newmeta = relocate newmeta menv to_be_relocated in
+  let ty = Subst.apply_subst subst ty in
+  let proof = 
+    match proof with
+    | [] -> assert false (* is a nonsense to relocate the initial goal *)
+    | (r,pos,id,s,p) :: tl -> (r,pos,id,Subst.concat subst s,p) :: tl
+  in
+  newmeta+1,(proof, menv, ty)
+;;
 
 let fix_metas newmeta eq = 
   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
@@ -989,3 +1022,47 @@ let symmetric eq_ty l id uri m =
     (Demodulation,id1,(Utils.Left,id),pred))
 ;;
 
+module IntOT = struct
+  type t = int
+  let compare = Pervasives.compare
+end
+
+module IntSet = Set.Make(IntOT);;
+
+let n_purged = ref 0;;
+
+let collect alive1 alive2 alive3 =
+  let _ = <:start<collect>> in
+  let deps_of id = 
+    let p,_,_ = proof_of_id id in  
+    match p with
+    | Exact _ -> IntSet.empty
+    | Step (_,(_,id1,(_,id2),_)) ->
+          IntSet.add id1 (IntSet.add id2 IntSet.empty)
+  in
+  let rec close s = 
+    let news = IntSet.fold (fun id s -> IntSet.union (deps_of id) s) s s in
+    if IntSet.equal news s then s else close news
+  in
+  let l_to_s s l = List.fold_left (fun s x -> IntSet.add x s) s l in
+  let alive_set = l_to_s (l_to_s (l_to_s IntSet.empty alive2) alive1) alive3 in
+  let closed_alive_set = close alive_set in
+  let to_purge = 
+    Hashtbl.fold 
+      (fun k _ s -> 
+        if not (IntSet.mem k closed_alive_set) then
+          k::s else s) id_to_eq []
+  in
+  n_purged := !n_purged + List.length to_purge;
+  List.iter (Hashtbl.remove id_to_eq) to_purge;
+  let _ = <:stop<collect>> in ()  
+;;
+
+let id_of e = 
+  let _,_,_,_,id = open_equality e in id
+;;
+
+let get_stats () = 
+  <:show<Equality.>> ^ 
+  "# of purged eq by the collector: " ^ string_of_int !n_purged ^ "\n"
+;;