3 > Chalk is under heavy development, so if any of these links are broken or if
4 > any of the information is inconsistent with the code or outdated, please
5 > [open an issue][rustc-issues] so we can fix it. If you are able to fix the
6 > issue yourself, we would love your contribution!
8 [Chalk][chalk] recasts Rust's trait system explicitly in terms of logic
9 programming by "lowering" Rust code into a kind of logic program we can then
10 execute queries against (see [*Lowering to Logic*][lowering-to-logic] and
11 [*Lowering Rules*][lowering-rules]). Its goal is to be an executable, highly
12 readable specification of the Rust trait system.
14 There are many expected benefits from this work. It will consolidate our
15 existing, somewhat ad-hoc implementation into something far more principled and
16 expressive, which should behave better in corner cases, and be much easier to
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.
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.
29 Here's a sample session in the chalk repl, chalki. After feeding it our
30 program, we perform some queries on it.
34 Enter a program; press Ctrl-D when finished
39 | impl<T> Clone for Vec<T> where T: Clone { }
40 | impl Clone for Foo { }
43 Unique; substitution [], lifetime constraints []
48 ?- exists<T> { Vec<T>: Clone }
49 Ambiguous; no inference guidance
52 You can see more examples of programs and queries in the [unit
53 tests][chalk-test-example].
55 Next we'll go through each stage required to produce the output above.
57 ### Parsing ([chalk_parse])
59 Chalk is designed to be incorporated with the Rust compiler, so the syntax and
60 concepts it deals with heavily borrow from Rust. It is convenient for the sake
61 of testing to be able to run chalk on its own, so chalk includes a parser for a
62 Rust-like syntax. This syntax is orthogonal to the Rust AST and grammar. It is
63 not intended to look exactly like it or support the exact same syntax.
65 The parser takes that syntax and produces an [Abstract Syntax Tree (AST)][ast].
66 You can find the [complete definition of the AST][chalk-ast] in the source code.
68 The syntax contains things from Rust that we know and love, for example: traits,
69 impls, and struct definitions. Parsing is often the first "phase" of
70 transformation that a program goes through in order to become a format that
73 ### Rust Intermediate Representation ([chalk_rust_ir])
75 After getting the AST we convert it to a more convenient intermediate
76 representation called [`chalk_rust_ir`][chalk_rust_ir]. This is sort of
77 analogous to the [HIR] in Rust. The process of converting to IR is called
80 The [`chalk::program::Program`][chalk-program] struct contains some "rust things"
81 but indexed and accessible in a different way. For example, if you have a
82 type like `Foo<Bar>`, we would represent `Foo` as a string in the AST but in
83 `chalk::program::Program`, we use numeric indices (`ItemId`).
85 The [IR source code][ir-code] contains the complete definition.
87 ### Chalk Intermediate Representation ([chalk_ir])
89 Once we have Rust IR it is time to convert it to "program clauses". A
90 [`ProgramClause`] is essentially one of the following:
92 * A [clause] of the form `consequence :- conditions` where `:-` is read as
93 "if" and `conditions = cond1 && cond2 && ...`
94 * A universally quantified clause of the form
95 `forall<T> { consequence :- conditions }`
96 * `forall<T> { ... }` is used to represent [universal quantification]. See the
97 section on [Lowering to logic][lowering-forall] for more information.
98 * A key thing to note about `forall` is that we don't allow you to "quantify"
99 over traits, only types and regions (lifetimes). That is, you can't make a
100 rule like `forall<Trait> { u32: Trait }` which would say "`u32` implements
101 all traits". You can however say `forall<T> { T: Trait }` meaning "`Trait`
102 is implemented by all types".
103 * `forall<T> { ... }` is represented in the code using the [`Binders<T>`
104 struct][binders-struct].
106 *See also: [Goals and Clauses][goals-and-clauses]*
108 This is where we encode the rules of the trait system into logic. For
109 example, if we have the following Rust:
112 impl<T: Clone> Clone for Vec<T> {}
115 We generate the following program clause:
118 forall<T> { (Vec<T>: Clone) :- (T: Clone) }
121 This rule dictates that `Vec<T>: Clone` is only satisfied if `T: Clone` is also
122 satisfied (i.e. "provable").
124 Similar to [`chalk::program::Program`][chalk-program] which has "rust-like
125 things", chalk_ir defines [`ProgramEnvironment`] which is "pure logic".
126 The main field in that struct is `program_clauses`, which contains the
127 [`ProgramClause`]s generated by the rules module.
129 ### Rules ([chalk_solve])
131 The `chalk_solve` crate ([source code][chalk_solve]) defines the logic rules we
132 use for each item in the Rust IR. It works by iterating over every trait, impl,
133 etc. and emitting the rules that come from each one.
135 *See also: [Lowering Rules][lowering-rules]*
137 #### Well-formedness checks
139 As part of lowering to logic, we also do some "well formedness" checks. See
140 the [`chalk_solve::wf` source code][solve-wf-src] for where those are done.
142 *See also: [Well-formedness checking][wf-checking]*
146 The method `CoherenceSolver::specialization_priorities` in the `coherence` module
147 ([source code][coherence-src]) checks "coherence", which means that it
148 ensures that two impls of the same trait for the same type cannot exist.
150 ### Solver ([chalk_solve])
152 Finally, when we've collected all the program clauses we care about, we want
153 to perform queries on it. The component that finds the answer to these
154 queries is called the *solver*.
156 *See also: [The SLG Solver][slg]*
160 Chalk's functionality is broken up into the following crates:
161 - [**chalk_engine**][chalk_engine]: Defines the core [SLG solver][slg].
162 - [**chalk_rust_ir**][chalk_rust_ir], containing the "HIR-like" form of the AST
163 - [**chalk_ir**][chalk_ir]: Defines chalk's internal representation of
164 types, lifetimes, and goals.
165 - [**chalk_solve**][chalk_solve]: Combines `chalk_ir` and `chalk_engine`,
166 effectively, which implements logic rules converting `chalk_rust_ir` to
168 - Defines the `coherence` module, which implements coherence rules
169 - [`chalk_engine::context`][engine-context] provides the necessary hooks.
170 - [**chalk_parse**][chalk_parse]: Defines the raw AST and a parser.
171 - [**chalk**][doc-chalk]: Brings everything together. Defines the following
173 - `chalk::lowering`, which converts AST to `chalk_rust_ir`
174 - Also includes [chalki][chalki], chalk's REPL.
176 [Browse source code on GitHub](https://github.com/rust-lang/chalk)
180 chalk has a test framework for lowering programs to logic, checking the
181 lowered logic, and performing queries on it. This is how we test the
182 implementation of chalk itself, and the viability of the [lowering
183 rules][lowering-rules].
185 The main kind of tests in chalk are **goal tests**. They contain a program,
186 which is expected to lower to logic successfully, and a set of queries
187 (goals) along with the expected output. Here's an
188 [example][chalk-test-example]. Since chalk's output can be quite long, goal
189 tests support specifying only a prefix of the output.
191 **Lowering tests** check the stages that occur before we can issue queries
192 to the solver: the [lowering to chalk_rust_ir][chalk-test-lowering], and the
193 [well-formedness checks][chalk-test-wf] that occur after that.
195 ### Testing internals
197 Goal tests use a [`test!` macro][test-macro] that takes chalk's Rust-like
198 syntax and runs it through the full pipeline described above. The macro
199 ultimately calls the [`solve_goal` function][solve_goal].
201 Likewise, lowering tests use the [`lowering_success!` and
202 `lowering_error!` macros][test-lowering-macros].
206 * [Chalk Source Code](https://github.com/rust-lang/chalk)
207 * [Chalk Glossary](https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md)
211 * [Lowering Rust traits to logic](http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/)
212 * [Unification in Chalk, part 1](http://smallcultfollowing.com/babysteps/blog/2017/03/25/unification-in-chalk-part-1/)
213 * [Unification in Chalk, part 2](http://smallcultfollowing.com/babysteps/blog/2017/04/23/unification-in-chalk-part-2/)
214 * [Negative reasoning in Chalk](https://aturon.github.io/blog/2017/04/24/negative-chalk/)
215 * [Query structure in chalk](http://smallcultfollowing.com/babysteps/blog/2017/05/25/query-structure-in-chalk/)
216 * [Cyclic queries in chalk](http://smallcultfollowing.com/babysteps/blog/2017/09/12/tabling-handling-cyclic-queries-in-chalk/)
217 * [An on-demand SLG solver for chalk](http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/)
219 [goals-and-clauses]: ./goals-and-clauses.html
221 [lowering-forall]: ./lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses
222 [lowering-rules]: ./lowering-rules.html
223 [lowering-to-logic]: ./lowering-to-logic.html
225 [wf-checking]: ./wf.html
227 [ast]: https://en.wikipedia.org/wiki/Abstract_syntax_tree
228 [chalk]: https://github.com/rust-lang/chalk
229 [rustc-issues]: https://github.com/rust-lang/rustc-dev-guide/issues
230 [universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification
232 [`ProgramClause`]: https://rust-lang.github.io/chalk/chalk_ir/struct.ProgramClause.html
233 [`ProgramEnvironment`]: https://rust-lang.github.io/chalk/chalk_integration/program_environment/struct.ProgramEnvironment.html
234 [chalk_engine]: https://rust-lang.github.io/chalk/chalk_engine
235 [chalk_ir]: https://rust-lang.github.io/chalk/chalk_ir/index.html
236 [chalk_parse]: https://rust-lang.github.io/chalk/chalk_parse/index.html
237 [chalk_solve]: https://rust-lang.github.io/chalk/chalk_solve/index.html
238 [chalk_rust_ir]: https://rust-lang.github.io/chalk/chalk_rust_ir/index.html
239 [doc-chalk]: https://rust-lang.github.io/chalk/chalk/index.html
240 [engine-context]: https://rust-lang.github.io/chalk/chalk_engine/context/index.html
241 [chalk-program]: https://rust-lang.github.io/chalk/chalk_integration/program/struct.Program.html
243 [binders-struct]: https://rust-lang.github.io/chalk/chalk_ir/struct.Binders.html
244 [chalk-ast]: https://rust-lang.github.io/chalk/chalk_parse/ast/index.html
245 [chalk-test-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115
246 [chalk-test-lowering-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs#L8-L31
247 [chalk-test-lowering]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs
248 [chalk-test-wf]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf/test.rs#L1
249 [chalki]: https://github.com/rust-lang/chalk/blob/master/src/main.rs
250 [clause]: https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md#clause
251 [coherence-src]: https://rust-lang.github.io/chalk/chalk_solve/coherence/index.html
252 [ir-code]: https://rust-lang.github.io/chalk/chalk_rust_ir/
253 [solve-wf-src]: https://rust-lang.github.io/chalk/chalk_solve/wf/index.html
254 [solve_goal]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L85
255 [test-lowering-macros]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test_util.rs#L21-L54
256 [test-macro]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L33