From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 25 Oct 2006 09:41:45 +0000 (+0000)
Subject: Added a couple of flags to auto
X-Git-Tag: 0.4.95@7852~853
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fa8d697d64d04b11ca967ec983990837c27b1122;p=helm.git

Added a couple of flags to auto
---

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 06aa8b303..698053b40 100644
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -933,9 +933,11 @@ let int params name default =
 let flags_of_params params ?(for_applyS=false) () =
  let int = int params in
  let bool = bool params in
+ let close_more = bool "close_more" false in
  let use_paramod = bool "use_paramod" true in
  let use_only_paramod =
   if for_applyS then true else bool "paramodulation" false in
+ let use_library = bool "library" (not use_only_paramod) in
  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
  let timeout = int "timeout" 0 in
@@ -948,9 +950,11 @@ let flags_of_params params ?(for_applyS=false) () =
        else
          infinity
       else
-       Unix.gettimeofday() +. (float_of_int timeout); 
+       Unix.gettimeofday() +. (float_of_int timeout);
+    AutoTypes.use_library = use_library; 
     AutoTypes.use_paramod = use_paramod;
     AutoTypes.use_only_paramod = use_only_paramod;
+    AutoTypes.close_more = close_more;
     AutoTypes.dont_cache_failures = false;
   }
 
@@ -1111,11 +1115,14 @@ let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) =
       let _,context,_ = CicUtil.lookup_meta goal metasenv in
       let flags = flags_of_params params () in
       (* just for testing *)
-      let use_library = not flags.use_only_paramod in
+      let use_library = flags.use_library in
       let tables,cache,newmeta =
 	init_cache_and_tables dbd use_library (proof, goal) in
       let tables,cache,newmeta =
-	close_more tables newmeta context (proof, goal) auto_all_solutions cache in
+        if flags.close_more then
+	  close_more 
+	    tables newmeta context (proof, goal) auto_all_solutions cache 
+	else tables,cache,newmeta in
       let initial_time = Unix.gettimeofday() in
       let (_,oldmetasenv,_,_) = proof in
       let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
diff --git a/components/tactics/autoTypes.ml b/components/tactics/autoTypes.ml
index 93205c836..9031a0338 100644
--- a/components/tactics/autoTypes.ml
+++ b/components/tactics/autoTypes.ml
@@ -27,8 +27,10 @@ type flags = {
   maxwidth: int;
   maxdepth: int;
   timeout: float;
+  use_library: bool;
   use_paramod: bool;
   use_only_paramod : bool;
+  close_more : bool; 
   dont_cache_failures: bool;
 }
 
@@ -36,8 +38,10 @@ let default_flags _ =
   {maxwidth=3;
    maxdepth=3;
    timeout=Unix.gettimeofday() +.3.0;
+   use_library=true;
    use_paramod=true;
    use_only_paramod=false;
+   close_more=false; 
    dont_cache_failures=false}
 ;;
 
diff --git a/components/tactics/autoTypes.mli b/components/tactics/autoTypes.mli
index d3081b0ab..5014f41ce 100644
--- a/components/tactics/autoTypes.mli
+++ b/components/tactics/autoTypes.mli
@@ -27,8 +27,10 @@ type flags = {
   maxwidth: int;
   maxdepth: int;
   timeout: float;
+  use_library: bool;
   use_paramod: bool;
   use_only_paramod : bool;
+  close_more : bool;
   dont_cache_failures: bool
 }