added homepage URL, now we have one

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

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index def8047901aaf9ced990e9b66af64debeb8149bf..85c5c54be30300beb690e0d20a7c946afe11925a 100644 (file)
--- 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 _ -> () *)
 
@@ -53,13 +53,12 @@ let search_theorems_in_context status =
   let module PT = PrimitiveTactics in 
   let _,metasenv,_,_ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
-  let ctxlen = List.length context in
   let rec find n = function 
     | [] -> []
     | hd::tl ->
         let res =
           (* we should check that the hypothesys has not been cleared *)
-          if List.nth context (ctxlen - n) = None then
+          if List.nth context (n-1) = None then
             None
           else
             try
@@ -72,7 +71,7 @@ let search_theorems_in_context status =
               *)
               Some (subst,(proof, goal_list))
             with 
-              PET.Fail _ -> None 
+             PET.Fail _ -> None 
         in
         (match res with
         | Some res -> res::(find (n+1) tl)
@@ -276,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)
   ()
 =
@@ -284,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)
+;;