X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FautoTactic.ml;h=85c5c54be30300beb690e0d20a7c946afe11925a;hb=fafa203bb8521f516a0e87ef28d2cedccb72f795;hp=568e12ca40c4b303bd182ea3688efba78070ea0f;hpb=3064844b2f594cfce55c0140ecb4d15e35364486;p=helm.git

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 568e12ca4..85c5c54be 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
- let debug_print = ignore (*prerr_endline *)
+ let debug_print = (* ignore *) prerr_endline
 
 (* let debug_print = fun _ -> () *)
 
@@ -275,6 +275,7 @@ and auto_new_aux dbd width already_seen_goals universe = function
 let default_depth = 5
 let default_width = 3
 
+(*
 let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd)
   ()
 =
@@ -283,17 +284,68 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd)
   Hashtbl.clear inspected_goals;
   debug_print "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("Auto failed");
 	raise (ProofEngineTypes.Fail "No Applicable theorem")
-    | (_,(proof,[],_))::_ ->  
+    | (_,(proof,[],_))::_ ->
+        let t2 = Unix.gettimeofday () in
 	debug_print "AUTO_TAC HA FINITO";
 	let _,_,p,_ = proof in
 	debug_print (CicPp.ppterm p);
+        Printf.printf "tempo: %.9f\n" (t2 -. t1);
 	(proof,[])
     | _ -> assert false
   in
   ProofEngineTypes.mk_tactic (auto_tac dbd)
 ;;
+*)
+
+let paramodulation_tactic = ref
+  (fun dbd status -> raise (ProofEngineTypes.Fail "Not Ready yet..."));;
+
+let term_is_equality = ref
+  (fun term -> debug_print "term_is_equality E` DUMMY!!!!"; false);;
 
 
+let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd:Mysql.dbd) () =
+  let auto_tac dbd (proof, goal) =
+    let normal_auto () = 
+      let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in
+      Hashtbl.clear inspected_goals;
+      debug_print "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("Auto failed");
+	  raise (ProofEngineTypes.Fail "No Applicable theorem")
+      | (_,(proof,[],_))::_ ->
+          let t2 = Unix.gettimeofday () in
+	  debug_print "AUTO_TAC HA FINITO";
+	  let _,_,p,_ = proof in
+	  debug_print (CicPp.ppterm p);
+          debug_print (Printf.sprintf "tempo: %.9f\n" (t2 -. t1));
+	  (proof,[])
+      | _ -> assert false
+    in
+    let paramodulation_ok =
+      match paramodulation with
+      | None -> false
+      | Some _ ->
+          let _, metasenv, _, _ = proof in
+          let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
+          !term_is_equality meta_goal
+    in
+    if paramodulation_ok then (
+      debug_print "USO PARAMODULATION...";
+(*       try *)
+        !paramodulation_tactic dbd (proof, goal)
+(*       with ProofEngineTypes.Fail _ -> *)
+(*         normal_auto () *)
+    ) else
+      normal_auto () 
+  in
+  ProofEngineTypes.mk_tactic (auto_tac dbd)
+;;