The two forms a parsed TPTP statement takes.
<TPTP_input> ::= <annotated_formula> | <include>, so there are exactly two.
They are separate structs rather than one struct with a discriminator, since they
share no fields and a consumer requires one or the other.
Tptp.Statement.Annotated is the thf, tff, tcf, fof, cnf and tpi
form. Tptp.Statement.Include is the include directive, which makes a set of
files a graph rather than a list.
Summary
Functions
A copy whose every leaf owns its bytes, so the file it came from can be collected.
Every CST subtree the statement holds, in source order.
The statement's extent, as a span in the file it was read from.
The bytes the statement covers, terminating . included.
Types
@type t() :: Tptp.Statement.Annotated.t() | Tptp.Statement.Include.t()
Either kind of top-level input the grammar admits.
Functions
A copy whose every leaf owns its bytes, so the file it came from can be collected.
See Tptp.Node.detach/1 for why this is not the default.
@spec roots(t()) :: [Tptp.Node.t()]
Every CST subtree the statement holds, in source order.
A statement is a handful of named slots rather than one tree, because its shape is fixed by the grammar and naming the slots is more useful than making a caller index into children. This is the escape hatch for the operations that genuinely want all of them — walking for symbols, checking span invariants, detaching.
iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("fof(a,axiom,p).")
iex> statement |> Tptp.Statement.roots() |> Enum.map(& &1.kind)
[:name, :formula_role, :constant]@spec span(t(), Tptp.Span.file_id()) :: Tptp.Span.t()
The statement's extent, as a span in the file it was read from.
The bytes the statement covers, terminating . included.