All the debug_print are now lazy.

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index e86f79af5f38d4dccedad03d601a9ac253a46534..ddeab3e6e685892cda6ada1eab64db1cfdc0473a 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -30,7 +30,8 @@ module PET = ProofEngineTypes
 
 exception Goal_is_not_an_equation
 
-let debug_print = fun _ -> ()
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s)
 
   (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for
   * the "like" operator (which uses '%' and '_'). Does not support escaping. *)
@@ -61,7 +62,7 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
       (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false))
 
 let match_term ~(dbd:Mysql.dbd) ty =
-(*   debug_print (CicPp.ppterm ty); *)
+(*   debug_print (lazy (CicPp.ppterm ty)); *)
   let metadata = MetadataExtractor.compute ~body:None ~ty in
   let constants_no =
     MetadataConstraints.UriManagerSet.cardinal (MetadataConstraints.constants_of ty)
@@ -316,15 +317,15 @@ let experimental_hint
   let other_constants = 
     Constr.UriManagerSet.diff all_constants_closed types_constants
   in
-  debug_print "all_constants_closed";
-  Constr.UriManagerSet.iter debug_print all_constants_closed;
-  debug_print "other_constants";
-  Constr.UriManagerSet.iter debug_print other_constants;
+  debug_print (lazy "all_constants_closed");
+  if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) all_constants_closed;
+  debug_print (lazy "other_constants");
+  if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) other_constants;
   let uris = 
     let pow = 2 ** (Constr.UriManagerSet.cardinal other_constants) in
     if ((List.length uris < pow) or (pow <= 0))
     then begin
-      debug_print "MetadataQuery: large sig, falling back to old method";
+      debug_print (lazy "MetadataQuery: large sig, falling back to old method");
       filter_uris_forward ~dbd (main, other_constants) uris
     end else
       filter_uris_backward ~dbd ~facts (main, other_constants) uris
@@ -335,7 +336,7 @@ let experimental_hint
         (let status' =
             try
               let (subst,(proof, goal_list)) =
-                  (* debug_print ("STO APPLICANDO" ^ uri); *)
+                  (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
                   apply_tac_verbose 
                    ~term:(CicUtil.term_of_uri uri)
                   status
@@ -383,7 +384,7 @@ let new_experimental_hint
         (let status' =
             try
               let (subst,(proof, goal_list)) =
-                  (* debug_print ("STO APPLICANDO" ^ uri); *)
+                  (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
                   apply_tac_verbose 
                    ~term:(CicUtil.term_of_uri uri)
                   status
@@ -433,7 +434,7 @@ let instance ~dbd t =
 (*   List.iter 
     (fun x -> 
        debug_print 
-         (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))) 
+         (lazy (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x)))) 
     metadata; *)
   let no_concl = MetadataDb.count_distinct `Conclusion metadata in
   let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in
@@ -455,7 +456,7 @@ let instance ~dbd t =
   in
   match (look_for_dummy_main metadata) with
     | None->
-(*         debug_print "Caso None"; *)
+(*         debug_print (lazy "Caso None"); *)
         (* no dummy in main position *)
         let metadata = List.filter is_dummy metadata in
         let constraints = List.map MetadataTypes.constr_of_metadata metadata in
@@ -465,7 +466,7 @@ let instance ~dbd t =
           Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints
     | Some (depth, dummy_type) ->
 (*         debug_print 
-          (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type)); *)
+          (lazy (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type))); *)
         (* a dummy in main position *)
         let metadata_for_dummy_type = 
           MetadataExtractor.compute ~body:None ~ty:dummy_type in