A named producer of diagnostics over a Tptp.Analysis.
Tptp.Lint is one implementation. A prover-backend probe, a project naming
convention or a style pass would be others: an analyzer declares the dialects it
applies to and returns diagnostics for an analysis. run_all/3 dispatches one
analysis to the applicable analyzers and returns their findings grouped by
identifier.
Input
An analyzer receives a Tptp.Analysis rather than a Tptp.File so that the
symbol table, the dialect and the source are already available. Reconstructing
the table would require a second traversal.
Dialect gating
dialects/0 returns one of three forms:
:any— applies to every file.- a list, such as
[:th0]— applies where the file's dialect is within one of them byTptp.Query.within?/2.[:th0]therefore admits a FOF file, since FOF is within TH0, and[:tf0]does not admit TF1. {:exactly, [:tf0]}— applies to exactly these dialects, with no containment reasoning.
A gated-out analyzer is reported as {id, :skipped}, which is distinct from
{id, []}, so that a caller can separate "did not apply" from "applied and found
nothing".
Both list forms exist because within?/2 is a judgement rather than a statement
of the BNF. An analyzer depending on the exact statement keywords — one invoking
a TF0-only implementation, for instance — should use {:exactly, ...}.
Failure containment
run_all/3 catches an analyzer that raises, exits or throws, and converts it
into a single TPTP0800 diagnostic naming the analyzer, so that a third-party
analyzer cannot terminate the run.
Summary
Types
How an analyzer says which files it wants.
One analyzer's result: its diagnostics, or :skipped when its dialects excluded the file.
Callbacks
This analyzer's diagnostics for one analysis.
The files this analyzer wants. See gate/0 and the module documentation.
A stable atom identifying this analyzer; the key its findings are grouped under.
A short human name, for a list of available analyzers.
Functions
Run each analyzer that fits the analysis's dialect and return {id, outcome}
pairs, in the order given.
Types
@type gate() :: :any | [Tptp.Query.dialect()] | {:exactly, [Tptp.Query.dialect()]}
How an analyzer says which files it wants.
:any takes everything; a bare list takes anything within one of the named
dialects by Tptp.Query.within?/2; {:exactly, dialects} takes those dialects and
nothing else.
@type outcome() :: [Tptp.Diagnostic.t()] | :skipped
One analyzer's result: its diagnostics, or :skipped when its dialects excluded the file.
Callbacks
@callback analyze( Tptp.Analysis.t(), keyword() ) :: [Tptp.Diagnostic.t()]
This analyzer's diagnostics for one analysis.
options are whatever run_all/3 was passed under this analyzer's id/0.
@callback dialects() :: gate()
The files this analyzer wants. See gate/0 and the module documentation.
@callback id() :: atom()
A stable atom identifying this analyzer; the key its findings are grouped under.
@callback label() :: String.t()
A short human name, for a list of available analyzers.
Functions
@spec run_all(Tptp.Analysis.t(), [module()], keyword()) :: [{atom(), outcome()}]
Run each analyzer that fits the analysis's dialect and return {id, outcome}
pairs, in the order given.
A gated-out analyzer yields {id, :skipped} rather than being dropped. An
analyzer that raises, exits or throws is caught and turned into one TPTP0800
diagnostic naming it.
Per-analyzer options are read from options under each analyzer's id/0:
Tptp.Analyzer.run_all(analysis, [Tptp.Lint], tptp_lint: [only: [Tptp.Lint.Rules.Role]])