src/doc/rustc-guide/src/traits/chalk-overview.md

   1 # An Overview of Chalk
   2
   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!
   7
   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.
  13
  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
  17 extend.
  18
  19 ## Chalk Structure
  20
  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.
  24
  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.
  28
  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].
  54
  55 Next we'll go through each stage required to produce the output above.
  56
  57 ### Parsing ([chalk_parse])
  58
  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.
  64
  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.
  67
  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
  71 chalk can understand.
  72
  73 ### Rust Intermediate Representation ([chalk_rust_ir])
  74
  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
  78 *lowering*.
  79
  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`).
  84
  85 The [IR source code][ir-code] contains the complete definition.
  86
  87 ### Chalk Intermediate Representation ([chalk_ir])
  88
  89 Once we have Rust IR it is time to convert it to "program clauses". A
  90 [`ProgramClause`] is essentially one of the following:
  91
  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].
 105
 106 *See also: [Goals and Clauses][goals-and-clauses]*
 107
 108 This is where we encode the rules of the trait system into logic. For
 109 example, if we have the following Rust:
 110
 111 ```rust,ignore
 112 impl<T: Clone> Clone for Vec<T> {}
 113 ```
 114
 115 We generate the following program clause:
 116
 117 ```rust,ignore
 118 forall<T> { (Vec<T>: Clone) :- (T: Clone) }
 119 ```
 120
 121 This rule dictates that `Vec<T>: Clone` is only satisfied if `T: Clone` is also
 122 satisfied (i.e. "provable").
 123
 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.
 128
 129 ### Rules ([chalk_solve])
 130
 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.
 134
 135 *See also: [Lowering Rules][lowering-rules]*
 136
 137 #### Well-formedness checks
 138
 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.
 141
 142 *See also: [Well-formedness checking][wf-checking]*
 143
 144 #### Coherence
 145
 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.
 149
 150 ### Solver ([chalk_solve])
 151
 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*.
 155
 156 *See also: [The SLG Solver][slg]*
 157
 158 ## Crates
 159
 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
 167   `chalk_ir`
 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
 172   modules:
 173   - `chalk::lowering`, which converts AST to `chalk_rust_ir`
 174   - Also includes [chalki][chalki], chalk's REPL.
 175
 176 [Browse source code on GitHub](https://github.com/rust-lang/chalk)
 177
 178 ## Testing
 179
 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].
 184
 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.
 190
 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.
 194
 195 ### Testing internals
 196
 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].
 200
 201 Likewise, lowering tests use the [`lowering_success!` and
 202 `lowering_error!` macros][test-lowering-macros].
 203
 204 ## More Resources
 205
 206 * [Chalk Source Code](https://github.com/rust-lang/chalk)
 207 * [Chalk Glossary](https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md)
 208
 209 ### Blog Posts
 210
 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/)
 218
 219 [goals-and-clauses]: ./goals-and-clauses.html
 220 [HIR]: ../hir.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
 224 [slg]: ./slg.html
 225 [wf-checking]: ./wf.html
 226
 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-guide/issues
 230 [universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification
 231
 232 [`ProgramClause`]: https://rust-lang.github.io/chalk/chalk_ir/enum.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
 242
 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