New version of deep_subsumption

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index c4aaa1ca485979031e2b7ad434e8c5783eb4d3f6..5248a6a924c84bf6f2b06c1d36c5f16bff12dd4a 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -355,6 +355,17 @@ let string_of_proof_new ?(names=[]) p gp =
       gp)
 ;;
 
+let rec depend eq id =
+  let (_,(p,_),(_,_,_,_),_,ideq) = open_equality eq in
+  if id = ideq then true else  
+  match p with
+      Exact _ -> false
+    | Step (_,(_,id1,(_,id2),_)) ->
+       let eq1 = Hashtbl.find id_to_eq id1 in
+       let eq2 = Hashtbl.find id_to_eq id2 in  
+        depend eq1 id || depend eq1 id2 
+;;
+    
 let ppsubst = ppsubst ~names:[]
 
 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
@@ -537,6 +548,7 @@ let build_proof_step subst p1 p2 pos l r pred =
    CicSubstitution.subst (Cic.Rel 1) t
   in
     match body,pos with
+(*
       |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left ->
          let third = CicSubstitution.subst (Cic.Implicit None) third in
          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
@@ -689,6 +701,7 @@ let build_proof_step subst p1 p2 pos l r pred =
           in
            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 ->
@@ -708,7 +721,7 @@ let build_proof_term_new proof =
    aux proof
 ;;
 
-let wfo goalproof =
+let wfo goalproof proof =
   let rec aux acc id =
     let p,_,_ = proof_of_id id in
     match p with
@@ -718,7 +731,12 @@ let wfo goalproof =
         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 acc = 
+    match proof with
+      | Exact _ -> []
+      | Step (_,(_,id1, (_,id2), _)) -> aux (aux [] id1) id2
+  in 
+  List.fold_left (fun acc (_,id,_,_) -> aux acc id) acc goalproof
 ;;
 
 let string_of_id names id = 
@@ -735,8 +753,8 @@ let string_of_id names id =
   with
       Not_found -> assert false
 
-let pp_proof names goalproof =
-  String.concat "\n" (List.map (string_of_id names) (wfo goalproof)) ^ 
+let pp_proof names goalproof proof =
+  String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof)) ^ 
   "\ngoal is demodulated with " ^ 
     (String.concat " " 
       ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))

diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli
index 2d7e48e5cb13dd18ba66d6f0f7543622630b26e3..1a2a3a2808d3d284a4f00f4eda4ebe289f5b2ca5 100644 (file)
--- a/components/tactics/paramodulation/equality.mli
+++ b/components/tactics/paramodulation/equality.mli
@@ -46,7 +46,7 @@ and old_proof =
 
 and goal_proof = (Utils.pos * int * substitution * Cic.term) list
 
-val pp_proof: (Cic.name option) list -> goal_proof -> string
+val pp_proof: (Cic.name option) list -> goal_proof -> new_proof -> string
 
 val empty_subst : substitution
 val apply_subst : substitution -> Cic.term -> Cic.term

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 1cb6d351433f158a52aa5511b51e0c36c32b1bd1..6b1b65e276eef42a34c2426490a62da745cbace4 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -358,7 +358,7 @@ let check_for_deep_subsumption env active_table eq =
   let _,_,(eq_ty, left, right, order),metas,id = Equality.open_equality eq in
   if id = 14242 then assert false;
   
-  let check deep l r = 
+  let check_subsumed deep l r = 
     let eqtmp = 
       Equality.mk_tmp_equality(0,(eq_ty,l,r,Utils.Incomparable),metas)in
     match Indexing.subsumption env active_table eqtmp with
@@ -370,18 +370,24 @@ let check_for_deep_subsumption env active_table eq =
           Equality.string_of_equality ~env eq' ^ "\n\n");
         true        
   in 
-  let rec aux b = function
-    | Cic.Rel n, Cic.Rel m -> if n = m then true else false
-    | ((Cic.Appl l) as left),((Cic.Appl l') as right) ->
-        check b left right ||
-        (try 
-          List.for_all2 (fun t t' -> aux true (t,t')) (List.tl l) (List.tl l')
-        with Invalid_argument _ -> false)
-    | (Cic.Meta _),_ 
-    | _,(Cic.Meta _) -> false
-    | _ -> false
+  let rec aux b (ok_so_far, subsumption_used) t1 t2  = 
+    match t1,t2 with
+      | t1, t2 when not ok_so_far -> ok_so_far, subsumption_used
+      | t1, t2 when subsumption_used -> t1 = t2, subsumption_used
+      | Cic.Appl (h1::l),Cic.Appl (h2::l') when h1 = h2 ->
+          let rc = check_subsumed b t1 t1 in 
+            if rc then 
+             true, true
+           else
+              (try 
+                List.fold_left2 
+                  (fun (ok_so_far, subsumption_used) t t' -> 
+                     aux true (ok_so_far, subsumption_used) t t')
+                  (ok_so_far, subsumption_used) l l'
+               with Invalid_argument _ -> false,subsumption_used)
+    | _ -> false, subsumption_used
   in
-  aux false (left,right)
+  fst (aux false (true,false) left right)
 ;;
 
 (*
@@ -618,21 +624,21 @@ let simplify_goals env goals ?passive active =
 (** simplifies active usign new *)
 let backward_simplify_active env new_pos new_table min_weight active =
   let active_list, active_table = active in
-  let active_list, newa = 
+  let active_list, newa, pruned = 
     List.fold_right
-      (fun equality (res, newn) ->
-         let ew, _, _, _,_ = Equality.open_equality equality in
+      (fun equality (res, newn,pruned) ->
+         let ew, _, _, _,id = Equality.open_equality equality in
          if ew < min_weight then
-           equality::res, newn
+           equality::res, newn,pruned
          else
            match forward_simplify env (Utils.Positive, equality) (new_pos, new_table) with
-           | None -> res, newn
+           | None -> res, newn, id::pruned
            | Some e ->
                if Equality.compare equality e = 0 then
-                 e::res, newn
+                 e::res, newn, pruned
                else 
-                 res, e::newn)
-      active_list ([], [])
+                 res, e::newn, pruned)
+      active_list ([], [],[])
   in
   let find eq1 where =
     List.exists (Equality.meta_convertibility_eq eq1) where
@@ -891,6 +897,7 @@ let print_goals goals =
 ;;
 
 let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table =
+  prerr_endline "check_goal_subsumed";
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
@@ -902,8 +909,10 @@ let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table =
            | Some (subst, equality ) ->
                let (_,(np,p),(ty,l,r,_),m,id) = 
                  Equality.open_equality equality in
+              prerr_endline "1";
                let p = Equality.apply_subst subst 
                  (Equality.build_proof_term_old p) in
+              prerr_endline "2";
                let newp =
                  let rec repl = function
                    | Equality.ProofGoalBlock (_, gp) ->
@@ -919,9 +928,12 @@ let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table =
                  in
                    repl proof
                in
+              prerr_endline "3";
                let newcicp,np,subst,cicmenv = 
-                 cicproof,np, subst, Equality.apply_subst_metasenv subst (m @ menv) 
+                 cicproof,np, subst, 
+                 Equality.apply_subst_metasenv subst (m @ menv) 
                in
+              prerr_endline ".";
                  Some 
                   ((newcicp,np,subst,cicmenv),
                    (newp, Equality.apply_subst_metasenv subst m @ menv ))
@@ -1119,8 +1131,8 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
           (* weight_age_counter := !weight_age_counter + 1; *)
           given_clause_fullred dbd env goals theorems passive active
       | Some current ->
-          prerr_endline (Printf.sprintf "selected sipl: %s"
-                               (Equality.string_of_equality ~env current));
+(*          prerr_endline (Printf.sprintf "selected simpl: %s"
+                               (Equality.string_of_equality ~env current));*)
           let t1 = Unix.gettimeofday () in
           let new' = infer env current active in
           let _ =
@@ -1478,6 +1490,7 @@ let saturate
   let goal' = goal in
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+  let names = names_of_context context in
   let eq_indexes, equalities, maxm = find_equalities context proof in
   let new_meta_goal, metasenv, type_of_goal =
     let irl =
@@ -1555,6 +1568,11 @@ let saturate
          (proof, proof_menv))) (* OLD *)
       ->
       prerr_endline "OK, found a proof!";
+
+      prerr_endline "NEWPROOF";
+     (* prerr_endline (Equality.string_of_proof_new ~names newproof
+      * goalproof);*)
+      prerr_endline (Equality.pp_proof names goalproof newproof);
       
       (* generation of the old proof *)
       let cic_proof = Equality.build_proof_term_old proof in
@@ -1607,15 +1625,10 @@ let saturate
       in
 
       (* 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 "NEWPROOF";
-     (* 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); *)
 
@@ -1627,9 +1640,8 @@ let saturate
         in
         List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
       in
-      let newmetasenv = newmetasenv@proof_menv in
       let newmetasenv_new = newmetasenv@newproof_menv in
-
+      let newmetasenv = newmetasenv@proof_menv in
       (* check/refine/... build the new proof *)
       let newstatus =
         let cic_proof,newmetasenv,proof_menv,ty, ug =
@@ -1670,8 +1682,8 @@ let saturate
           in
           if List.length newmetasenv_new <> 0 then
             prerr_endline 
-              ("Some METAS are still open: " ^ CicMetaSubst.ppmetasenv
-               [] newmetasenv_new);
+              ("Some METAS are still open: "(* ^ CicMetaSubst.ppmetasenv
+               [] newmetasenv_new*));
           cic_proof_new, newmetasenv_new, newmetasenv_new,new_ty, newug
           (* THE OLD PROOF: cic_proof,newmetasenv,proof_menv,oldty,oldug *)
         in