# 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.

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).