New modules stack:

[helm.git] / helm / software / components / tactics / paramodulation / saturation.ml

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index b2970d209c39c5edbd3e2d5057b933bc4942ef42..5fa1dafeb288c537e1d67a98d2b7ebd6ec6880b1 100644 (file)
--- 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 *)
@@ -820,8 +824,8 @@ let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) =
          Equality.mk_equality bag
            (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) 
       in
-(*      match Indexing.subsumption env table goal_equation with*)
-       match Indexing.unification env table goal_equation with 
+       match Indexing.subsumption env table goal_equation with 
+       (* match Indexing.unification env table goal_equation with *)
         | Some (subst, equality, swapped ) ->
 (*
             prerr_endline 
@@ -862,7 +866,8 @@ let find_all_subsumed bag maxm env table (goalproof,menv,ty) =
               else
                  p
              in (goalproof, p, id, subst, cicmenv))
-         (Indexing.unification_all env table goal_equation)
+          (Indexing.subsumption_all env table goal_equation)
+         (* (Indexing.unification_all env table goal_equation) *)
   | _ -> assert false
 ;;
 
@@ -882,7 +887,7 @@ let check_if_goal_is_identity env = function
       let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in
       let m = Subst.apply_subst_metasenv s m in
       Some (goalproof, reflproof, 0, s,m)
-    with _ -> None)
+    with CicUnification.UnificationFailure _ -> None)
   | _ -> None
 ;;                              
     
@@ -1592,7 +1597,7 @@ let all_subsumed bag maxm status active passive =
   let cleaned_goal = Utils.remove_local_context type_of_goal in
   let canonical_menv,other_menv = 
     List.partition (fun (_,c,_) -> c = context)  metasenv in
-  prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); 
+  (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv));   *)
   let metasenv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in
   let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
   debug_print (lazy (string_of_int (List.length (fst active))));
@@ -1612,6 +1617,7 @@ let all_subsumed bag maxm status active passive =
     match (check_if_goal_is_identity env goal) with
        None -> subsumed
       | Some id -> id::subsumed in
+  debug_print (lazy "dopo subsumed");
   let res =
     List.map 
       (fun 
@@ -1621,9 +1627,15 @@ 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
+  in 
+  res, !maxmeta
 
 
 let given_clause 
@@ -1650,7 +1662,7 @@ let given_clause
   let cleaned_goal = Utils.remove_local_context type_of_goal in
   let canonical_menv,other_menv = 
     List.partition (fun (_,c,_) -> c = context)  metasenv in
-  prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv));
+  (* 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 metasenv' = List.filter (fun (i,_,_)->i<>goalno) canonical_menv in