X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=6b1b65e276eef42a34c2426490a62da745cbace4;hb=1a65db059b643422fc8eded4f4e03b512071515b;hp=1cb6d351433f158a52aa5511b51e0c36c32b1bd1;hpb=f820f75a0b94bcc6b6d31c9471c8921ce098427d;p=helm.git

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 1cb6d3514..6b1b65e27 100644
--- 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