X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=7f093e3f88085e9c3505ed66a25f3d3278fab1f4;hb=0978a9c19e672bb0b505f25737078409381700c7;hp=10a64af19d09a15d762697512ba00de2270a964d;hpb=cee1c02ad6a113b711b9d93176296cf16b9ec351;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 10a64af19..7f093e3f8 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -202,7 +202,7 @@ let build_ens uri termlist =
   let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
   match obj with
   | Cic.Constant (_, _, _, uris, _) ->
-      assert (List.length uris <= List.length termlist);
+      (* assert (List.length uris <= List.length termlist); *)
       let rec aux = function
         | [], tl -> [], tl
         | (uri::uris), (term::tl) ->
@@ -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 =