[WIP] Initial draft of engine book

book/src/SUMMARY.md

@@ -14,4 +14,7 @@
 - [Lowering Rust IR to logic](./clauses.md)
     - [Unification and type equality](./clauses/type_equality.md)
 - [How does the engine work](./engine.md)
+    - [Major concepts](./engine/major_concepts.md)
+    - [Logic](./engine/logic.md)
+        - [Coinduction](./engine/logic/coinduction.md)
 - [Glossary and terminology](./glossary.md)

book/src/engine.md

@@ -1,3 +1,23 @@
-# How does the engine work
+# Chalk engine
 
-*TBD:* Explain how chalk-engine 
+The `chalk-engine` crate is the core PROLOG-like solver for logical
+predicates. Importantly, it is very general and not specific to Rust,
+Rust types, or Rust logic.
+
+## Implemented PROLOG concepts
+
+The engine implements the following PROLOG logic concepts. Some of these
+have been published on previously, and some are `Chalk`-specific. This isn't
+necesarily an exhaustive list:
+- Basic logic
+- Negation
+- Floundering
+- Coinductive solving
+
+## Note
+
+Throughout most of this chapter, the specifics in regards to
+`Canonicalization` and `UCanonicalization` are avoided. These are important
+concepts to understand, but don't particulary help to understand how
+`chalk-engine` *works*. In a few places, it may be highlighted if it *is*
+important.

book/src/engine/logic.md

@@ -0,0 +1,132 @@
+# Logic
+
+## Overview
+
+`chalk-engine` solves a `Goal` using a hybrid search strategy with elements of depth- and breadth-first search. When asked to solve a
+particular `Goal` it hasn't seen before, it will first ask the [`Context`] to
+generate a set of program clauses, that get turned into [`Strand`]s, that could
+solve that goal. Otherwise, if asked to solve a `Goal` it has seen before, it
+will select the existing table.
+
+Once a table is selected, it will pick a `Strand` and a subgoal of that
+`Strand`, try to solve that `Goal`, repeating the process.
+
+When an `Answer` is found for a `Goal`, it is merged into the parent `Strand`,
+or returned if it was the root `Goal`. It will then go on to pick the next
+subgoal of the `Strand` and continue on.
+
+If at any point the solving stops being "successful" (i.e. we definitely found
+something to be unsolvable), the solving is restarted at the root `Goal`.
+
+## The stack
+
+In order to detect cycles (talked more about later), as well as keep track of
+the selected [`Strand`] for each table, `chalk-engine` stores a [`Stack`] on the
+`Forest`. Whenever a new goal is selected, a [`StackEntry`] is pushed onto the
+`Stack`, as well as the the "time" (which also gets incremented) that it was
+pushed. This "time" can be compared later to check if all the `Strands` of a
+[`Table`] have been checked in a single solve.
+
+As either `Answer`s are found for the selected `Table`, entries on the stack are
+`pop`ed. If something is found to be unsolvable, the complete stack is unwound.
+
+## Table creation
+
+As mentioned before, whenever a new `Goal` is encounted, a new [`Table`] is
+created to store current and future answers. First, the [`Goal`] is converted into
+an [`HhGoal`]. If it can be simplified, then a `Strand` with one or more
+subgoals will be generated and can be followed as above. Otherwise, if it is a
+`DomainGoal` (see above), then
+[`program_clauses`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.ContextOps.html#tymethod.program_clauses)
+is called and each clause is converted into a `Strand` and can be followed.
+
+## `root_answer` and `ensure_root_answer`
+
+The [`root_answer`](https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html#method.root_answer) function is the entry point to solve a `Goal`. Up until now,
+the idea of `Answer` versus `CompleteAnswer` have been ignored. However, in
+reality `Answer`s to `Goal`s may actually have delayed subgoals (see `ExClause`
+and [Coinduction and refinement strands]), whereas [`CompleteAnswer`]s may not.
+`root_answer` essentially just wraps [`ensure_root_answer`](https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html#method.ensure_root_answer) and converts the
+`Goal`'s [`Answer`] to a [`CompleteAnswer`].
+
+The [`ensure_root_answer`](https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html#method.ensure_root_answer) function contains the core skeleton of the logic around
+`Strand` and subgoal selection. The majority of the logic, however, is split out
+into separate functions that branch out from `ensure_root_answer`.
+
+## Subgoal selection
+
+Once a given `Strand` for a table has been selected, a subgoal has to be
+selected. If there are no subgoals left, then there is nothing to do. Otherwise,
+if there are subgoals left, then a subgoal will attempt to be selected (from
+[`next_subgoal_index`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#tymethod.next_subgoal_index)).
+If the table for that subgoal had previously floundered (see next section), then
+we mark that subgoal as floundered and try the next subgoal. If all subgoals are
+marked as floundered, then this entire `Strand` is marked as floundered. If a
+subgoal is successfully selected, there is nothing left to do.
+
+## Floundering
+
+There a couple cases where we "give up" - here called floundering - on trying to
+solve a goal. The most easy to understand case is if the types for a `Goal` or
+`Answer` are too large. (Side note, we *could* actually handle this - by
+generalizing - but turns out to be quite buggy and probably unnecessary).
+Another case where we flounder is if we try to solve a `Goal` where we try to
+**enumerate** non-enumerable types (like auto traits). In general, floundering
+just means that we *can't* know any more answers about a `Goal`, for some
+reason. However, if there are other `Strands` that don't flounder, there may
+still be other `Answer`s available.
+
+## Answers
+
+After an answer has been found for a subgoal, it must be *applied* to the parent
+`Strand`. Specifically, it must be able to unify with any existing `Answers`. If
+the `Answer`s are incompatible, the `Strand` is dropped since it can't lead
+anywhere.
+
+## Cycles
+
+If while pursuing a `Goal`, the engine encounters the same `Table` twice, then a
+cycle has occured. If the cycle is not coinductive (see next), then there is
+nothing that can be gained from taking this route. We mark how far up the stack
+is in the cycle, and try the next `Strand`. If all `Strand`s for a table
+encounter a cycle, then we know that the current selected `Goal` has no more
+answers.
+
+## Coinduction and refinement strands
+[Coinduction and refinement strands]: #coinduction-and-refinement-strands
+
+Coinduction basically means that two statements can rely on each other being
+true, unless either is proven false.
+
+For example with the following program:
+```notrust
+#[coinductive]
+trait C1<T> { }
+forall<A, B> { A: C1<B> if B: C1<A> }
+```
+Then the goal `exists<T, U> { T: C1<U> }` holds for all `T` and `U`. If the `C1`
+trait was not coinductive, this would be a simple cycle.
+
+To implement coinduction in the engine, delayed subgoals were introduced.
+Essentially, if a cycle is found, and the `Goal` is coinductive, then this is
+"delayed" until the stack unwinds back to the top `Goal` and all other
+non-coinductive cycles have been proven. Then, `Goal` has been proven itself. In
+some cases, it is the *root* `Goal` that has delayed coinductive subgoals (see
+above example). In this case, we create another "Refinement Strand" where the
+only subgoals are the delayed coinductive subgoals. If this new `Strand` can be
+proven, then any `Answer`s from that are valid answers for the root `Goal`.
+However, since there are currently delayed coinductive subgoals, there are no
+answers available yet.
+
+For much more in-depth 
+
+
+[`Strand`]: https://rust-lang.github.io/chalk/chalk_engine/strand/struct.Strand.html
+[`Context`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html
+[`HhGoal`]: https://rust-lang.github.io/chalk/chalk_engine/hh/enum.HhGoal.html
+[`Stack`]: https://rust-lang.github.io/chalk/chalk_engine/stack/struct.Stack.html
+[`StackEntry`]: https://rust-lang.github.io/chalk/chalk_engine/stack/struct.StackEntry.html
+[`Table`]: https://rust-lang.github.io/chalk/chalk_engine/table/struct.Table.html
+[`Goal`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#associatedtype.Goal
+[`Answer`]: https://rust-lang.github.io/chalk/chalk_engine/struct.Answer.html
+[`CompleteAnswer`]: https://rust-lang.github.io/chalk/chalk_engine/struct.CompleteAnswer.html