types2006 patch

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

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 6c0b24327d6fca5dcedc1a0417d8f6caa8999056..5248a6a924c84bf6f2b06c1d36c5f16bff12dd4a 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -264,6 +264,12 @@ let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) =
   eq
 ;;
 
+let mk_tmp_equality (weight,(ty,l,r,o),m) =
+  let id = -1 in
+  uncomparable,weight,(Exact (Cic.Implicit None),NoProof),(ty,l,r,o),m,id
+;;
+
+
 let open_equality (_,weight,proof,(ty,l,r,o),m,id) = 
   (weight,proof,(ty,l,r,o),m,id)
 
@@ -349,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 *)
@@ -531,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
@@ -683,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 ->
@@ -702,17 +721,22 @@ 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
-    | Exact _ -> id :: acc
+    | Exact _ -> if (List.mem id acc) then acc else id :: acc
     | Step (_,(_,id1, (_,id2), _)) -> 
         let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
         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 = 
@@ -723,14 +747,18 @@ let string_of_id names id =
         Printf.sprintf "%d = %s: %s = %s" id
           (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
     | Step (_,(step,id1, (_,id2), _) ) ->
-        Printf.sprintf "%5d: %s %4d %4d   %s = %s" id
+        Printf.sprintf "%6d: %s %6d %6d   %s = %s" id
           (if step = SuperpositionRight then "SupR" else "Demo") 
           id1 id2 (CicPp.pp l names) (CicPp.pp r names)
   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)))
+;;
 
 let build_goal_proof l initial =
   let proof =