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

Prints a concrete syntax tree to TPTP, deterministically and without comments.

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

## Contract

`from_string(print(tree))` yields a tree with the same shape as `tree`, where
shape is `Tptp.Node.shape/1`: kinds, texts and structure, with positions removed,
since printing relocates everything. The property is verified over the whole TPTP
library.

## Parenthesisation

The printer neither introduces nor removes parentheses. A formula language
without a precedence table would ordinarily require parenthesising every
subterm, but the tree already records where the parentheses occurred:
`<fof_unitary_formula> ::= (<fof_logic_formula>)` is retained as a node rather
than spliced away, so that `a | (b | c)` and `(a | b) | c` are distinct trees.
The round trip therefore follows from fidelity rather than from
over-parenthesisation.

## Spellings

`Tptp.Printer.Shapes` determines how each node kind is written and is generated
from the same BNF as the parser, in the same `mix tptp.gen` run. A hand-written
printer would agree with the grammar only until the grammar was regenerated.

## Empty collections

`[]` is a `general_list` with no children, and a `~` connective is a leaf with
neither children nor text. Both are childless, so the shape is consulted before
the leaf case; the reverse order prints every empty list as nothing, rendering
`inference(r, [], [a])` as `inference(r,, [a])`.

## Spacing

Sufficient for legibility and never sufficient to alter the token sequence. No
space precedes `)`, `]`, `}`, `,`, `.` or `:`; none follows `(`, `[` or `{`; and
none precedes an opening bracket following a word or a prefix operator, so `p(a)`
and `![X]:` are reproduced as written. A single space is emitted elsewhere, which
prevents two adjacent operators from combining into a third.

# `printable`

```elixir
@type printable() ::
  Tptp.Node.t() | Tptp.Statement.t() | Tptp.File.t() | Tptp.Unit.t()
```

Anything this printer knows how to write.

# `to_file`

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

Write a file's canonical form to disk.

# `to_iodata`

```elixir
@spec to_iodata(printable()) :: iodata()
```

Print as iodata, which is what to hand `IO.write/2` or `:file.write/2`.

Building iodata rather than a binary is the difference between one allocation per
fragment and one copy of the whole file per concatenation, and a 455 MB axiom set
makes that difference visible.

# `to_string`

```elixir
@spec to_string(printable()) :: binary()
```

Print as a binary.

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

# `tokens`

```elixir
@spec tokens(printable()) :: [binary()]
```

The token sequence a printable spells out, before any white space is chosen.

Public because `Tptp.Printer.Pretty` starts here: it decides only where the line
breaks go, so it must be spelling the same tokens as this module rather than a
parallel set that could drift from them.

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

---

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