goal demodulated with new

[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 6c0b24327d6fca5dcedc1a0417d8f6caa8999056..c4aaa1ca485979031e2b7ad434e8c5783eb4d3f6 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/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)
 
@@ -706,7 +712,7 @@ let wfo goalproof =
   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
@@ -723,14 +729,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))
+  String.concat "\n" (List.map (string_of_id names) (wfo goalproof)) ^ 
+  "\ngoal is demodulated with " ^ 
+    (String.concat " " 
+      ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
+;;
 
 let build_goal_proof l initial =
   let proof =