X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTactic.ml;h=964959ea9b4092ff134c0449e5e2b5cd0a841d5a;hb=e1f0bb910f75b8b21f2c5e394ebb4c5a63ef4945;hp=25696d7945448532efe981a56979a6bb61398320;hpb=46834f1afe49d481045a40fb1bf6ddbddcfef9f5;p=helm.git

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 25696d794..964959ea9 100644
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/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,_subst,_,_, _ = 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,_subst,_,_, _ = 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,_subst, p,_, _ = proof in
     (* first of all we check if the goal has been already
        inspected *)
   assert (CicUtil.exists_meta goal metasenv);
@@ -148,12 +148,13 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
               (* if we just apply the subtitution, the type 
                  is irrelevant: we may use Implicit, since it will 
                  be dropped *)
-              CicMetaSubst.apply_subst 
-                [(goal,(ey, bo, Cic.Implicit None))] in
+                [(goal,(ey, bo, Cic.Implicit None))] 
+            in
+            let _ = assert false in
             let (proof,_) = 
               ProofEngineHelpers.subst_meta_and_metasenv_in_proof 
                 proof goal subst_in metasenv in
-              [(subst_in,(proof,[],sign))]
+              [(CicMetaSubst.apply_subst subst_in,(proof,[],sign))]
         | No d when (d >= depth) -> 
             (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *)
             [] (* the empty list means no choices, i.e. failure *)
@@ -228,7 +229,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, _subst, _,_, _ = proof in
       let goals'=
         List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
       in
@@ -244,7 +245,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,_subst,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
@@ -269,7 +270,7 @@ and auto_new_aux dbd width already_seen_goals universe = function
 let default_depth = 5
 let default_width = 3
 
-let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
+let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HSql.dbd)
   ()
 =
   let auto_tac dbd (proof,goal) =
@@ -284,9 +285,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 _,_,_subst,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 +318,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:HSql.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;;