More debug_print made lazy.

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

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
 ;;