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.
Summary
Types
How wide a line may be.
Anything this printer knows how to write, which is anything the canonical printer does.
Functions
Write the pretty form to disk.
Print to a width, as iodata.
Print to a width, as a binary.
Types
@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.
@type printable() :: Tptp.Printer.Canonical.printable()
Anything this printer knows how to write, which is anything the canonical printer does.
Functions
@spec to_file(printable(), Path.t(), [option()]) :: :ok | {:error, File.posix()}
Write the pretty form to disk.
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)."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"