mirror
/
rustc-dev-guide
mirror of https://github.com/rust-lang/rustc-dev-guide.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Chalk Overview: Update old content

This commit is contained in:
Tyler Mandry 2018-10-29 22:31:59 -05:00
parent c50ab556c0
commit 4a8803cd10
1 changed files with 59 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

99
src/traits/chalk-overview.md
View File

@ -55,7 +55,7 @@ Next we'll go through each stage required to produce the output above.
[chalk-tests]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115 [chalk-tests]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115
### Parsing ### Parsing ([chalk_parse])
Chalk is designed to be incorporated with the Rust compiler, so the syntax and 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 concepts it deals with heavily borrow from Rust. It is convenient for the sake
@ -71,11 +71,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 transformation that a program goes through in order to become a format that
chalk can understand. chalk can understand.
### Lowering ### Rust Intermediate Representation ([rust_ir])
After parsing, there is a "lowering" phase. This aims to convert traits/impls After getting the AST we convert it to a more convenient intermediate
into "program clauses". A [`ProgramClause` (source code)][programclause] is representation called [`rust_ir`][rust_ir]. This is sort of analogous to the
essentially one of the following: [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 * A [clause] of the form `consequence :- conditions` where `:-` is read as
"if" and `conditions = cond1 && cond2 && ...` "if" and `conditions = cond1 && cond2 && ...`
@ -93,8 +105,8 @@ essentially one of the following:
*See also: [Goals and Clauses][goals-and-clauses]* *See also: [Goals and Clauses][goals-and-clauses]*
Lowering is the phase where we encode the rules of the trait system into logic. This is where we encode the rules of the trait system into logic. For
For example, if we have the following Rust: example, if we have the following Rust:
```rust,ignore ```rust,ignore
impl<T: Clone> Clone for Vec<T> {} impl<T: Clone> Clone for Vec<T> {}
@ -109,54 +121,61 @@ forall<T> { (Vec<T>: Clone) :- (T: Clone) }
This rule dictates that `Vec<T>: Clone` is only satisfied if `T: Clone` is also This rule dictates that `Vec<T>: Clone` is only satisfied if `T: Clone` is also
satisfied (i.e. "provable"). satisfied (i.e. "provable").
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]*
[`ProgramEnvironment`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/struct.ProgramEnvironment.html
[`ProgramClause`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/enum.ProgramClause.html
[rules-src]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules.rs
#### Well-formedness checks #### Well-formedness checks
As part of lowering from the AST to the internal IR, we also do some "well As part of lowering to logic, we also do some "well formedness" checks. See
formedness" checks. See the [source code][well-formedness-checks] for where the [`rules::wf` source code][rules-wf-src] for where those are done.
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.
### Intermediate Representation (IR) *See also: [Well-formedness checking][wf-checking]*
The second intermediate representation in chalk is called, well, the "ir". :) [rules-wf-src]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf.rs
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.
For example, if you have a type like `Foo<Bar>`, we would represent `Foo` as a #### Coherence
string in the AST but in `ir::Program`, we use numeric indices (`ItemId`).
In addition to `ir::Program` which has "rust-like things", there is also The function `record_specialization_priorities` in the `coherence` module
`ir::ProgramEnvironment` which is "pure logic". The main field in that struct is ([source code][coherence-src]) checks "coherence", which means that it
`program_clauses` which contains the `ProgramClause`s that we generated ensures that two impls of the same trait for the same type cannot exist.
previously.
### Rules [coherence-src]: https://github.com/rust-lang-nursery/chalk/blob/master/src/coherence.rs
The `rules` module works by iterating over every trait, impl, etc. and emitting ### Solver ([chalk_solve])
the rules that come from each one. See [Lowering Rules][lowering-rules] for the
most up-to-date reference on that.
The `ir::ProgramEnvironment` is created [in this module][rules-environment]. 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*.
### Solver *See also: [The SLG Solver][slg]*
See [The SLG Solver][slg].
## Crates ## Crates
Chalk's functionality is broken up into the following crates: Chalk's functionality is broken up into the following crates:
- [**chalk_engine**][doc-chalk-engine]: Defines the core [SLG solver][slg]. - [**chalk_engine**][doc-chalk-engine]: Defines the core [SLG solver][slg].
- [**chalk_ir**][doc-chalk-ir]: Defines chalk's internal representation of - [**chalk_ir**][chalk_ir]: Defines chalk's internal representation of
types, lifetimes, and goals. types, lifetimes, and goals.
- [**chalk_solve**][doc-chalk-solve]: Combines `chalk_ir` and `chalk_engine`, - [**chalk_solve**][doc-chalk-solve]: Combines `chalk_ir` and `chalk_engine`,
effectively. effectively.
- [`chalk_engine::context`][engine-context] provides the necessary hooks. - [`chalk_engine::context`][engine-context] provides the necessary hooks.
- [**chalk_parse**][doc-chalk-parse]: Defines the raw AST and a parser. - [**chalk_parse**][chalk_parse]: Defines the raw AST and a parser.
- [**chalk**][doc-chalk]: Brings everything together. Defines the following - [**chalk**][doc-chalk]: Brings everything together. Defines the following
modules: modules:
- [`rust_ir`][doc-chalk-rust-ir], containing the "HIR-like" form of the AST - [`rust_ir`][rust_ir], containing the "HIR-like" form of the AST
- `rust_ir::lowering`, which converts AST to `rust_ir` - `rust_ir::lowering`, which converts AST to `rust_ir`
- `rules`, which implements logic rules converting `rust_ir` to `chalk_ir` - `rules`, which implements logic rules converting `rust_ir` to `chalk_ir`
- `coherence`, which implements coherence rules - `coherence`, which implements coherence rules
@ -167,11 +186,12 @@ Chalk's functionality is broken up into the following crates:
[engine-context]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/context/index.html [engine-context]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/context/index.html
[doc-chalk-engine]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/index.html [doc-chalk-engine]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/index.html
[doc-chalk-ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/index.html [chalk_ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/index.html
[doc-chalk-solve]: https://rust-lang-nursery.github.io/chalk/doc/chalk_solve/index.html [doc-chalk-solve]: https://rust-lang-nursery.github.io/chalk/doc/chalk_solve/index.html
[doc-chalk-parse]: https://rust-lang-nursery.github.io/chalk/doc/chalk_parse/index.html [chalk_parse]: https://rust-lang-nursery.github.io/chalk/doc/chalk_parse/index.html
[doc-chalk]: https://rust-lang-nursery.github.io/chalk/doc/chalk/index.html [doc-chalk]: https://rust-lang-nursery.github.io/chalk/doc/chalk/index.html
[doc-chalk-rust-ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rules/index.html [rust_ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rust_ir/index.html
[rust_ir-program]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rust_ir/struct.Program.html
[doc-chalki]: https://rust-lang-nursery.github.io/chalk/doc/chalki/index.html [doc-chalki]: https://rust-lang-nursery.github.io/chalk/doc/chalki/index.html
## Testing ## Testing
@ -201,15 +221,14 @@ is the function that is ultimately called.
[chalk]: https://github.com/rust-lang-nursery/chalk [chalk]: https://github.com/rust-lang-nursery/chalk
[lowering-to-logic]: ./lowering-to-logic.html [lowering-to-logic]: ./lowering-to-logic.html
[lowering-rules]: ./lowering-rules.html [lowering-rules]: ./lowering-rules.html
[wf-checking]: ./wf.html
[ast]: https://en.wikipedia.org/wiki/Abstract_syntax_tree [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-ast]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-parse/src/ast.rs
[universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification [universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification
[lowering-forall]: ./lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses [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 [clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause
[goals-and-clauses]: ./goals-and-clauses.html [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/blob/master/src/rust_ir.rs
[ir-code]: https://github.com/rust-lang-nursery/chalk/tree/master/chalk-ir
[HIR]: ../hir.html [HIR]: ../hir.html
[binders-struct]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L661 [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 [rules-environment]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/rules.rs#L9