Changed auto from implicit to option and renamed a few functions.

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

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index b5026d32079bcb435d6301da675e9f9b9969234a..dc1f1273f650731f130d5f00d77c794363f5566a 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -1367,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
@@ -1375,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 >>>>>>>>>>>>" ^
@@ -1402,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);
@@ -1431,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;
@@ -1447,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;
@@ -1557,10 +1557,10 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
   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
+    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
   if library_equalities = [] then prerr_endline "VUOTA!!!";
@@ -1638,7 +1638,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
@@ -1743,12 +1743,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
@@ -1827,9 +1827,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