1. applyS now uses its ~params

2. autoTactic.ml* is going to be deprecated.
   auto.ml* has now the expected interface (that of a tactic)
   and it is almost ready to replace autoTactic.ml

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 117978d8c646c3b06f932fc497b277f3bea8ec50..305a42ab1adfab718e77d1e4d8f33bd7b919045e 100644 (file)
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -75,7 +75,8 @@ let given_clause dbd ?tables maxm auto cache subst flags smart_flag status =
 (* {{{ **************** applyS *******************)
 
 let new_metasenv_and_unify_and_t 
-  dbd proof goal ?tables newmeta' metasenv' context term' ty termty goal_arity 
+ dbd flags proof goal ?tables newmeta' metasenv' context term' ty termty
+ goal_arity 
 =
  let (consthead,newmetasenv,arguments,_) =
    ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
@@ -108,10 +109,7 @@ let new_metasenv_and_unify_and_t
    PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal) 
  in
  match 
-   let cache, flags = cache_empty, default_flags() in
-   let flags = 
-     {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0} 
-   in
+   let cache = cache_empty in
    given_clause dbd ?tables 0 None cache [] flags true (proof'''',newmeta) 
  with
  | None, active, passive, bag,_,_ -> 
@@ -127,7 +125,7 @@ let rec count_prods context ty =
     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
   | _ -> 0
 
-let apply_smart ~dbd ~term ~subst ?tables (proof, goal) =
+let apply_smart ~dbd ~term ~subst ?tables flags (proof, goal) =
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
@@ -173,7 +171,7 @@ let apply_smart ~dbd ~term ~subst ?tables (proof, goal) =
    let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
    let goal_arity = count_prods context ty in
    let subst, proof, gl, active, passive =
-    new_metasenv_and_unify_and_t dbd proof goal ?tables
+    new_metasenv_and_unify_and_t dbd flags proof goal ?tables
      newmeta' metasenv' context term' ty termty goal_arity
    in
     subst, proof, gl, active, passive
@@ -533,14 +531,110 @@ let auto dbd cache context metasenv gl flags =
   | Fail s,tables,cache,maxm -> None,cache
 ;;
 
+let bool params name default =
+    try 
+      let s = List.assoc name params in 
+      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,on and 0,false,no,off" in
+        raise (ProofEngineTypes.Fail (lazy msg))
+    with Not_found -> default
+;; 
+
+let string params name default =
+    try List.assoc name params with
+    | Not_found -> default
+;; 
+
+let int params name default =
+    try int_of_string (List.assoc name params) with
+    | Not_found -> default
+    | Failure _ -> 
+        raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
+;;  
+
+let flags_of_params params ?(use_only_paramod = bool params "paramodulation" false) () =
+ let int = int params in
+ let bool = bool params in
+ let use_paramod = bool "use_paramod" true 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
+  { AutoTypes.maxdepth = 
+      if use_only_paramod then 2 else depth;
+    AutoTypes.maxwidth = width;
+    AutoTypes.timeout = 
+      if timeout = 0 then
+       if use_only_paramod then Unix.gettimeofday () +. 30.0
+       else
+        0.0
+      else
+       Unix.gettimeofday() +. (float_of_int timeout); 
+    AutoTypes.use_paramod = use_paramod;
+    AutoTypes.use_only_paramod = use_only_paramod;
+    AutoTypes.dont_cache_failures = false
+  }
+
 let applyS_tac ~dbd ~term ~params =
  ProofEngineTypes.mk_tactic
   (fun status ->
     try 
-      let _, proof, gl,_,_ = apply_smart ~dbd ~term ~subst:[] status in 
-      proof, gl
+      let _, proof, gl,_,_ =
+       apply_smart ~dbd ~term ~subst:[]
+        (flags_of_params params ~use_only_paramod:true ()) status
+      in 
+       proof, gl
     with 
     | CicUnification.UnificationFailure msg
     | CicTypeChecker.TypeCheckerFailure msg ->
         raise (ProofEngineTypes.Fail msg))
 
+let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) =
+  (* argument parsing *)
+  let string = string params in
+  let bool = bool params 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
+  match superposition with
+  | true -> 
+      (* this is the ugly hack to debug paramod *)
+      Saturation.superposition_tac 
+        ~target ~table ~subterms_only ~demod_table (proof,goal)
+  | false -> 
+      (* 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 = flags_of_params params () in
+      match 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 auto_tac ~dbd ~params = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd);;

diff --git a/components/tactics/auto.mli b/components/tactics/auto.mli
index c9f3b9b095655944a41c0471e02aa8eadbd25c8b..301aa4b45c83bcb44b8ce346b3eced71c843dad1 100644 (file)
--- a/components/tactics/auto.mli
+++ b/components/tactics/auto.mli
@@ -24,23 +24,8 @@
  *)
 
 (* stops at the first solution *)
-val auto: 
-  HMysql.dbd ->
-  AutoCache.cache ->
-  Cic.context ->
-  Cic.metasenv ->
-  ProofEngineTypes.goal list -> (* goals in AND *)
-  AutoTypes.flags ->
-    (Cic.substitution * Cic.metasenv) option * AutoCache.cache
-
-val auto_all_solutions: 
-  HMysql.dbd ->
-  AutoCache.cache ->
-  Cic.context ->
-  Cic.metasenv ->
-  ProofEngineTypes.goal list ->
-  AutoTypes.flags ->
-    (Cic.substitution * Cic.metasenv) list * AutoCache.cache
+val auto_tac:
+ dbd:HMysql.dbd -> params:(string * string) list -> ProofEngineTypes.tactic
 
 val applyS_tac:
  dbd:HMysql.dbd -> term: Cic.term -> params:(string * string) list ->

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index 050d5c64333d223a7dbe3a2702495256867233e9..25696d7945448532efe981a56979a6bb61398320 100644 (file)
--- a/components/tactics/autoTactic.ml
+++ b/components/tactics/autoTactic.ml
@@ -319,70 +319,15 @@ 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
-;;
+   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)

diff --git a/components/tactics/autoTactic.mli b/components/tactics/autoTactic.mli
index fadb603ebf484a5c90c4d60e9a360f10e3b3106d..23f1b813fdf727b635906c26d335bfaeeb11c839 100644 (file)
--- a/components/tactics/autoTactic.mli
+++ b/components/tactics/autoTactic.mli
@@ -25,8 +25,6 @@
  *)
 
 val auto_tac:
-  params:(string * string) list ->
-  dbd:HMysql.dbd -> 
-  ProofEngineTypes.tactic
+ params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
 
 val pp_proofterm: Cic.term -> string