tablesolve

Reusable proof-forest mechanics for tabled type-class resolution.

The crate implements the generator/consumer/tabling algorithm from Selsam, Ullrich, and de Moura, "Tabled Typeclass Resolution". It deliberately does not impose a type representation, unifier, instance database, evidence term, coherence policy, or diagnostics framework.

Examples

Run the two standalone adapters with:

cargo run --example horn
cargo run --example typeclass

horn is a minimal ground Horn-clause adapter. It shows shared subgoals, a seeded cycle, a seedless cycle, duplicate suppression, and the saturated answerless graph.

typeclass is closer to a compiler integration. It implements a small cloneable unifier and demonstrates generic instances, canonical variables, caller rebasing, shared polymorphic subgoals, and evidence construction. The example is dependency-free, but a production adapter may store an ena table, a persistent unifier, or an existing compiler inference state in its opaque State type.

Always inspect completion before classifying the answers. Prefer Report::answers_complete() when completeness matters and Report::proves_no_answer() when reporting failure. An empty partial answer set does not prove that resolution failed.

Abstraction boundary

ResolutionContext is the language adapter. It supplies these hooks:

1. canonicalize a caller-local goal into a hashable table key;
2. enumerate applicable clauses in language-defined order;
3. match a clause and either reject, answer, suspend, or request an incomplete stop;
4. resume suspended state with a tabled subgoal answer;
5. map root answers back to caller coordinates;
6. derive a hashable answer identity for duplicate elimination; and
7. cooperatively poll language-specific bounds or cancellation.

The library owns the reusable nonlinear part: one generator per canonical subgoal, suspended consumers, replay of old answers to late consumers, propagation of new answers, duplicate suppression, scheduling, resource bounds, statistics, and the answerless dependency graph.

This boundary is intentionally above unification. Adapters retain their own inference environments and canonicalization rules; forcing them into one universal term model would couple the library to a particular language and erase useful invariants.

A suspended goal must include every substitution and unification accumulated by its branch and must use the caller coordinates captured by its State. Rebase must map the canonical subgoal's answers back into exactly those coordinates. Returning a stale pre-unification goal can make table sharing or candidate indexing unsound; the engine cannot check this adapter invariant.

Controlled stops

Callbacks report a bound at the point where it is discovered:

• CanonicalizeOutcome::Stop retains the canonical key and caller mapping, so even a root canonicalization stop produces a normal partial Report;
• CallbackOutcome::Stop stops clause enumeration before a table is created; and
• Transition::Stop stops from clause application or consumer resumption.

ResolutionContext::check_stop has a narrower purpose: polling externally changing state, such as IDE cancellation, at work-item boundaries. The first observed stop wins, and all non-saturated completions leave the report intentionally incomplete.

Diagnostics

The engine does not format user-facing errors. Report instead exposes:

• an explicit completion reason (saturated, requested answer cutoff, step, table, or pending-work limit, or an adapter-defined stop);
• stable counters;
• root answers; and
• optional answerless diagnostics (answerless).

The default solve and solve_with_observer entry points collect a dependency graph. Use report options to skip that post-processing when it is unnecessary:

use tablesolve::{AnswerlessMode, ReportOptions};

let options = ReportOptions::default().with_answerless(AnswerlessMode::Omit);

Pass options to solve_with_options or solve_with_observer_and_options. AnswerlessReport::Omitted is deliberately different from a collected but empty DependencyGraph. Omitting the graph does not change exploration, answers, completion, statistics, or observer events. Each deduplicated dependency edge includes consumer_count; this is an aggregate count, not continuation lineage. The graph is a proven failure graph only when Report::proves_no_answer() is true. Otherwise it is a partial snapshot that may include failed alternatives beside successful proofs.

For richer explanations, solve_with_observer emits zero-copy structural events containing the adapter's own keys, clauses, states, rebasing mappings, and answers. TableId, ConsumerId, and AnswerId are opaque correlation tokens scoped to one solve; they are not persistent identities or stable across schedulers. Suspension events identify their parent and subgoal tables and, for continuations, the exact consumer-answer pair that produced the next branch. Resume attempts and rejections carry that same pair. Event references are valid only during the observer callback, so an observer that needs a durable trace must retain its own diagnostic data. Report does not retain State or Rebase values.

This lets an adapter keep source spans and instance origins in its own types without coupling the engine to a diagnostics framework.

Scheduling and termination

Scheduling::DepthFirst follows the paper's two-stack control policy. Scheduling::Fair provides the single FIFO worklist used by some compiler implementations. They reach the same saturated set only for a positive, monotone, finite adapter satisfying the documented correctness contract; answer order differs, and a root-answer cutoff makes the returned subset scheduler- dependent. Tabling terminates under the paper's bounded term-size assumption plus finite continuation/answer-key conditions. The default configuration also applies generous step, table, and pending-work limits as guards against growing programs and fan-out. Use Config::unbounded() only when the surrounding language enforces equivalent bounds.