Commit 6b7621bf authored by Guillaume Melquiond's avatar Guillaume Melquiond

Avoid using the effectful str_formatter whenever possible.

parent 8b5a0505
...@@ -47,13 +47,9 @@ module Sexpr = Set.Make(ExprNode) ...@@ -47,13 +47,9 @@ module Sexpr = Set.Make(ExprNode)
(** prints the given expression, transforming spaces into _ *) (** prints the given expression, transforming spaces into _ *)
let string_of_expr_node node = let string_of_expr_node node =
let print_in_buf printer x =
Format.fprintf Format.str_formatter "@[%a@]" printer x;
Format.flush_str_formatter()
in
let white_space = Str.regexp "[ ()]" in let white_space = Str.regexp "[ ()]" in
let translate x = Str.global_replace white_space "_" x in let translate x = Str.global_replace white_space "_" x in
let repr = print_in_buf Pretty.print_term node in let repr = Format.asprintf "@[%a@]" Pretty.print_term node in
translate repr translate repr
(* for debugging (graph printing) purposes *) (* for debugging (graph printing) purposes *)
......
...@@ -441,8 +441,7 @@ let print_model ?(me_name_trans = why_name_trans) ...@@ -441,8 +441,7 @@ let print_model ?(me_name_trans = why_name_trans)
let model_to_string let model_to_string
?(me_name_trans = why_name_trans) ?(me_name_trans = why_name_trans)
model = model =
print_model ~me_name_trans str_formatter model; Format.asprintf "%a" (print_model ~me_name_trans) model
flush_str_formatter ()
let get_model_file model filename = let get_model_file model filename =
try try
...@@ -474,8 +473,7 @@ let model_vc_term_to_string ...@@ -474,8 +473,7 @@ let model_vc_term_to_string
?(me_name_trans = why_name_trans) ?(me_name_trans = why_name_trans)
?(sep = "\n") ?(sep = "\n")
model = model =
print_model_vc_term ~me_name_trans ~sep str_formatter model; Format.asprintf "%a" (print_model_vc_term ~me_name_trans ~sep) model
flush_str_formatter ()
let get_padding line = let get_padding line =
try try
...@@ -523,10 +521,12 @@ let interleave_line ...@@ -523,10 +521,12 @@ let interleave_line
let list_loc = List.map (add_offset offset) list_loc in let list_loc = List.map (add_offset offset) list_loc in
try try
let model_elements = IntMap.find line_number model_file in let model_elements = IntMap.find line_number model_file in
print_model_elements print_model_value_human me_name_trans str_formatter model_elements ~sep:"; ";
let cntexmp_line = let cntexmp_line =
(get_padding line) ^ start_comment ^ (flush_str_formatter ()) ^ end_comment asprintf "%s%s%a%s"
in (get_padding line)
start_comment
(print_model_elements ~sep:"; " print_model_value_human me_name_trans) model_elements
end_comment in
(* We need to know how many lines will be taken by the counterexample. This (* We need to know how many lines will be taken by the counterexample. This
is ad hoc as we don't really know how the lines are split in IDE. *) is ad hoc as we don't really know how the lines are split in IDE. *)
...@@ -648,8 +648,7 @@ let model_to_string_json ...@@ -648,8 +648,7 @@ let model_to_string_json
?(me_name_trans = why_name_trans) ?(me_name_trans = why_name_trans)
?(vc_line_trans = (fun i -> string_of_int i)) ?(vc_line_trans = (fun i -> string_of_int i))
model = model =
print_model_json str_formatter ~me_name_trans ~vc_line_trans model; asprintf "%a" (print_model_json ~me_name_trans ~vc_line_trans) model
flush_str_formatter ()
(* (*
......
...@@ -594,8 +594,8 @@ let read_config conf_file = ...@@ -594,8 +594,8 @@ let read_config conf_file =
try try
get_config filenamerc get_config filenamerc
with e when not (Debug.test_flag Debug.stack_trace) -> with e when not (Debug.test_flag Debug.stack_trace) ->
Format.fprintf str_formatter "%a" Exn_printer.exn_printer e; let s = Format.asprintf "%a" Exn_printer.exn_printer e in
raise (ConfigFailure (fst filenamerc, flush_str_formatter ())) raise (ConfigFailure (fst filenamerc, s))
(** filter prover *) (** filter prover *)
type regexp_desc = { reg : Str.regexp; desc : string} type regexp_desc = { reg : Str.regexp; desc : string}
......
...@@ -987,6 +987,7 @@ let clear_message_zone () = ...@@ -987,6 +987,7 @@ let clear_message_zone () =
(* Function used to print stuff on the message_zone *) (* Function used to print stuff on the message_zone *)
let print_message ~kind ~notif_kind fmt = let print_message ~kind ~notif_kind fmt =
(* TODO: use kasprintf once OCaml 4.03 is used *)
Format.kfprintf Format.kfprintf
(fun _ -> let s = flush_str_formatter () in (fun _ -> let s = flush_str_formatter () in
let s = try_convert s in let s = try_convert s in
...@@ -1005,37 +1006,30 @@ let print_message ~kind ~notif_kind fmt = ...@@ -1005,37 +1006,30 @@ let print_message ~kind ~notif_kind fmt =
str_formatter str_formatter
fmt fmt
let display_warnings () = let display_warnings fmt warnings =
if Queue.is_empty warnings then () else let nwarn = ref 0 in
begin try
let nwarn = ref 0 in Queue.iter (fun (loc,msg) ->
begin try if !nwarn = 4 then begin
Queue.iter Format.fprintf fmt "[%d more warnings. See stderr for details]@\n" (Queue.length warnings - !nwarn);
(fun (loc,msg) -> raise Exit
if !nwarn = 4 then
begin
Format.fprintf Format.str_formatter "[%d more warnings. See stderr for details]@\n" (Queue.length warnings - !nwarn);
raise Exit
end
else
begin
incr nwarn;
match loc with
| None ->
Format.fprintf Format.str_formatter "%s@\n@\n" msg
| Some l ->
(* scroll_to_loc ~color:error_tag ~yalign:0.5 loc; *)
Format.fprintf Format.str_formatter "%a: %s@\n@\n"
Loc.gen_report_position l msg
end) warnings;
with Exit -> ();
end; end;
Queue.clear warnings; incr nwarn;
let msg = match loc with
Format.flush_str_formatter () | None ->
in Format.fprintf fmt "%s@\n@\n" msg
print_message ~kind:1 ~notif_kind:"warning" "%s" msg | Some l ->
end (* scroll_to_loc ~color:error_tag ~yalign:0.5 loc; *)
Format.fprintf fmt "%a: %s@\n@\n" Loc.gen_report_position l msg
) warnings;
with Exit -> ()
let display_warnings () =
if Queue.is_empty warnings then ()
else begin
print_message ~kind:1 ~notif_kind:"warning" "%a" display_warnings warnings;
Queue.clear warnings;
end
let print_message ~kind ~notif_kind fmt = let print_message ~kind ~notif_kind fmt =
display_warnings (); print_message ~kind ~notif_kind fmt display_warnings (); print_message ~kind ~notif_kind fmt
......
...@@ -1662,8 +1662,7 @@ let print_spec args pre post xpost oldies eff fmt ity = ...@@ -1662,8 +1662,7 @@ let print_spec args pre post xpost oldies eff fmt ity =
fprintf fmt "@\nold { %a -> %a }" print_pv o print_pv v in fprintf fmt "@\nold { %a -> %a }" print_pv o print_pv v in
let print_post fmt q = let print_post fmt q =
let v, q = open_post q in let v, q = open_post q in
fprintf str_formatter "%a" print_vs v; let n = asprintf "%a" print_vs v in
let n = flush_str_formatter () in
if n = "result" || t_v_occurs v q = 0 then if n = "result" || t_v_occurs v q = 0 then
fprintf fmt "@\nensures { @[%a@] }" print_term q else fprintf fmt "@\nensures { @[%a@] }" print_term q else
fprintf fmt "@\nreturns { %s ->@ @[%a@] }" n print_term q; fprintf fmt "@\nreturns { %s ->@ @[%a@] }" n print_term q;
......
...@@ -394,8 +394,7 @@ let print_info_model info = ...@@ -394,8 +394,7 @@ let print_info_model info =
begin begin
let model_map = let model_map =
S.fold (fun f acc -> S.fold (fun f acc ->
fprintf str_formatter "%a" (print_fmla info) f; let s = asprintf "%a" (print_fmla info) f in
let s = flush_str_formatter () in
Mstr.add s f acc) Mstr.add s f acc)
info_model info_model
Mstr.empty in (); Mstr.empty in ();
......
...@@ -164,12 +164,10 @@ type constant = Enum of term * int | Value of term | Varying ...@@ -164,12 +164,10 @@ type constant = Enum of term * int | Value of term | Varying
let rec constant_value defs t = let rec constant_value defs t =
match t.t_node with match t.t_node with
| Tconst c -> | Tconst c ->
fprintf str_formatter "%a" (Number.print number_format) c; asprintf "%a" (Number.print number_format) c
flush_str_formatter ()
| Tapp (ls, [{ t_node = Tconst c}]) | Tapp (ls, [{ t_node = Tconst c}])
when ls_equal ls !int_minus || ls_equal ls !real_minus -> when ls_equal ls !int_minus || ls_equal ls !real_minus ->
fprintf str_formatter "-%a" (Number.print number_format) c; asprintf "-%a" (Number.print number_format) c
flush_str_formatter ()
| Tapp (ls, []) -> | Tapp (ls, []) ->
begin begin
match Hid.find defs ls.ls_name with match Hid.find defs ls.ls_name with
......
...@@ -134,12 +134,10 @@ let print_const fmt c = ...@@ -134,12 +134,10 @@ let print_const fmt c =
let constant_value = let constant_value =
fun t -> match t.t_node with fun t -> match t.t_node with
| Tconst c -> | Tconst c ->
fprintf str_formatter "%a" print_const c; asprintf "%a" print_const c
flush_str_formatter ()
| Tapp(ls, [{ t_node = Tconst c}]) | Tapp(ls, [{ t_node = Tconst c}])
when ls_equal ls !int_minus || ls_equal ls !real_minus -> when ls_equal ls !int_minus || ls_equal ls !real_minus ->
fprintf str_formatter "-%a" print_const c; asprintf "-%a" print_const c
flush_str_formatter ()
| _ -> raise Not_found | _ -> raise Not_found
......
...@@ -497,8 +497,7 @@ let print_info_model info = ...@@ -497,8 +497,7 @@ let print_info_model info =
begin begin
let model_map = let model_map =
S.fold (fun f acc -> S.fold (fun f acc ->
fprintf str_formatter "%a" (print_fmla info) f; let s = asprintf "%a" (print_fmla info) f in
let s = flush_str_formatter () in
Mstr.add s f acc) Mstr.add s f acc)
info_model info_model
Mstr.empty in Mstr.empty in
......
...@@ -96,10 +96,8 @@ let elim le_int le_real neg_real type_kept kn ...@@ -96,10 +96,8 @@ let elim le_int le_real neg_real type_kept kn
let emax = BigInt.pow_int_pos_bigint 2 (BigInt.pred eb) in let emax = BigInt.pow_int_pos_bigint 2 (BigInt.pred eb) in
let m = BigInt.pred (BigInt.pow_int_pos_bigint 2 sb) in let m = BigInt.pred (BigInt.pow_int_pos_bigint 2 sb) in
let e = BigInt.sub emax sb in let e = BigInt.sub emax sb in
Number.print_in_base 16 None Format.str_formatter m; let m_string = Format.asprintf "%a" (Number.print_in_base 16 None) m in
let m_string = Format.flush_str_formatter () in let e_string = Format.asprintf "%a" (Number.print_in_base 10 None) e in
Number.print_in_base 10 None Format.str_formatter e;
let e_string = Format.flush_str_formatter () in
let e_val = Number.real_const_hex m_string "" (Some e_string) in let e_val = Number.real_const_hex m_string "" (Some e_string) in
let max_term = t_const let max_term = t_const
Number.(ConstReal { rc_negative = false ; rc_abs = e_val }) Number.(ConstReal { rc_negative = false ; rc_abs = e_val })
......
...@@ -146,9 +146,7 @@ module Task = ...@@ -146,9 +146,7 @@ module Task =
| _ -> [] | _ -> []
let task_to_string t = let task_to_string t =
ignore (flush_str_formatter ()); Format.asprintf "%a" (Driver.print_task alt_ergo_driver) t
Driver.print_task alt_ergo_driver str_formatter t;
flush_str_formatter ()
let gen_id = let gen_id =
let c = ref 0 in let c = ref 0 in
......
...@@ -154,8 +154,7 @@ and scan_isolated fmt empty in_pre delayed = parse ...@@ -154,8 +154,7 @@ and scan_isolated fmt empty in_pre delayed = parse
{ comment fmt false lexbuf; { comment fmt false lexbuf;
scan_isolated fmt empty in_pre delayed lexbuf } scan_isolated fmt empty in_pre delayed lexbuf }
| space* "(**" | space* "(**"
{ doc str_formatter false [] lexbuf; { let d = asprintf "%s%a" delayed (fun fmt -> doc fmt false []) lexbuf in
let d = delayed ^ flush_str_formatter () in
scan_isolated fmt false in_pre d lexbuf } scan_isolated fmt false in_pre d lexbuf }
| eof { if in_pre then pp_print_string fmt "</pre>\n"; | eof { if in_pre then pp_print_string fmt "</pre>\n";
if delayed <> "" then pp_print_string fmt delayed } if delayed <> "" then pp_print_string fmt delayed }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment