X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReduction.ml;h=fe0c09aaeff029c860c1d8abb07c4ab9cc0d2a41;hb=8b55faddb06e3c4b0a13839210bb49170939b33e;hp=aaca61942aa323467bfb0d29a4914f3405681005;hpb=e1518f70bdddd0bc19cdf34e6fc9564e158ae35e;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index aaca61942..fe0c09aae 100644
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -43,7 +43,7 @@ let debug t env s =
    CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  in
   if !fdebug = 0 then
-   debug_print (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
+   debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) ""))
 ;;
 
 module type Strategy =
@@ -349,7 +349,7 @@ module Reduction(RS : Strategy) =
             )
        | C.Var (uri,exp_named_subst) ->
 (*
-debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
+debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens))) ;
 *)
          if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
           CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
@@ -495,11 +495,11 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) ->
         | _::tl -> filter_and_lift already_instantiated tl
 (*
         | (uri,_)::tl ->
-debug_print ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
+debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ;
 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
-exp_named_subst' then debug_print "---- OK1" ;
-debug_print ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-if List.mem uri params then debug_print "---- OK2" ;
+exp_named_subst' then debug_print (lazy "---- OK1") ;
+debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
+if List.mem uri params then debug_print (lazy "---- OK2") ;
         filter_and_lift tl
 *)
       in
@@ -760,7 +760,7 @@ if List.mem uri params then debug_print "---- OK2" ;
     try 
       reduce context (0, [], [], t, [])
     with Not_found -> 
-      debug_print (CicPp.ppterm t) ; 
+      debug_print (lazy (CicPp.ppterm t)) ; 
       raise Not_found
   ;;
   *)
@@ -776,11 +776,11 @@ let whd context t =
  let rescsc = CicReductionNaif.whd context t in
   if not (CicReductionNaif.are_convertible context res rescsc) then
    begin
-    debug_print ("PRIMA: " ^ CicPp.ppterm t) ;
+    debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
     flush stderr ;
-    debug_print ("DOPO: " ^ CicPp.ppterm res) ;
+    debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
     flush stderr ;
-    debug_print ("CSC: " ^ CicPp.ppterm rescsc) ;
+    debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
     flush stderr ;
 CicReductionNaif.fdebug := 0 ;
 let _ =  CicReductionNaif.are_convertible context res rescsc in
@@ -1026,10 +1026,10 @@ let are_convertible ?(subst=[]) ?(metasenv=[])  =
      (* 
      (match t1 with 
          Cic.Meta _ -> 
-           debug_print (CicPp.ppterm t1);
-           debug_print (CicPp.ppterm (whd ~subst context t1));
-           debug_print (CicPp.ppterm t2);
-           debug_print (CicPp.ppterm (whd ~subst context t2))
+           debug_print (lazy (CicPp.ppterm t1));
+           debug_print (lazy (CicPp.ppterm (whd ~subst context t1)));
+           debug_print (lazy (CicPp.ppterm t2));
+           debug_print (lazy (CicPp.ppterm (whd ~subst context t2)))
        | _ -> ()); *)
      let t1' = whd ~subst context t1 in
      let t2' = whd ~subst context t2 in