Major concepts

This section goes over a few different concepts that are crucial to understanding how chalk-engine works, without going over the exact solving logic.

Goals

A "goal" in Chalk can be thought of as "something we want to prove". The engine itself understands GoalDatas. GoalDatas consist of the most basic logic, such as introducing Binders (Forall or Exists) or combining goals (All). On the other hand, DomainGoal represents an opaque goal generated externally. As such, it may contain any extra information or may be interned. When solving a logic predicate, Chalk will lazily convert DomainGoals into GoalDatas.

There are three types of completely opaque GoalDatas that Chalk can solve: Unify, DomainGoal, and CannotProve. Unlike the other types of goals, these three cannot be simplified any further. Unify is the goal of unifying any two types. DomainGoal is any goal that can solve by applying a ProgramClause. To solve this, more Goals may generated. Finally, CannotProve is a special goal that cannot be proven true or false.

Answers and Solutions

For every Goal, there are zero or more Answers. Each Answer contains values for the inference variables in the goal.

For example, given the following program:

trait Clone {}
struct A {}
struct B {}
impl Clone for A {}
impl Clone for B {}

With the following goal: exists<T> { T: Clone } The following solutions would be given:

T = A
T = B

In other words, either A or B can substituted for T and the goal will hold true. Moreover, either answer could be used when further solving other goals that depend on this goal.

However, oftentimes, this is not what external crates want when solving for a goal. Instead, the may want a unique solution to this goal. Indeed, when we solve for a given root Goal, we return a single Solution. The AntiUnifier struct from chalk-solve then finds that solution, by finding a minimal generalization of answers which don't unify. (For the example above, it would return only Ambiguous, since A and B can't unify.)

ExClauses and Strands

An ExClause is described in literature as A :- D | G or A holds given that G holds with D delayed goals. In chalk-engine, an ExClause stores the current state of proving a goal, including existing substitutions already found, subgoals yet to be proven, or delayed subgoals. A Strand wraps both an ExClause and an InferenceTable together.

Tables and Forests

A Strand represents a single direction to find an Answer - for example, an implementation of a trait with a set of where clauses. However, in a program, there may be multiple possible implementations that match a goal - e.g. multiple impls with different where clauses. Every Table has a goal, and stores existing Answers, as well as all Strands that may result in more answers.

A Forest holds all the Tables that program generates, and is what most of the logic is implemented on. It also stores the current state of solving (the stack).