some fixed done in Orsay:

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

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 1282ed27f1cd9f9726baccb892c06dd3c73ee6fb..fe63c7d669abed002c73b8876b60bba5abd0f834 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -708,7 +708,6 @@ let backward_simplify env new' ?passive active =
       active, passive, newa, newp *)
 ;;
 
-
 let close env new' given =
   let new_pos, new_table, min_weight =
     List.fold_left
@@ -1202,6 +1201,17 @@ let check_if_goal_is_identity env = function
     when left = right && iseq uri ->
       let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
       Some (goalproof, reflproof, 0, Subst.empty_subst,m)
+  | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) 
+    when iseq uri ->
+    (let _,context,_ = env in
+    try 
+     let s,m,_ = 
+       Inference.unification m m context left right CicUniv.empty_ugraph 
+     in
+      let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
+      let m = Subst.apply_subst_metasenv s m in
+      Some (goalproof, reflproof, 0, s,m)
+    with _ -> None)
   | _ -> None
 ;;                              
     
@@ -1270,10 +1280,16 @@ let infer_goal_set env active goals =
 let infer_goal_set_with_current env current goals = 
   let active_goals, passive_goals = goals in
   let _,table,_ = build_table [current] in
+  let _,_,_,_,id = Equality.open_equality current in
   active_goals,
   List.fold_left 
     (fun acc g ->
       let new' = Indexing.superposition_left env table g in
+      if id = 2 then
+        begin
+        prerr_endline "XXXXXXX";
+        List.iter (fun _,_,e -> prerr_endline (CicPp.ppterm e)) new' ;
+       end;
       acc @ new')
     passive_goals active_goals
 ;;
@@ -1288,6 +1304,7 @@ let size_of_goal_set_p (_,l) = List.length l;;
 let given_clause 
   ((_,context,_) as env) goals theorems passive active max_iterations max_time
 = 
+  let names = names_of_context context in
   let initial_time = Unix.gettimeofday () in
   let iterations_left iterno = 
     let now = Unix.gettimeofday () in
@@ -1339,13 +1356,18 @@ let given_clause
             ParamodulationFailure "No more passive"(*maybe this is a success! *)
           else
             begin
+              let goals = infer_goal_set env active goals in
+              let goals = infer_goal_set env active goals in
               let goals = infer_goal_set env active goals in
               let current, passive = select env goals passive in
+              let _,_,goaltype = List.hd (fst goals) in                
+              prerr_endline (Printf.sprintf  "Current goal = %s\n"
+                (CicPp.pp goaltype names));
               prerr_endline (Printf.sprintf  "Selected = %s\n"
                 (Equality.string_of_equality ~env current));
               (* SIMPLIFICATION OF CURRENT *)
               let res = 
-                forward_simplify env (Positive, current) ~passive active 
+                forward_simplify env (Positive, current) (*~passive*) active 
               in
               match res with
               | None -> step goals theorems passive active (iterno+1)
@@ -1376,6 +1398,14 @@ let given_clause
                     | Some p, Some rp -> simplify (new' @ p @ rp) active passive
                   in
                   let active, passive, new' = simplify new' active passive in
+                  if iterno = 36 || iterno = 654 then
+                   begin 
+                     prerr_endline "...................";
+                     List.iter 
+                       (fun x -> prerr_endline (Equality.string_of_equality 
+~env:env x)) new';
+                     prerr_endline "FINE...................";
+                   end;
                   prerr_endline "simpl goal with new";
                   let goals = 
                     let a,b,_ = build_table new' in
@@ -1732,6 +1762,8 @@ let saturate
         let initial = Equality.add_subst subsumption_subst newproof in
         Equality.build_goal_proof goalproof initial type_of_goal side_effects
       in
+      let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
+      let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
 (*prerr_endline (CicPp.pp goal_proof names);*)
       (* ?? *)
       let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in
@@ -1750,7 +1782,10 @@ let saturate
                | None ->
                    [i,context,ty], (Cic.Meta(i,[]))::acc2, 
                    (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) 
-          ([],[],[],None) proof_menv 
+          ([],[],[],None) 
+          (List.filter 
+          (fun (i,_,_) -> List.mem i metas_still_open_in_proof) 
+          proof_menv)
       in
       let replace where = 
         (* we need this fake equality since the metas of the hypothesis may be