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

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index c65826a4feab8e9e319df6219c65a8db70d516ca..1e99c9b640f4f78fbfd09d2f4702f5b7ca768005 100644 (file)
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -30,13 +30,13 @@ let debug_print s = () (*prerr_endline s;;*)
 
 (* {{{ *********** local given_clause wrapper ***********)
 
-let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status =
+let given_clause dbd ?tables maxm auto cache subst flags smart_flag status =
   let active,passive,bag,cache,maxmeta,goal_steps,saturation_steps,timeout =
     match tables with
     | None -> 
         (* first time, do a huge saturation *)
         let bag, equalities, cache, maxmeta = 
-          Saturation.find_equalities dbd status ?auto smart_flag cache
+          Saturation.find_equalities dbd status smart_flag auto cache
         in
         let passive = Saturation.make_passive equalities in
         let active = Saturation.make_active [] in
@@ -50,8 +50,8 @@ let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status =
         (* saturate a bit more if cache cahnged *)
         let bag, equalities, cache, maxm = 
           if cache_size oldcache <> cache_size cache then 
-            Saturation.saturate_more
-              bag active maxm status smart_flag ?auto cache
+            Saturation.close_more
+              bag active maxm status smart_flag auto cache
           else
             bag, [], cache, maxm
         in
@@ -112,7 +112,7 @@ let new_metasenv_and_unify_and_t
    let flags = 
      {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0} 
    in
-   given_clause dbd ?tables 0 cache [] flags true (proof'''',newmeta) 
+   given_clause dbd ?tables 0 None cache [] flags true (proof'''',newmeta) 
  with
  | None, active, passive, bag,_,_ -> 
      raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) 
@@ -269,7 +269,7 @@ let is_an_equational_goal = function
 ;;
 
 let equational_case 
-  dbd tables maxm ?auto cache depth fake_proof goalno goalty subst context 
+  dbd tables maxm auto cache depth fake_proof goalno goalty subst context 
     flags
 =
   let ppterm = ppterm context in
@@ -280,7 +280,7 @@ let equational_case
   prerr_endline "</CACHE>";
 *)
   match 
-    given_clause dbd ?tables maxm ?auto cache subst flags false (fake_proof,goalno) 
+    given_clause dbd ?tables maxm auto cache subst flags false (fake_proof,goalno) 
   with
   | None, active,passive, bag, cache, maxmeta -> 
       let tables = Some (active,passive,bag,cache) in
@@ -475,7 +475,7 @@ let rec auto_main dbd tables maxm context flags elems cache =
           if is_equational_case goalty flags then
             match 
               equational_case dbd tables maxm
-                ~auto:callback_for_paramod cache
+                (Some callback_for_paramod) cache
                 depth fake_proof goalno goalty subst context flags 
             with
             | Some elems, tables, cache, maxm -> 

diff --git a/components/tactics/paramodulation/equality_retrieval.ml b/components/tactics/paramodulation/equality_retrieval.ml
index 4637a1a4342a1a389a45a6a504d719fd57146b9b..886cc7ffe2e1ca03840279ea0d71d115d2c7cfd6 100644 (file)
--- a/components/tactics/paramodulation/equality_retrieval.ml
+++ b/components/tactics/paramodulation/equality_retrieval.ml
@@ -133,12 +133,12 @@ let equations_blacklist =
 *)
 let equations_blacklist = UriManager.UriSet.empty;;
 
-(* {{{ ****************** SATURATION STUFF ***************************)
-exception UnableToSaturate of AutoCache.cache * int
+(*****************************************************************)
+exception AutoFailure of AutoCache.cache * int
 
-let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;;
+let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;; 
 
-let saturate_term context metasenv oldnewmeta term cache auto fast = 
+let close_hypothesis_of_term context metasenv oldnewmeta term cache auto fast = 
   let head, metasenv, args, newmeta =
     ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
   in
@@ -181,7 +181,7 @@ let saturate_term context metasenv oldnewmeta term cache auto fast =
            use_paramod=true;use_only_paramod=false} 
       in
       match auto newmeta flags proof context cache args_for_auto with
-      | [],cache,newmeta -> raise (UnableToSaturate (cache,newmeta))
+      | [],cache,newmeta -> raise (AutoFailure (cache,newmeta))
       | substs,cache,newmeta ->
           List.map 
             (fun subst ->
@@ -202,7 +202,7 @@ let saturate_term context metasenv oldnewmeta term cache auto fast =
 (* }}} ***************************************************************)
 
 let find_context_equalities 
-  maxmeta bag ?(auto = default_auto) context proof cache 
+  maxmeta bag auto context proof cache 
 =
   prerr_endline "find_equalities";
   let module C = Cic in
@@ -210,6 +210,12 @@ let find_context_equalities
   let module T = CicTypeChecker in
   let _,metasenv,_,_ = proof in
   let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
+  let use_auto, auto =
+    match auto with
+      | None -> false, default_auto
+      | Some auto -> true, auto in
+  (* if use_auto is true, we try to close the hypothesis of equational
+    statements using auto; a naif, and probably wrong approach *)
   let rec aux cache index newmeta = function
     | [] -> [], newmeta,cache
     | (Some (_, C.Decl (term)))::tl ->
@@ -218,11 +224,11 @@ let find_context_equalities
              (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
         let do_find context term =
           match term with
-          | C.Prod (name, s, t) when is_an_equality t ->
+          | C.Prod (name, s, t) when (is_an_equality t && use_auto) ->
               (try 
                 let term = S.lift index term in
                 let saturated,cache,newmeta = 
-                  saturate_term context metasenv newmeta term 
+                  close_hypothesis_of_term context metasenv newmeta term 
                     cache auto false
                 in
                 let eqs,newmeta = 
@@ -236,7 +242,7 @@ let find_context_equalities
                    ([],newmeta) saturated
                 in
                  eqs, newmeta, cache
-              with UnableToSaturate (cache,newmeta) ->
+              with AutoFailure (cache,newmeta) ->
                 [],newmeta,cache)
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
               when LibraryObjects.is_eq_URI uri ->
@@ -261,7 +267,7 @@ let find_context_equalities
 ;;
 
 let find_library_equalities bag
-  ?(auto = default_auto) caso_strano dbd context status maxmeta cache 
+  auto caso_strano dbd context status maxmeta cache 
 = 
   let module C = Cic in
   let module S = CicSubstitution in
@@ -296,6 +302,12 @@ let find_library_equalities bag
  let candidates = List.map utty_of_u eqs in
  let candidates = List.filter is_monomorphic_eq candidates in
  let candidates = List.filter is_var_free candidates in
+ let use_auto, auto =
+    match auto with
+      | None -> false, default_auto
+      | Some auto -> true, auto in
+  (* if use_auto is true, we try to close the hypothesis of equational
+    statements using auto; a naif, and probably wrong approach *)
  let rec aux cache newmeta = function
     | [] -> [], newmeta, cache
     | (uri, term, termty)::tl ->
@@ -305,10 +317,10 @@ let find_library_equalities bag
                 (CicPp.ppterm term) (CicPp.ppterm termty)));
         let res, newmeta, cache = 
           match termty with
-          | C.Prod (name, s, t) ->
+          | C.Prod (name, s, t) when use_auto ->
               (try
                 let saturated,cache,newmeta = 
-                  saturate_term context metasenv newmeta termty 
+                  close_hypothesis_of_term context metasenv newmeta termty 
                     cache auto true
                 in
                 let eqs,newmeta = 
@@ -327,8 +339,9 @@ let find_library_equalities bag
                    ([],newmeta) saturated
                 in
                  eqs, newmeta , cache
-              with UnableToSaturate (cache,newmeta) ->
+               with AutoFailure (cache,newmeta) ->
                 [], newmeta , cache)
+          | C.Prod _ ->  [], newmeta, cache
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] -> 
               let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in
               [e], newmeta+1, cache

diff --git a/components/tactics/paramodulation/equality_retrieval.mli b/components/tactics/paramodulation/equality_retrieval.mli
index e9506580dc2792dc9ab709f894487f687cbe9aa5..7a24e3a556ee0142fbc6abfe478a666e191d94b4 100644 (file)
--- a/components/tactics/paramodulation/equality_retrieval.mli
+++ b/components/tactics/paramodulation/equality_retrieval.mli
@@ -43,7 +43,7 @@ type auto_type =
 val find_context_equalities:
   int -> (* maxmeta *)
   Equality.equality_bag ->
-  ?auto:auto_type ->
+  auto_type option ->
   Cic.context -> ProofEngineTypes.proof -> (* FIXME:Why bot context and proof?*)
   AutoCache.cache -> 
     int list * Equality.equality list * int * AutoCache.cache
@@ -53,7 +53,7 @@ val find_context_equalities:
 *)
 val find_library_equalities:
   Equality.equality_bag ->
-  ?auto:auto_type ->
+  auto_type option->
   bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
   AutoCache.cache ->  
     UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int *

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

diff --git a/components/tactics/paramodulation/saturation.mli b/components/tactics/paramodulation/saturation.mli
index d16c9e28a8aa9f8653b149c82b8c03fd025f5e5c..aa8f24ec3f0a842b011d95ba6fc14634ba13a791 100644 (file)
--- a/components/tactics/paramodulation/saturation.mli
+++ b/components/tactics/paramodulation/saturation.mli
@@ -32,7 +32,7 @@ val saturate : (* FIXME: should be exported a a tactic *)
   ?depth:int ->
   ?width:int ->
   ?timeout:float ->
-  ?auto:Equality_retrieval.auto_type ->
+  Equality_retrieval.auto_type option ->
   ProofEngineTypes.status ->
   ProofEngineTypes.proof * ProofEngineTypes.goal list
 
@@ -46,17 +46,18 @@ val find_equalities:
   HMysql.dbd ->
   ProofEngineTypes.status ->
   bool -> (* smart_flag *)
-  ?auto:Equality_retrieval.auto_type -> 
-  AutoCache.cache ->
+  Equality_retrieval.auto_type option -> 
+  AutoCache.cache -> 
   Equality.equality_bag *
     Equality.equality list * AutoCache.cache * int
-val saturate_more: 
+
+val close_more: 
   Equality.equality_bag ->
   active_table ->
   int -> (* maxmeta *)
   ProofEngineTypes.status ->
   bool -> (* smart flag *)
-  ?auto:Equality_retrieval.auto_type ->
+  Equality_retrieval.auto_type option ->
   AutoCache.cache ->
     Equality.equality_bag * Equality.equality list * AutoCache.cache * int