# The stack

The first "layer" of the recursive solver is the `Stack`. It is really just what it sounds like: a stack that stores each thing that the recursive solver is solving. Initially, it contains only one item, the root goal that was given by the user.

Each frame on the stack has an associated `StackDepth`, which is basically an index that increases (so 0 is the top of the stack, 1 is the next thing pushed, etc).

## How the recursive solver works at the highest level

At the highest level, the recursive solver works like so.

• Push the initial goal `G0` onto the stack.
• Find all the program clauses `G1 :- G2...Gn` that could apply to the goal `G0`.
• For each program clause, unify `G1` and `G0`. If that succeeds, then recursively try to prove each goal `Gi` in the list `G2..Gn`:
• If proving `Gi` yields an error, return an error.
• If proving `Gi` yields an ambiguity, keep going, but remember that we got an ambiguous result.
• If proving `Gi` succeeded, apply the resulting answer to our inference variables and keep going.
• At the end, if any result proved ambiguous, return ambiguous, otherwise construct the final answer and return success.

## Example

``````
#![allow(unused)]
fn main() {
trait A { }
trait B { }

impl<T: B> A for Vec<T> { }

impl B for u32 { }
}
``````

Imagine we are trying to prove `Implemented(Vec<?X>: A)`. There is one unbound inference variable here, `?X`. We will ultimately get the result `Provable(?X = u32)`. But how do we find it?

• Initially we are solving `Implemented(Vec<?X>: A)`
• we find one applicable program clause, `forall<T> { Implemented(Vec<T>: A) :- Implemented(T: B) }`.
• after unification, the list of subgoals is `[Implemented(?X: B)]`.
• we recursively try to solve `Implemented(?X: B)`
• we find one applicable program clause, `Implemented(u32: B)`.
• after unification, `?X = u32`, but there are no more subgoals.
• we return the answer `Provable(?X = u32)`.
• we apply the substitution `?X = u32`, and find there are no more subgoals.
• we return the answer `Provable(?X = u32)`.

## Why do we need the stack?

You may have noticed that the description above never seemed to use the `Stack`, it only relied on the program stack. That's because I left out any discussion of cycles. In fact, the `Stack` data structure does mirror the program stack, it just adds some extra information we use in resolving cycles. We'll discuss cycles in the next chapter, when we discuss the search graph.

## Figuring out if something is on the stack

The stack itself never stores the goal associated with a particular entry. That information is found in the search graph, which will be covered in detail in the next section. For now it suffices to say that the search graph maps from "some goal that we are currently solving" to "information about that goal", and one of the bits of information is the `StackDepth` of its entry on the stack (if any).

Therefore, when we are about to start solving some (canonical) goal G, we can detect a cycle by checking in the search graph to see whether G has an associated `StackDepth`. If so, it must be on the stack already (and we can set the `cycle` field to true...but I get ahead of myself, read the next chapters to learn more about that).