New version of deep_subsumption

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

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index c4aaa1ca485979031e2b7ad434e8c5783eb4d3f6..5248a6a924c84bf6f2b06c1d36c5f16bff12dd4a 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -355,6 +355,17 @@ let string_of_proof_new ?(names=[]) p gp =
       gp)
 ;;
 
+let rec depend eq id =
+  let (_,(p,_),(_,_,_,_),_,ideq) = open_equality eq in
+  if id = ideq then true else  
+  match p with
+      Exact _ -> false
+    | Step (_,(_,id1,(_,id2),_)) ->
+       let eq1 = Hashtbl.find id_to_eq id1 in
+       let eq2 = Hashtbl.find id_to_eq id2 in  
+        depend eq1 id || depend eq1 id2 
+;;
+    
 let ppsubst = ppsubst ~names:[]
 
 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
@@ -537,6 +548,7 @@ let build_proof_step subst p1 p2 pos l r pred =
    CicSubstitution.subst (Cic.Rel 1) t
   in
     match body,pos with
+(*
       |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left ->
          let third = CicSubstitution.subst (Cic.Implicit None) third in
          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
@@ -689,6 +701,7 @@ let build_proof_step subst p1 p2 pos l r pred =
           in
            mk_trans uri_trans ty lhs pred_of_what pred_of_other 
              p1 (inject ty rhs other what p2)
+*)
       | _, Utils.Left ->
         mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
       | _, Utils.Right ->
@@ -708,7 +721,7 @@ let build_proof_term_new proof =
    aux proof
 ;;
 
-let wfo goalproof =
+let wfo goalproof proof =
   let rec aux acc id =
     let p,_,_ = proof_of_id id in
     match p with
@@ -718,7 +731,12 @@ let wfo goalproof =
         let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
         id :: acc
   in
-  List.fold_left (fun acc (_,id,_,_) -> aux acc id) [] goalproof
+  let acc = 
+    match proof with
+      | Exact _ -> []
+      | Step (_,(_,id1, (_,id2), _)) -> aux (aux [] id1) id2
+  in 
+  List.fold_left (fun acc (_,id,_,_) -> aux acc id) acc goalproof
 ;;
 
 let string_of_id names id = 
@@ -735,8 +753,8 @@ let string_of_id names id =
   with
       Not_found -> assert false
 
-let pp_proof names goalproof =
-  String.concat "\n" (List.map (string_of_id names) (wfo goalproof)) ^ 
+let pp_proof names goalproof proof =
+  String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof)) ^ 
   "\ngoal is demodulated with " ^ 
     (String.concat " " 
       ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))