X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=aed51e35bd2d66bd1b3c44289d75d229f50538ae;hb=246f3c2f2d26655129efacf830ecff47094795b4;hp=c8ab4e428cfecdc9f9e92f672b55fdb532b00f52;hpb=b3e08a6954c8b6946f42f5c7e0bed7912d5ac87c;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index c8ab4e428..aed51e35b 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -125,8 +125,11 @@ let make_passive eq_list =
   let set =
     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list
   in
-  (*EqualitySet.elements set*) eq_list, set (* see applys.ma *)
+  (* we have the invariant that the list and the set have the same
+   * cardinality *)
+  EqualitySet.elements set, set
 ;;
+
 let make_empty_active () = [], Indexing.empty ;;
 let make_active eq_list = 
   eq_list, List.fold_left Indexing.index Indexing.empty eq_list
@@ -134,6 +137,7 @@ let make_active eq_list =
 
 let size_of_passive (passive_list, _) = List.length passive_list;;
 let size_of_active (active_list, _) = List.length active_list;;
+
 let passive_is_empty = function
   | [], s when EqualitySet.is_empty s -> true
   | [], s -> assert false (* the set and the list should be in sync *)
@@ -773,7 +777,7 @@ let simplify_equalities bag eq_uri env equalities =
        (Printf.sprintf "equalities:\n%s\n"
           (String.concat "\n"
              (List.map Equality.string_of_equality equalities))));
-  Utils.debug_print (lazy "SIMPLYFYING EQUALITIES...");
+Utils.debug_print (lazy "SIMPLYFYING EQUALITIES...");
   match equalities with
     | [] -> []
     | hd::tl ->
@@ -935,17 +939,16 @@ let infer_goal_set bag env active goals =
     | [] -> active_goals, []
     | hd::tl ->
         let changed,selected = simplify_goal bag env hd active in
-(*
-        if changed then
-          prerr_endline ("--------------- goal semplificato");
-*)
         let (_,_,t1) = selected in
+        (* 
+        if changed && Utils.debug then
+          prerr_endline ("goal semplificato: " ^  CicPp.ppterm t1); *)
         let already_in = 
           List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) 
               active_goals
         in
         if already_in then 
-             aux tl
+             aux tl 
           else
             let passive_goals = tl in
             let new_passive_goals =
@@ -1437,7 +1440,6 @@ let build_proof
       (* replacing fake mets with real ones *)
       (* prerr_endline "replacing metas..."; *)
       let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
-      if proof_menv = [] then prerr_endline "VUOTA";
       CicMetaSubst.ppmetasenv [] proof_menv;
       let what, with_what = 
         List.fold_left 
@@ -1486,7 +1488,6 @@ let build_proof
           ~where:type_of_goal
       in
       let goal_proof,goal_ty,real_menv,_ = 
-        prerr_endline "parte la refine";
         try
           CicRefine.type_of_aux' metasenv context goal_proof
             CicUniv.empty_ugraph
@@ -1623,7 +1624,12 @@ let all_subsumed bag maxm status active passive =
                status goalproof newproof subsumption_id subsumption_subst proof_menv
 	   in
 	   let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
-	   let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in
+           let newmetasenv = 
+             other_menv @ 
+             List.filter
+               (fun x,_,_ -> not (List.exists (fun y,_,_ -> x=y) other_menv)) metasenv
+           in
+	   let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in
 	     (subst, proof,gl)) subsumed_or_id 
   in 
   res, !maxmeta
@@ -1655,7 +1661,10 @@ let given_clause
     List.partition (fun (_,c,_) -> c = context)  metasenv in
   (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv));  *)
   Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
-  let canonical_menv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in
+  let canonical_menv = 
+    List.map 
+     (fun (i,_,ty)-> (i,[],Utils.remove_local_context ty)) canonical_menv 
+  in
   let metasenv' = List.filter (fun (i,_,_)->i<>goalno) canonical_menv in
   let goal = [], metasenv', cleaned_goal in
   let env = metasenv,context,CicUniv.empty_ugraph in