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
| 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))
)
with
Invalid_argument s ->
- (*debug_print s;*)
+ (*debug_print (lazy s);*)
uobj,ugraph1_dust
in
match cobj with
raise CicEnvironmentError)
with
Invalid_argument s ->
- (*debug_print s;*)
+ (*debug_print (lazy s);*)
uobj,ugraph1_dust
in
match cobj with
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")
~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)
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? *)
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
*)
;;
(* ??? 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;
object.
*)
Invalid_argument s ->
- (*debug_print s;*)
+ (*debug_print (lazy s);*)
uobj,ugraph
;;