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.
Summary
Types
Anything this printer knows how to write.
Functions
Write a file's canonical form to disk.
Print as iodata, which is what to hand IO.write/2 or :file.write/2.
Print as a binary.
The token sequence a printable spells out, before any white space is chosen.
Types
@type printable() :: Tptp.Node.t() | Tptp.Statement.t() | Tptp.File.t() | Tptp.Unit.t()
Anything this printer knows how to write.
Functions
@spec to_file(printable(), Path.t()) :: :ok | {:error, File.posix()}
Write a file's canonical form to disk.
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.
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)."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", ")", "."]