From a93a94942ad58d8645af1fd94bef8fa31d9541a4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 21 Sep 2005 09:03:52 +0000 Subject: [PATCH] More debug_print made lazy. --- helm/ocaml/cic_proof_checking/cicElim.ml | 10 +++---- .../cic_proof_checking/cicEnvironment.ml | 24 ++++++++-------- helm/ocaml/cic_proof_checking/cicReduction.ml | 28 +++++++++---------- .../cic_proof_checking/cicSubstitution.ml | 22 +++++++-------- .../cic_proof_checking/cicTypeChecker.ml | 28 +++++++++---------- .../cic_proof_checking/freshNamesGenerator.ml | 2 +- helm/ocaml/cic_unification/cicMetaSubst.ml | 22 +++++++-------- helm/ocaml/cic_unification/cicRefine.ml | 16 +++++------ helm/ocaml/cic_unification/cicUnification.ml | 4 +-- helm/ocaml/cic_unification/coercGraph.ml | 14 +++++----- 10 files changed, 85 insertions(+), 85 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index e3fca907d..fb568613c 100644 --- 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 c111acd6c..4a62aaa24 100644 --- 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 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 diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index 2abce6a0e..a9fa1d9b1 100644 --- 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 f2c0ebbcc..c16385e5d 100644 --- 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 58ff7f96e..113edd1ff 100755 --- 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 aea2a2625..614faf6df 100644 --- 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 a5221c229..b0bc8c623 100644 --- 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 fe5ae7650..27150461f 100644 --- 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 57274e616..c6a929619 100644 --- 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 = -- 2.39.2