Skip to content

Commit 9fe13e7

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #223 from tmandry/improve-chalk-overview
Update chalk overview
2 parents 9805434 + cf2682a commit 9fe13e7

File tree

1 file changed

+169
-60
lines changed

1 file changed

+169
-60
lines changed

‎src/traits/chalk-overview.md

+169-60
Original file line numberDiff line numberDiff line change
@@ -16,23 +16,45 @@ existing, somewhat ad-hoc implementation into something far more principled and
1616
expressive, which should behave better in corner cases, and be much easier to
1717
extend.
1818

19-
## Resources
19+
## Chalk Structure
2020

21-
* [Chalk Source Code](https://github.com/rust-lang-nursery/chalk)
22-
* [Chalk Glossary](https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md)
23-
* The traits section of the rustc guide (you are here)
21+
Chalk has two main "products". The first of these is the
22+
[`chalk_engine`][chalk_engine] crate, which defines the core [SLG
23+
solver][slg]. This is the part rustc uses.
2424

25-
### Blog Posts
25+
The rest of chalk can be considered an elaborate testing harness. Chalk is
26+
capable of parsing Rust-like "programs", lowering them to logic, and
27+
performing queries on them.
2628

27-
* [Lowering Rust traits to logic](http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/)
28-
* [Unification in Chalk, part 1](http://smallcultfollowing.com/babysteps/blog/2017/03/25/unification-in-chalk-part-1/)
29-
* [Unification in Chalk, part 2](http://smallcultfollowing.com/babysteps/blog/2017/04/23/unification-in-chalk-part-2/)
30-
* [Negative reasoning in Chalk](http://aturon.github.io/blog/2017/04/24/negative-chalk/)
31-
* [Query structure in chalk](http://smallcultfollowing.com/babysteps/blog/2017/05/25/query-structure-in-chalk/)
32-
* [Cyclic queries in chalk](http://smallcultfollowing.com/babysteps/blog/2017/09/12/tabling-handling-cyclic-queries-in-chalk/)
33-
* [An on-demand SLG solver for chalk](http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/)
29+
Here's a sample session in the chalk repl, chalki. After feeding it our
30+
program, we perform some queries on it.
31+
32+
```rust,ignore
33+
?- program
34+
Enter a program; press Ctrl-D when finished
35+
| struct Foo { }
36+
| struct Bar { }
37+
| struct Vec<T> { }
38+
| trait Clone { }
39+
| impl<T> Clone for Vec<T> where T: Clone { }
40+
| impl Clone for Foo { }
41+
42+
?- Vec<Foo>: Clone
43+
Unique; substitution [], lifetime constraints []
44+
45+
?- Vec<Bar>: Clone
46+
No possible solution.
47+
48+
?- exists<T> { Vec<T>: Clone }
49+
Ambiguous; no inference guidance
50+
```
51+
52+
You can see more examples of programs and queries in the [unit
53+
tests][chalk-test-example].
3454

35-
## Parsing
55+
Next we'll go through each stage required to produce the output above.
56+
57+
### Parsing ([chalk_parse])
3658

3759
Chalk is designed to be incorporated with the Rust compiler, so the syntax and
3860
concepts it deals with heavily borrow from Rust. It is convenient for the sake
@@ -48,11 +70,23 @@ impls, and struct definitions. Parsing is often the first "phase" of
4870
transformation that a program goes through in order to become a format that
4971
chalk can understand.
5072

51-
## Lowering
73+
### Rust Intermediate Representation ([rust_ir])
74+
75+
After getting the AST we convert it to a more convenient intermediate
76+
representation called [`rust_ir`][rust_ir]. This is sort of analogous to the
77+
[HIR] in Rust. The process of converting to IR is called *lowering*.
5278

53-
After parsing, there is a "lowering" phase. This aims to convert traits/impls
54-
into "program clauses". A [`ProgramClause` (source code)][programclause] is
55-
essentially one of the following:
79+
The [`rust_ir::Program`][rust_ir-program] struct contains some "rust things"
80+
but indexed and accessible in a different way. For example, if you have a
81+
type like `Foo<Bar>`, we would represent `Foo` as a string in the AST but in
82+
`rust_ir::Program`, we use numeric indices (`ItemId`).
83+
84+
The [IR source code][ir-code] contains the complete definition.
85+
86+
### Chalk Intermediate Representation ([chalk_ir])
87+
88+
Once we have Rust IR it is time to convert it to "program clauses". A
89+
[`ProgramClause`] is essentially one of the following:
5690

5791
* A [clause] of the form `consequence :- conditions` where `:-` is read as
5892
"if" and `conditions = cond1 && cond2 && ...`
@@ -70,8 +104,8 @@ essentially one of the following:
70104

71105
*See also: [Goals and Clauses][goals-and-clauses]*
72106

73-
Lowering is the phase where we encode the rules of the trait system into logic.
74-
For example, if we have the following Rust:
107+
This is where we encode the rules of the trait system into logic. For
108+
example, if we have the following Rust:
75109

76110
```rust,ignore
77111
impl<T: Clone> Clone for Vec<T> {}
@@ -86,63 +120,138 @@ forall<T> { (Vec<T>: Clone) :- (T: Clone) }
86120
This rule dictates that `Vec<T>: Clone` is only satisfied if `T: Clone` is also
87121
satisfied (i.e. "provable").
88122

89-
### Well-formedness checks
123+
Similar to [`rust_ir::Program`][rust_ir-program] which has "rust-like
124+
things", chalk_ir defines [`ProgramEnvironment`] which which is "pure logic".
125+
The main field in that struct is `program_clauses`, which contains the
126+
[`ProgramClause`]s generated by the rules module.
127+
128+
#### Rules
129+
130+
The `rules` module ([source code][rules-src]) defines the logic rules we use
131+
for each item in the Rust IR. It works by iterating over every trait, impl,
132+
etc. and emitting the rules that come from each one.
133+
134+
*See also: [Lowering Rules][lowering-rules]*
135+
136+
#### Well-formedness checks
137+
138+
As part of lowering to logic, we also do some "well formedness" checks. See
139+
the [`rules::wf` source code][rules-wf-src] for where those are done.
90140

91-
As part of lowering from the AST to the internal IR, we also do some "well
92-
formedness" checks. See the [source code][well-formedness-checks] for where
93-
those are done. The call to `record_specialization_priorities` checks
94-
"coherence" which means that it ensures that two impls of the same trait for the
95-
same type cannot exist.
141+
*See also: [Well-formedness checking][wf-checking]*
96142

97-
## Intermediate Representation (IR)
143+
#### Coherence
98144

99-
The second intermediate representation in chalk is called, well, the "ir". :)
100-
The [IR source code][ir-code] contains the complete definition. The
101-
`ir::Program` struct contains some "rust things" but indexed and accessible in
102-
a different way. This is sort of analogous to the [HIR] in Rust.
145+
The function `record_specialization_priorities` in the `coherence` module
146+
([source code][coherence-src]) checks "coherence", which means that it
147+
ensures that two impls of the same trait for the same type cannot exist.
103148

104-
For example, if you have a type like `Foo<Bar>`, we would represent `Foo` as a
105-
string in the AST but in `ir::Program`, we use numeric indices (`ItemId`).
149+
### Solver ([chalk_solve])
106150

107-
In addition to `ir::Program` which has "rust-like things", there is also
108-
`ir::ProgramEnvironment` which is "pure logic". The main field in that struct is
109-
`program_clauses` which contains the `ProgramClause`s that we generated
110-
previously.
151+
Finally, when we've collected all the program clauses we care about, we want
152+
to perform queries on it. The component that finds the answer to these
153+
queries is called the *solver*.
111154

112-
## Rules
155+
*See also: [The SLG Solver][slg]*
113156

114-
The `rules` module works by iterating over every trait, impl, etc. and emitting
115-
the rules that come from each one. See [Lowering Rules][lowering-rules] for the
116-
most up-to-date reference on that.
157+
## Crates
117158

118-
The `ir::ProgramEnvironment` is created [in this module][rules-environment].
159+
Chalk's functionality is broken up into the following crates:
160+
- [**chalk_engine**][chalk_engine]: Defines the core [SLG solver][slg].
161+
- [**chalk_ir**][chalk_ir]: Defines chalk's internal representation of
162+
types, lifetimes, and goals.
163+
- [**chalk_solve**][chalk_solve]: Combines `chalk_ir` and `chalk_engine`,
164+
effectively.
165+
- [`chalk_engine::context`][engine-context] provides the necessary hooks.
166+
- [**chalk_parse**][chalk_parse]: Defines the raw AST and a parser.
167+
- [**chalk**][doc-chalk]: Brings everything together. Defines the following
168+
modules:
169+
- [`rust_ir`][rust_ir], containing the "HIR-like" form of the AST
170+
- `rust_ir::lowering`, which converts AST to `rust_ir`
171+
- `rules`, which implements logic rules converting `rust_ir` to `chalk_ir`
172+
- `coherence`, which implements coherence rules
173+
- Also includes [chalki][chalki], chalk's REPL.
174+
175+
[Browse source code on GitHub](https://github.com/rust-lang-nursery/chalk)
119176

120177
## Testing
121178

122-
TODO: Basically, [there is a macro](https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/solve/test.rs#L112-L148)
123-
that will take chalk's Rust-like syntax and run it through the full pipeline
124-
described above.
125-
[This](https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/solve/test.rs#L83-L110)
126-
is the function that is ultimately called.
179+
chalk has a test framework for lowering programs to logic, checking the
180+
lowered logic, and performing queries on it. This is how we test the
181+
implementation of chalk itself, and the viability of the [lowering
182+
rules][lowering-rules].
127183

128-
## Solver
184+
The main kind of tests in chalk are **goal tests**. They contain a program,
185+
which is expected to lower to logic successfully, and a set of queries
186+
(goals) along with the expected output. Here's an
187+
[example][chalk-test-example]. Since chalk's output can be quite long, goal
188+
tests support specifying only a prefix of the output.
129189

130-
See [The SLG Solver][slg].
190+
**Lowering tests** check the stages that occur before we can issue queries
191+
to the solver: the [lowering to rust_ir][chalk-test-lowering], and the
192+
[well-formedness checks][chalk-test-wf] that occur after that.
131193

132-
[rustc-issues]: https://github.com/rust-lang-nursery/rustc-guide/issues
133-
[chalk]: https://github.com/rust-lang-nursery/chalk
134-
[lowering-to-logic]: ./lowering-to-logic.html
194+
### Testing internals
195+
196+
Goal tests use a [`test!` macro][test-macro] that takes chalk's Rust-like
197+
syntax and runs it through the full pipeline described above. The macro
198+
ultimately calls the [`solve_goal` function][solve_goal].
199+
200+
Likewise, lowering tests use the [`lowering_success!` and
201+
`lowering_error!` macros][test-lowering-macros].
202+
203+
## More Resources
204+
205+
* [Chalk Source Code](https://github.com/rust-lang-nursery/chalk)
206+
* [Chalk Glossary](https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md)
207+
208+
### Blog Posts
209+
210+
* [Lowering Rust traits to logic](http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/)
211+
* [Unification in Chalk, part 1](http://smallcultfollowing.com/babysteps/blog/2017/03/25/unification-in-chalk-part-1/)
212+
* [Unification in Chalk, part 2](http://smallcultfollowing.com/babysteps/blog/2017/04/23/unification-in-chalk-part-2/)
213+
* [Negative reasoning in Chalk](http://aturon.github.io/blog/2017/04/24/negative-chalk/)
214+
* [Query structure in chalk](http://smallcultfollowing.com/babysteps/blog/2017/05/25/query-structure-in-chalk/)
215+
* [Cyclic queries in chalk](http://smallcultfollowing.com/babysteps/blog/2017/09/12/tabling-handling-cyclic-queries-in-chalk/)
216+
* [An on-demand SLG solver for chalk](http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/)
217+
218+
[goals-and-clauses]: ./goals-and-clauses.html
219+
[HIR]: ../hir.html
220+
[lowering-forall]: ./lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses
135221
[lowering-rules]: ./lowering-rules.html
222+
[lowering-to-logic]: ./lowering-to-logic.html
223+
[slg]: ./slg.html
224+
[wf-checking]: ./wf.html
225+
136226
[ast]: https://en.wikipedia.org/wiki/Abstract_syntax_tree
137-
[chalk-ast]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-parse/src/ast.rs
227+
[chalk]: https://github.com/rust-lang-nursery/chalk
228+
[rustc-issues]: https://github.com/rust-lang-nursery/rustc-guide/issues
138229
[universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification
139-
[lowering-forall]: ./lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses
140-
[programclause]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L721
141-
[clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause
142-
[goals-and-clauses]: ./goals-and-clauses.html
143-
[well-formedness-checks]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir/lowering.rs#L230-L232
144-
[ir-code]: https://github.com/rust-lang-nursery/chalk/tree/master/chalk-ir
145-
[HIR]: ../hir.html
230+
231+
[`ProgramClause`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/enum.ProgramClause.html
232+
[`ProgramEnvironment`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/struct.ProgramEnvironment.html
233+
[chalk_engine]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/index.html
234+
[chalk_ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/index.html
235+
[chalk_parse]: https://rust-lang-nursery.github.io/chalk/doc/chalk_parse/index.html
236+
[chalk_solve]: https://rust-lang-nursery.github.io/chalk/doc/chalk_solve/index.html
237+
[doc-chalk]: https://rust-lang-nursery.github.io/chalk/doc/chalk/index.html
238+
[engine-context]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/context/index.html
239+
[rust_ir-program]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rust_ir/struct.Program.html
240+
[rust_ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rust_ir/index.html
241+
146242
[binders-struct]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L661
243+
[chalk-ast]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-parse/src/ast.rs
244+
[chalk-test-example]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115
245+
[chalk-test-lowering-example]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs#L8-L31
246+
[chalk-test-lowering]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs
247+
[chalk-test-wf]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf/test.rs#L1
248+
[chalki]: https://rust-lang-nursery.github.io/chalk/doc/chalki/index.html
249+
[clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause
250+
[coherence-src]: https://github.com/rust-lang-nursery/chalk/blob/master/src/coherence.rs
251+
[ir-code]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rust_ir.rs
147252
[rules-environment]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/rules.rs#L9
148-
[slg]: ./slg.html
253+
[rules-src]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules.rs
254+
[rules-wf-src]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf.rs
255+
[solve_goal]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L85
256+
[test-lowering-macros]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test_util.rs#L21-L54
257+
[test-macro]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L33

0 commit comments

Comments
 (0)