diff --git a/src/traits/chalk-overview.md b/src/traits/chalk-overview.md index 3473a0764..59572479d 100644 --- a/src/traits/chalk-overview.md +++ b/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 { } +| trait Clone { } +| impl Clone for Vec where T: Clone { } +| impl Clone for Foo { } + +?- Vec: Clone +Unique; substitution [], lifetime constraints [] + +?- Vec: Clone +No possible solution. + +?- exists { Vec: 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`, 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 Clone for Vec {} @@ -86,63 +120,138 @@ forall { (Vec: Clone) :- (T: Clone) } This rule dictates that `Vec: 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`, 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