timeout if unspecfied should be set to infinity, not 0, since the timeout inside...

[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 625beb839834c27a21b0b5bc17aec3a01afa3629..c23401e9cd6a0c4eba84a5fde37475ed332ca809 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -120,7 +120,7 @@ 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
+  (*EqualitySet.elements set*) eq_list, set (* see applys.ma *)
 ;;
 let make_empty_active () = [], Indexing.empty ;;
 let make_active eq_list = 
@@ -444,7 +444,7 @@ let forward_simplify bag eq_uri env current (active_list, active_table) =
       Indexing.demodulation_equality bag eq_uri !maxmeta env table current
     in
     maxmeta := newmeta;
-    if Equality.is_weak_identity newcurrent then None else Some newcurrent
+    if Equality.is_identity env newcurrent then None else Some newcurrent
   in
   let demod current =
     if Utils.debug_metas then
@@ -489,7 +489,7 @@ let forward_simplify_new bag eq_uri env new_pos active =
   let new_pos_set =
     List.fold_left
       (fun s e ->
-         if not (Equality.is_weak_identity e) then
+         if not (Equality.is_identity env e) then
            EqualitySet.add e s
          else s)
       EqualitySet.empty new_pos
@@ -556,7 +556,7 @@ let backward_simplify_active
       (fun eq ((res,pruned), tbl) ->
          if List.mem eq res then
            (res, (id_of_eq eq)::pruned),tbl 
-         else if (Equality.is_weak_identity eq) || (find eq res) then (
+         else if (Equality.is_identity env eq) || (find eq res) then (
            (res, (id_of_eq eq)::pruned),tbl
          ) 
          else
@@ -564,7 +564,7 @@ let backward_simplify_active
       active_list (([],pruned), Indexing.empty),
     List.fold_right
       (fun eq p ->
-         if (Equality.is_weak_identity eq) then p
+         if (Equality.is_identity env eq) then p
          else eq::p)
       newa []
   in
@@ -743,7 +743,7 @@ let rec simpl bag eq_uri env e others others_simpl =
   let tbl =
     List.fold_left
       (fun t e -> 
-         if Equality.is_weak_identity e then t else Indexing.index t e) 
+         if Equality.is_identity env e then t else Indexing.index t e) 
       Indexing.empty active
   in
   let res = 
@@ -1138,7 +1138,7 @@ let rec saturate_equations bag eq_uri env goal accept_fun passive active =
                              (Equality.string_of_equality ~env current)));
         let new' = infer bag eq_uri env current active in
         let active =
-          if Equality.is_weak_identity (*env*) current then active
+          if Equality.is_identity env current then active
           else
             let al, tbl = active in
             al @ [current], Indexing.index tbl current
@@ -1249,31 +1249,33 @@ let build_proof
           eq_uri goalproof initial type_of_goal side_effects
           context proof_menv
       in
-(*       prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
+      (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
       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);*)
-      (* ?? *)
+      (* prerr_endline (CicPp.pp goal_proof names); *)
       let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in
       let side_effects_t = 
         List.map (Subst.apply_subst subsumption_subst) side_effects_t
       in
       (* replacing fake mets with real ones *)
-(*       prerr_endline "replacing metas..."; *)
+      (* prerr_endline "replacing metas..."; *)
       let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
       let goal_proof_menv, what, with_what,free_meta = 
         List.fold_left 
           (fun (acc1,acc2,acc3,uniq) (i,_,ty) -> 
              match uniq with
                | Some m -> 
-(*                    acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq *)
-                   (i,context,ty)::acc1, (Cic.Meta(i,[]))::acc2, (Cic.Meta(i,irl))::acc3, uniq
+(*                     acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq  *)
+                   (i,context,ty)::acc1, (Cic.Meta(i,[]))::acc2,
+                     (Cic.Meta(i,irl))::acc3, uniq
                | None ->
                    [i,context,ty], (Cic.Meta(i,[]))::acc2, 
                    (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) 
           ([],[],[],None) 
           (List.filter 
-           (fun (i,_,_) -> List.mem i metas_still_open_in_proof) 
+           (fun (i,_,_) -> 
+             List.mem i metas_still_open_in_proof
+             (*&& not(List.mem i metas_still_open_in_goal)*)) 
            proof_menv)
       in
       let replace where = 
@@ -1293,8 +1295,9 @@ let build_proof
           (ProofEngineHelpers.compare_metasenvs 
             ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
       in
-(* prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int
- * free_metas) ); *)
+      (* prerr_endline 
+       *   ("freemetas: " ^ 
+       *   String.concat "," (List.map string_of_int free_metas) ); *)
       (* check/refine/... build the new proof *)
       let replaced_goal = 
         ProofEngineReduction.replace
@@ -1340,13 +1343,20 @@ let build_proof
             prerr_endline "THE PROOF DOES NOT TYPECHECK!";
             raise exn
       in
+
+      let metas_of_proof = Utils.metas_of_term goal_proof in
+
       let proof, real_metasenv = 
         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
           proof goalno (CicMetaSubst.apply_subst final_subst) real_menv
       in
       let open_goals = 
+        HExtlib.list_uniq (List.sort Pervasives.compare metas_of_proof) 
+      in
+(*
         match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[] 
       in
+*)
 (*
       Printf.eprintf 
         "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n" 
@@ -1357,7 +1367,7 @@ let build_proof
       final_subst, proof, open_goals
 ;;
 
-let find_equalities dbd status smart_flag ?auto cache =
+let find_equalities dbd status smart_flag auto cache =
   let proof, goalno = status in
   let _, metasenv,_,_ = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
@@ -1365,14 +1375,14 @@ let find_equalities dbd status smart_flag ?auto cache =
   let env = (metasenv, context, CicUniv.empty_ugraph) in 
   let bag = Equality.mk_equality_bag () in
   let eq_indexes, equalities, maxm, cache = 
-    Equality_retrieval.find_context_equalities 0 bag ?auto context proof cache
+    Equality_retrieval.find_context_equalities 0 bag auto context proof cache
   in
   prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>";
   List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
   prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
   let lib_eq_uris, library_equalities, maxm, cache =
     Equality_retrieval.find_library_equalities bag
-      ?auto smart_flag dbd context (proof, goalno) (maxm+2)
+      auto smart_flag dbd context (proof, goalno) (maxm+2)
       cache
   in
   prerr_endline (">>>>>>>>>>  gained from the library >>>>>>>>>>>>" ^
@@ -1392,14 +1402,14 @@ let find_equalities dbd status smart_flag ?auto cache =
   bag, equalities, cache, maxm
 ;;
 
-let saturate_more bag active maxmeta status smart_flag ?auto cache =
+let close_more bag active maxmeta status smart_flag auto cache =
   let proof, goalno = status in
   let _, metasenv,_,_ = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
   let env = (metasenv, context, CicUniv.empty_ugraph) in 
   let eq_indexes, equalities, maxm, cache = 
-    Equality_retrieval.find_context_equalities maxmeta bag ?auto context proof cache
+    Equality_retrieval.find_context_equalities maxmeta bag auto context proof cache
   in
   prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
     string_of_int maxm);
@@ -1421,7 +1431,7 @@ let saturate_more bag active maxmeta status smart_flag ?auto cache =
 let saturate 
     smart_flag 
     dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) 
-    ?(timeout=600.) ?auto status = 
+    ?(timeout=600.) auto status = 
   let module C = Cic in
   reset_refs ();
   maxdepth := depth;
@@ -1437,7 +1447,7 @@ let saturate
   let env = (metasenv, context, ugraph) in 
   let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
   let bag, equalities, cache, maxm = 
-    find_equalities dbd status smart_flag ?auto AutoCache.cache_empty 
+    find_equalities dbd status smart_flag auto AutoCache.cache_empty 
   in
   let res, time =
     maxmeta := maxm+2;
@@ -1544,23 +1554,12 @@ let given_clause
 let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = 
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let eq_uri = eq_of_goal ty in
-  let bag = Equality.mk_equality_bag () in
-  let eq_indexes, equalities, maxm, cache = 
-    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty
-  in
-  let lib_eq_uris, library_equalities, maxm, cache =
-    Equality_retrieval.find_library_equalities bag 
-      false dbd context (proof, goal) (maxm+2)  cache 
-  in
-  if library_equalities = [] then prerr_endline "VUOTA!!!";
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-  let library_equalities = List.map snd library_equalities in
   let initgoal = [], [], ty in
-  let env = (metasenv, context, CicUniv.empty_ugraph) in
-  let equalities = 
-    simplify_equalities bag eq_uri env (equalities@library_equalities) 
-  in   
+  let eq_uri = eq_of_goal ty in
+  let bag, equalities, cache, maxm =
+    find_equalities dbd (proof,goal) false None AutoCache.cache_empty 
+  in 
   let table = 
     List.fold_left 
       (fun tbl eq -> Indexing.index tbl eq) 
@@ -1628,7 +1627,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
   let names = Utils.names_of_context context in
   let bag = Equality.mk_equality_bag () in
   let eq_index, equalities, maxm,cache  = 
-    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty 
+    Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty 
   in
   let eq_what = 
     let what = find_in_ctx 1 target context in
@@ -1733,12 +1732,12 @@ let retrieve_and_print dbd term metasenv ugraph =
   let eq_uri = eq_of_goal type_of_goal in
   let bag = Equality.mk_equality_bag () in
   let eq_indexes, equalities, maxm,cache = 
-    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in
+    Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty in
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in
   let t1 = Unix.gettimeofday () in
   let lib_eq_uris, library_equalities, maxm, cache =
-    Equality_retrieval.find_library_equalities bag
+    Equality_retrieval.find_library_equalities bag None
       false dbd context (proof, goal') (maxm+2)  cache
   in 
   let t2 = Unix.gettimeofday () in
@@ -1817,9 +1816,9 @@ let main_demod_equalities dbd term metasenv ugraph =
   let eq_uri = eq_of_goal goal in 
   let bag = Equality.mk_equality_bag () in
   let eq_indexes, equalities, maxm,  cache = 
-    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in
+    Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty in
   let lib_eq_uris, library_equalities, maxm,cache =
-    Equality_retrieval.find_library_equalities bag
+    Equality_retrieval.find_library_equalities bag None
       false dbd context (proof, goal') (maxm+2)  cache
   in
   let library_equalities = List.map snd library_equalities in