Implemented:

[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 050d5c64333d223a7dbe3a2702495256867233e9..cdfcf8c73ec560dfaf887bb9540e0267e4503659 100644 (file)
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -319,70 +319,17 @@ let int params name default =
 
 let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
   (* argument parsing *)
-  let int = int params 
-  and string = string params 
-  and bool = bool params in
+  let int = int params in
+  let 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
-  let use_paramod = bool "use_paramod" true in
   let use_only_paramod = bool "paramodulation" false in
-  (* hacks to debug paramod *)
-  let superposition = bool "superposition" false in
-  let target = string "target" "" in
-  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 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 oldmetasenv = metasenv in
-      let flags = {
-        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.dont_cache_failures = false
-      }
-      in
-      match Auto.auto dbd cache context metasenv [goal] flags with
-      | None,cache -> 
-          raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
-      | Some (subst,metasenv),cache -> 
-          let proof,metasenv = 
-            ProofEngineHelpers.subst_meta_and_metasenv_in_proof
-              proof goal (CicMetaSubst.apply_subst subst) metasenv
-          in
-          let opened = 
-            ProofEngineHelpers.compare_metasenvs ~oldmetasenv
-              ~newmetasenv:metasenv
-          in
-          proof,opened
-;;
+  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
+  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
+   if not newauto then 
+    auto_tac_old ~depth ~width ~dbd () (proof,goal)
+   else
+    ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params) (proof,goal)
 
 let auto_tac ~params ~dbd =
       ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd)