new pp function for proofs

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 7ad20206a448a9f2a5fce4ab45d49e02b6c58afc..6c0b24327d6fca5dcedc1a0417d8f6caa8999056 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/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 = 

diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli
index 4d48f22aade7a4aa888b99d924963731e918f3ce..ea0cefd55113dca76d0f48b236246a2363fbdc2e 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.mli
+++ b/helm/software/components/tactics/paramodulation/equality.mli
@@ -45,7 +45,8 @@ and old_proof =
   | SubProof of Cic.term * int * old_proof
 
 and goal_proof = (Utils.pos * int * substitution * Cic.term) list
-       
+
+val pp_proof: (Cic.name option) list -> goal_proof -> string
 
 val empty_subst : substitution
 val apply_subst : substitution -> Cic.term -> Cic.term

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 4423661b00b118073a45e4d0d071bfec56c8921a..f1cec900f1d54eaa100f1a0f8006d490c9bc176b 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1540,14 +1540,16 @@ let saturate
 
       (* pp new/old proof *)
       let names = names_of_context context in
-      prerr_endline "OLDPROOF";
-      prerr_endline (Equality.string_of_proof_old proof);
-      prerr_endline "OLDPROOFCIC";
-      prerr_endline (CicPp.pp cic_proof names); 
+(*      prerr_endline "OLDPROOF";*)
+(*      prerr_endline (Equality.string_of_proof_old proof);*)
+(*      prerr_endline "OLDPROOFCIC";*)
+(*      prerr_endline (CicPp.pp cic_proof names); *)
       prerr_endline "NEWPROOF";
-      prerr_endline (Equality.string_of_proof_new ~names newproof goalproof); 
-      prerr_endline "NEWPROOFCIC";
-      prerr_endline (CicPp.pp cic_proof_new names); 
+     (* prerr_endline (Equality.string_of_proof_new ~names newproof
+      * goalproof);*)
+      prerr_endline (Equality.pp_proof names goalproof);
+(*      prerr_endline "NEWPROOFCIC";*)
+(*      prerr_endline (CicPp.pp cic_proof_new names); *)
 
       (* generation of proof metasenv *)
       let newmetasenv =
@@ -1605,8 +1607,8 @@ let saturate
           cic_proof_new, newmetasenv_new, newmetasenv_new,new_ty, newug
           (* THE OLD PROOF: cic_proof,newmetasenv,proof_menv,oldty,oldug *)
         in
-        prerr_endline "FINAL PROOF";
-        prerr_endline (CicPp.pp cic_proof names);
+(*        prerr_endline "FINAL PROOF";*)
+(*        prerr_endline (CicPp.pp cic_proof names);*)
         prerr_endline "ENDOFPROOFS";
         (*  
         debug_print