pp.ml 5.26 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1
2
(**************************************************************************)
(*                                                                        *)
3
4
5
6
7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(*i $Id: pp.ml,v 1.22 2009-10-19 11:55:33 bobot Exp $ i*)

(*s Pretty-print library *)

open Format

let print_option f fmt = function
  | None -> ()
  | Some x -> f fmt x

let print_option_or_default default f fmt = function
  | None -> fprintf fmt "%s" default
  | Some x -> f fmt x

let rec print_list sep print fmt = function
  | [] -> ()
  | [x] -> print fmt x
  | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r

let print_list_or_default default sep print fmt = function
  | [] -> fprintf fmt "%s" default
  | l -> print_list sep print fmt l

let print_list_par sep pr fmt l =
  print_list sep (fun fmt x -> fprintf fmt "(%a)" pr x) fmt l

let print_list_delim start stop sep pr fmt = function
  | [] -> ()
  | l -> fprintf fmt "%a%a%a" start () (print_list sep pr) l stop ()

50
51
52

let print_iter1 iter sep print fmt l =
  let first = ref true in
53
  iter (fun x ->
54
55
          if !first
          then first := false
56
          else sep fmt ();
57
58
59
60
          print fmt x ) l

let print_iter2 iter sep1 sep2 print1 print2 fmt l =
  let first = ref true in
61
  iter (fun x y ->
62
63
          if !first
          then first := false
64
          else sep1 fmt ();
65
66
67
          print1 fmt x;sep2 fmt (); print2 fmt y) l


68
69
70
71
72
73
74
75
76
let print_iter22 iter sep print fmt l =
  let first = ref true in
  iter (fun x y ->
          if !first
          then first := false
          else sep fmt ();
          print fmt x y) l


Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
77
78
79
let print_pair_delim start sep stop pr1 pr2 fmt (a,b) =
  fprintf fmt "%a%a%a%a%a" start () pr1 a sep () pr2 b stop ()

80
let dot fmt () = fprintf fmt ".@ "
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
81
let comma fmt () = fprintf fmt ",@ "
MARCHE Claude's avatar
MARCHE Claude committed
82
let star fmt () = fprintf fmt "*@ "
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
83
84
85
let simple_comma fmt () = fprintf fmt ", "
let underscore fmt () = fprintf fmt "_"
let semi fmt () = fprintf fmt ";@ "
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
86
let space fmt () = fprintf fmt "@ "
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87
let alt fmt () = fprintf fmt "|@ "
Francois Bobot's avatar
Francois Bobot committed
88
let equal fmt () = fprintf fmt "@ =@ "
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
89
let newline fmt () = fprintf fmt "@\n"
90
let newline2 fmt () = fprintf fmt "@\n@\n"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
91
92
93
94
95
96
97
98
99
let arrow fmt () = fprintf fmt "@ -> "
let lbrace fmt () = fprintf fmt "{"
let rbrace fmt () = fprintf fmt "}"
let lsquare fmt () = fprintf fmt "["
let rsquare fmt () = fprintf fmt "]"
let lparen fmt () = fprintf fmt "("
let rparen fmt () = fprintf fmt ")"
let lchevron fmt () = fprintf fmt "<"
let rchevron fmt () = fprintf fmt ">"
MARCHE Claude's avatar
MARCHE Claude committed
100
let nothing _fmt _ = ()
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
101
102
let string fmt s = fprintf fmt "%s" s
let constant_string s fmt () = string fmt s
103
let add_flush sep fmt x = sep fmt x; pp_print_flush fmt ()
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104
105
106
107
108
109
110
111

let print_pair pr1 = print_pair_delim lparen comma rparen pr1

let hov n fmt f x = pp_open_hovbox fmt n; f x; pp_close_box fmt ()

let open_formatter ?(margin=78) cout =
  let fmt = formatter_of_out_channel cout in
  pp_set_margin fmt margin;
112
  pp_open_box fmt 0;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
113
114
  fmt

115
let close_formatter fmt =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
  pp_close_box fmt ();
  pp_print_flush fmt ()

let open_file_and_formatter ?(margin=78) f =
  let cout = open_out f in
  let fmt = open_formatter ~margin cout in
  cout,fmt

let close_file_and_formatter (cout,fmt) =
  close_formatter fmt;
  close_out cout

let print_in_file_no_close ?(margin=78) p f =
  let cout,fmt = open_file_and_formatter ~margin f in
  p fmt;
  close_formatter fmt;
  cout

let print_in_file ?(margin=78) p f =
  let cout = print_in_file_no_close ~margin p f in
  close_out cout


139
140
141
142
143

(* With optional separation *)
let rec print_list_opt sep print fmt = function
  | [] -> false
  | [x] -> print fmt x
144
  | x :: r ->
145
146
147
148
      let notempty1 = print fmt x in
      if notempty1 then sep fmt ();
      let notempty2 = print_list_opt sep print fmt r in
      notempty1 || notempty2
MARCHE Claude's avatar
MARCHE Claude committed
149
150
151


let string_of p x =
152
153
154
155
156
157
158
  let b = Buffer.create 100 in
  let fmt = formatter_of_buffer b in
  fprintf fmt "%a@?" p x;
  Buffer.contents b


let string_of_wnl p x =
MARCHE Claude's avatar
MARCHE Claude committed
159
160
  let b = Buffer.create 100 in
  let fmt = formatter_of_buffer b in
161
162
163
164
  let out,flush,_newline,spaces =
    pp_get_all_formatter_output_functions fmt () in
  pp_set_all_formatter_output_functions fmt
    ~out ~flush ~newline:(fun () -> spaces 1) ~spaces;
MARCHE Claude's avatar
MARCHE Claude committed
165
166
  fprintf fmt "%a@?" p x;
  Buffer.contents b