# `mix tptp.census`
[🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/mix/tasks/tptp.census.ex#L1)

Read every problem and axiom file of a local TPTP library and count where it
applies a type constructor — `list($i)`, `map(A, B)`, `tree @ $i` — and in which
dialects.

    mix tptp.census
    mix tptp.census --check

TPTP's type grammar admits type application: `<tff_atomic_type> ::=
<type_functor>(<tff_type_arguments>)` and, in THF, an apply spine in type
position. Whether the library actually uses it, how widely and in which
dialects, is a fact worth having written down rather than guessed. The report is
committed and kept current the way `reports/CORPUS.md` is: counts, not conclusions.

## What is exact and what is a heuristic

A `<tff_atomic_type>` node is only ever built for an application, so the TFF
count is exact. THF does not separate a type from a term —
`<thf_unitary_type> ::= <thf_unitary_formula>` — so the THF figure is a
heuristic: an apply spine inside a `type`-role statement. It is reported on its
own line.

A file counts as outside the base languages when its dialect is none of `cnf`,
`fof`, `tf0` and `th0`, that is, when it requires polymorphism, arithmetic or a
higher-order feature. That count refines the TFF row and only
the TFF row: it is taken over the files an exact `<tff_atomic_type>` was found
in, so it says nothing about the heuristic's files.

The heuristic's files are instead broken down by dialect, which indicates whether
it is identifying types. An all-TH1 distribution indicates that it is; any TH0 in
the distribution indicates that it is matching something other than polymorphism.

## The constructor table is TFF only

`record_thf/3` sets a boolean and never populates `constructors`. The names,
arities and domains below therefore come from the exact TFF walk alone, and the
heuristic's files contribute none of them — `fun`, `list` and `option` are not a
census of the library's type constructors, they are a census of the ones TFF
spells in a form the grammar makes unambiguous.

## Arity 2 over a type variable

A constructor applied at arity 1, or at any arity over ground arguments, can be
monomorphised into a fresh sort by an elaborator: `list($i)` is a sort. A
constructor applied at arity ≥ 2 with a type variable among its arguments cannot
be — `fun(A, B)` has to enter type unification as a constructor. That is a fork
in the road for anything built on this library, so it is counted, twice: once for
a variable as a direct argument, once for a variable anywhere beneath one, since
`fun(list(A), $i)` is no more monomorphisable than `fun(A, B)` and the gap
between the two counts is how much nesting the library actually does.

## Reading the library

Each file is read with `Tptp.from_string/2` and nothing else, exactly as
`mix tptp.corpus` does; the same 20 MB size cap keeps the enormous axiom sets
out. Run it separately: it performs one pass over the whole library.

## Options

  * `--every N` — sweep one file in N. The full sweep is the default.
  * `--timeout MS` — per-file budget, default 60 s, as `mix tptp.corpus`.
  * `--max-bytes N` — skip files larger than this, default 20 MB.
  * `--concurrency N` — workers in the smallest size tier, default 4.
  * `--heap BYTES` — peak heap across all workers, default 6 GB. See
    `mix help tptp.corpus` for why the budget is heap rather than bytes of source.
  * `--out PATH` — where to write, default `reports/CENSUS.md`.
  * `--check` — write nothing; fail if the committed report's results differ
    from this run's.

# `t`

```elixir
@type t() :: %{
  scanned: non_neg_integer(),
  tff_applied: non_neg_integer(),
  applied_outside_base: non_neg_integer(),
  var_direct: non_neg_integer(),
  var_nested: non_neg_integer(),
  thf_applied_heuristic: non_neg_integer(),
  thf_dialects: %{optional(Tptp.Query.dialect()) =&gt; non_neg_integer()},
  type_forall: non_neg_integer(),
  constructors: %{
    optional(binary()) =&gt; %{
      arities: [non_neg_integer()],
      domains: [binary()],
      files: non_neg_integer(),
      var_direct: non_neg_integer(),
      var_nested: non_neg_integer()
    }
  }
}
```

What one sweep found.

  * `scanned` — files read, parse failures included.
  * `tff_applied` — files with at least one applied `<tff_atomic_type>`.
  * `applied_outside_base` — of the TFF applied files, those whose dialect is not
    a base language.
  * `var_direct` — of the TFF applied files, those applying a constructor at
    arity ≥ 2 with a type variable as a direct argument.
  * `var_nested` — the same, counting a type variable anywhere beneath an
    argument. `var_direct` is a subset of it.
  * `thf_applied_heuristic` — files with an apply spine in a THF type position.
  * `thf_dialects` — those files by dialect, indicating whether the heuristic is
    identifying types.
  * `type_forall` — files using `!>`.
  * `constructors` — each TFF type constructor seen, with the arities it was
    applied at, the domains it appeared in, how many files used it, and in how
    many of those it took a type variable at arity ≥ 2, directly and nested.

# `census`

```elixir
@spec census(
  [Path.t()],
  keyword()
) :: t()
```

Sweep a list of problem and axiom paths and total up the type application in
them.

Each path is read with `Tptp.from_string/2`; a file that does not parse still
counts toward `scanned` and contributes nothing else.

# `render`

```elixir
@spec render(t(), %{
  root: Path.t(),
  every: pos_integer(),
  elapsed: non_neg_integer(),
  tiers: [{pos_integer(), pos_integer(), [Path.t()]}]
}) :: binary()
```

Render the committed report from a set of totals and the run metadata.

---

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