New implementation of experimental_hint/auto (called new_experimental_hint) that

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

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 13dac415f8298af2bc7b4f4ba486008eb72f68fb..c7cdc97acf202e72a46439e1434a1085f01602ef 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -27,10 +27,10 @@
 
 (* let debug_print = fun _ -> () *)
 
-let experimental_hint =
- let profile = CicUtil.profile "experimental_hint" in
- fun ~dbd ~facts ?signature status ->
-  profile (MetadataQuery.experimental_hint ~dbd ~facts ?signature) status
+let new_experimental_hint =
+ let profile = CicUtil.profile "new_experimental_hint" in
+ fun ~dbd ~facts ?signature ~universe status ->
+  profile (MetadataQuery.new_experimental_hint ~dbd ~facts ?signature ~universe) status
 
 let search_theorems_in_context status =
   let (proof, goal) = status in
@@ -246,6 +246,7 @@ let is_in_metasenv goal metasenv =
   with _ -> false 
 
 let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
+ universe
   =
   if depth = 0 then [] else
   if List.mem ty already_seen_goals then [] else
@@ -296,8 +297,8 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
              new_search_theorems 
                (fun status -> 
                   List.map snd
-                  (experimental_hint 
-                     ~dbd ~facts:facts ?signature:sign status))
+                  (new_experimental_hint 
+                     ~dbd ~facts:facts ?signature:sign ~universe status))
                dbd proof goal (depth-1) new_sign in 
            let all_choices =
              local_choices@global_choices in
@@ -307,7 +308,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
                   Pervasives.compare 
                   (List.length goals1) (List.length goals2))
                all_choices in 
-             (match (auto_new dbd width already_seen_goals sorted_choices) 
+             (match (auto_new dbd width already_seen_goals universe sorted_choices) 
               with
                   [] -> 
                     (* no proof has been found; we update the
@@ -347,7 +348,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
                 | _ -> assert false)
     end
       
-and auto_new dbd width already_seen_goals = function
+and auto_new dbd width already_seen_goals universe = function
     [] -> []
   | (subst,(proof, goals, sign))::tl ->
       let _,metasenv,_,_ = proof in
@@ -358,24 +359,24 @@ and auto_new dbd width already_seen_goals = function
            true
        with _ -> false in
       let goals'= List.filter is_in_metasenv goals in
-       auto_new_aux dbd width already_seen_goals 
+       auto_new_aux dbd width already_seen_goals universe
          ((subst,(proof, goals', sign))::tl)
 
-and auto_new_aux dbd width already_seen_goals = function
+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 tl 
+      auto_new dbd width already_seen_goals universe tl
   | (subst,(proof, goals, _))::tl when 
       (List.length goals) > width -> 
-      auto_new dbd width already_seen_goals tl 
+      auto_new dbd width already_seen_goals universe tl 
   | (subst,(proof, (goal,depth)::gtl, sign))::tl -> 
       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) 
+       (width - (List.length gtl)) sign already_seen_goals) universe
       with
-         [] -> auto_new dbd width already_seen_goals tl
+         [] -> auto_new dbd width already_seen_goals universe tl 
        | (local_subst,(proof,[],sign))::tl1 -> 
            let new_subst f t = f (subst t) in
            let is_meta_closed = CicUtil.is_meta_closed ty in
@@ -388,7 +389,7 @@ and auto_new_aux dbd width already_seen_goals = function
                     (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
                in                       
                  (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
-             auto_new dbd width already_seen_goals all_choices 
+             auto_new dbd width already_seen_goals universe all_choices
        | _ -> assert false
  ;; 
 
@@ -399,10 +400,11 @@ let auto_tac_new ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd)
   ()
 =
   let auto_tac dbd (proof,goal) =
+  let universe = MetadataQuery.signature_of_goal ~dbd (proof,goal) in
   Hashtbl.clear inspected_goals;
   debug_print "Entro in Auto";
   let id t = t in
-  match (auto_new dbd width [] [id,(proof, [(goal,depth)],None)]) with
+  match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with
       [] ->  debug_print("Auto failed");
        raise (ProofEngineTypes.Fail "No Applicable theorem")
     | (_,(proof,[],_))::_ ->