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 d0a44c561057b3d0a0b51dad25a7c5e31f602402..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 _ -> () *)
 
@@ -54,27 +54,32 @@ let search_theorems_in_context status =
   let _,metasenv,_,_ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
   let rec find n = function 
-      [] -> []
+    | [] -> []
     | hd::tl ->
-       let res =
-         try
-           let (subst,(proof, goal_list)) =
-              PT.apply_tac_verbose ~term:(C.Rel n) status  in
-            (* 
-           let goal_list =
-              List.stable_sort (compare_goal_list proof) goal_list in 
-            *)
-           Some (subst,(proof, goal_list))
-         with 
-           PET.Fail _ -> None in
-       (match res with
-         Some res -> res::(find (n+1) tl)
-       | None -> find (n+1) tl)
+        let res =
+          (* we should check that the hypothesys has not been cleared *)
+          if List.nth context (n-1) = None then
+            None
+          else
+            try
+              let (subst,(proof, goal_list)) =
+                PT.apply_tac_verbose ~term:(C.Rel n) status  
+              in
+              (* 
+                 let goal_list =
+                   List.stable_sort (compare_goal_list proof) goal_list in 
+              *)
+              Some (subst,(proof, goal_list))
+            with 
+             PET.Fail _ -> None 
+        in
+        (match res with
+        | Some res -> res::(find (n+1) tl)
+        | None -> find (n+1) tl)
   in
   try 
     find 1 context
-  with Failure s -> 
-    []
+  with Failure s -> []
 ;;     
 
 
@@ -117,7 +122,7 @@ let is_in_metasenv goal metasenv =
     let (_, ey ,ty) =
       CicUtil.lookup_meta goal metasenv in
       true
-  with _ -> false 
+  with CicUtil.Meta_not_found _ -> false 
 
 let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
  universe
@@ -223,21 +228,21 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
     end
       
 and auto_new dbd width already_seen_goals universe = function
-    [] -> []
+  | [] -> []
   | (subst,(proof, goals, sign))::tl ->
       let _,metasenv,_,_ = proof in
       let is_in_metasenv (goal, _) =
-       try
-         let (_, ey ,ty) =
-           CicUtil.lookup_meta goal metasenv in
-           true
-       with _ -> false in
+        try
+          let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
+          true
+        with CicUtil.Meta_not_found _ -> false 
+      in
       let goals'= List.filter is_in_metasenv goals in
-       auto_new_aux dbd width already_seen_goals universe
-         ((subst,(proof, goals', sign))::tl)
+       auto_new_aux dbd 
+        width already_seen_goals universe ((subst,(proof, goals', sign))::tl)
 
 and auto_new_aux dbd width already_seen_goals universe = function
-  [] -> []
+  | [] -> []
   | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
   | (subst,(proof, (goal,0)::_, _))::tl -> 
       auto_new dbd width already_seen_goals universe tl
@@ -270,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)
   ()
 =
@@ -278,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)
+;;