subst tactic put in a file on its own

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

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index 25696d7945448532efe981a56979a6bb61398320..79cf52e65fa7bfe791474ef02e08a52c6530e5c6 100644 (file)
--- a/components/tactics/autoTactic.ml
+++ b/components/tactics/autoTactic.ml
@@ -56,7 +56,7 @@ let search_theorems_in_context status =
   let module S = CicSubstitution in
   let module PET = ProofEngineTypes in 
   let module PT = PrimitiveTactics in 
-  let _,metasenv,_,_ = proof in
+  let _,metasenv,_,_, _ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
   let rec find n = function 
     | [] -> []
@@ -89,7 +89,7 @@ let search_theorems_in_context status =
 
 
 let compare_goals proof goal1 goal2 =
-  let _,metasenv,_,_ = proof in
+  let _,metasenv,_,_, _ = proof in
   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
   let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1 
@@ -129,7 +129,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
   if List.mem ty already_seen_goals then [] else
   let already_seen_goals = ty::already_seen_goals in
   let facts = (depth = 1) in  
-  let _,metasenv,p,_ = proof in
+  let _,metasenv,p,_, _ = proof in
     (* first of all we check if the goal has been already
        inspected *)
   assert (CicUtil.exists_meta goal metasenv);
@@ -228,7 +228,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
 and auto_new dbd width already_seen_goals universe = function
   | [] -> []
   | (subst,(proof, goals, sign))::tl ->
-      let _,metasenv,_,_ = proof in
+      let _,metasenv,_,_, _ = proof in
       let goals'=
         List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
       in
@@ -244,7 +244,7 @@ and auto_new_aux dbd width already_seen_goals universe = function
       (List.length goals) > width -> 
       auto_new dbd width already_seen_goals universe tl 
   | (subst,(proof, (goal,depth)::gtl, sign))::tl -> 
-      let _,metasenv,p,_ = proof in
+      let _,metasenv,p,_, _ = proof in
       let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
       match (auto_single dbd proof goal ey ty depth
         (width - (List.length gtl)) sign already_seen_goals) universe
@@ -284,9 +284,9 @@ let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
     | (_,(proof,[],_))::_ ->
         let t2 = Unix.gettimeofday () in
         debug_print (lazy "AUTO_TAC HA FINITO");
-        let _,_,p,_ = proof in
+        let _,_,p,_, _ = proof in
         debug_print (lazy (CicPp.ppterm p));
-        Printf.printf "tempo: %.9f\n" (t2 -. t1);
+        debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)));
         (proof,[])
     | _ -> assert false
   in
@@ -317,20 +317,22 @@ let int params name default =
         raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
 ;;  
 
-let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
+let auto_tac ~params ~(dbd:HMysql.dbd) ~universe (proof, goal) =
   (* argument parsing *)
   let int = int params in
   let bool = bool params in
-  let newauto = bool "new" false in
+  let oldauto = bool "old" false in
+  let use_only_paramod = bool "paramodulation" false in
+  let oldauto = if use_only_paramod then false else oldauto in
   let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
   let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
-   if not newauto then 
+   if oldauto then 
     auto_tac_old ~depth ~width ~dbd () (proof,goal)
    else
-    ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params) (proof,goal)
+    ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params ~universe) (proof,goal)
 
-let auto_tac ~params ~dbd =
-      ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd)
+let auto_tac ~params ~dbd ~universe=
+      ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe)
 ;;
 
 let pp_proofterm = Equality.pp_proofterm;;