Merge pull request #223 from tmandry/improve-chalk-overview

Update chalk overview

1 files changed, 169 insertions, 60 deletions

diff --git a/src/doc/rustc-dev-guide/src/traits/chalk-overview.md b/src/doc/rustc-dev-guide/src/traits/chalk-overview.md
index 3473a076438..59572479d03 100644
--- a/src/doc/rustc-dev-guide/src/traits/chalk-overview.md
+++ b/src/doc/rustc-dev-guide/src/traits/chalk-overview.md
@@ -16,23 +16,45 @@ existing, somewhat ad-hoc implementation into something far more principled and
 expressive, which should behave better in corner cases, and be much easier to
 extend.
 
-## Resources
+## Chalk Structure
 
-* [Chalk Source Code](https://github.com/rust-lang-nursery/chalk)
-* [Chalk Glossary](https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md)
-* The traits section of the rustc guide (you are here)
+Chalk has two main "products". The first of these is the
+[`chalk_engine`][chalk_engine] crate, which defines the core [SLG
+solver][slg]. This is the part rustc uses.
 
-### Blog Posts
+The rest of chalk can be considered an elaborate testing harness. Chalk is
+capable of parsing Rust-like "programs", lowering them to logic, and
+performing queries on them.
 
-* [Lowering Rust traits to logic](http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/)
-* [Unification in Chalk, part 1](http://smallcultfollowing.com/babysteps/blog/2017/03/25/unification-in-chalk-part-1/)
-* [Unification in Chalk, part 2](http://smallcultfollowing.com/babysteps/blog/2017/04/23/unification-in-chalk-part-2/)
-* [Negative reasoning in Chalk](http://aturon.github.io/blog/2017/04/24/negative-chalk/)
-* [Query structure in chalk](http://smallcultfollowing.com/babysteps/blog/2017/05/25/query-structure-in-chalk/)
-* [Cyclic queries in chalk](http://smallcultfollowing.com/babysteps/blog/2017/09/12/tabling-handling-cyclic-queries-in-chalk/)
-* [An on-demand SLG solver for chalk](http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/)
+Here's a sample session in the chalk repl, chalki. After feeding it our
+program, we perform some queries on it.
+
+```rust,ignore
+?- program
+Enter a program; press Ctrl-D when finished
+| struct Foo { }
+| struct Bar { }
+| struct Vec<T> { }
+| trait Clone { }
+| impl<T> Clone for Vec<T> where T: Clone { }
+| impl Clone for Foo { }
+
+?- Vec<Foo>: Clone
+Unique; substitution [], lifetime constraints []
+
+?- Vec<Bar>: Clone
+No possible solution.
+
+?- exists<T> { Vec<T>: Clone }
+Ambiguous; no inference guidance
+```
+
+You can see more examples of programs and queries in the [unit
+tests][chalk-test-example].
 
-## Parsing
+Next we'll go through each stage required to produce the output above.
+
+### Parsing ([chalk_parse])
 
 Chalk is designed to be incorporated with the Rust compiler, so the syntax and
 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
 transformation that a program goes through in order to become a format that
 chalk can understand.
 
-## Lowering
+### Rust Intermediate Representation ([rust_ir])
+
+After getting the AST we convert it to a more convenient intermediate
+representation called [`rust_ir`][rust_ir]. This is sort of analogous to the
+[HIR] in Rust. The process of converting to IR is called *lowering*.
 
-After parsing, there is a "lowering" phase. This aims to convert traits/impls
-into "program clauses". A [`ProgramClause` (source code)][programclause] is
-essentially one of the following:
+The [`rust_ir::Program`][rust_ir-program] struct contains some "rust things"
+but indexed and accessible in a different way. For example, if you have a
+type like `Foo<Bar>`, we would represent `Foo` as a string in the AST but in
+`rust_ir::Program`, we use numeric indices (`ItemId`).
+
+The [IR source code][ir-code] contains the complete definition.
+
+### Chalk Intermediate Representation ([chalk_ir])
+
+Once we have Rust IR it is time to convert it to "program clauses". A
+[`ProgramClause`] is essentially one of the following:
 
 * A [clause] of the form `consequence :- conditions` where `:-` is read as
   "if" and `conditions = cond1 && cond2 && ...`
@@ -70,8 +104,8 @@ essentially one of the following:
 
 *See also: [Goals and Clauses][goals-and-clauses]*
 
-Lowering is the phase where we encode the rules of the trait system into logic.
-For example, if we have the following Rust:
+This is where we encode the rules of the trait system into logic. For
+example, if we have the following Rust:
 
 ```rust,ignore
 impl<T: Clone> Clone for Vec<T> {}
@@ -86,63 +120,138 @@ forall<T> { (Vec<T>: Clone) :- (T: Clone) }
 This rule dictates that `Vec<T>: Clone` is only satisfied if `T: Clone` is also
 satisfied (i.e. "provable").
 
-### Well-formedness checks
+Similar to [`rust_ir::Program`][rust_ir-program] which has "rust-like
+things", chalk_ir defines [`ProgramEnvironment`] which which is "pure logic".
+The main field in that struct is `program_clauses`, which contains the
+[`ProgramClause`]s generated by the rules module.
+
+#### Rules
+
+The `rules` module ([source code][rules-src]) defines the logic rules we use
+for each item in the Rust IR. It works by iterating over every trait, impl,
+etc. and emitting the rules that come from each one.
+
+*See also: [Lowering Rules][lowering-rules]*
+
+#### Well-formedness checks
+
+As part of lowering to logic, we also do some "well formedness" checks. See
+the [`rules::wf` source code][rules-wf-src] for where those are done.
 
-As part of lowering from the AST to the internal IR, we also do some "well
-formedness" checks. See the [source code][well-formedness-checks] for where
-those are done. The call to `record_specialization_priorities` checks
-"coherence" which means that it ensures that two impls of the same trait for the
-same type cannot exist.
+*See also: [Well-formedness checking][wf-checking]*
 
-## Intermediate Representation (IR)
+#### Coherence
 
-The second intermediate representation in chalk is called, well, the "ir". :)
-The [IR source code][ir-code] contains the complete definition. The
-`ir::Program` struct contains some "rust things" but indexed and accessible in
-a different way. This is sort of analogous to the [HIR] in Rust.
+The function `record_specialization_priorities` in the `coherence` module
+([source code][coherence-src]) checks "coherence", which means that it
+ensures that two impls of the same trait for the same type cannot exist.
 
-For example, if you have a type like `Foo<Bar>`, we would represent `Foo` as a
-string in the AST but in `ir::Program`, we use numeric indices (`ItemId`).
+### Solver ([chalk_solve])
 
-In addition to `ir::Program` which has "rust-like things", there is also
-`ir::ProgramEnvironment` which is "pure logic". The main field in that struct is
-`program_clauses` which contains the `ProgramClause`s that we generated
-previously.
+Finally, when we've collected all the program clauses we care about, we want
+to perform queries on it. The component that finds the answer to these
+queries is called the *solver*.
 
-## Rules
+*See also: [The SLG Solver][slg]*
 
-The `rules` module works by iterating over every trait, impl, etc. and emitting
-the rules that come from each one. See [Lowering Rules][lowering-rules] for the
-most up-to-date reference on that.
+## Crates
 
-The `ir::ProgramEnvironment` is created [in this module][rules-environment].
+Chalk's functionality is broken up into the following crates:
+- [**chalk_engine**][chalk_engine]: Defines the core [SLG solver][slg].
+- [**chalk_ir**][chalk_ir]: Defines chalk's internal representation of
+  types, lifetimes, and goals.
+- [**chalk_solve**][chalk_solve]: Combines `chalk_ir` and `chalk_engine`,
+  effectively.
+  - [`chalk_engine::context`][engine-context] provides the necessary hooks.
+- [**chalk_parse**][chalk_parse]: Defines the raw AST and a parser.
+- [**chalk**][doc-chalk]: Brings everything together. Defines the following
+  modules:
+  - [`rust_ir`][rust_ir], containing the "HIR-like" form of the AST
+    - `rust_ir::lowering`, which converts AST to `rust_ir`
+  - `rules`, which implements logic rules converting `rust_ir` to `chalk_ir`
+  - `coherence`, which implements coherence rules
+  - Also includes [chalki][chalki], chalk's REPL.
+
+[Browse source code on GitHub](https://github.com/rust-lang-nursery/chalk)
 
 ## Testing
 
-TODO: Basically, [there is a macro](https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/solve/test.rs#L112-L148)
-that will take chalk's Rust-like syntax and run it through the full pipeline
-described above.
-[This](https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/solve/test.rs#L83-L110)
-is the function that is ultimately called.
+chalk has a test framework for lowering programs to logic, checking the
+lowered logic, and performing queries on it. This is how we test the
+implementation of chalk itself, and the viability of the [lowering
+rules][lowering-rules].
 
-## Solver
+The main kind of tests in chalk are **goal tests**. They contain a program,
+which is expected to lower to logic successfully, and a set of queries
+(goals) along with the expected output. Here's an
+[example][chalk-test-example]. Since chalk's output can be quite long, goal
+tests support specifying only a prefix of the output.
 
-See [The SLG Solver][slg].
+**Lowering tests** check the stages that occur before we can issue queries
+to the solver: the [lowering to rust_ir][chalk-test-lowering], and the
+[well-formedness checks][chalk-test-wf] that occur after that.
 
-[rustc-issues]: https://github.com/rust-lang-nursery/rustc-guide/issues
-[chalk]: https://github.com/rust-lang-nursery/chalk
-[lowering-to-logic]: ./lowering-to-logic.html
+### Testing internals
+
+Goal tests use a [`test!` macro][test-macro] that takes chalk's Rust-like
+syntax and runs it through the full pipeline described above. The macro
+ultimately calls the [`solve_goal` function][solve_goal].
+
+Likewise, lowering tests use the [`lowering_success!` and
+`lowering_error!` macros][test-lowering-macros].
+
+## More Resources
+
+* [Chalk Source Code](https://github.com/rust-lang-nursery/chalk)
+* [Chalk Glossary](https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md)
+
+### Blog Posts
+
+* [Lowering Rust traits to logic](http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/)
+* [Unification in Chalk, part 1](http://smallcultfollowing.com/babysteps/blog/2017/03/25/unification-in-chalk-part-1/)
+* [Unification in Chalk, part 2](http://smallcultfollowing.com/babysteps/blog/2017/04/23/unification-in-chalk-part-2/)
+* [Negative reasoning in Chalk](http://aturon.github.io/blog/2017/04/24/negative-chalk/)
+* [Query structure in chalk](http://smallcultfollowing.com/babysteps/blog/2017/05/25/query-structure-in-chalk/)
+* [Cyclic queries in chalk](http://smallcultfollowing.com/babysteps/blog/2017/09/12/tabling-handling-cyclic-queries-in-chalk/)
+* [An on-demand SLG solver for chalk](http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/)
+
+[goals-and-clauses]: ./goals-and-clauses.html
+[HIR]: ../hir.html
+[lowering-forall]: ./lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses
 [lowering-rules]: ./lowering-rules.html
+[lowering-to-logic]: ./lowering-to-logic.html
+[slg]: ./slg.html
+[wf-checking]: ./wf.html
+
 [ast]: https://en.wikipedia.org/wiki/Abstract_syntax_tree
-[chalk-ast]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-parse/src/ast.rs
+[chalk]: https://github.com/rust-lang-nursery/chalk
+[rustc-issues]: https://github.com/rust-lang-nursery/rustc-guide/issues
 [universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification
-[lowering-forall]: ./lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses
-[programclause]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L721
-[clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause
-[goals-and-clauses]: ./goals-and-clauses.html
-[well-formedness-checks]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir/lowering.rs#L230-L232
-[ir-code]: https://github.com/rust-lang-nursery/chalk/tree/master/chalk-ir
-[HIR]: ../hir.html
+
+[`ProgramClause`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/enum.ProgramClause.html
+[`ProgramEnvironment`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/struct.ProgramEnvironment.html
+[chalk_engine]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/index.html
+[chalk_ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/index.html
+[chalk_parse]: https://rust-lang-nursery.github.io/chalk/doc/chalk_parse/index.html
+[chalk_solve]: https://rust-lang-nursery.github.io/chalk/doc/chalk_solve/index.html
+[doc-chalk]: https://rust-lang-nursery.github.io/chalk/doc/chalk/index.html
+[engine-context]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/context/index.html
+[rust_ir-program]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rust_ir/struct.Program.html
+[rust_ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rust_ir/index.html
+
 [binders-struct]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L661
+[chalk-ast]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-parse/src/ast.rs
+[chalk-test-example]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115
+[chalk-test-lowering-example]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs#L8-L31
+[chalk-test-lowering]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs
+[chalk-test-wf]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf/test.rs#L1
+[chalki]: https://rust-lang-nursery.github.io/chalk/doc/chalki/index.html
+[clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause
+[coherence-src]: https://github.com/rust-lang-nursery/chalk/blob/master/src/coherence.rs
+[ir-code]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rust_ir.rs
 [rules-environment]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/rules.rs#L9
-[slg]: ./slg.html
+[rules-src]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules.rs
+[rules-wf-src]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf.rs
+[solve_goal]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L85
+[test-lowering-macros]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test_util.rs#L21-L54
+[test-macro]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L33