X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=6c0b24327d6fca5dcedc1a0417d8f6caa8999056;hb=6421979dbececb04f6ab0d3534f2489d7f151c5f;hp=7ad20206a448a9f2a5fce4ab45d49e02b6c58afc;hpb=80a0de7252db131efb4d0058cb8bfdad8221d71f;p=helm.git

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 7ad20206a..6c0b24327 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -555,7 +555,6 @@ let build_proof_step subst p1 p2 pos l r pred =
         ->
           let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
           let uri_trans = LibraryObjects.trans_eq_URI ~eq in
-          let uri_sym = LibraryObjects.sym_eq_URI ~eq in
           let pred_of t = CicSubstitution.subst t lhs in
           let pred_of_what = pred_of what in
           let pred_of_other = pred_of other in
@@ -563,27 +562,31 @@ let build_proof_step subst p1 p2 pos l r pred =
            * ====================================
            *  inject p2:  P(what) = P(other)
            *)
-          let inject ty lhs what other p2 =
+          let rec inject ty lhs what other p2 =
+           match p2 with
+           | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
+               when LibraryObjects.is_trans_eq_URI uri_trans ->
+               let ty,l,m,r,plm,pmr = open_trans ens tl in
+               mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
+                 (inject ty lhs m r pmr) (inject ty lhs l m plm)
+           | _ -> 
            let liftedty = CicSubstitution.lift 1 ty in
            let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
            let refl_eq_part =
             Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
            in
-            mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
+            (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
              (Cic.Lambda (Cic.Name "foo",ty,
                (Cic.Appl
-                 [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
-                refl_eq_part what p2
+               [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
+                refl_eq_part what p2)
           in
            mk_trans uri_trans ty pred_of_other pred_of_what rhs
-            (mk_sym uri_sym ty pred_of_what pred_of_other
-             (inject ty lhs what other p2)
-            ) p1
+             (inject ty lhs what other p2) p1
       | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs
         ->
           let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
           let uri_trans = LibraryObjects.trans_eq_URI ~eq in
-          let uri_sym = LibraryObjects.sym_eq_URI ~eq in
           let pred_of t = CicSubstitution.subst t lhs in
           let pred_of_what = pred_of what in
           let pred_of_other = pred_of other in
@@ -591,27 +594,33 @@ let build_proof_step subst p1 p2 pos l r pred =
            * ====================================
            *  inject p2:  P(what) = P(other)
            *)
-          let inject ty lhs what other p2 =
-           let liftedty = CicSubstitution.lift 1 ty in
-           let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
-           let refl_eq_part =
-            Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
-           in
-            mk_eq_ind (Utils.eq_ind_URI ()) ty other
-             (Cic.Lambda (Cic.Name "foo",ty,
-               (Cic.Appl
-                 [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
-                refl_eq_part what p2
+          let rec inject ty lhs what other p2 =
+           match p2 with
+           | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
+               when LibraryObjects.is_trans_eq_URI uri_trans ->
+               let ty,l,m,r,plm,pmr = open_trans ens tl in
+               mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
+                 (inject ty lhs m l plm)
+                 (inject ty lhs r m pmr)
+           | _ ->
+             let liftedty = CicSubstitution.lift 1 ty in
+             let lifted_pred_of_other = 
+               CicSubstitution.lift 1 (pred_of other) in
+             let refl_eq_part =
+              Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
+             in
+              mk_eq_ind (Utils.eq_ind_URI ()) ty other
+               (Cic.Lambda (Cic.Name "foo",ty,
+                 (Cic.Appl
+                 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
+                  refl_eq_part what p2
           in
            mk_trans uri_trans ty pred_of_other pred_of_what rhs
-            (mk_sym uri_sym ty pred_of_other pred_of_what
-             (inject ty lhs what other p2)
-            ) p1
+            (inject ty lhs what other p2) p1
       | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs
         ->
           let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
           let uri_trans = LibraryObjects.trans_eq_URI ~eq in
-          let uri_sym = LibraryObjects.sym_eq_URI ~eq in
           let pred_of t = CicSubstitution.subst t rhs in
           let pred_of_what = pred_of what in
           let pred_of_other = pred_of other in
@@ -619,26 +628,32 @@ let build_proof_step subst p1 p2 pos l r pred =
            * ====================================
            *  inject p2:  P(what) = P(other)
            *)
-          let inject ty lhs what other p2 =
+          let rec inject ty lhs what other p2 =
+           match p2 with
+           | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
+               when LibraryObjects.is_trans_eq_URI uri_trans ->
+               let ty,l,m,r,plm,pmr = open_trans ens tl in
+                 mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
+                   (inject ty lhs m r pmr)
+                   (inject ty lhs l m plm)
+           | _ ->
            let liftedty = CicSubstitution.lift 1 ty in
            let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
            let refl_eq_part =
             Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
            in
-            mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
+            (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
              (Cic.Lambda (Cic.Name "foo",ty,
                (Cic.Appl
-                 [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
-                refl_eq_part what p2
+               [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
+                refl_eq_part what p2)
           in
-           mk_trans uri_trans ty lhs pred_of_what pred_of_other p1
-            (mk_sym uri_sym ty pred_of_what pred_of_other
-             (inject ty rhs other what p2))
+           mk_trans uri_trans ty lhs pred_of_what pred_of_other
+             p1 (inject ty rhs other what p2)
       | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs
         ->
           let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
           let uri_trans = LibraryObjects.trans_eq_URI ~eq in
-          let uri_sym = LibraryObjects.sym_eq_URI ~eq in
           let pred_of t = CicSubstitution.subst t rhs in
           let pred_of_what = pred_of what in
           let pred_of_other = pred_of other in
@@ -646,7 +661,15 @@ let build_proof_step subst p1 p2 pos l r pred =
            * ====================================
            *  inject p2:  P(what) = P(other)
            *)
-          let inject ty lhs what other p2 =
+          let rec inject ty lhs what other p2 =
+           match p2 with
+           | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
+               when LibraryObjects.is_trans_eq_URI uri_trans ->
+               let ty,l,m,r,plm,pmr = open_trans ens tl in
+                 (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
+                   (inject ty lhs m l plm)
+                   (inject ty lhs r m pmr))
+           | _ ->
            let liftedty = CicSubstitution.lift 1 ty in
            let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
            let refl_eq_part =
@@ -655,12 +678,11 @@ let build_proof_step subst p1 p2 pos l r pred =
             mk_eq_ind (Utils.eq_ind_URI ()) ty other
              (Cic.Lambda (Cic.Name "foo",ty,
                (Cic.Appl
-                 [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
+               [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
                 refl_eq_part what p2
           in
-           mk_trans uri_trans ty lhs pred_of_what pred_of_other p1
-            (mk_sym uri_sym ty pred_of_other pred_of_what
-             (inject ty rhs other what p2))
+           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 ->
@@ -678,6 +700,37 @@ let build_proof_term_new proof =
            build_proof_step subst p1 p2 pos l r pred
   in
    aux proof
+;;
+
+let wfo goalproof =
+  let rec aux acc id =
+    let p,_,_ = proof_of_id id in
+    match p with
+    | Exact _ -> 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 string_of_id names id = 
+  try
+    let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+    match p with
+    | Exact t -> 
+        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
+          (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 build_goal_proof l initial =
   let proof =