From: Claudio Sacerdoti Coen Date: Wed, 23 May 2007 14:58:59 +0000 (+0000) Subject: prerr_endine ==> debug_print everywhere X-Git-Tag: make_still_working~6311 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b109559ac6795075508fd5c231a1bf2a3223031a;p=helm.git prerr_endine ==> debug_print everywhere --- diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index d9e16a255..30138b378 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -260,7 +260,7 @@ let open_pred pred = match pred with | Cic.Lambda (_,_,(Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r])) when LibraryObjects.is_eq_URI uri -> ty,uri,l,r - | _ -> prerr_endline (CicPp.ppterm pred); assert false + | _ -> Utils.debug_print (lazy (CicPp.ppterm pred)); assert false ;; let is_not_fixed t = @@ -290,7 +290,7 @@ let canonical t context menv = [] -> List.rev acc | (l',p)::tl when l=l' -> if acc <> [] then -prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI"); +Utils.debug_print (lazy ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI")); cut_to_last_duplicate l [l',p] tl | (l',p)::tl -> cut_to_last_duplicate l ((l',p)::acc) tl @@ -358,7 +358,7 @@ prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI"); Cic.Const (LibraryObjects.eq_f_sym_URI ~eq, []) in let rc = Cic.Appl [eq_f_sym;ty1;ty2;f;x;y;p] in - prerr_endline ("CANONICAL " ^ CicPp.ppterm rc); + Utils.debug_print (lazy ("CANONICAL " ^ CicPp.ppterm rc)); rc | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t when LibraryObjects.is_eq_URI uri -> t @@ -1328,7 +1328,7 @@ let draw_proof bag names goal_proof proof id = let oc = open_out "/tmp/matita_paramod.dot" in Buffer.output_buffer oc b; close_out oc; - prerr_endline "dot!"; + Utils.debug_print (lazy "dot!"); ignore(Unix.system "dot -Tps -o /tmp/matita_paramod.eps /tmp/matita_paramod.dot" (* "cat /tmp/matita_paramod.dot| tred | dot -Tps -o /tmp/matita_paramod.eps" *) diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index f8b0ff45f..6e7922019 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -31,6 +31,7 @@ let connect_to_auto = true;; +let debug_print = Utils.debug_print;; (* profiling statistics... *) let infer_time = ref 0.;; @@ -801,13 +802,13 @@ let print_goals goals = let pp_goal_set msg goals names = let active_goals, passive_goals = goals in - prerr_endline ("////" ^ msg); - prerr_endline ("ACTIVE G: " ^ + debug_print (lazy ("////" ^ msg)); + debug_print (lazy ("ACTIVE G: " ^ (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names) - active_goals))); - prerr_endline ("PASSIVE G: " ^ + active_goals)))); + debug_print (lazy ("PASSIVE G: " ^ (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names) - passive_goals))) + passive_goals)))) ;; let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) = @@ -990,21 +991,21 @@ let pp_goals label goals context = let names = Utils.names_of_context context in List.iter (fun _,_,g -> - prerr_endline - (Printf.sprintf "Current goal: %s = %s\n" label (CicPp.pp g names))) + debug_print (lazy + (Printf.sprintf "Current goal: %s = %s\n" label (CicPp.pp g names)))) (fst goals); List.iter (fun _,_,g -> - prerr_endline - (Printf.sprintf "PASSIVE goal: %s = %s\n" label (CicPp.pp g names))) + debug_print (lazy + (Printf.sprintf "PASSIVE goal: %s = %s\n" label (CicPp.pp g names)))) (snd goals); ;; let print_status iterno goals active passive = - prerr_endline + debug_print (lazy (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)" iterno (size_of_active active) (size_of_passive passive) - (size_of_goal_set_a goals) (size_of_goal_set_p goals)) + (size_of_goal_set_a goals) (size_of_goal_set_p goals))) ;; (** given-clause algorithm with full reduction strategy: NEW implementation *) @@ -1055,9 +1056,9 @@ let given_clause in match check_if_goals_set_is_solved bag env active goals with | Some p -> - prerr_endline + debug_print (lazy (Printf.sprintf "\nFound a proof in: %f\n" - (Unix.gettimeofday() -. initial_time)); + (Unix.gettimeofday() -. initial_time))); ParamodulationSuccess (p,active,passive) | None -> (* SELECTION *) @@ -1083,9 +1084,9 @@ let given_clause if s_iterno < saturation_steps then let current, passive = select env goals passive in (* SIMPLIFICATION OF CURRENT *) - prerr_endline + debug_print (lazy ("Selected : " ^ - Equality.string_of_equality ~env current); + Equality.string_of_equality ~env current)); forward_simplify bag eq_uri env current active, passive else None, passive @@ -1255,7 +1256,7 @@ let fix_proof metasenv context all_implicits p = try let _ = CicUtil.lookup_meta i metasenv in metasenv with CicUtil.Meta_not_found _ -> - prerr_endline ("not found: "^(string_of_int i)); + debug_print (lazy ("not found: "^(string_of_int i))); let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in (i,context,Cic.Meta(j,irl))::metasenv in @@ -1316,17 +1317,17 @@ let build_proof bag status goalproof newproof subsumption_id subsumption_subst proof_menv = - if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA" - else prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv); + if proof_menv = [] then debug_print (lazy "+++++++++++++++VUOTA") + else debug_print (lazy (CicMetaSubst.ppmetasenv [] proof_menv)); let proof, goalno = status in let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let eq_uri = eq_of_goal type_of_goal in let names = Utils.names_of_context context in - prerr_endline "Proof:"; - prerr_endline + debug_print (lazy "Proof:"); + debug_print (lazy (Equality.pp_proof bag names goalproof newproof subsumption_subst - subsumption_id type_of_goal); + subsumption_id type_of_goal)); (* prerr_endline ("max weight: " ^ (string_of_int (Equality.max_weight goalproof newproof))); @@ -1363,7 +1364,7 @@ let build_proof let goal_proof,goal_ty,real_menv,_ = (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *) try - prerr_endline (CicPp.ppterm goal_proof); + debug_print (lazy (CicPp.ppterm goal_proof)); CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph with | CicRefine.RefineFailure s @@ -1385,7 +1386,7 @@ let build_proof | CicUnification.AssertFailure s -> assert false (* fail "Maybe the local context of metas in the goal was not an IRL" s *) in - prerr_endline "+++++++++++++ FINE UNIF"; + Utils.debug_print (lazy "+++++++++++++ FINE UNIF"); let final_subst = (goalno,(context,goal_proof,type_of_goal))::subst_side_effects in @@ -1573,7 +1574,7 @@ let all_subsumed bag maxm status active passive = let env = metasenv,context,CicUniv.empty_ugraph in let cleaned_goal = Utils.remove_local_context type_of_goal in let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in - prerr_endline (string_of_int (List.length (fst active))); + debug_print (lazy (string_of_int (List.length (fst active)))); (* we simplify using both actives passives *) let table = List.fold_left @@ -1581,7 +1582,7 @@ let all_subsumed bag maxm status active passive = active (list_of_passive passive) in let _,goal = simplify_goal bag env goal table in let (_,_,ty) = goal in - prerr_endline (CicPp.ppterm ty); + debug_print (lazy (CicPp.ppterm ty)); let subsumed = find_all_subsumed bag env (snd table) goal in let subsumed_or_id = match (check_if_goal_is_identity env goal) with @@ -1623,10 +1624,10 @@ let given_clause let metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in let goal = [], metasenv', cleaned_goal in let env = metasenv,context,CicUniv.empty_ugraph in - prerr_endline ">>>>>> ACTIVES >>>>>>>>"; - List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e)) + debug_print (lazy ">>>>>> ACTIVES >>>>>>>>"); + List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e))) active_l; - prerr_endline ">>>>>>>>>>>>>>"; + debug_print (lazy ">>>>>>>>>>>>>>"); let goals = make_goal_set goal in match (* given_caluse non prende in input maxm ????? *) diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml index 00d745fd9..c6e64b898 100644 --- a/helm/software/components/tactics/paramodulation/utils.ml +++ b/helm/software/components/tactics/paramodulation/utils.ml @@ -753,8 +753,7 @@ let guarded_simpl ?(debug=false) context t = if t = t' then t else begin let simpl_order = !compare_terms t t' in - if debug then - prerr_endline ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t')); + debug_print (lazy ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t'))); if simpl_order = Gt then (if debug then prerr_endline "GT";t') else (if debug then prerr_endline "NO_GT";t) end