src/Pure/Syntax/pretty.ML
author paulson
Thu Sep 25 12:09:41 1997 +0200 (1997-09-25)
changeset 3706 e57b5902822f
parent 2695 871b69a4b78f
child 3738 27f7473d029a
permissions -rw-r--r--
Generalized and exported biresolution_from_nets_tac to allow the declaration
of Clarify_tac
wenzelm@18
     1
(*  Title:      Pure/Syntax/pretty.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Lawrence C Paulson
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
wenzelm@18
     6
Generic pretty printing module.
clasohm@0
     7
clasohm@0
     8
Loosely based on
clasohm@0
     9
  D. C. Oppen, "Pretty Printing",
clasohm@0
    10
  ACM Transactions on Programming Languages and Systems (1980), 465-483.
clasohm@0
    11
clasohm@0
    12
The object to be printed is given as a tree with indentation and line
clasohm@0
    13
breaking information.  A "break" inserts a newline if the text until
clasohm@0
    14
the next break is too long to fit on the current line.  After the newline,
clasohm@0
    15
text is indented to the level of the enclosing block.  Normally, if a block
clasohm@0
    16
is broken then all enclosing blocks will also be broken.  Only "inconsistent
clasohm@0
    17
breaks" are provided.
clasohm@0
    18
clasohm@0
    19
The stored length of a block is used in breakdist (to treat each inner block as
clasohm@0
    20
a unit for breaking).
clasohm@0
    21
*)
clasohm@0
    22
wenzelm@18
    23
type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
wenzelm@18
    24
  (unit -> unit) * (unit -> unit);
clasohm@0
    25
clasohm@0
    26
signature PRETTY =
paulson@1508
    27
  sig
clasohm@0
    28
  type T
wenzelm@2695
    29
  val str: string -> T
wenzelm@2695
    30
  val strlen: string -> int -> T
wenzelm@18
    31
  val brk: int -> T
wenzelm@18
    32
  val fbrk: T
wenzelm@2695
    33
  val blk: int * T list -> T
wenzelm@18
    34
  val lst: string * string -> T list -> T
wenzelm@18
    35
  val quote: T -> T
wenzelm@236
    36
  val commas: T list -> T list
wenzelm@236
    37
  val breaks: T list -> T list
wenzelm@236
    38
  val fbreaks: T list -> T list
wenzelm@236
    39
  val block: T list -> T
wenzelm@261
    40
  val strs: string list -> T
lcp@512
    41
  val enclose: string -> string -> T list -> T
wenzelm@236
    42
  val list: string -> string -> T list -> T
wenzelm@236
    43
  val str_list: string -> string -> string list -> T
wenzelm@261
    44
  val big_list: string -> T list -> T
wenzelm@18
    45
  val string_of: T -> string
wenzelm@261
    46
  val writeln: T -> unit
wenzelm@18
    47
  val str_of: T -> string
wenzelm@18
    48
  val pprint: T -> pprint_args -> unit
clasohm@0
    49
  val setdepth: int -> unit
clasohm@0
    50
  val setmargin: int -> unit
paulson@1508
    51
  end;
clasohm@0
    52
paulson@1508
    53
structure Pretty : PRETTY =
clasohm@0
    54
struct
clasohm@0
    55
wenzelm@2695
    56
(*printing items: compound phrases, strings, and breaks*)
wenzelm@2695
    57
datatype T =
wenzelm@2695
    58
  Block of T list * int * int |         (*body, indentation, length*)
wenzelm@2695
    59
  String of string * int |              (*text, length*)
wenzelm@2695
    60
  Break of bool * int;                  (*mandatory flag, width if not taken*);
clasohm@0
    61
clasohm@0
    62
(*Add the lengths of the expressions until the next Break; if no Break then
clasohm@0
    63
  include "after", to account for text following this block. *)
clasohm@0
    64
fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
wenzelm@2695
    65
  | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
clasohm@0
    66
  | breakdist (Break _ :: es, after) = 0
clasohm@0
    67
  | breakdist ([], after) = after;
clasohm@0
    68
clasohm@0
    69
fun repstring a 0 = ""
clasohm@0
    70
  | repstring a 1 = a
clasohm@0
    71
  | repstring a k =
clasohm@0
    72
      if k mod 2 = 0 then repstring(a^a) (k div 2)
clasohm@0
    73
                     else repstring(a^a) (k div 2) ^ a;
clasohm@0
    74
clasohm@0
    75
(*** Type for lines of text: string, # of lines, position on line ***)
clasohm@0
    76
clasohm@0
    77
type text = {tx: string, nl: int, pos: int};
clasohm@0
    78
clasohm@0
    79
val emptytext = {tx="", nl=0, pos=0};
clasohm@0
    80
clasohm@0
    81
fun blanks wd {tx,nl,pos} =
lcp@118
    82
    {tx  = tx ^ repstring " " wd,
clasohm@0
    83
     nl  = nl,
clasohm@0
    84
     pos = pos+wd};
clasohm@0
    85
clasohm@0
    86
fun newline {tx,nl,pos} =
clasohm@0
    87
    {tx  = tx ^ "\n",
clasohm@0
    88
     nl  = nl+1,
clasohm@0
    89
     pos = 0};
clasohm@0
    90
wenzelm@2695
    91
fun string s len {tx,nl,pos:int} =
clasohm@0
    92
    {tx  = tx ^ s,
clasohm@0
    93
     nl  = nl,
wenzelm@2695
    94
     pos = pos + len};
wenzelm@2695
    95
clasohm@0
    96
clasohm@0
    97
(*** Formatting ***)
clasohm@0
    98
clasohm@0
    99
val margin      = ref 80        (*right margin, or page width*)
clasohm@0
   100
and breakgain   = ref 4         (*minimum added space required of a break*)
clasohm@0
   101
and emergencypos = ref 40;      (*position too far to right*)
clasohm@0
   102
clasohm@0
   103
fun setmargin m =
clasohm@0
   104
    (margin     := m;
clasohm@0
   105
     breakgain  := !margin div 20;
clasohm@0
   106
     emergencypos := !margin div 2);
clasohm@0
   107
lcp@118
   108
(*Search for the next break (at this or higher levels) and force it to occur*)
clasohm@0
   109
fun forcenext [] = []
clasohm@0
   110
  | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
clasohm@0
   111
  | forcenext (e :: es) = e :: forcenext es;
clasohm@0
   112
lcp@118
   113
(*es is list of expressions to print;
lcp@118
   114
  blockin is the indentation of the current block;
lcp@118
   115
  after is the width of the following context until next break. *)
clasohm@0
   116
fun format ([], _, _) text = text
clasohm@0
   117
  | format (e::es, blockin, after) (text as {pos,nl,...}) =
clasohm@0
   118
    (case e of
clasohm@0
   119
       Block(bes,indent,wd) =>
clasohm@0
   120
         let val blockin' = (pos + indent) mod !emergencypos
clasohm@0
   121
             val btext = format(bes, blockin', breakdist(es,after)) text
lcp@118
   122
             (*If this block was broken then force the next break.*)
wenzelm@236
   123
             val es2 = if nl < #nl(btext) then forcenext es else es
clasohm@0
   124
         in  format (es2,blockin,after) btext  end
wenzelm@2695
   125
     | String (s, len) => format (es,blockin,after) (string s len text)
lcp@118
   126
     | Break(force,wd) => (*no break if text to next break fits on this line
wenzelm@236
   127
                            or if breaking would add only breakgain to space *)
clasohm@0
   128
           format (es,blockin,after)
clasohm@0
   129
               (if not force andalso
paulson@2149
   130
                   pos+wd <= Int.max(!margin - breakdist(es,after),
wenzelm@2695
   131
                                     blockin + !breakgain)
lcp@118
   132
                then blanks wd text  (*just insert wd blanks*)
clasohm@0
   133
                else blanks blockin (newline text)));
clasohm@0
   134
wenzelm@2695
   135
clasohm@0
   136
(*** Exported functions to create formatting expressions ***)
clasohm@0
   137
wenzelm@2695
   138
fun length (Block (_, _, len)) = len
wenzelm@2695
   139
  | length (String (_, len)) = len
wenzelm@2695
   140
  | length (Break(_, wd)) = wd;
clasohm@0
   141
wenzelm@2695
   142
fun str s = String (s, size s);
wenzelm@2695
   143
fun strlen s len = String (s, len);
clasohm@0
   144
wenzelm@2695
   145
fun brk wd = Break (false, wd);
wenzelm@2695
   146
val fbrk = Break (true, 0);
clasohm@0
   147
wenzelm@2695
   148
fun blk (indent, es) =
wenzelm@2695
   149
  let
wenzelm@2695
   150
    fun sum([], k) = k
wenzelm@2695
   151
      | sum(e :: es, k) = sum (es, length e + k);
wenzelm@2695
   152
  in Block (es, indent, sum (es, 0)) end;
clasohm@0
   153
lcp@118
   154
(*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
clasohm@0
   155
fun lst(lp,rp) es =
clasohm@0
   156
  let fun add(e,es) = str"," :: brk 1 :: e :: es;
clasohm@0
   157
      fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
clasohm@0
   158
        | list(e::[]) = [str lp, e, str rp]
clasohm@0
   159
        | list([]) = []
clasohm@0
   160
  in blk(size lp, list es) end;
clasohm@0
   161
wenzelm@236
   162
wenzelm@236
   163
(* utils *)
wenzelm@236
   164
wenzelm@236
   165
fun quote prt =
wenzelm@236
   166
  blk (1, [str "\"", prt, str "\""]);
wenzelm@236
   167
wenzelm@236
   168
fun commas prts =
wenzelm@236
   169
  flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
wenzelm@236
   170
wenzelm@236
   171
fun breaks prts = separate (brk 1) prts;
wenzelm@236
   172
wenzelm@236
   173
fun fbreaks prts = separate fbrk prts;
wenzelm@236
   174
wenzelm@236
   175
fun block prts = blk (2, prts);
wenzelm@236
   176
wenzelm@261
   177
val strs = block o breaks o (map str);
wenzelm@261
   178
lcp@512
   179
fun enclose lpar rpar prts =
wenzelm@236
   180
  block (str lpar :: (prts @ [str rpar]));
wenzelm@236
   181
wenzelm@236
   182
fun list lpar rpar prts =
lcp@512
   183
  enclose lpar rpar (commas prts);
wenzelm@236
   184
wenzelm@236
   185
fun str_list lpar rpar strs =
wenzelm@236
   186
  list lpar rpar (map str strs);
wenzelm@236
   187
wenzelm@261
   188
fun big_list name prts =
wenzelm@261
   189
  block (fbreaks (str name :: prts));
wenzelm@261
   190
clasohm@0
   191
clasohm@0
   192
clasohm@0
   193
(*** Pretty printing with depth limitation ***)
clasohm@0
   194
clasohm@0
   195
val depth       = ref 0;        (*maximum depth; 0 means no limit*)
clasohm@0
   196
clasohm@0
   197
fun setdepth dp = (depth := dp);
clasohm@0
   198
lcp@118
   199
(*Recursively prune blocks, discarding all text exceeding depth dp*)
clasohm@0
   200
fun pruning dp (Block(bes,indent,wd)) =
clasohm@0
   201
      if dp>0 then blk(indent, map (pruning(dp-1)) bes)
wenzelm@2695
   202
              else str "..."
clasohm@0
   203
  | pruning dp e = e;
clasohm@0
   204
clasohm@0
   205
fun prune dp e = if dp>0 then pruning dp e else e;
clasohm@0
   206
clasohm@0
   207
lcp@118
   208
fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
clasohm@0
   209
wenzelm@261
   210
val writeln = writeln o string_of;
wenzelm@261
   211
clasohm@0
   212
lcp@118
   213
(*Create a single flat string: no line breaking*)
clasohm@0
   214
fun str_of prt =
clasohm@0
   215
  let
clasohm@0
   216
    fun s_of (Block (prts, _, _)) = implode (map s_of prts)
wenzelm@2695
   217
      | s_of (String (s, _)) = s
wenzelm@18
   218
      | s_of (Break (false, wd)) = repstring " " wd
wenzelm@18
   219
      | s_of (Break (true, _)) = " ";
clasohm@0
   220
  in
clasohm@0
   221
    s_of (prune (! depth) prt)
clasohm@0
   222
  end;
clasohm@0
   223
lcp@118
   224
(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
wenzelm@18
   225
fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
clasohm@0
   226
  let
clasohm@0
   227
    fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
wenzelm@2695
   228
      | pp (String (s, _)) = put_str s
wenzelm@18
   229
      | pp (Break (false, wd)) = put_brk wd
wenzelm@18
   230
      | pp (Break (true, _)) = put_fbrk ()
clasohm@0
   231
    and pp_lst [] = ()
clasohm@0
   232
      | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
clasohm@0
   233
  in
clasohm@0
   234
    pp (prune (! depth) prt)
clasohm@0
   235
  end;
clasohm@0
   236
clasohm@0
   237
clasohm@0
   238
(*** Initialization ***)
clasohm@0
   239
clasohm@0
   240
val () = setmargin 80;
clasohm@0
   241
clasohm@0
   242
end;