From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 6 Dec 2006 15:54:39 +0000 (+0000)
Subject: Experimental: cycles in proofs generated by paramodulation are now detected
X-Git-Tag: 0.4.95@7852~746
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e6454d89343d6ad3195360a0d5a584d5ad3a3575;p=helm.git

Experimental: cycles in proofs generated by paramodulation are now detected
and removed.
However, letins that become useless after this operation are not simplified.
Simplifying them (when they became linear) could introduce more cycles that
require a second simplification and so on.
---

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 1d798f9dc..7f093e3f8 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -269,6 +269,48 @@ let is_not_fixed t =
 ;;
 
 let canonical t context menv = 
+  let remove_cycles t =
+   let is_transitive =
+    function
+       Cic.Appl (Cic.Const (uri_trans,_)::_)
+        when LibraryObjects.is_trans_eq_URI uri_trans ->
+         true
+     | _ -> false in
+   let rec collect =
+    function
+       Cic.Appl (Cic.Const (uri_trans,ens)::tl)
+        when LibraryObjects.is_trans_eq_URI uri_trans ->
+         let ty,l,m,r,p1,p2 = open_trans ens tl in
+          (if is_transitive p1 then fst (collect p1) else [l,p1]) @
+           (if is_transitive p2 then fst (collect p2) else [m,p2]),
+          (r, uri_trans, ty)
+     | t -> assert false in
+   let rec cut_to_last_duplicate l acc =
+    function
+       [] -> List.rev acc
+     | (l',p)::tl when l=l' -> 
+if acc <> [] then
+prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI");
+         cut_to_last_duplicate l [l',p] tl
+     | (l',p)::tl ->
+         cut_to_last_duplicate l ((l',p)::acc) tl
+   in
+   let rec rebuild =
+    function
+       (l,_)::_::_ as steps, ((r,uri_trans,ty) as last) ->
+         (match cut_to_last_duplicate l [] steps with
+             (l,p1)::((m,_)::_::_ as tl) ->
+               mk_trans uri_trans ty l m r p1 (rebuild (tl,last))
+           | [l,p1 ; m,p2] -> mk_trans uri_trans ty l m r p1 p2
+           | [l,p1] -> p1
+           | [] -> assert false)
+     | _ -> assert false
+   in
+    if is_transitive t then
+     rebuild (collect t)
+    else
+     t
+  in
   let rec remove_refl t =
     match t with
     | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
@@ -314,7 +356,7 @@ let canonical t context menv =
       | Cic.Appl l -> Cic.Appl (List.map (canonical context) l)
       | _ -> t
   in
-  remove_refl (canonical context t)
+   remove_cycles (remove_refl (canonical context t))
 ;;
   
 let compose_contexts ctx1 ctx2 =