first snapshot of the night-profiling

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

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 3d4fc7126bcc781d041c0f6acf194696cf266b4a..13dac415f8298af2bc7b4f4ba486008eb72f68fb 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -27,29 +27,10 @@
 
 (* let debug_print = fun _ -> () *)
 
-(* Da rimuovere, solo per debug*)
-let print_context ctx =
-    let print_name =
-     function
-        Cic.Name n -> n
-      | Cic.Anonymous -> "_"
-    in
-     List.fold_right
-      (fun i (output,context) ->
-        let (newoutput,context') =
-         match i with
-            Some (n,Cic.Decl t) ->
-              print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context
-          | Some (n,Cic.Def (t,None)) ->
-              print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context
-          | None ->
-              "_ ?= _\n", None::context
-          | Some (_,Cic.Def (_,Some _)) -> assert false
-        in
-         output^newoutput,context'
-      ) ctx ("",[])
-  ;;
-
+let experimental_hint =
+ let profile = CicUtil.profile "experimental_hint" in
+ fun ~dbd ~facts ?signature status ->
+  profile (MetadataQuery.experimental_hint ~dbd ~facts ?signature) status
 
 let search_theorems_in_context status =
   let (proof, goal) = status in
@@ -110,9 +91,9 @@ let rec auto dbd = function
          Some (ey, ty) ->
             (* the goal is still there *)
             (*
-           debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
-           debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p));
-           debug_print ("CURRENT HYP = " ^ (fst (print_context ey)));
+           debug_print ("CURRENT GOAL = " ^ CicPp.ppterm ty);
+           debug_print ("CURRENT PROOF = " ^ CicPp.ppterm p);
+           debug_print ("CURRENT HYP = " ^ CicPp.ppcontext ey);
             *)
             (* if the goal contains metavariables we use the input
                signature for at_most constraints *)
@@ -300,9 +281,9 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
            [] (* the empty list means no choices, i.e. failure *)
        | No _ 
        | NotYetInspected ->
-             debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
-             debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p));
-             debug_print ("CURRENT HYP = " ^ (fst (print_context ey)));
+             debug_print ("CURRENT GOAL = " ^ CicPp.ppterm ty);
+             debug_print ("CURRENT PROOF = " ^ CicPp.ppterm p);
+             debug_print ("CURRENT HYP = " ^ CicPp.ppcontext ey);
            let sign, new_sign =
              if is_meta_closed then
                None, Some (MetadataConstraints.signature_of ty)
@@ -315,7 +296,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
              new_search_theorems 
                (fun status -> 
                   List.map snd
-                  (MetadataQuery.experimental_hint 
+                  (experimental_hint 
                      ~dbd ~facts:facts ?signature:sign status))
                dbd proof goal (depth-1) new_sign in 
            let all_choices =