# 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 `GoalData`

s. `GoalData`

s 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 `DomainGoal`

s
into `GoalData`

s.

There are three types of completely opaque `GoalData`

s 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 `Goal`

s 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 `Answer`

s. 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 `Strand`

s that may result in more
answers.

A `Forest`

holds all the `Table`

s that program generates, and is what most of
the logic is implemented on. It also stores the current state of solving (the
stack).