Merge pull request #223 from tmandry/improve-chalk-overview
Update chalk overview
This commit is contained in:
Niko Matsakis
GitHub
commit
9fe13e7182
|
|
@ -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.
|
||||
|
||||
## Parsing
|
||||
```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].
|
||||
|
||||
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 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:
|
||||
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*.
|
||||
|
||||
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.
|
||||
|
||||
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.
|
||||
#### Rules
|
||||
|
||||
## Intermediate Representation (IR)
|
||||
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.
|
||||
|
||||
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.
|
||||
*See also: [Lowering Rules][lowering-rules]*
|
||||
|
||||
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`).
|
||||
#### Well-formedness checks
|
||||
|
||||
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.
|
||||
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.
|
||||
|
||||
## Rules
|
||||
*See also: [Well-formedness checking][wf-checking]*
|
||||
|
||||
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.
|
||||
#### Coherence
|
||||
|
||||
The `ir::ProgramEnvironment` is created [in this module][rules-environment].
|
||||
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.
|
||||
|
||||
### Solver ([chalk_solve])
|
||||
|
||||
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*.
|
||||
|
||||
*See also: [The SLG Solver][slg]*
|
||||
|
||||
## Crates
|
||||
|
||||
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.
|
||||
|
||||
### 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/)
|
||||
|
||||
[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
|
||||
[lowering-rules]: ./lowering-rules.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
|
||||
[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
|
||||
[binders-struct]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L661
|
||||
[rules-environment]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/rules.rs#L9
|
||||
[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]: 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
|
||||
|
||||
[`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
|
||||
[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
|
||||
|
|
|
|||
Loading…
Reference in New Issue