From cfda0acfce3f5e0b843bfe2b7ba7c371e5690db0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 21 Sep 2005 09:59:58 +0000 Subject: [PATCH] All the debug_print are now lazy. --- helm/ocaml/cic/cicParser.ml | 17 ++-- helm/ocaml/cic_notation/cicNotationRew.ml | 12 +-- helm/ocaml/hbugs/broker.ml | 20 ++--- helm/ocaml/paramodulation/indexing.ml | 8 +- helm/ocaml/paramodulation/inference.ml | 32 ++++---- helm/ocaml/paramodulation/saturation.ml | 88 ++++++++++----------- helm/ocaml/paramodulation/utils.ml | 20 ++--- helm/ocaml/paramodulation/utils.mli | 2 +- helm/ocaml/registry/helm_registry.ml | 6 +- helm/ocaml/tactics/autoTactic.ml | 41 +++++----- helm/ocaml/tactics/discriminationTactics.ml | 34 ++++---- helm/ocaml/tactics/eliminationTactics.ml | 18 ++--- helm/ocaml/tactics/metadataQuery.ml | 25 +++--- helm/ocaml/tactics/ring.ml | 35 ++++---- helm/ocaml/tactics/tacticals.ml | 38 +++++---- helm/ocaml/thread/extThread.ml | 4 +- helm/ocaml/thread/threadSafe.ml | 14 ++-- helm/ocaml/utf8_macros/make_table.ml | 4 +- helm/ocaml/utf8_macros/pa_unicode_macro.ml | 6 +- 19 files changed, 211 insertions(+), 213 deletions(-) diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index a28968377..4b7c940e9 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -23,7 +23,8 @@ * http://helm.cs.unibo.it/ *) -let debug_print = prerr_endline +let debug = false +let debug_print s = if debug then prerr_endline (Lazy.force s) open Printf @@ -134,17 +135,17 @@ let attribute_error ctxt tag = (** {2 Parsing context management} *) let pop ctxt = -(* debug_print "pop";*) +(* debug_print (lazy "pop");*) match ctxt.stack with | hd :: tl -> (ctxt.stack <- tl) | _ -> assert false let push ctxt v = -(* debug_print "push";*) +(* debug_print (lazy "push");*) ctxt.stack <- v :: ctxt.stack let set_top ctxt v = -(* debug_print "set_top";*) +(* debug_print (lazy "set_top");*) match ctxt.stack with | _ :: tl -> (ctxt.stack <- v :: tl) | _ -> assert false @@ -335,12 +336,12 @@ let find_helm_exception ctxt = * each callback needs to be instantiated to a parsing context *) let start_element ctxt tag attrs = -(* debug_print (sprintf "<%s%s>" tag (match attrs with | [] -> "" | _ -> " " ^ String.concat " " (List.map (fun (a,v) -> sprintf "%s=\"%s\"" a v) attrs)));*) +(* debug_print (lazy (sprintf "<%s%s>" tag (match attrs with | [] -> "" | _ -> " " ^ String.concat " " (List.map (fun (a,v) -> sprintf "%s=\"%s\"" a v) attrs))));*) push ctxt (Tag (tag, attrs)) let end_element ctxt tag = -(* debug_print (sprintf "" tag);*) -(* debug_print (string_of_stack ctxt);*) +(* debug_print (lazy (sprintf "" tag));*) +(* debug_print (lazy (string_of_stack ctxt));*) let attribute_error () = attribute_error ctxt tag in let parse_error = parse_error ctxt in let sort_of_string = sort_of_string ctxt in @@ -705,7 +706,7 @@ let parse uri filename = * leak when used in conjunction with such structures *) raise exn); ctxt.xml_parser <- None; (* ZACK: same comment as above *) -(* debug_print (string_of_stack stack);*) +(* debug_print (lazy (string_of_stack stack));*) (* assert (List.length ctxt.stack = 1) *) List.hd ctxt.stack with diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index d65eb0a50..3d684fe39 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -28,7 +28,7 @@ open Printf module Ast = CicNotationPt 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 () type pattern_id = int type interpretation_id = pattern_id @@ -567,17 +567,17 @@ let load_patterns21 t = set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t)) let ast_of_acic id_to_sort annterm = - debug_print ("ast_of_acic <- " - ^ CicPp.ppterm (Deannotate.deannotate_term annterm)); + debug_print (lazy ("ast_of_acic <- " + ^ CicPp.ppterm (Deannotate.deannotate_term annterm))); let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in let ast = ast_of_acic1 term_info annterm in - debug_print ("ast_of_acic -> " ^ CicNotationPp.pp_term ast); + debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast)); ast, term_info.uri let pp_ast ast = - debug_print "pp_ast <-"; + debug_print (lazy "pp_ast <-"); let ast' = pp_ast1 ast in - debug_print ("pp_ast -> " ^ CicNotationPp.pp_term ast'); + debug_print (lazy ("pp_ast -> " ^ CicNotationPp.pp_term ast')); ast' let fresh_id = diff --git a/helm/ocaml/hbugs/broker.ml b/helm/ocaml/hbugs/broker.ml index b86c08b9b..6b62af946 100644 --- a/helm/ocaml/hbugs/broker.ml +++ b/helm/ocaml/hbugs/broker.ml @@ -30,7 +30,7 @@ open Hbugs_types;; open Printf;; let debug = true ;; -let debug_print s = if debug then prerr_endline s ;; +let debug_print s = if debug then prerr_endline (Lazy.force s) ;; let daemon_name = "H-Bugs Broker" ;; let default_port = 49081 ;; @@ -66,13 +66,13 @@ let do_critical = let mutex = Mutex.create () in fun action -> try -(* debug_print "Acquiring lock ..."; *) +(* debug_print (lazy "Acquiring lock ..."); *) Mutex.lock mutex; -(* debug_print "Lock Acquired!"; *) +(* debug_print (lazy "Lock Acquired!"); *) let res = Lazy.force action in -(* debug_print "Releaseing lock ..."; *) +(* debug_print (lazy "Releaseing lock ..."); *) Mutex.unlock mutex; -(* debug_print "Lock released!"; *) +(* debug_print (lazy "Lock released!"); *) res with e -> Mutex.unlock mutex; raise e ;; @@ -232,7 +232,7 @@ let handle_msg outchan msg = )) | msg -> (* unexpected message *) - debug_print "Unknown message!"; + debug_print (lazy "Unknown message!"); Hbugs_messages.respond_exc "unexpected_msg" (Hbugs_messages.string_of_msg msg) outchan) in @@ -241,7 +241,7 @@ let handle_msg outchan = if debug then (fun msg -> (* filter handle_msg through a function which dumps input messages *) - debug_print (Hbugs_messages.string_of_msg msg); + debug_print (lazy (Hbugs_messages.string_of_msg msg)); handle_msg outchan msg) else handle_msg outchan @@ -251,8 +251,8 @@ in (* thread action *) let callback (req: Http_types.request) outchan = try - debug_print ("Connection from " ^ req#clientAddr); - debug_print ("Received request: " ^ req#path); + debug_print (lazy ("Connection from " ^ req#clientAddr)); + debug_print (lazy ("Received request: " ^ req#path)); (match req#path with (* TODO write help message *) | "/help" -> return_xml_msg " not yet written " outchan @@ -265,7 +265,7 @@ let callback (req: Http_types.request) outchan = else Http_daemon.respond_error ~code:400 outchan | _ -> Http_daemon.respond_error ~code:400 outchan); - debug_print "Done!\n" + debug_print (lazy "Done!\n") with | Http_types.Param_not_found attr_name -> Hbugs_messages.respond_exc "missing_parameter" attr_name outchan diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 698175d1b..5b84bb72a 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -182,9 +182,9 @@ let rec find_matches metasenv context ugraph lift_amount term termty = let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in (* if not (fst (CicReduction.are_convertible *) (* ~metasenv context termty ty ugraph)) then ( *) -(* (\* debug_print ( *\) *) +(* (\* debug_print (lazy ( *\) *) (* (\* Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *) -(* (\* (CicPp.pp termty names) (CicPp.pp ty names)); *\) *) +(* (\* (CicPp.pp termty names) (CicPp.pp ty names))); *\) *) (* find_matches metasenv context ugraph lift_amount term termty tl *) (* ) else *) let do_match c other eq_URI = @@ -253,9 +253,9 @@ let rec find_all_matches ?(unif_fun=Inference.unification) let pos, (_, _, (ty, left, right, o), metas, args) = candidate in (* if not (fst (CicReduction.are_convertible *) (* ~metasenv context termty ty ugraph)) then ( *) -(* (\* debug_print ( *\) *) +(* (\* debug_print (lazy ( *\) *) (* (\* Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *) -(* (\* (CicPp.pp termty names) (CicPp.pp ty names)); *\) *) +(* (\* (CicPp.pp termty names) (CicPp.pp ty names))); *\) *) (* find_all_matches ~unif_fun metasenv context ugraph *) (* lift_amount term termty tl *) (* ) else *) diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 5ccd87412..a0cf2bb21 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -492,10 +492,10 @@ let unification_simple metasenv context t1 t2 ugraph = subst, menv with CicUtil.Meta_not_found m -> let names = names_of_context context in - debug_print ( + debug_print (lazy ( Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m (CicPp.pp t1 names) (CicPp.pp t2 names) - (print_metasenv menv) (print_metasenv metasenv)); + (print_metasenv menv) (print_metasenv metasenv))); assert false ) | _, C.Meta _ -> unif subst menv t s @@ -527,9 +527,9 @@ let unification metasenv context t1 t2 ugraph = (* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *) let subst, menv, ug = if not (is_simple_term t1) || not (is_simple_term t2) then ( - debug_print ( + debug_print (lazy ( Printf.sprintf "NOT SIMPLE TERMS: %s %s" - (CicPp.ppterm t1) (CicPp.ppterm t2)); + (CicPp.ppterm t1) (CicPp.ppterm t2))); CicUnification.fo_unif metasenv context t1 t2 ugraph ) else unification_simple metasenv context t1 t2 ugraph @@ -1066,14 +1066,14 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = match head with | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) -> - debug_print ( - Printf.sprintf "OK: %s" (CicPp.ppterm term)); -(* debug_print ( *) + debug_print (lazy ( + Printf.sprintf "OK: %s" (CicPp.ppterm term))); +(* debug_print (lazy ( *) (* Printf.sprintf "args: %s\n" *) -(* (String.concat ", " (List.map CicPp.ppterm args))); *) -(* debug_print ( *) +(* (String.concat ", " (List.map CicPp.ppterm args)))); *) +(* debug_print (lazy ( *) (* Printf.sprintf "newmetas:\n%s\n" *) -(* (print_metasenv newmetas)); *) +(* (print_metasenv newmetas))); *) let o = !Utils.compare_terms t1 t2 in let w = compute_equality_weight ty t1 t2 in let proof = BasicProof p in @@ -1154,9 +1154,9 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = let rec aux newmeta = function | [] -> [], newmeta | (term, termty)::tl -> - debug_print ( + debug_print (lazy ( Printf.sprintf "Examining: %s (%s)" - (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty)); + (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty))); let res, newmeta = match termty with | C.Prod (name, s, t) -> @@ -1172,8 +1172,8 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = match head with | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when (iseq uri) && (ok_types ty newmetas) -> - debug_print ( - Printf.sprintf "OK: %s" (CicPp.ppterm term)); + debug_print (lazy ( + Printf.sprintf "OK: %s" (CicPp.ppterm term))); let o = !Utils.compare_terms t1 t2 in let w = compute_equality_weight ty t1 t2 in let proof = BasicProof p in @@ -1199,8 +1199,8 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = (List.fold_left (fun l e -> if List.exists (meta_convertibility_eq e) l then ( - debug_print ( - Printf.sprintf "NO!! %s already there!" (string_of_equality e)); + debug_print (lazy ( + Printf.sprintf "NO!! %s already there!" (string_of_equality e))); l ) else e::l) diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 6d5ecee15..a3dff3eb3 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -288,7 +288,7 @@ let prune_passive howmany (active, _) passive = in let in_weight = round (howmany *. ratio /. (ratio +. 1.)) and in_age = round (howmany /. (ratio +. 1.)) in - debug_print (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age); + debug_print (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age)); let symbols, card = match active with | (Negative, e)::_ -> @@ -734,7 +734,7 @@ let backward_simplify_passive env new_pos new_table min_weight passive = let f sign equality (resl, ress, newn) = let ew, _, _, _, _ = equality in if ew < min_weight then -(* let _ = debug_print (Printf.sprintf "OK: %d %d" ew min_weight) in *) +(* let _ = debug_print (lazy (Printf.sprintf "OK: %d %d" ew min_weight)) in *) equality::resl, ress, newn else match forward_simplify env (sign, equality) (new_pos, new_table) with @@ -796,13 +796,13 @@ let rec given_clause env passive active = if !time_limit = 0. || !processed_clauses = 0 then passive else if !elapsed_time > !time_limit then ( - debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time); + debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" + !time_limit !elapsed_time)); make_passive [] [] ) else if kept > selection_estimate then ( - debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^ + debug_print (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^ "(kept: %d, selection_estimate: %d)\n") - kept selection_estimate); + kept selection_estimate)); prune_passive selection_estimate active passive ) else passive @@ -826,14 +826,14 @@ let rec given_clause env passive active = given_clause env passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( - debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current)); + debug_print (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) + (string_of_equality ~env current))); ParamodulationSuccess (Some current, env) ) else ( - debug_print "\n================================================"; - debug_print (Printf.sprintf "selected: %s %s" + debug_print (lazy "\n================================================"); + debug_print (lazy (Printf.sprintf "selected: %s %s" (string_of_sign sign) - (string_of_equality ~env current)); + (string_of_equality ~env current))); let t1 = Unix.gettimeofday () in let new' = infer env sign current active in @@ -931,13 +931,13 @@ let rec given_clause_fullred env passive active = if !time_limit = 0. || !processed_clauses = 0 then passive else if !elapsed_time > !time_limit then ( - debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time); + debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" + !time_limit !elapsed_time)); make_passive [] [] ) else if kept > selection_estimate then ( - debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^ + debug_print (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^ "(kept: %d, selection_estimate: %d)\n") - kept selection_estimate); + kept selection_estimate)); prune_passive selection_estimate active passive ) else passive @@ -961,14 +961,14 @@ let rec given_clause_fullred env passive active = given_clause_fullred env passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( - debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current)); + debug_print (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) + (string_of_equality ~env current))); ParamodulationSuccess (Some current, env) ) else ( - debug_print "\n================================================"; - debug_print (Printf.sprintf "selected: %s %s" + debug_print (lazy "\n================================================"); + debug_print (lazy (Printf.sprintf "selected: %s %s" (string_of_sign sign) - (string_of_equality ~env current)); + (string_of_equality ~env current))); let t1 = Unix.gettimeofday () in let new' = infer env sign current active in @@ -1010,17 +1010,17 @@ let rec given_clause_fullred env passive active = processed_clauses := !processed_clauses + (kept - 1 - k); let _ = - debug_print ( + debug_print (lazy ( Printf.sprintf "active:\n%s\n" (String.concat "\n" ((List.map (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) (fst active))))) + (string_of_equality ~env e)) (fst active)))))) in let _ = match new' with | neg, pos -> - debug_print ( + debug_print (lazy ( Printf.sprintf "new':\n%s\n" (String.concat "\n" ((List.map @@ -1028,7 +1028,7 @@ let rec given_clause_fullred env passive active = (string_of_equality ~env e)) neg) @ (List.map (fun e -> "Positive " ^ - (string_of_equality ~env e)) pos)))) + (string_of_equality ~env e)) pos))))) in match contains_empty env new' with | false, _ -> @@ -1098,11 +1098,11 @@ let main dbd term metasenv ugraph = else let equalities = let equalities = equalities @ library_equalities in - debug_print ( + debug_print (lazy ( Printf.sprintf "equalities:\n%s\n" (String.concat "\n" - (List.map string_of_equality equalities))); - debug_print "SIMPLYFYING EQUALITIES..."; + (List.map string_of_equality equalities)))); + debug_print (lazy "SIMPLYFYING EQUALITIES..."); let rec simpl e others others_simpl = let active = others @ others_simpl in let tbl = @@ -1130,10 +1130,10 @@ let main dbd term metasenv ugraph = let res = List.rev (List.map snd (simpl (Positive, hd) others [])) in - debug_print ( + debug_print (lazy ( Printf.sprintf "equalities AFTER:\n%s\n" (String.concat "\n" - (List.map string_of_equality res))); + (List.map string_of_equality res)))); res in let active = make_active () in @@ -1230,7 +1230,7 @@ let saturate dbd (proof, goal) = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let _, context, ty = CicUtil.lookup_meta goal' metasenv in - debug_print (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)); + debug_print (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty))); Cic.Meta (maxm+1, irl), (maxm+1, context, ty)::metasenv, ty @@ -1257,11 +1257,11 @@ let saturate dbd (proof, goal) = maxmeta := maxm+2; let equalities = let equalities = equalities @ library_equalities in - debug_print ( + debug_print (lazy ( Printf.sprintf "equalities:\n%s\n" (String.concat "\n" - (List.map string_of_equality equalities))); - debug_print "SIMPLYFYING EQUALITIES..."; + (List.map string_of_equality equalities)))); + debug_print (lazy "SIMPLYFYING EQUALITIES..."); let rec simpl e others others_simpl = let active = others @ others_simpl in let tbl = @@ -1289,10 +1289,10 @@ let saturate dbd (proof, goal) = let res = List.rev (List.map snd (simpl (Positive, hd) others [])) in - debug_print ( + debug_print (lazy ( Printf.sprintf "equalities AFTER:\n%s\n" (String.concat "\n" - (List.map string_of_equality res))); + (List.map string_of_equality res)))); res in let active = make_active () in @@ -1304,7 +1304,7 @@ let saturate dbd (proof, goal) = in match res with | ParamodulationSuccess (Some goal, env) -> - debug_print "OK, found a proof!"; + debug_print (lazy "OK, found a proof!"); let proof = Inference.build_proof_term goal in let names = names_of_context context in let newmetasenv = @@ -1328,14 +1328,14 @@ let saturate dbd (proof, goal) = let ty, ug = CicTypeChecker.type_of_aux' newmetasenv context proof ugraph in - debug_print (CicPp.pp proof [](* names *)); - debug_print + debug_print (lazy (CicPp.pp proof [](* names *))); + debug_print (lazy (Printf.sprintf "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n" (CicPp.pp type_of_goal names) (CicPp.pp ty names) (string_of_bool (fst (CicReduction.are_convertible - context type_of_goal ty ug)))); + context type_of_goal ty ug))))); let equality_for_replace i t1 = match t1 with | C.Meta (n, _) -> n = i @@ -1347,21 +1347,21 @@ let saturate dbd (proof, goal) = ~what:[goal'] ~with_what:[proof] ~where:meta_proof in - debug_print ( + debug_print (lazy ( Printf.sprintf "status:\n%s\n%s\n%s\n%s\n" (match uri with Some uri -> UriManager.string_of_uri uri | None -> "") (print_metasenv newmetasenv) (CicPp.pp real_proof [](* names *)) - (CicPp.pp term_to_prove names)); + (CicPp.pp term_to_prove names))); ((uri, newmetasenv, real_proof, term_to_prove), []) with CicTypeChecker.TypeCheckerFailure _ -> - debug_print "THE PROOF DOESN'T TYPECHECK!!!"; - debug_print (CicPp.pp proof names); + debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!"); + debug_print (lazy (CicPp.pp proof names)); raise (ProofEngineTypes.Fail "Found a proof, but it doesn't typecheck") in - debug_print (Printf.sprintf "\nTIME NEEDED: %.9f" time); + debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time)); newstatus | _ -> raise (ProofEngineTypes.Fail "NO proof found") diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index c1c9086de..681a371e1 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -1,6 +1,6 @@ let debug = true;; -let debug_print = if debug then prerr_endline else ignore;; +let debug_print s = if debug then prerr_endline (Lazy.force s);; let print_metasenv metasenv = @@ -289,9 +289,9 @@ let rec aux_ordering ?(recursion=true) t1 t2 = aux_ordering h1 h2 | t1, t2 -> - debug_print ( + debug_print (lazy ( Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n" - (CicPp.ppterm t1) (CicPp.ppterm t2)); + (CicPp.ppterm t1) (CicPp.ppterm t2))); Incomparable ;; @@ -318,8 +318,8 @@ let nonrec_kbo t1 t2 = let rec kbo t1 t2 = -(* debug_print ( *) -(* Printf.sprintf "kbo %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2)); *) +(* debug_print (lazy ( *) +(* Printf.sprintf "kbo %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2))); *) (* if t1 = t2 then *) (* Eq *) (* else *) @@ -333,23 +333,23 @@ let rec kbo t1 t2 = | [], _ -> Lt | hd1::tl1, hd2::tl2 -> let o = -(* debug_print ( *) +(* debug_print (lazy ( *) (* Printf.sprintf "recursion kbo on %s %s" *) -(* (CicPp.ppterm hd1) (CicPp.ppterm hd2)); *) +(* (CicPp.ppterm hd1) (CicPp.ppterm hd2))); *) kbo hd1 hd2 in if o = Eq then cmp tl1 tl2 else o in let comparison = compare_weights ~normalize:true w1 w2 in -(* debug_print ( *) +(* debug_print (lazy ( *) (* Printf.sprintf "Weights are: %s %s: %s" *) (* (string_of_weight w1) (string_of_weight w2) *) -(* (string_of_comparison comparison)); *) +(* (string_of_comparison comparison))); *) match comparison with | Le -> let r = aux t1 t2 in -(* debug_print ("HERE! " ^ (string_of_comparison r)); *) +(* debug_print (lazy ("HERE! " ^ (string_of_comparison r))); *) if r = Lt then Lt else if r = Eq then ( match t1, t2 with diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli index 34e261d17..7814a4b88 100644 --- a/helm/ocaml/paramodulation/utils.mli +++ b/helm/ocaml/paramodulation/utils.mli @@ -44,4 +44,4 @@ val string_of_pos: pos -> string val compute_equality_weight: Cic.term -> Cic.term -> Cic.term -> int -val debug_print: string -> unit +val debug_print: string Lazy.t -> unit diff --git a/helm/ocaml/registry/helm_registry.ml b/helm/ocaml/registry/helm_registry.ml index 7767e4da2..b0fcdab85 100644 --- a/helm/ocaml/registry/helm_registry.ml +++ b/helm/ocaml/registry/helm_registry.ml @@ -27,7 +27,7 @@ open Printf let debug = false let debug_print s = - if debug then prerr_endline ("Helm_registry debugging: " ^ s) + if debug then prerr_endline ("Helm_registry debugging: " ^ (Lazy.force s)) (** *) @@ -118,7 +118,7 @@ let key_is_valid key = raise (Malformed_key key) let set' registry ~key ~value = - debug_print (sprintf "Setting %s = %s" key value); + debug_print (lazy (sprintf "Setting %s = %s" key value)); key_is_valid key; Hashtbl.add registry key value @@ -275,7 +275,7 @@ let rec load_from_absolute ?path registry fname = | "key", ["name", name] -> in_key := true; push_path name | "helm_registry", _ -> () | "include", ["href", fname] -> - debug_print ("including file " ^ fname); + debug_print (lazy ("including file " ^ fname)); load_from_absolute ~path:!_path registry fname | tag, _ -> raise (Parse_error (fname, ~-1, ~-1, diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index 38a5d59d3..e89608cd4 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -23,7 +23,8 @@ * http://cs.unibo.it/helm/. *) - let debug_print = (* ignore *) prerr_endline + let debug = false + let debug_print s = if debug then prerr_endline (Lazy.force s) (* let debug_print = fun _ -> () *) @@ -145,8 +146,8 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals match exitus with Yes (bo,_) -> (* - debug_print "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; - debug_print (CicPp.ppterm ty); + debug_print (lazy "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); + debug_print (lazy (CicPp.ppterm ty)); *) let subst_in = (* if we just apply the subtitution, the type @@ -159,13 +160,13 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals proof goal subst_in metasenv in [(subst_in,(proof,[],sign))] | No d when (d >= depth) -> - (* debug_print "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *) + (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *) [] (* the empty list means no choices, i.e. failure *) | No _ | NotYetInspected -> - debug_print ("CURRENT GOAL = " ^ CicPp.ppterm ty); - debug_print ("CURRENT PROOF = " ^ CicPp.ppterm p); - debug_print ("CURRENT HYP = " ^ CicPp.ppcontext ey); + debug_print (lazy ("CURRENT GOAL = " ^ CicPp.ppterm ty)); + debug_print (lazy ("CURRENT PROOF = " ^ CicPp.ppterm p)); + debug_print (lazy ("CURRENT HYP = " ^ CicPp.ppcontext ey)); let sign, new_sign = if is_meta_closed then None, Some (MetadataConstraints.signature_of ty) @@ -216,8 +217,8 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals in if not (cty = ty) then begin - debug_print ("ty = "^CicPp.ppterm ty); - debug_print ("cty = "^CicPp.ppterm cty); + debug_print (lazy ("ty = "^CicPp.ppterm ty)); + debug_print (lazy ("cty = "^CicPp.ppterm cty)); assert false end Hashtbl.add inspected_goals @@ -284,17 +285,17 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) let auto_tac dbd (proof,goal) = let universe = MetadataQuery.signature_of_goal ~dbd (proof,goal) in Hashtbl.clear inspected_goals; - debug_print "Entro in Auto"; + debug_print (lazy "Entro in Auto"); let id t = t in let t1 = Unix.gettimeofday () in match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with - [] -> debug_print("Auto failed"); + [] -> debug_print (lazy "Auto failed"); raise (ProofEngineTypes.Fail "No Applicable theorem") | (_,(proof,[],_))::_ -> let t2 = Unix.gettimeofday () in - debug_print "AUTO_TAC HA FINITO"; + debug_print (lazy "AUTO_TAC HA FINITO"); let _,_,p,_ = proof in - debug_print (CicPp.ppterm p); + debug_print (lazy (CicPp.ppterm p)); Printf.printf "tempo: %.9f\n" (t2 -. t1); (proof,[]) | _ -> assert false @@ -307,7 +308,7 @@ let paramodulation_tactic = ref (fun dbd status -> raise (ProofEngineTypes.Fail "Not Ready yet..."));; let term_is_equality = ref - (fun term -> debug_print "term_is_equality E` DUMMY!!!!"; false);; + (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);; let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd:Mysql.dbd) () = @@ -315,20 +316,20 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd let normal_auto () = let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in Hashtbl.clear inspected_goals; - debug_print "Entro in Auto"; + debug_print (lazy "Entro in Auto"); let id t = t in let t1 = Unix.gettimeofday () in match auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)] with - [] -> debug_print("Auto failed"); + [] -> debug_print(lazy "Auto failed"); raise (ProofEngineTypes.Fail "No Applicable theorem") | (_,(proof,[],_))::_ -> let t2 = Unix.gettimeofday () in - debug_print "AUTO_TAC HA FINITO"; + debug_print (lazy "AUTO_TAC HA FINITO"); let _,_,p,_ = proof in - debug_print (CicPp.ppterm p); - debug_print (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)); + debug_print (lazy (CicPp.ppterm p)); + debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1))); (proof,[]) | _ -> assert false in @@ -341,7 +342,7 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd !term_is_equality meta_goal in if paramodulation_ok then ( - debug_print "USO PARAMODULATION..."; + debug_print (lazy "USO PARAMODULATION..."); (* try *) !paramodulation_tactic dbd (proof, goal) (* with ProofEngineTypes.Fail _ -> *) diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 1a05bce1b..b80772827 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -423,8 +423,8 @@ let discriminate_tac ~term status = let (t1',t2',consno2') = (* bruuutto: uso un eccezione per terminare con successo! buuu!! :-/ *) try let rec traverse t1 t2 = -debug_print ("XXXX t1 " ^ CicPp.ppterm t1) ; -debug_print ("XXXX t2 " ^ CicPp.ppterm t2) ; +debug_print (lazy ("XXXX t1 " ^ CicPp.ppterm t1)) ; +debug_print (lazy ("XXXX t2 " ^ CicPp.ppterm t2)) ; match t1,t2 with ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) @@ -454,7 +454,7 @@ debug_print ("XXXX t2 " ^ CicPp.ppterm t2) ; in traverse t1 t2 with (TwoDifferentSubtermsFound (t1,t2,consno2)) -> (t1,t2,consno2) in -debug_print ("XXXX consno2' " ^ (string_of_int consno2')) ; +debug_print (lazy ("XXXX consno2' " ^ (string_of_int consno2'))) ; if consno2' = 0 then raise (ProofEngineTypes.Fail "Discriminate: Discriminating terms are structurally equal") else @@ -464,11 +464,11 @@ debug_print ("XXXX consno2' " ^ (string_of_int consno2')) ; match fst(CicEnvironment.get_obj turi CicUniv.empty_ugraph) with C.InductiveDefinition (ind_type_list,_,nr_ind_params) -> -debug_print ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno)) ; +debug_print (lazy ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno))) ; let _,_,_,constructor_list = (List.nth ind_type_list typeno) in -debug_print ("XXXX nth " ^ (string_of_int (List.length constructor_list)) ^ " " ^ (string_of_int consno2')) ; +debug_print (lazy ("XXXX nth " ^ (string_of_int (List.length constructor_list)) ^ " " ^ (string_of_int consno2'))) ; let false_constr_id,_ = List.nth constructor_list (consno2' - 1) in -debug_print ("XXXX nth funzionano ") ; +debug_print (lazy "XXXX nth funzionano ") ; List.map (function (id,cty) -> let red_ty = CicReduction.whd context cty in (* dubbio: e' corretto ridurre in questo context ??? *) @@ -518,22 +518,22 @@ debug_print ("XXXX nth funzionano ") ; ) ~continuation: ( -debug_print ("XXXX rewrite<-: " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2']))); -debug_print ("XXXX rewrite<-: " ^ CicPp.ppterm (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2'])) ; -debug_print ("XXXX equri: " ^ U.string_of_uri equri) ; -debug_print ("XXXX tty : " ^ CicPp.ppterm tty) ; -debug_print ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1')) ; -debug_print ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ; -if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> tty then debug_print ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1')) ; -if (CicTypeChecker.type_of_aux' metasenv' context' t2') <> tty then debug_print ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ; +debug_print (lazy ("XXXX rewrite<-: " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2'])))); +debug_print (lazy ("XXXX rewrite<-: " ^ CicPp.ppterm (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2']))) ; +debug_print (lazy ("XXXX equri: " ^ U.string_of_uri equri)) ; +debug_print (lazy ("XXXX tty : " ^ CicPp.ppterm tty)) ; +debug_print (lazy ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1'))) ; +debug_print (lazy ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2'))) ; +if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> tty then debug_print (lazy ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1'))) ; +if (CicTypeChecker.type_of_aux' metasenv' context' t2') <> tty then debug_print (lazy ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2'))) ; if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> (CicTypeChecker.type_of_aux' metasenv' context' t2') - then debug_print ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' - metasenv' context' t1')) ; debug_print ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ; + then debug_print (lazy ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' + metasenv' context' t1'))) ; debug_print (lazy ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2'))) ; let termty' = ProofEngineReduction.replace_lifting ~equality:(==) ~what:t1 ~with_what:t1' ~where:termty in let termty'' = ProofEngineReduction.replace_lifting ~equality:(==) ~what:t2 ~with_what:t2' ~where:termty' in -debug_print ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' term)); +debug_print (lazy ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' term))); T.then_ ~start:(EqualityTactics.rewrite_back_simpl_tac ~term:term) ~continuation:(IntroductionTactics.constructor_tac ~n:1) diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index 96dc5d15a..0aa33c2db 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -123,9 +123,7 @@ let debug = false let debug_print = fun _ -> () (** debugging print *) -let warn s = - if debug then - debug_print ("DECOMPOSE: " ^ s) +let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s))) (* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *) let search_inductive_types ty = @@ -161,7 +159,7 @@ module R = CicReduction let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim status = let (proof, goal) = status in - warn ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim)); + warn (lazy ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim))); if nr_of_hyp_still_to_elim <> 0 then let _,metasenv,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in @@ -169,12 +167,12 @@ module R = CicReduction let termty,_ = CicTypeChecker.type_of_aux' metasenv context term' CicUniv.empty_ugraph in - warn ("elim_clear termty= " ^ CicPp.ppterm termty); + warn (lazy ("elim_clear termty= " ^ CicPp.ppterm termty)); match termty with C.MutInd (uri,typeno,exp_named_subst) | C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_) when (List.mem (uri,typeno,exp_named_subst) urilist) -> - warn ("elim " ^ CicPp.ppterm termty); + warn (lazy ("elim " ^ CicPp.ppterm termty)); ProofEngineTypes.apply_tactic (T.then_ ~start:(P.elim_intros_simpl_tac term') @@ -185,7 +183,7 @@ module R = CicReduction let _,metasenv,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let new_context_len = List.length context in - warn ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim)); + warn (lazy ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim))); let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in let hyp_name = match List.nth context new_nr_of_hyp_still_to_elim with @@ -197,15 +195,15 @@ module R = CicReduction (T.then_ ~start:( if (term'==term) (* if it's the first application of elim, there's no need to clear the hyp *) - then begin debug_print ("%%%%%%% no clear"); T.id_tac end - else begin debug_print ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:hyp_name) end) + then begin debug_print (lazy ("%%%%%%% no clear")); T.id_tac end + else begin debug_print (lazy ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim)))); (S.clear ~hyp:hyp_name) end) ~continuation:(ProofEngineTypes.mk_tactic (elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim))) status ))) status | _ -> let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in - warn ("fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim)); + warn (lazy ("fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim))); elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim status else (* no hyp to elim left in this goal *) ProofEngineTypes.apply_tactic T.id_tac status diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index e86f79af5..ddeab3e6e 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -30,7 +30,8 @@ module PET = ProofEngineTypes exception Goal_is_not_an_equation -let debug_print = fun _ -> () +let debug = false +let debug_print s = if debug then prerr_endline (Lazy.force s) (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for * the "like" operator (which uses '%' and '_'). Does not support escaping. *) @@ -61,7 +62,7 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) pat = (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)) let match_term ~(dbd:Mysql.dbd) ty = -(* debug_print (CicPp.ppterm ty); *) +(* debug_print (lazy (CicPp.ppterm ty)); *) let metadata = MetadataExtractor.compute ~body:None ~ty in let constants_no = MetadataConstraints.UriManagerSet.cardinal (MetadataConstraints.constants_of ty) @@ -316,15 +317,15 @@ let experimental_hint let other_constants = Constr.UriManagerSet.diff all_constants_closed types_constants in - debug_print "all_constants_closed"; - Constr.UriManagerSet.iter debug_print all_constants_closed; - debug_print "other_constants"; - Constr.UriManagerSet.iter debug_print other_constants; + debug_print (lazy "all_constants_closed"); + if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) all_constants_closed; + debug_print (lazy "other_constants"); + if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) other_constants; let uris = let pow = 2 ** (Constr.UriManagerSet.cardinal other_constants) in if ((List.length uris < pow) or (pow <= 0)) then begin - debug_print "MetadataQuery: large sig, falling back to old method"; + debug_print (lazy "MetadataQuery: large sig, falling back to old method"); filter_uris_forward ~dbd (main, other_constants) uris end else filter_uris_backward ~dbd ~facts (main, other_constants) uris @@ -335,7 +336,7 @@ let experimental_hint (let status' = try let (subst,(proof, goal_list)) = - (* debug_print ("STO APPLICANDO" ^ uri); *) + (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *) apply_tac_verbose ~term:(CicUtil.term_of_uri uri) status @@ -383,7 +384,7 @@ let new_experimental_hint (let status' = try let (subst,(proof, goal_list)) = - (* debug_print ("STO APPLICANDO" ^ uri); *) + (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *) apply_tac_verbose ~term:(CicUtil.term_of_uri uri) status @@ -433,7 +434,7 @@ let instance ~dbd t = (* List.iter (fun x -> debug_print - (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))) + (lazy (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x)))) metadata; *) let no_concl = MetadataDb.count_distinct `Conclusion metadata in let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in @@ -455,7 +456,7 @@ let instance ~dbd t = in match (look_for_dummy_main metadata) with | None-> -(* debug_print "Caso None"; *) +(* debug_print (lazy "Caso None"); *) (* no dummy in main position *) let metadata = List.filter is_dummy metadata in let constraints = List.map MetadataTypes.constr_of_metadata metadata in @@ -465,7 +466,7 @@ let instance ~dbd t = Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints | Some (depth, dummy_type) -> (* debug_print - (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type)); *) + (lazy (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type))); *) (* a dummy in main position *) let metadata_for_dummy_type = MetadataExtractor.compute ~body:None ~ty:dummy_type in diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index c505807f2..8f6369d51 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -35,9 +35,7 @@ let debug = false let debug_print = fun _ -> () (** debugging print *) -let warn s = - if debug then - debug_print ("RING WARNING: " ^ s) +let warn s = debug_print (lazy ("RING WARNING: " ^ (Lazy.force s))) (** CIC URIS *) @@ -199,10 +197,10 @@ let ringable = in function | Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) -> - warn "Goal Ringable!"; + warn (lazy "Goal Ringable!"); true | _ -> - warn "Goal Not Ringable :-(("; + warn (lazy "Goal Not Ringable :-(("); false (** @@ -214,8 +212,8 @@ let ringable = *) let split_eq = function | (Cic.Appl (_::_::t1::t2::[])) as term when ringable term -> - warn ("" ^ (CicPp.ppterm t1) ^ ""); - warn ("" ^ (CicPp.ppterm t2) ^ ""); + warn (lazy ("" ^ (CicPp.ppterm t1) ^ "")); + warn (lazy ("" ^ (CicPp.ppterm t2) ^ "")); (t1, t2) | _ -> raise GoalUnringable @@ -377,7 +375,7 @@ let status_of_single_goal_tactic_result = @param term term to cut *) let elim_type_tac ~term status = - warn "in Ring.elim_type_tac"; + warn (lazy "in Ring.elim_type_tac"); Tacticals.thens ~start:(cut_tac ~term) ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] status *) @@ -392,7 +390,7 @@ let elim_type_tac ~term status = let elim_type2_tac ~term ~proof = let elim_type2_tac ~term ~proof status = let module E = EliminationTactics in - warn "in Ring.elim_type2"; + warn (lazy "in Ring.elim_type2"); ProofEngineTypes.apply_tactic (Tacticals.thens ~start:(E.elim_type_tac term) ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status @@ -407,7 +405,7 @@ let elim_type2_tac ~term ~proof = @param status current proof engine status *) let reflexivity_tac (proof, goal) = - warn "in Ring.reflexivity_tac"; + warn (lazy "in Ring.reflexivity_tac"); let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in try apply_tac (proof, goal) ~term:refl_eqt @@ -464,7 +462,7 @@ let purge_hyps_tac ~count = let ring_tac status = let (proof, goal) = status in - warn "in Ring tactic"; + warn (lazy "in Ring tactic"); let eqt = mkMutInd (HelmLibraryObjects.Logic.eq_URI, 0) [] in let r = HelmLibraryObjects.Reals.r in let metasenv = metasenv_of_status status in @@ -472,9 +470,10 @@ let ring_tac status = let (t1, t2) = split_eq ty in (* goal like t1 = t2 *) match (build_segments ~terms:[t1; t2]) with | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin + if debug then List.iter (* debugging, feel free to remove *) (fun (descr, term) -> - warn (descr ^ " " ^ (CicPp.ppterm term))) + warn (lazy (descr ^ " " ^ (CicPp.ppterm term)))) (List.combine ["t1"; "t1'"; "t1''"; "t1'_eq_t1''"; "t2"; "t2'"; "t2''"; "t2'_eq_t2''"] @@ -504,7 +503,7 @@ let ring_tac status = let b,_ = (*TASSI : FIXME*) are_convertible context t1'' t1 CicUniv.empty_ugraph in if not b then begin - warn "t1'' and t1 are NOT CONVERTIBLE"; + warn (lazy "t1'' and t1 are NOT CONVERTIBLE"); let newstatus = ProofEngineTypes.apply_tactic (elim_type2_tac (* 1st elim_type use *) @@ -517,7 +516,7 @@ let ring_tac status = (proof,[goal]) -> proof,goal | _ -> assert false end else begin - warn "t1'' and t1 are CONVERTIBLE"; + warn (lazy "t1'' and t1 are CONVERTIBLE"); status end in @@ -548,7 +547,7 @@ let ring_tac status = are_convertible context t2'' t2 CicUniv.empty_ugraph in if not b then begin - warn "t2'' and t2 are NOT CONVERTIBLE"; + warn (lazy "t2'' and t2 are NOT CONVERTIBLE"); let newstatus = ProofEngineTypes.apply_tactic (elim_type2_tac (* 2nd elim_type use *) @@ -561,16 +560,16 @@ let ring_tac status = (proof,[goal]) -> proof,goal | _ -> assert false end else begin - warn "t2'' and t2 are CONVERTIBLE"; + warn (lazy "t2'' and t2 are CONVERTIBLE"); status end in try (* try to solve main goal *) - warn "trying reflexivity ...."; + warn (lazy "trying reflexivity ...."); ProofEngineTypes.apply_tactic EqualityTactics.reflexivity_tac status' with (Fail _) -> (* leave conclusion to the user *) - warn "reflexivity failed, solution's left as an ex :-)"; + warn (lazy "reflexivity failed, solution's left as an ex :-)"); ProofEngineTypes.apply_tactic (purge_hyps_tac ~count:!new_hyps) status')]) status' diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index 934b88a5a..94b5d379d 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -34,9 +34,7 @@ let debug = false let debug_print = fun _ -> () (** debugging print *) -let warn s = - if debug then - debug_print ("TACTICALS WARNING: " ^ s) +let warn s = debug_print (lazy ("TACTICALS WARNING: " ^ (Lazy.force s))) let id_tac = let id_tac (proof,goal) = @@ -100,13 +98,13 @@ type tactic = S.tactic *) let first ~tactics = let rec first ~(tactics: (string * tactic) list) status = - warn "in Tacticals.first"; + warn (lazy "in Tacticals.first"); match tactics with | (descr, tac)::tactics -> - warn ("Tacticals.first IS TRYING " ^ descr); + warn (lazy ("Tacticals.first IS TRYING " ^ descr)); (try let res = S.apply_tactic tac status in - warn ("Tacticals.first: " ^ descr ^ " succedeed!!!"); + warn (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!")); res with e -> @@ -114,9 +112,9 @@ let first ~tactics = (Fail _) | (CicTypeChecker.TypeCheckerFailure _) | (CicUnification.UnificationFailure _) -> - warn ( + warn (lazy ( "Tacticals.first failed with exn: " ^ - Printexc.to_string e); + Printexc.to_string e)); first ~tactics status | _ -> raise e (* [e] must not be caught ; let's re-raise it *) ) @@ -181,7 +179,7 @@ let rec seq ~tactics = let repeat_tactic ~tactic = let rec repeat_tactic ~tactic status = - warn "in repeat_tactic"; + warn (lazy "in repeat_tactic"); try let output_status = S.apply_tactic tactic status in let goallist = S.goals output_status in @@ -199,7 +197,7 @@ let repeat_tactic ~tactic = S.set_goals output_status goallist with (Fail _) as e -> - warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; + warn (lazy ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e)) ; S.apply_tactic S.id_tac status in S.mk_tactic (repeat_tactic ~tactic) @@ -228,7 +226,7 @@ let do_tactic ~n ~tactic = S.set_goals output_status goals with (Fail _) as e -> - warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; + warn (lazy ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e)) ; S.apply_tactic S.id_tac status in S.mk_tactic (do_tactic ~n ~tactic) @@ -238,12 +236,12 @@ let do_tactic ~n ~tactic = (* This applies tactic and catches its possible failure *) let try_tactic ~tactic = let rec try_tactic ~tactic status = - warn "in Tacticals.try_tactic"; + warn (lazy "in Tacticals.try_tactic"); try S.apply_tactic tactic status with (Fail _) as e -> - warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e); + warn (lazy ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e)); S.apply_tactic S.id_tac status in S.mk_tactic (try_tactic ~tactic) @@ -252,26 +250,26 @@ let try_tactic ~tactic = (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *) let solve_tactics ~tactics = let rec solve_tactics ~(tactics: (string * tactic) list) status = - warn "in Tacticals.solve_tactics"; + warn (lazy "in Tacticals.solve_tactics"); match tactics with | (descr, currenttactic)::moretactics -> - warn ("Tacticals.solve_tactics is trying " ^ descr); + warn (lazy ("Tacticals.solve_tactics is trying " ^ descr)); (try let output_status = S.apply_tactic currenttactic status in let goallist = S.goals output_status in match goallist with - [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ - " solved the goal!!!"); + [] -> warn (lazy ("Tacticals.solve_tactics: " ^ descr ^ + " solved the goal!!!")); (* questo significa che non ci sono piu' goal, o che current_tactic non ne ha aperti di nuovi? (la 2a!) ##### nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *) output_status - | _ -> warn ("Tacticals.solve_tactics: try the next tactic"); + | _ -> warn (lazy ("Tacticals.solve_tactics: try the next tactic")); solve_tactics ~tactics:(moretactics) status with (Fail _) as e -> - warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ - Printexc.to_string e); + warn (lazy ("Tacticals.solve_tactics: current tactic failed with exn: " ^ + Printexc.to_string e)); solve_tactics ~tactics status ) | [] -> raise (Fail "solve_tactics cannot solve the goal"); diff --git a/helm/ocaml/thread/extThread.ml b/helm/ocaml/thread/extThread.ml index 1b34e09c7..2162251ac 100644 --- a/helm/ocaml/thread/extThread.ml +++ b/helm/ocaml/thread/extThread.ml @@ -27,7 +27,7 @@ *) let debug = true -let debug_print s = if debug then prerr_endline s +let debug_print s = if debug then prerr_endline (Lazy.force s) exception Can_t_kill of Thread.t * string (* thread, reason *) exception Thread_not_found of Thread.t @@ -99,7 +99,7 @@ let _ = | sg when (sg = kill_signal) && (PidSet.mem myself !dead_threads_walking) -> dead_threads_walking := PidSet.remove myself !dead_threads_walking; - debug_print "AYEEEEH!"; + debug_print (lazy "AYEEEEH!"); Thread.exit () | _ -> ()))) diff --git a/helm/ocaml/thread/threadSafe.ml b/helm/ocaml/thread/threadSafe.ml index 4be6618e7..affeae137 100644 --- a/helm/ocaml/thread/threadSafe.ml +++ b/helm/ocaml/thread/threadSafe.ml @@ -27,7 +27,7 @@ *) let debug = false -let debug_print s = if debug then prerr_endline s +let debug_print s = if debug then prerr_endline (Lazy.force s) class threadSafe = object (self) @@ -57,12 +57,12 @@ class threadSafe = method private doCritical: 'a. 'a lazy_t -> 'a = fun action -> - debug_print ""; + debug_print (lazy ""); (try Mutex.lock mutex; let res = Lazy.force action in Mutex.unlock mutex; - debug_print ""; + debug_print (lazy ""); res with e -> Mutex.unlock mutex; @@ -70,7 +70,7 @@ class threadSafe = method private doReader: 'a. 'a lazy_t -> 'a = fun action -> - debug_print ""; + debug_print (lazy ""); let cleanup () = self#decrReadersCount; self#signalNoReaders @@ -78,19 +78,19 @@ class threadSafe = self#incrReadersCount; let res = (try Lazy.force action with e -> (cleanup (); raise e)) in cleanup (); - debug_print ""; + debug_print (lazy ""); res (* TODO may starve!!!! is what we want or not? *) method private doWriter: 'a. 'a lazy_t -> 'a = fun action -> - debug_print ""; + debug_print (lazy ""); self#doCritical (lazy ( while readersCount > 0 do Condition.wait noReaders mutex done; let res = Lazy.force action in - debug_print ""; + debug_print (lazy ""); res )) diff --git a/helm/ocaml/utf8_macros/make_table.ml b/helm/ocaml/utf8_macros/make_table.ml index 377fea64a..68309b1c4 100644 --- a/helm/ocaml/utf8_macros/make_table.ml +++ b/helm/ocaml/utf8_macros/make_table.ml @@ -26,7 +26,7 @@ open Printf let debug = false -let debug_print s = if debug then prerr_endline s +let debug_print s = if debug then prerr_endline (Lazy.force s) (* source files for tables xml parsing (if unmarshall=false) *) let xml_tables = [ @@ -63,7 +63,7 @@ let iter_dictionary_file = iter_gen "entry" "name" "val" let parse_from_xml () = let (macro2utf8, utf82macro) = (Hashtbl.create 2000, Hashtbl.create 2000) in let add_macro macro utf8 = - debug_print (sprintf "Adding macro %s = '%s'" macro utf8); + debug_print (lazy (sprintf "Adding macro %s = '%s'" macro utf8)); Hashtbl.replace macro2utf8 macro utf8; Hashtbl.replace utf82macro utf8 macro in diff --git a/helm/ocaml/utf8_macros/pa_unicode_macro.ml b/helm/ocaml/utf8_macros/pa_unicode_macro.ml index 88ba8b5a8..d14401f84 100644 --- a/helm/ocaml/utf8_macros/pa_unicode_macro.ml +++ b/helm/ocaml/utf8_macros/pa_unicode_macro.ml @@ -24,7 +24,7 @@ *) let debug = false -let debug_print s = if debug then prerr_endline s +let debug_print s = if debug then prerr_endline (Lazy.force s) let loc = let dummy_pos = @@ -34,7 +34,7 @@ let loc = (dummy_pos, dummy_pos) let expand_unicode_macro macro = - debug_print (Printf.sprintf "Expanding macro '%s' ..." macro); + debug_print (lazy (Printf.sprintf "Expanding macro '%s' ..." macro)); let expansion = Utf8Macro.expand macro in <:expr< $str:expansion$ >> @@ -53,7 +53,7 @@ EXTEND (String.sub q 0 pos, String.sub q (pos + 1) (String.length q - pos - 1)) in - debug_print (Printf.sprintf "QUOTATION = %s; ARG = %s" quotation arg); + debug_print (lazy (Printf.sprintf "QUOTATION = %s; ARG = %s" quotation arg)); if quotation = "unicode" then let text = TXtok (loc, x, expand_unicode_macro arg) in {used = []; text = text; styp = STlid (loc, "string")} -- 2.39.2