All the debug_print are now lazy.

[helm.git] / helm / ocaml / paramodulation / inference.ml

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index e92117334acb7cf22964be509ca75d7887ea671b..a0cf2bb2180674e1ce5c03856189c88ce643567c 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -480,7 +480,7 @@ let unification_simple metasenv context t1 t2 ugraph =
     | C.Meta (i, _), C.Meta (j, _) when i > j ->
         unif subst menv t s
     | C.Meta _, t when occurs_check subst s t ->
-        raise (U.UnificationFailure "Inference.unification.unif")
+        raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
     | C.Meta (i, l), t -> (
         try
           let _, _, ty = CicUtil.lookup_meta i menv in
@@ -492,24 +492,24 @@ let unification_simple metasenv context t1 t2 ugraph =
           subst, menv
         with CicUtil.Meta_not_found m ->
           let names = names_of_context context in
-          debug_print (
+          debug_print (lazy (
             Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
               (CicPp.pp t1 names) (CicPp.pp t2 names)
-              (print_metasenv menv) (print_metasenv metasenv));
+              (print_metasenv menv) (print_metasenv metasenv)));
           assert false
       )
     | _, C.Meta _ -> unif subst menv t s
     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
-        raise (U.UnificationFailure "Inference.unification.unif")
+        raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
         try
           List.fold_left2
             (fun (subst', menv) s t -> unif subst' menv s t)
             (subst, menv) tls tlt
         with Invalid_argument _ ->
-          raise (U.UnificationFailure "Inference.unification.unif")
+          raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
       )
-    | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
+    | _, _ -> raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
   in
   let subst, menv = unif [] metasenv t1 t2 in
   let menv =
@@ -527,9 +527,9 @@ let unification metasenv context t1 t2 ugraph =
 (*   Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
   let subst, menv, ug =
     if not (is_simple_term t1) || not (is_simple_term t2) then (
-      debug_print (
+      debug_print (lazy (
         Printf.sprintf "NOT SIMPLE TERMS: %s %s"
-          (CicPp.ppterm t1) (CicPp.ppterm t2));
+          (CicPp.ppterm t1) (CicPp.ppterm t2)));
       CicUnification.fo_unif metasenv context t1 t2 ugraph
     ) else
       unification_simple metasenv context t1 t2 ugraph
@@ -1055,7 +1055,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 (*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
               let (head, newmetas, args, newmeta) =
                 ProofEngineHelpers.saturate_term newmeta []
-                  context (S.lift index term)
+                  context (S.lift index term) 0
               in
               let p =
                 if List.length args = 0 then
@@ -1066,14 +1066,14 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
                 match head with
                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
                     when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
-                    debug_print (
-                      Printf.sprintf "OK: %s" (CicPp.ppterm term));
-(*                     debug_print ( *)
+                    debug_print (lazy (
+                      Printf.sprintf "OK: %s" (CicPp.ppterm term)));
+(*                     debug_print (lazy ( *)
 (*                       Printf.sprintf "args: %s\n" *)
-(*                         (String.concat ", " (List.map CicPp.ppterm args))); *)
-(*                     debug_print ( *)
+(*                         (String.concat ", " (List.map CicPp.ppterm args)))); *)
+(*                     debug_print (lazy ( *)
 (*                       Printf.sprintf "newmetas:\n%s\n" *)
-(*                         (print_metasenv newmetas)); *)
+(*                         (print_metasenv newmetas))); *)
                     let o = !Utils.compare_terms t1 t2 in
                     let w = compute_equality_weight ty t1 t2 in
                     let proof = BasicProof p in
@@ -1154,14 +1154,14 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
   let rec aux newmeta = function
     | [] -> [], newmeta
     | (term, termty)::tl ->
-        debug_print (
+        debug_print (lazy (
           Printf.sprintf "Examining: %s (%s)"
-            (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty));
+            (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty)));
         let res, newmeta = 
           match termty with
           | C.Prod (name, s, t) ->
               let head, newmetas, args, newmeta =
-                ProofEngineHelpers.saturate_term newmeta [] context termty
+                ProofEngineHelpers.saturate_term newmeta [] context termty 0
               in
               let p =
                 if List.length args = 0 then
@@ -1172,8 +1172,8 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
                 match head with
                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
                     when (iseq uri) && (ok_types ty newmetas) ->
-                    debug_print (
-                      Printf.sprintf "OK: %s" (CicPp.ppterm term));
+                    debug_print (lazy (
+                      Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
                     let w = compute_equality_weight ty t1 t2 in
                     let proof = BasicProof p in
@@ -1199,8 +1199,8 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
   (List.fold_left
      (fun l e ->
         if List.exists (meta_convertibility_eq e) l then (
-          debug_print (
-            Printf.sprintf "NO!! %s already there!" (string_of_equality e));
+          debug_print (lazy (
+            Printf.sprintf "NO!! %s already there!" (string_of_equality e)));
           l
         )
         else e::l)