aboutccvisual

Strictly Annotated: A Pretty-Printer With Support for Annotations

June 17, 2021

The source code for Strictly Annotated is available at gh:ayazhafiz/strictly-annotated.

Problem Statement

Suppose we are working on a system that emits some kind of human-readable documents. Natural examples here are compilers of all kinds, static analyzers, term rewriting systems, automated theorem provers, grammar checkers, among others. We would like the presentation an emitted document to reflect its semantic structure, so this emission will involve the use of a pretty-printer (formatter) of some sort.

Now suppose that in addition to an intuitive formatting of the semantic terms composing the document, we would like to attach arbitrary, nicely-rendered annotations at certain locations in the document. For example, we may want to annotate source code with generated comments, or annotate the input to an analysis tool with discoveries made by the analyzer. Concretely, we may imagine a pedagogical C compiler that annotates assembly with its generating source code:

fibonacci(int n):
   mov   eax, 1    ; int nth = 1
   xor   ebx, ebx  ; int last = 0
   mov   ecx, 1    ; int i = 1
L1:
   cmp   ecx, edi  ; while (i < n)
   jge   L2
   mov   esi, eax  ; int next = nth
   add   esi, ebx  ;            + last
   mov   ebx, eax  ; last = nth
   mov   eax, esi  ; nth = next
   inc   ecx       ; ++i
   jmp   L1
L2:
   ret             ; return nth

or a computer algebra system that communicates rewrite steps:

latex
d/dx [x^3 + 6x^2 + 12x - 2]
  =    3x^2     %(by the power rule)
    + 12x       %(by the power rule)
    + 12        %(by d/dx x = 1)
    - 0         %(by d/dx c = 0   when c is independent of x)
  = 3x^2 + 12x + 12  %(by simplification)
  = 3(x^2 + 4x + 4)  %(by gcd(3, 12, 12) = 3)
  = 3(x + 2)^2       %(by factorization in \Z)

Indeed such applications are common. It is not too difficult to imagine how we might implement the pedagogical C compiler's printer. The semantic structure of the computer algebra system's output is more involved, but an ad-hoc design for its printer does not take much additional work. But as we increase the complexity of a document's structure, it becomes more difficult to imagine how a standard pretty-printer should treat annotations when trying to layout the semantically-relevant parts of the document.

This cc will describe Strictly Annotated's solution to this challenge. In a nutshell, our approach will be to format semantic terms and annotations independently, with few layout decisions involving both terms and annotations. Our pretty-printing library is general-purpose, not unlike formatting modules in the standard libraries of OCaml and Haskell, but with a bold opinion that annotations are independent of other content in a document, and less important to layout.

I think that Strictly Annotated does a pretty good job; here is an example of a research language source code with typechecker annotations, printed by the library:

latex
fn f(x: any) =  % => int | (int, int)
  if x is int   % if .. ~> int | (int, int)
  then 1
  else (0, 0)   % (int, int)
in
  (f 1,         % f .. ~> int
   f            % f .. ~> (int, int)
     (1, 2)     % (int, int)
  )             % (int, (int, int))

Opinions we will make

It is important to note that our library distinguishes annotations from any other kind of term in a document. As mentioned above, we are saying that annotations are less important to the semantic structure of a document and should only serve as "addons" to a regular document.

What this means is that Strictly Annotated does not make for a good code formatter, without additional guidance from the library user. Indeed, most code formatters for programming languages treat comments in source code as semantic terms themselvesFor code formatters, layout of comments is a common and tricky problem., aligning comments in certain locations and adapting layouts to ensure that comments "look nice". Our opinion is that the layout of comments in this way is domain-specific, and we would rather lay out annotations just by saying "this note is associated with this term, place it somewhere reasonable but don't worry about it too much".

The Design

We now present an overview of the design of our library. We first briefly recount the base pretty-printer design given by Lindig, then elaborate our contribution in supporting and printing annotations.

Lindig's printing of semantic terms

Lindig's 2000 note Strictly Annotated describes an eager implementation of the algebra-based pretty-printer designed in a A prettier printer (Walder, 1999). As we have already mentioned, our pretty-printer is a fork of Lindig's. While it is useful to read the entirety of Lindig's short and pleasant note, we will briefly recap the key ideas for those that do not wish a diversion, and so that it is clear how our additions modify the basic design.

Per Walder's algebraWe will not discuss Walder's algebraic results here, as it is much better explained by Walder himself and not necessary for understanding the essence of the pretty-printing idea. and Lindig's note, there are six constructors for a document (here presented in OCaml):

ocaml
type doc = Nil
         | Text  of string
         | Break of string
         | Cons  of doc * doc
         | Nest  of int * doc
         | Group of doc

The Nil and Text constructors are straightforward. Cons(x, y) concatenates documents x and y. Group doc describes a "group" in a document that a pretty-printer may choose to layout either horizontally or vertically. Break sep is a directive to the pretty-printer that a newline should be inserted if the enclosing group is in is laid out vertically, or else sep should be printed. Nest(indent, d) instructs the pretty-printer to indent text following a newline in d by indent spaces.

A simple example comes from pages 3 and 7 of Lindig's note. Taking $[\dots]$ as the Group constructor, ${}^n\langle d \rangle$ as Nest(n, d), $\cdot$ as Cons, and $-$ as Break " ", the document

may be printed at different widths as

if maybe x then pos() else neg()        if maybe x        if
                                        then pos()          maybe x
                                        else neg()        then
                                                            pos()
                                                          else
                                                            neg()

The principal decision to be made in the pretty-printing process is whether a group should be laid out horizontally or vertically. Unsurprisingly, Lindig proposes that this decision be made by first checking if a group can be laid out entirely horizontally without surpassing a maximum line width; if this check fails, the group should be laid out vertically (Lindig, 5-6). Lindig implements this check via an algorithm fits, invoked during a function format that performs a top-down traversal of a document to decide the layout of its subgroups.

Lindig does not mention it, but his format procedure observes the property that if a group is given a vertical layout, all its parent groups are given vertical layouts. We will call this property waterfalling.

$\Def$ Let $D$ be a $\texttt{doc}$ and $\Gr(D)$ denote the $\tt Group$s of $D$, endowed with a strict preorder given by $g < h \iff g \in h %>$. Let $\vert(g)$ be true only when $g$ has a vertical layout. $D$ is a waterfall if $\forall g\in \Gr(D)\ \ \vert(g)\implies \left(\forall h\in \Gr(D)\ \ g < h\implies \vert(h)\right)%>$.

Waterfalling is an important property because it gives the user some guarantees about the behavior of the pretty-printer. To see why, suppose the example above was instead given a cascading layout, where the outer group has a horizontal layout but every other group has a vertical layout. Then the document would be printed as

if
  maybe
    x then
  pos() else
  neg()

While cascading printers are more expressive than waterfalling printers, they are also more complex:

  • A cascading printing library must provide mechanisms to force horizontal or vertical layouts to be of any use.

  • A cascading printing library may explore as many as $2^g$ layouts, where $g$ is the number of groups in a document, clobbering efficiency of the library.A cascading printer could decide parent layouts once and never revisit them based off child layouts, but this would result in very poor document layouts in general.

  • The user is burdened with understanding and dealing with the fact that their document may be printed in an exponential number of ways, as opposed to a linear number of ways with a waterfalling printer.

  • A developer of a cascading printer has more cases to prove or test in verifying its correctness.

These issues only worsen with the introduction of a variable number of annotations, so Strictly Annotated will stick working with waterfalling printer.

Printing annotations

We will allow users to attach arbitrary annotations to Text termsWe could permit annotations attached to any term, but I do not believe this increases expressiveness and only complicates the discussion here.. Our library datatypes are now

ocaml
type annotation = Annot of string
type doc = ...
         | Text of string * annotation option
         | ...

There are two questions to answer in the design of annotation layout.

Annotation placement

Where should we place annotations when printing a document? We have already expressed the opinion that annotations are not semantic terms, and so they should be separated from the rest of a formatted document in some way.

The most natural choice here is place annotations at the end of the formatted line containing the term they are attached to. For example, attaching annotations to the $\tt if$, $\tt then$, and $\tt else$ terms in our running example may yield the printed document

if         // new conditional              if maybe x  // new conditional
  maybe x                                  then pos()  // true branch
then       // true branch          or      else neg()  // false branch
  pos()
else       // false branch
  neg()

as demonstrated above, we may align annotations as well - either with nearby annotations, or with all annotations in the document.

Dealing with multi-line annotations is straightforward. When printing a line, we split an annotation by newlines and then print multiple lines with appropriate alignment. For example, a multi-line annotation on the $\tt if$ term could yield the printed document

if         // new conditional
           // likely path: true branch
  maybe x
then       // true branch
  pos()
else       // false branch
  neg()

Annotations and layout decisions

Unfortunately, we cannot make all layout decisions independently of annotations. Consider if $\tt maybe$, $\tt pos()$, and $\tt neg()$ were also given annotations. In the most compact layout presented above, these annotations would be printed reasonably:

if         // new conditional
  maybe x  // -> bool
then       // true branch
  pos()    // -> T
else       // false branch
  neg()    // -> U

but how are we to print these annotations in three-line layout we saw earlier? One option is to push all annotations to the end of the printed line and treat them as a multi-line annotation:

if maybe x  // new conditional
            // -> bool
then pos()  // true branch
            // -> T
else neg()  // false branch
            // -> U

but the problem with this is we lose some information about the terms annotations are attached to, and indeed we may expect that the document be split across 6 lines as in the most compact layout to better preserve term-annotation relationships.

This leads us to the idea of distinguishing between compact and sparse groups.

$\Def$ A group is compact if it is has a horizontal layout and at least two annotations with a Break between them.

That is, a group is compact if we could have laid it out vertically to split up annotations but decided not to.

$\Def$ A group is sparse if it is not compact.

Our goal be to make all groups sparse so as to preserve a reasonable relationship between terms and annotations. When we end up with multiple annotations at the end of a line anyway (e.g. because there are no breaks between annotations), we will print annotations using the multi-line approach.

An Implementation

Now that we have a design in place, we are ready to complete an implementation. As we will see, the simple design lends to a very straightforward encoding.

Choosing a layout

Recall that we want to ensure two conditions when choosing a layout for a document's groups: waterfalling and sparseness. Our layout procedure traverse a document top-down, choosing a layout for groups as it encounters them. layout takes a list of triples (i, m, doc) consisting of the cumulative indentation, the layout mode of the current group, and the document itself. As part of the layout process, we lower a document to a simpler doc_ir form:

type doc_ir = IrDone
            | IrText    of string * annotation list * doc_ir
            | IrNewline of int * doc_ir

IrDone marks the end of a document. IrText denotes some text, with annotations attached to it, and the rest of the document. IrNewline denotes a newline with some indentation, and the rest of the document.

doc_ir is exactly Lindig's sdoc with a different name and support for annotations. The rest of layout is exactly Lindig's pretty, with an added call to sparse during the choosing of a group's layout.

ocaml
type mode = Horizontal | Vertical
let layout w =
  let rec go l = function
    | [] -> IrDone
    | (_, _, Nil)                 :: rest -> go l rest
    | (_, _, Text (s, a))         :: rest ->
         IrText (s, Option.to_list a, go (l + strlen s) rest)
    | (_, Horizontal, Break s)    :: rest -> IrText (s, [], go (l + strlen s) rest)
    | (i, Vertical, Break _)      :: rest -> IrNewline (i, go i rest)
    | (i, m, Cons (x, y))         :: rest -> go l ((i, m, x) :: (i, m, y) :: rest)
    | (i, m, Nest (j, x))         :: rest -> go l ((i + j, m, x) :: rest)
    | (i, _, Group x)             :: rest ->
        if sparse [ x ] && fits (w - l) [ (i, Horizontal, x) ] then
          go l ((i, Horizontal, x) :: rest)
        else go l ((i, Vertical, x) :: rest)
  in
  go

fits is exactly Lindig's fits (page 5); we will not regurgitate it here. sparse is defined as follows:

ocaml
let sparse d =
  let rec check annots seenbrk = function
    | [] -> true
    | Nil              :: rest -> check annots seenbrk rest
    | Cons (x, y)      :: rest -> check annots seenbrk (x :: y :: rest)
    | Nest (_, x)      :: rest -> check annots seenbrk (x :: rest)
    | Text (_, None)   :: rest -> check annots seenbrk rest
    | Text (_, Some _) :: _ when annots >= 1 && seenbrk -> false
    | Text (_, Some _) :: rest -> check (annots + 1) seenbrk rest
    | Break _          :: rest -> check annots true rest
    | Group x          :: rest -> check annots seenbrk (x :: rest)
  in
  check 0 false d

$\text{Proposition.}$ $\tt layout$ yields a waterfalled document.

$\text{Proof.}$ Straightforward by inspection of $\tt fits$ (Lindig, 5) and $\tt sparse$. $\tt fits\ g$ descends into subgroups of $\tt g$, so if $\tt fits\ sg = false$ for any subgroup $\tt sg$, it must be that $\tt fits\ g = false$. The argument for $\tt sparse$ is similar.

$\text{Proposition.}$ $\tt layout$ yields a sparse document.

$\text{Proof.}$ Straightforward by inspection of $\tt sparse$.

Linearizing a document

After determining a document's layout and lowering it to a doc_ir, we convert the document into a list of lines to print. Each line consists of its indentation, its text, and the annotation (if any) that should be printed at its end:

ocaml
type line = Line of int * string * annotation option

Linearizing a doc_ir is straightforward. The only interesting bit is the splitting of a line with multiple or multi-line annotations into multiple lines aligned with the first-line annotation.

ocaml
let linearize ir =
  let distribute_line (indent, text, annots) =
    match annots with
    | [] -> [ Line (indent, text, None) ]
    | a :: rest ->
        let textspaces = spaces (strlen text) in
        Line (indent, text, Some a)
        :: List.map (fun a -> Line (indent, textspaces, Some a)) rest
  in
  let rec linear lines curline = function
    | IrDone -> lines @ distribute_line curline
    | IrNewline (i, ir) ->
        linear (lines @ distribute_line curline) (i, "", []) ir
    | IrText (s1, annots1, ir) ->
        let i, s, annots = curline in
        linear lines (i, s ^ s1, annots @ annots1) ir
  in
  linear [] (0, "", []) ir

Aligning annotations and printing lines

Finally, we may want to align annotations locally among other nearby annotations, or globally among all annotations in the document.

After annotation alignment, we complete the formatting by simply printing the list of produced lines as a string.

Both annotation alignment and line printing are very straightforward; the interested reader can check out the implementation.

Is it efficient?

Let $\depth(d)$ be the total number of terms in a doc $d$. It is clear that ${\tt fits}$ and ${\tt sparse}$ explore each term in a document at most once, and hence ${\tt input}(d), {\tt sparse}(d) = \O(d)$. layout explores each term in a document at most once, but in the pathological case we end up calling $\tt fits$ and $\tt sparse$ for each term, so ${\tt layout}(d) = \O(\depth(d)^2)$.

Let us now denote $\s(d)$ to be the total number of string characters in a document $d$. In the pathological case every term in a document is lowered and every annotation needs to be put on a separate line, so ${\tt linearize}(ir_d) = \O(d + \s(d))$.

Alignment of annotations may require appending ${\s(d)}$ characters to every line in the pathological case, so ${\tt align}(lines_d) = \O(\s(d)^2)$. Done well, printing lines after alignment will be linear in the number of characters, so ${\tt print}({\tt align}(lines_d)) = \O(\s(d)^2)$.

Putting these passes all together yields a procedure $\texttt{pretty-print}(d) = \O(\depth(d)^2 + \s(d)^2)$. There need not be an ordering relation between $\depth(d)$ and $\s(d)$, but actual uses of this library suggest that in general $\depth(d) < \s(d) %>$.

I think this is reasonably efficient, as it seems impossible to choose the best layout for a document without considering each group at least once, and it is impossible to align annotations without introducing at most $\s(d)$ additional characters to each line.

There are simple ways to improve constants of proportionality in the implementation presented here - for example, $\tt fits$ and $\tt sparse$ could be combined into one procedure.

History of Lindig's Printer

Lindig wrote his 2000 note Strictly Pretty following Walder's 1999 paper A prettier printer. Walder designed a pretty-printing algebra, proving equational laws that led to an expressive and efficient implementation in the lazy language Haskell. Walder's algebra was inspired by Hughes's 1995 The Design of a Pretty-printing Library. Both Walder's and Hughes's libraries necessitated lazy execution - their implementations described all possible layouts and then evaluated a small amount to find "the best". Having to eagerly expand all layouts would be a non-starter. Lindig was aware of this, and in his note attempted to translate the essence of Walder's pretty-printing system for use in an eager evaluation.

« A Flying Tour of Kan Extensions door  ​ Type Inference for sound and Complete Flow Typing »
Analytics By visiting this site, you agree to its use of Cloudflare Analytics. No identifiable information is transmitted to Cloudflare. See Cloudflare Analytics user privacy.