More debug_print made lazy.

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index e3fca907dd562f494a479333400c33ef069f08b8..fb568613c943c8b3b7389d9d09d039d8e88b8046 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicElim.ml
+++ b/helm/ocaml/cic_proof_checking/cicElim.ml
@@ -29,7 +29,7 @@ exception Elim_failure of string
 exception Can_t_eliminate
 
 let debug_print = fun _ -> ()
-(*let debug_print = prerr_endline *)
+(*let debug_print s = prerr_endline (Lazy.force s) *)
 
 let counter = ref ~-1 ;;
 
@@ -367,16 +367,16 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
         add_params (fun b s t -> Cic.Lambda (b, s, t)) leftno ty cic
       in
 (*
-debug_print (CicPp.ppterm eliminator_type);
-debug_print (CicPp.ppterm eliminator_body);
+debug_print (lazy (CicPp.ppterm eliminator_type));
+debug_print (lazy (CicPp.ppterm eliminator_body));
 *)
       let eliminator_type = 
        FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_type in
       let eliminator_body = 
        FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_body in
 (*
-debug_print (CicPp.ppterm eliminator_type);
-debug_print (CicPp.ppterm eliminator_body);
+debug_print (lazy (CicPp.ppterm eliminator_type));
+debug_print (lazy (CicPp.ppterm eliminator_body));
 *)
       let (computed_type, ugraph) =
         try

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index c111acd6cf3b75d37c7301a0a90919b02051a2c9..4a62aaa24741d672e46695cb237ec718557424a3 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -430,18 +430,18 @@ module Cache :
               frozen_list := List.remove_assoc uri !frozen_list;
               frozen_list := (uri,(o,Some real_ugraph))::!frozen_list;
           | Some g -> 
-              debug_print (
+              debug_print (lazy (
                 "You are probably hacking an object already hacked or an"^
                 " object that has the universe file but is not"^
-                " yet committed.");
+                " yet committed."));
               assert false
      with
         Not_found -> 
-          debug_print (
+          debug_print (lazy (
             "You are hacking an object that is not in the"^
             " frozen_list, this means you are probably generating an"^
             " universe file for an object that already"^
-             " as an universe file");
+             " as an universe file"));
           assert false
    ;;
 
@@ -523,8 +523,8 @@ let get_object_to_add uri =
         (Some (CicUniv.ugraph_of_xml filename_univ),Some filename_univ)
     with Failure s ->
       
-      debug_print (
-        "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri));
+      debug_print (lazy (
+        "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)));
         Inix.unlink
       None,None
       *)
@@ -552,21 +552,21 @@ let find_or_add_to_unchecked uri =
 let set_type_checking_info ?(replace_ugraph=None) uri =
 (*
   if not (Cache.can_be_cooked uri) && replace_ugraph <> None then begin
-    debug_print (
+    debug_print (lazy (
       "?replace_ugraph must be None if you are not committing an "^
       "object that has a universe graph associated "^
-      "(can happen only in the fase of universes graphs generation).");
+      "(can happen only in the fase of universes graphs generation)."));
     assert false
   else
 *)
   match Cache.can_be_cooked uri, replace_ugraph with
   | true, Some _
   | false, None ->
-      debug_print (
+      debug_print (lazy (
         "?replace_ugraph must be (Some ugraph) when committing an object that "^
         "has no associated universe graph. If this is in make_univ phase you "^
         "should drop this exception and let univ_make commit thi object with "^
-        "proper arguments");
+        "proper arguments"));
       assert false
   | _ ->
       (match replace_ugraph with 
@@ -602,7 +602,7 @@ let get_cooked_obj ?(trust=true) base_univ uri =
     else
       (* we don't trust the uri, so we fail *)
       begin
-        debug_print ("CACHE MISS: " ^ (UriManager.string_of_uri uri));
+        debug_print (lazy ("CACHE MISS: " ^ (UriManager.string_of_uri uri)));
         raise Not_found
       end
       
@@ -672,6 +672,6 @@ let list_obj () =
     (list_uri ())
   with
     Not_found -> 
-      debug_print "Who has removed the uri in the meanwhile?";
+      debug_print (lazy "Who has removed the uri in the meanwhile?");
       raise Not_found
 ;;

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index aaca61942aa323467bfb0d29a4914f3405681005..fe0c09aaeff029c860c1d8abb07c4ab9cc0d2a41 100644 (file)
--- 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

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 2abce6a0edc635fbfffc3df5bd40c4bf990fc78d..a9fa1d9b19e8e86ca8c8b89621e6fa4e13c365e1 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -191,7 +191,7 @@ let subst arg =
 (*CSC: per la roba che proviene da Coq questo non serve!                 *)
 let subst_vars exp_named_subst =
 (*
-debug_print ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
+debug_print (lazy ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS")) ;
 *)
  let rec substaux k =
   let module C = Cic in
@@ -216,17 +216,17 @@ debug_print ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
            )
           in
 (*
-debug_print "\n\n---- BEGIN " ;
-debug_print ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-debug_print ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst)) ;
-debug_print ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst')) ;
+debug_print (lazy "\n\n---- BEGIN ") ;
+debug_print (lazy ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
+debug_print (lazy ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst))) ;
+debug_print (lazy ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'))) ;
 *)
            let exp_named_subst'' =
             substaux_in_exp_named_subst uri k exp_named_subst' params
            in
 (*
-debug_print ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'')) ;
-debug_print "---- END\n\n " ;
+debug_print (lazy ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst''))) ;
+debug_print (lazy "---- END\n\n ") ;
 *)
             C.Var (uri,exp_named_subst'')
        )
@@ -331,11 +331,11 @@ debug_print "---- END\n\n " ;
     | _::tl -> filter_and_lift 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

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index f2c0ebbcc5d44555932c0fd715db21ddfe1622be..c16385e5d4597c5785ec2fd298f11f872972345e 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -186,7 +186,7 @@ let rec type_of_constant ~logger uri ugraph =
                CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
         with Invalid_argument s ->
-          (*debug_print s;*)
+          (*debug_print (lazy s);*)
           uobj,ugraph_dust       
   in
    match cobj,ugraph with
@@ -227,7 +227,7 @@ and type_of_variable ~logger uri ugraph =
             | CicEnvironment.CheckedObj _ 
              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
          with Invalid_argument s ->
-           (*debug_print s;*)
+           (*debug_print (lazy s);*)
            ty,ugraph2)
    |  _ ->
        raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
@@ -576,7 +576,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph =
             )
           with
               Invalid_argument s ->
-                (*debug_print s;*)
+                (*debug_print (lazy s);*)
                 uobj,ugraph1_dust
   in
     match cobj with
@@ -611,7 +611,7 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
                       raise CicEnvironmentError)
            with
                Invalid_argument s ->
-                 (*debug_print s;*)
+                 (*debug_print (lazy s);*)
                  uobj,ugraph1_dust
   in
     match cobj with
@@ -1485,7 +1485,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
             Some (_,C.Decl t) -> S.lift n t,ugraph
           | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph
           | Some (_,C.Def (bo,None)) ->
-             debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
+             debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ;
               type_of_aux ~logger context (S.lift n bo) ugraph
           | None -> raise 
              (TypeCheckerFailure "Reference to deleted hypothesis")
@@ -1783,9 +1783,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
                  ~subst ~metasenv context ty_p ty_branch ugraph3 
              in 
              if not b1 then
-               debug_print 
+               debug_print (lazy
                  ("#### " ^ CicPp.ppterm ty_p ^ 
-                 " <==> " ^ CicPp.ppterm ty_branch); 
+                 " <==> " ^ CicPp.ppterm ty_branch));
              (j + 1,b1,ugraph4)
            else
              (j,false,ugraph)
@@ -2021,12 +2021,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 
  in
 (*CSC
-debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
+debug_print (lazy ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t)) ; flush stderr ;
 let res =
 *)
   type_of_aux ~logger context t ugraph
 (*
-in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
+in debug_print (lazy "FINE TYPE_OF_AUX") ; flush stderr ; res
 *)
 
 (* is a small constructor? *)
@@ -2050,12 +2050,12 @@ and is_small ~logger context paramsno c ugraph =
 
 and type_of ~logger t ugraph =
 (*CSC
-debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
+debug_print (lazy ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t)) ; flush stderr ;
 let res =
 *)
  type_of_aux' ~logger [] [] t ugraph 
 (*CSC
-in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
+in debug_print (lazy "FINE TYPE_OF_AUX'") ; flush stderr ; res
 *)
 ;;
 
@@ -2121,12 +2121,12 @@ let typecheck uri =
    (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
    match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
      CicEnvironment.CheckedObj (cobj,ugraph') -> 
-       (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
+       (* debug_print (lazy ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri));*)
        cobj,ugraph'
    | CicEnvironment.UncheckedObj uobj ->
       (* let's typecheck the uncooked object *)
       logger#log (`Start_type_checking uri) ;
-      (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
+      (* debug_print (lazy ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri)); *)
       let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
        try
          CicEnvironment.set_type_checking_info uri;
@@ -2142,7 +2142,7 @@ let typecheck uri =
              object.
            *)
            Invalid_argument s -> 
-             (*debug_print s;*)
+             (*debug_print (lazy s);*)
              uobj,ugraph
 ;;
 

diff --git a/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml b/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml
index 58ff7f96efebf0a0c7de7fcf7d230be6640e9c0d..113edd1ff229ad00aecde38451ecb42339ff89a2 100755 (executable)
--- a/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml
+++ b/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml
@@ -256,7 +256,7 @@ let clean_dummy_dependent_types t =
             C.Anonymous ->
              if List.mem k rels2 then
 (
-              debug_print "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name" ;
+              debug_print (lazy "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name") ;
               C.Anonymous
 )
              else

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index aea2a262526a20aaeea0caa6f4b2cdcb41d8c1f0..614faf6df15f50d6af219ac90ccacf502afd04fb 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -47,7 +47,7 @@ let reset_counters () =
  metasenv_length := 0;
  context_length := 0
 let print_counters () =
-  debug_print (Printf.sprintf
+  debug_print (lazy (Printf.sprintf
 "apply_subst: %d
 apply_subst_context: %d
 apply_subst_metasenv: %d
@@ -64,7 +64,7 @@ context length: %d (avg = %.2f)
   ((float !metasenv_length) /. (float !apply_subst_metasenv_counter))
   !context_length
   ((float !context_length) /. (float !apply_subst_context_counter))
-  )*)
+  ))*)
 
 
 
@@ -573,10 +573,10 @@ let rec restrict subst to_be_restricted metasenv =
             (ppterm subst term)
          in 
           (* DEBUG
-          debug_print error_msg;
-          debug_print ("metasenv = \n" ^ (ppmetasenv metasenv subst));
-          debug_print ("subst = \n" ^ (ppsubst subst)); 
-          debug_print ("context = \n" ^ (ppcontext subst context)); *)
+          debug_print (lazy error_msg);
+          debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst)));
+          debug_print (lazy ("subst = \n" ^ (ppsubst subst)));
+          debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *)
           raise (MetaSubstFailure error_msg))) 
       subst ([], []) 
   in
@@ -592,8 +592,8 @@ let delift n subst context metasenv l t =
    otherwise the occur check does not make sense *)
 
 (*
- debug_print ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
- al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))); 
+ debug_print (lazy ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
+ al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))));
 *)
 
  let module S = CicSubstitution in
@@ -716,14 +716,14 @@ let delift n subst context metasenv l t =
       (* The reason is that our delift function is weaker than first  *)
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
-(* debug_print "First Order UnificationFailure during delift" ;
-debug_print(sprintf
+(* debug_print (lazy "First Order UnificationFailure during delift") ;
+debug_print(lazy (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)
         (String.concat "; "
           (List.map
             (function Some t -> ppterm subst t | None -> "_") l
-          ))); *)
+          )))); *)
       raise (Uncertain (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index a5221c22976f3d3c337121cbb116e82b7a0bb88c..b0bc8c623aaf5d1bdbc739b2f2090b9ca46af179 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -873,11 +873,11 @@ and type_of_aux' metasenv context t ugraph =
       try
        fo_unif_subst subst context metasenv hetype hetype' ugraph
       with exn ->
-       debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
+       debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
                         (CicPp.ppterm hetype)
                         (CicPp.ppterm hetype')
                          (CicMetaSubst.ppmetasenv [] metasenv)
-                        (CicMetaSubst.ppsubst subst));
+                        (CicMetaSubst.ppsubst subst)));
        raise exn
 
     in
@@ -1070,16 +1070,16 @@ let type_of_aux' metasenv context term =
  try
   let (t,ty,m) = 
       type_of_aux' metasenv context term in
-    debug_print
-     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
-   debug_print
-    ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
+    debug_print (lazy
+     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
+   debug_print (lazy
+    ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
    (t,ty,m)
  with
  | RefineFailure msg as e ->
-     debug_print ("@@@ REFINE FAILED: " ^ msg);
+     debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
      raise e
  | Uncertain msg as e ->
-     debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
+     debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
      raise e
 ;; *)

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index fe5ae76502ba2703cbb70519186eb1d29872abfb..27150461fb0038ba4c5e7d81f8ff0562d0dc2de3 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -291,7 +291,7 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
                             with
                                 Uncertain _
                               | UnificationFailure _ ->
-debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)); 
+debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j))); 
                                   let metasenv, subst = 
                                     CicMetaSubst.restrict 
                                       subst [(n,j)] metasenv in
@@ -346,7 +346,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
                 UnificationFailure msg ->raise (UnificationFailure msg)  
               | Uncertain msg -> raise (UnificationFailure (Reason msg))
               | AssertFailure _ ->
-                  debug_print "siamo allo huge hack";
+                  debug_print (lazy "siamo allo huge hack");
                   (* TODO huge hack!!!!
                    * we keep on unifying/refining in the hope that 
                    * the problem will be eventually solved. 

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index 57274e616446b3dab7b416c8db8f71f3aace8441..c6a929619f508d65bbeb6c307093322422683b54 100644 (file)
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -26,7 +26,7 @@
 open Printf;;
 
 let debug = false
-let debug_print = if debug then prerr_endline else ignore
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (* searches a coercion fron src to tgt in the !coercions list *)
 let look_for_coercion src tgt =
@@ -38,17 +38,17 @@ let look_for_coercion src tgt =
           (fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt) 
       in
       match l with
-      | [] -> debug_print ":( coercion non trovata"; None
+      | [] -> debug_print (lazy ":( coercion non trovata"); None
       | u::_ -> 
-          debug_print (
+          debug_print (lazy (
             sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" 
               (List.length l)
               (UriManager.name_of_uri src) 
               (UriManager.name_of_uri tgt)
-              (UriManager.name_of_uri u));
+              (UriManager.name_of_uri u)));
               Some (CicUtil.term_of_uri u)
     with Invalid_argument s -> 
-      debug_print (":( coercion non trovata (fallita la uri_of_term): " ^ s);
+      debug_print (lazy (":( coercion non trovata (fallita la uri_of_term): " ^ s));
       None
 ;;
 
@@ -97,8 +97,8 @@ let generate_composite_closure c1 c2 univ =
     try 
       CicTypeChecker.type_of_aux' [] [] c univ
     with CicTypeChecker.TypeCheckerFailure s as exn ->
-      debug_print (sprintf "Generated composite coercion:\n%s\n%s" 
-        (CicPp.ppterm c) s);
+      debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s" 
+        (CicPp.ppterm c) s));
       raise exn
   in
   let cleaned_ty =