# `Tptp.Query`
[🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/query.ex#L1)

Properties of a file or unit, determined before further processing.

The principal one is the dialect, which determines where a problem may be sent.
Deriving it from the statement keywords alone is inadequate in both directions: a
`thf` file using only first-order syntax remains THF to a prover, and a `tff`
file using `!>` requires a TF1 rather than a TF0 implementation. The keyword is
least informative in the higher-order family, where `thf` covers TH0, TH1, DH0,
DH1 and NHF alike.

## Derivation

The dialect is derived from the features accumulated by the lint traversal — from
the constructs a file uses rather than from its statement keywords — and requires
no traversal of its own.

It is validated against the TPTP's own classification rather than asserted. Over
the 26,021 problems of TPTP v9.3.1 that carry an `SPC` header and fall within the
sweep's size limit, it agrees with that header except where the evidence lies in
an unread file. `dialect/1` observes a single `Tptp.File`, so a problem whose type
constructors are supplied by an included axiom set is classified by what is
present: 220 `TH1` problems are reported as `:th0` until the same call is made on
a `Tptp.Unit`, which reports `:th1` for each of them.

# `dialect`

```elixir
@type dialect() ::
  :unknown
  | :cnf
  | :fof
  | :tcf
  | :tf0
  | :tf1
  | :tx0
  | :tx1
  | :th0
  | :th1
  | :dh0
  | :dh1
  | :nxf
  | :nhf
```

The TPTP dialects, in `rank/1` order.

`:unknown` is returned for an empty file, which provides no evidence of a
dialect.

# `conjectures`

```elixir
@spec conjectures(Tptp.File.t() | Tptp.Unit.t()) :: [Tptp.Statement.Annotated.t()]
```

Returns the conjecture statements.

    iex> {:ok, file, []} = Tptp.from_string("fof(a,axiom,p). fof(g,conjecture,q).")
    iex> file |> Tptp.Query.conjectures() |> Enum.map(& &1.name.text)
    ["g"]

# `dialect`

```elixir
@spec dialect(Tptp.File.t() | Tptp.Unit.t()) :: dialect()
```

Returns the narrowest dialect admitting every construct in the file.

    iex> {:ok, file, []} = Tptp.from_string("cnf(a, axiom, p | ~q).")
    iex> Tptp.Query.dialect(file)
    :cnf

    iex> {:ok, file, []} = Tptp.from_string("tff(a, type, f: $i > $o). tff(b, axiom, f(a)).")
    iex> Tptp.Query.dialect(file)
    :tf0

    iex> {:ok, file, []} = Tptp.from_string("thf(a, axiom, !! @ p).")
    iex> Tptp.Query.dialect(file)
    :th1

A `!>` that binds a *term* is a dependent type rather than a polymorphic one, which
is DH0 or DH1 and not TH1:

    iex> source = "thf(n, type, nat: $tType). thf(f, type, fin: nat > $tType)."
    iex> {:ok, file, []} = Tptp.from_string(source)
    iex> Tptp.Query.dialect(file)
    :dh0

# `dialects`

```elixir
@spec dialects() :: [dialect()]
```

Returns the dialects in `rank/1` order.

    iex> Tptp.Query.dialects() |> Enum.take(3)
    [:unknown, :cnf, :fof]

# `features`

```elixir
@spec features(Tptp.File.t() | Tptp.Unit.t()) :: [atom()]
```

Returns the features the file uses, as recorded by the lint traversal.

A type quantifier produces either `:polymorphic` or `:dependent` according to
what it binds rather than to the quantifier itself; see `Tptp.Lint.Collect`.

Use this where the dialect alone is insufficiently specific. A consumer selecting
a prover may need to know that a TF0 problem uses arithmetic, which does not
affect its dialect.

    iex> {:ok, file, []} = Tptp.from_string("thf(a, type, g: !>[A: $tType]: (A > A)).")
    iex> file |> Tptp.Query.features() |> Enum.sort()
    [:polymorphic, :thf, :typed]

# `from_features`

```elixir
@spec from_features(Enumerable.t()) :: dialect()
```

Returns the dialect implied by a set of features.

Separated from `dialect/1` so that the mapping can be read and tested
independently.

    iex> Tptp.Query.from_features([:fof])
    :fof
    iex> Tptp.Query.from_features([:tff, :typed, :polymorphic])
    :tf1

# `rank`

```elixir
@spec rank(dialect()) :: non_neg_integer()
```

Returns a dialect's position in a stable listing order, approximately narrowest
to widest.

Intended for ordering a table of dialects. Unlike `within?/2` it is total, and it
asserts nothing about containment: `rank(:tcf) < rank(:tf1)` determines their
order in a report only.

    iex> Tptp.Query.rank(:cnf) < Tptp.Query.rank(:th1)
    true

# `roles`

```elixir
@spec roles(Tptp.File.t() | Tptp.Unit.t()) :: %{required(binary()) =&gt; pos_integer()}
```

Returns the roles the file uses, with the number of statements carrying each.

    iex> {:ok, file, []} = Tptp.from_string("fof(a,axiom,p). fof(b,axiom,q). fof(c,conjecture,r).")
    iex> Tptp.Query.roles(file)
    %{"axiom" => 2, "conjecture" => 1}

# `symbols`

```elixir
@spec symbols(Tptp.File.t() | Tptp.Unit.t()) :: %{
  required(binary()) =&gt; Tptp.Lint.Table.symbol()
}
```

Returns the symbol table without applying any rule.

The table constructed by `Tptp.Lint`, for consumers requiring the declarations and
observed arities without the diagnostics.

Keyed by `Tptp.Node.value/1`, the atomic word, rather than by the spelling, so
that `'p'` and `p` are the single symbol the BNF defines them to be. A signature
derived from this table inherits that identity; keying on the spelling instead
yields two constants that never unify.

    iex> {:ok, file, []} = Tptp.from_string("tff(t, type, 'p': $i > $o). tff(a, axiom, p(x)).")
    iex> file |> Tptp.Query.symbols() |> Map.keys() |> Enum.sort()
    ["p", "x"]

# `within?`

```elixir
@spec within?(dialect(), dialect()) :: boolean()
```

Returns whether every file of one dialect is also a file of another.

A partial order. The TPTP dialects are not linearly ordered: TCF is typed clause
form, and TXF and the non-classical languages are separate branches, so there
exist incomparable pairs. A TH1 file is not an NXF file and an NXF file is not a
TH1 file.

    iex> Tptp.Query.within?(:fof, :th0)
    true
    iex> Tptp.Query.within?(:th1, :fof)
    false

    iex> {Tptp.Query.within?(:th1, :nxf), Tptp.Query.within?(:nxf, :th1)}
    {false, false}

## Provenance

The vendored BNF does not state this relation. Each language has its own
nonterminals and the grammar makes no claim about containment, so the relation is
a hand-written table: `@extends` records immediate edges only and is closed
transitively at compile time.

It is therefore a judgement of the same kind as the SZS `isa` hierarchy, which
`Tptp.Szs.Ontology` declines to model. The distinction is the use to which the
answer is put. An SZS precedence would constitute a claim about the meaning of a
prover's result. This relation determines only which analyzers
`Tptp.Analyzer.run_all/3` offers a file to, where an error causes an analyzer to
run that should have been skipped. An analyzer requiring no such inference can
decline it; see `t:Tptp.Analyzer.gate/0` and its `{:exactly, dialects}` form.

It is not a basis for deciding whether a given prover accepts a file.

Being partial, it is not a comparator. Use `rank/1` for ordering.

---

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