Skip to content

Commit 177d713

Browse files
jackh726jackh726
authored
[WIP] Initial draft of engine book (#326)
* Initial draft of engine book * Columns * Mark code blocks as notrust * Typo * More typos * More links * Other review comments and add coinduction doc as subchapter * Don't run code blocks in coinduction.md
1 parent a7e1d9c commit 177d713

File tree

5 files changed

+576
-2
lines changed

5 files changed

+576
-2
lines changed

‎book/src/SUMMARY.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,4 +16,7 @@
1616
- [Lowering Rust IR to logic](./clauses.md)
1717
- [Unification and type equality](./clauses/type_equality.md)
1818
- [How does the engine work](./engine.md)
19+
- [Major concepts](./engine/major_concepts.md)
20+
- [Logic](./engine/logic.md)
21+
- [Coinduction](./engine/logic/coinduction.md)
1922
- [Glossary and terminology](./glossary.md)

‎book/src/engine.md

Lines changed: 22 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,23 @@
1-
# How does the engine work
1+
# Chalk engine
22

3-
*TBD:* Explain how chalk-engine
3+
The `chalk-engine` crate is the core PROLOG-like solver for logical
4+
predicates. Importantly, it is very general and not specific to Rust,
5+
Rust types, or Rust logic.
6+
7+
## Implemented PROLOG concepts
8+
9+
The engine implements the following PROLOG logic concepts. Some of these
10+
have been published on previously, and some are `Chalk`-specific. This isn't
11+
necesarily an exhaustive list:
12+
- Basic logic
13+
- Negation
14+
- Floundering
15+
- Coinductive solving
16+
17+
## Note
18+
19+
Throughout most of this chapter, the specifics in regards to
20+
`Canonicalization` and `UCanonicalization` are avoided. These are important
21+
concepts to understand, but don't particulary help to understand how
22+
`chalk-engine` *works*. In a few places, it may be highlighted if it *is*
23+
important.

‎book/src/engine/logic.md

Lines changed: 132 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,132 @@
1+
# Logic
2+
3+
## Overview
4+
5+
`chalk-engine` solves a `Goal` using a hybrid search strategy with elements of depth- and breadth-first search. When asked to solve a
6+
particular `Goal` it hasn't seen before, it will first ask the [`Context`] to
7+
generate a set of program clauses, that get turned into [`Strand`]s, that could
8+
solve that goal. Otherwise, if asked to solve a `Goal` it has seen before, it
9+
will select the existing table.
10+
11+
Once a table is selected, it will pick a `Strand` and a subgoal of that
12+
`Strand`, try to solve that `Goal`, repeating the process.
13+
14+
When an `Answer` is found for a `Goal`, it is merged into the parent `Strand`,
15+
or returned if it was the root `Goal`. It will then go on to pick the next
16+
subgoal of the `Strand` and continue on.
17+
18+
If at any point the solving stops being "successful" (i.e. we definitely found
19+
something to be unsolvable), the solving is restarted at the root `Goal`.
20+
21+
## The stack
22+
23+
In order to detect cycles (talked more about later), as well as keep track of
24+
the selected [`Strand`] for each table, `chalk-engine` stores a [`Stack`] on the
25+
`Forest`. Whenever a new goal is selected, a [`StackEntry`] is pushed onto the
26+
`Stack`, as well as the the "time" (which also gets incremented) that it was
27+
pushed. This "time" can be compared later to check if all the `Strands` of a
28+
[`Table`] have been checked in a single solve.
29+
30+
As either `Answer`s are found for the selected `Table`, entries on the stack are
31+
`pop`ed. If something is found to be unsolvable, the complete stack is unwound.
32+
33+
## Table creation
34+
35+
As mentioned before, whenever a new `Goal` is encounted, a new [`Table`] is
36+
created to store current and future answers. First, the [`Goal`] is converted into
37+
an [`HhGoal`]. If it can be simplified, then a `Strand` with one or more
38+
subgoals will be generated and can be followed as above. Otherwise, if it is a
39+
`DomainGoal` (see above), then
40+
[`program_clauses`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.ContextOps.html#tymethod.program_clauses)
41+
is called and each clause is converted into a `Strand` and can be followed.
42+
43+
## `root_answer` and `ensure_root_answer`
44+
45+
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,
46+
the idea of `Answer` versus `CompleteAnswer` have been ignored. However, in
47+
reality `Answer`s to `Goal`s may actually have delayed subgoals (see `ExClause`
48+
and [Coinduction and refinement strands]), whereas [`CompleteAnswer`]s may not.
49+
`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
50+
`Goal`'s [`Answer`] to a [`CompleteAnswer`].
51+
52+
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
53+
`Strand` and subgoal selection. The majority of the logic, however, is split out
54+
into separate functions that branch out from `ensure_root_answer`.
55+
56+
## Subgoal selection
57+
58+
Once a given `Strand` for a table has been selected, a subgoal has to be
59+
selected. If there are no subgoals left, then there is nothing to do. Otherwise,
60+
if there are subgoals left, then a subgoal will attempt to be selected (from
61+
[`next_subgoal_index`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#tymethod.next_subgoal_index)).
62+
If the table for that subgoal had previously floundered (see next section), then
63+
we mark that subgoal as floundered and try the next subgoal. If all subgoals are
64+
marked as floundered, then this entire `Strand` is marked as floundered. If a
65+
subgoal is successfully selected, there is nothing left to do.
66+
67+
## Floundering
68+
69+
There a couple cases where we "give up" - here called floundering - on trying to
70+
solve a goal. The most easy to understand case is if the types for a `Goal` or
71+
`Answer` are too large. (Side note, we *could* actually handle this - by
72+
generalizing - but turns out to be quite buggy and probably unnecessary).
73+
Another case where we flounder is if we try to solve a `Goal` where we try to
74+
**enumerate** non-enumerable types (like auto traits). In general, floundering
75+
just means that we *can't* know any more answers about a `Goal`, for some
76+
reason. However, if there are other `Strands` that don't flounder, there may
77+
still be other `Answer`s available.
78+
79+
## Answers
80+
81+
After an answer has been found for a subgoal, it must be *applied* to the parent
82+
`Strand`. Specifically, it must be able to unify with any existing `Answers`. If
83+
the `Answer`s are incompatible, the `Strand` is dropped since it can't lead
84+
anywhere.
85+
86+
## Cycles
87+
88+
If while pursuing a `Goal`, the engine encounters the same `Table` twice, then a
89+
cycle has occured. If the cycle is not coinductive (see next), then there is
90+
nothing that can be gained from taking this route. We mark how far up the stack
91+
is in the cycle, and try the next `Strand`. If all `Strand`s for a table
92+
encounter a cycle, then we know that the current selected `Goal` has no more
93+
answers.
94+
95+
## Coinduction and refinement strands
96+
[Coinduction and refinement strands]: #coinduction-and-refinement-strands
97+
98+
Coinduction basically means that two statements can rely on each other being
99+
true, unless either is proven false.
100+
101+
For example with the following program:
102+
```notrust
103+
#[coinductive]
104+
trait C1<T> { }
105+
forall<A, B> { A: C1<B> if B: C1<A> }
106+
```
107+
Then the goal `exists<T, U> { T: C1<U> }` holds for all `T` and `U`. If the `C1`
108+
trait was not coinductive, this would be a simple cycle.
109+
110+
To implement coinduction in the engine, delayed subgoals were introduced.
111+
Essentially, if a cycle is found, and the `Goal` is coinductive, then this is
112+
"delayed" until the stack unwinds back to the top `Goal` and all other
113+
non-coinductive cycles have been proven. Then, `Goal` has been proven itself. In
114+
some cases, it is the *root* `Goal` that has delayed coinductive subgoals (see
115+
above example). In this case, we create another "Refinement Strand" where the
116+
only subgoals are the delayed coinductive subgoals. If this new `Strand` can be
117+
proven, then any `Answer`s from that are valid answers for the root `Goal`.
118+
However, since there are currently delayed coinductive subgoals, there are no
119+
answers available yet.
120+
121+
For much more in-depth
122+
123+
124+
[`Strand`]: https://rust-lang.github.io/chalk/chalk_engine/strand/struct.Strand.html
125+
[`Context`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html
126+
[`HhGoal`]: https://rust-lang.github.io/chalk/chalk_engine/hh/enum.HhGoal.html
127+
[`Stack`]: https://rust-lang.github.io/chalk/chalk_engine/stack/struct.Stack.html
128+
[`StackEntry`]: https://rust-lang.github.io/chalk/chalk_engine/stack/struct.StackEntry.html
129+
[`Table`]: https://rust-lang.github.io/chalk/chalk_engine/table/struct.Table.html
130+
[`Goal`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#associatedtype.Goal
131+
[`Answer`]: https://rust-lang.github.io/chalk/chalk_engine/struct.Answer.html
132+
[`CompleteAnswer`]: https://rust-lang.github.io/chalk/chalk_engine/struct.CompleteAnswer.html

0 commit comments

Comments
 (0)