* 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
(** {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
* 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 "</%s>" tag);*)
-(* debug_print (string_of_stack ctxt);*)
+(* debug_print (lazy (sprintf "</%s>" 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
* 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
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
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 =
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 ;;
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
;;
))
| 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
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
(* 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 "<help> not yet written </help>" 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
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 =
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 *)
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
(* 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
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
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) ->
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
(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)
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)::_ ->
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
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
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
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
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
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
(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, _ ->
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 =
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
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
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 =
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
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 =
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
~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")
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 =
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
;;
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 *)
| [], _ -> 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
val compute_equality_weight: Cic.term -> Cic.term -> Cic.term -> int
-val debug_print: string -> unit
+val debug_print: string Lazy.t -> unit
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))
(** <helpers> *)
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
| "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,
* 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 _ -> () *)
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
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)
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
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
(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) () =
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
!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 _ -> *)
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)))
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
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 ??? *)
)
~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)
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 =
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
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')
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
(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
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. *)
(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)
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
(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
(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
(* 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
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
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
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 *)
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
(**
*)
let split_eq = function
| (Cic.Appl (_::_::t1::t2::[])) as term when ringable term ->
- warn ("<term1>" ^ (CicPp.ppterm t1) ^ "</term1>");
- warn ("<term2>" ^ (CicPp.ppterm t2) ^ "</term2>");
+ warn (lazy ("<term1>" ^ (CicPp.ppterm t1) ^ "</term1>"));
+ warn (lazy ("<term2>" ^ (CicPp.ppterm t2) ^ "</term2>"));
(t1, t2)
| _ -> raise GoalUnringable
@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
*)
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
@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
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
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''"]
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 *)
(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
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 *)
(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'
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) =
*)
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 ->
(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 *)
)
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
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)
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)
(* 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)
(* 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");
*)
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
| 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 ()
| _ -> ())))
*)
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)
method private doCritical: 'a. 'a lazy_t -> 'a =
fun action ->
- debug_print "<doCritical>";
+ debug_print (lazy "<doCritical>");
(try
Mutex.lock mutex;
let res = Lazy.force action in
Mutex.unlock mutex;
- debug_print "</doCritical>";
+ debug_print (lazy "</doCritical>");
res
with e ->
Mutex.unlock mutex;
method private doReader: 'a. 'a lazy_t -> 'a =
fun action ->
- debug_print "<doReader>";
+ debug_print (lazy "<doReader>");
let cleanup () =
self#decrReadersCount;
self#signalNoReaders
self#incrReadersCount;
let res = (try Lazy.force action with e -> (cleanup (); raise e)) in
cleanup ();
- debug_print "</doReader>";
+ debug_print (lazy "</doReader>");
res
(* TODO may starve!!!! is what we want or not? *)
method private doWriter: 'a. 'a lazy_t -> 'a =
fun action ->
- debug_print "<doWriter>";
+ debug_print (lazy "<doWriter>");
self#doCritical (lazy (
while readersCount > 0 do
Condition.wait noReaders mutex
done;
let res = Lazy.force action in
- debug_print "</doWriter>";
+ debug_print (lazy "</doWriter>");
res
))
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 = [
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
*)
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 =
(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$ >>
(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")}
projects / helm.git / commitdiff