resumed ol auto

[helm.git] / helm / software / components / tactics / autoTactic.ml

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 03fdf9555ea00048d4bb4ef9c4784163d40094b8..050d5c64333d223a7dbe3a2702495256867233e9 100644 (file)
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -266,14 +266,41 @@ and auto_new_aux dbd width already_seen_goals universe = function
         | _ -> assert false
  ;; 
 
+let default_depth = 5
+let default_width = 3
+
+let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
+  ()
+=
+  let auto_tac dbd (proof,goal) =
+  let universe = MetadataQuery.signature_of_goal ~dbd (proof,goal) in
+  Hashtbl.clear inspected_goals;
+  debug_print (lazy "Entro in Auto");
+  let id t = t in
+  let t1 = Unix.gettimeofday () in
+  match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with
+      [] ->  debug_print (lazy "Auto failed");
+        raise (ProofEngineTypes.Fail (lazy "No Applicable theorem"))
+    | (_,(proof,[],_))::_ ->
+        let t2 = Unix.gettimeofday () in
+        debug_print (lazy "AUTO_TAC HA FINITO");
+        let _,_,p,_ = proof in
+        debug_print (lazy (CicPp.ppterm p));
+        Printf.printf "tempo: %.9f\n" (t2 -. t1);
+        (proof,[])
+    | _ -> assert false
+  in
+  auto_tac dbd
+;;
+
 let bool params name default =
     try 
       let s = List.assoc name params in 
-      if s = "" || s = "1" || s = "true" || s = "yes" then true
-      else if s = "0" || s = "false" || s = "no" then false
+      if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
+      else if s = "0" || s = "false" || s = "no" || s= "off" then false
       else 
         let msg = "Unrecognized value for parameter "^name^"\n" in
-        let msg = msg ^ "Accepted values are 1,true,yes and 0,false,no" in
+        let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
         raise (ProofEngineTypes.Fail (lazy msg))
     with Not_found -> default
 ;; 
@@ -295,6 +322,7 @@ let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
   let int = int params 
   and string = string params 
   and bool = bool params in
+  let newauto = bool "new" false 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
@@ -306,31 +334,42 @@ let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
   let table = string "table" "" in
   let subterms_only = bool "subterms_only" false in
   let demod_table = string "demod_table" "" in
+  let newauto = if use_only_paramod then true else newauto in
   match superposition with
   | true -> 
       (* this is the ugly hack to debug paramod *)
       Saturation.superposition_tac 
         ~target ~table ~subterms_only ~demod_table (proof,goal)
   | false -> 
+      if not newauto then 
+        auto_tac_old ~depth ~width ~dbd () (proof,goal)
+      else
       (* this is the real auto *)
       let _, metasenv, _, _ = proof in
       let _, context, goalty = CicUtil.lookup_meta goal metasenv in
-      let universe = 
-        AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe 
+      let cache = 
+        let cache = 
+          AutoCache.cache_add_context context metasenv AutoCache.cache_empty 
+        in
+        if use_only_paramod then (* only paramod *)
+          cache
+        else
+          AutoCache.cache_add_library dbd proof [goal] cache
       in 
-      let universe = AutoTypes.universe_of_context context metasenv universe in
       let oldmetasenv = metasenv in
       let flags = {
-        AutoTypes.maxdepth = depth;
+        AutoTypes.maxdepth = 
+          if use_only_paramod then 2 else depth;
         AutoTypes.maxwidth = width;
         AutoTypes.timeout = 
           if timeout = 0 then float_of_int timeout 
           else Unix.gettimeofday() +. (float_of_int timeout); 
         AutoTypes.use_paramod = use_paramod;
-        AutoTypes.use_only_paramod = use_only_paramod}
+        AutoTypes.use_only_paramod = use_only_paramod;
+        AutoTypes.dont_cache_failures = false
+      }
       in
-      let cache = AutoTypes.cache_empty in
-      match Auto.auto dbd universe cache context metasenv [goal] flags with
+      match Auto.auto dbd cache context metasenv [goal] flags with
       | None,cache -> 
           raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
       | Some (subst,metasenv),cache ->