# `Tptp.Printer.Pretty`
[🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/printer/pretty.ex#L1)

Prints a CST to a chosen width, breaking lines where a formula is too long to fit.

    iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("fof(a,axiom,p&q).")
    iex> Tptp.Printer.Pretty.to_string(statement)
    "fof(a, axiom, p & q)."

    iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("fof(a,axiom,p&q).")
    iex> Tptp.Printer.Pretty.to_string(statement, width: 12)
    "fof(\n  a,\n  axiom,\n  p\n  & q\n)."

At a width of twelve columns:

    fof(
      a,
      axiom,
      p
      & q
    ).

## Contract

The token sequence is that of `Tptp.Printer.Canonical`: the same tokens, in the
same order, with the same spellings, differing only in the white space between
them. This is not preserved by construction but inherited: this module obtains
the token list from the canonical printer and determines only where line breaks
occur, so a change to the grammar cannot cause the two printers to diverge.

Line breaking uses `Inspect.Algebra`, the Wadler–Lindig algebra in the standard
library, which introduces no dependency and produces an optimal rather than
greedy layout: a group is flattened when its entire contents fit, so
`p(a, b, c)` does not break its first argument before establishing that the
third would not have fitted.

## Structure

The token stream of a statement has balanced `(`, `[` and `{`. `[.]`, `<.>`,
`{.}` and `(.)` are single tokens after lexing, as are quoted atoms and distinct
objects, and the grammar guarantees the remainder. Bracket matching over the flat
token list therefore recovers the nesting without a second traversal of the tree.

Each bracket region becomes one group with a two-space indent, and whether it
breaks is determined independently, so an argument that does not fit does not
separate its siblings. The internal `item` type represents this recovery: either
a token, or an opener with its contents and its closer. The closer is `nil` only
for unbalanced brackets, which the grammar makes unreachable and which are
handled rather than raising.

## Permitted break positions

  * **After a comma**, giving one element per line where a list breaks.
  * **Before a binary connective**, never after, so that a broken chain reads

        p(X)
        & q(X)
        & r(X)

    with the connective at the start of the line, which is the convention in
    TPTP output and which allows a long conjunction to be scanned for the
    operator that differs. `@` is included, so a long THF application spine
    breaks in the same way, as is `>`, for a long type signature.
  * **Immediately inside a bracket**, which permits a region to open.

No other position. In particular no break occurs inside a quoted atom or a
distinct object, each being a single token, and this module does not examine the
interior of a token.

## Safety of white space

Every position at which a break may occur may also carry a space, and every
position at which it may not still receives the spacing prescribed by
`Tptp.Printer.Spacing`. White space between two TPTP tokens can neither merge nor
divide them: the longest-match cases that could, such as `~` adjacent to `|`, are
those `Spacing` already separates.

# `option`

```elixir
@type option() :: {:width, pos_integer()}
```

How wide a line may be.

`:width` is the column the algebra tries to keep within; it is a target and not a
guarantee, because a single token longer than the width cannot be broken.

# `printable`

```elixir
@type printable() :: Tptp.Printer.Canonical.printable()
```

Anything this printer knows how to write, which is anything the canonical printer does.

# `to_file`

```elixir
@spec to_file(printable(), Path.t(), [option()]) :: :ok | {:error, File.posix()}
```

Write the pretty form to disk.

# `to_iodata`

```elixir
@spec to_iodata(printable(), [option()]) :: iodata()
```

Print to a width, as iodata.

    iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("cnf(c,axiom,p|~q).")
    iex> statement |> Tptp.Printer.Pretty.to_iodata() |> IO.iodata_to_binary()
    "cnf(c, axiom, p | ~q)."

# `to_string`

```elixir
@spec to_string(printable(), [option()]) :: binary()
```

Print to a width, as a binary.

    iex> {:ok, file, []} = Tptp.from_string("fof(a,axiom,p(X)&q).")
    iex> Tptp.Printer.Pretty.to_string(file)
    "fof(a, axiom, p(X) & q).\n"

---

*Consult [api-reference.md](api-reference.md) for complete listing*