update chalk with new organization
This commit is contained in:
parent
caa5110dc0
commit
1cbf18e860
|
|
@ -70,16 +70,17 @@ 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.
|
||||||
|
|
||||||
### Rust Intermediate Representation ([rust_ir])
|
### Rust Intermediate Representation ([chalk_rust_ir])
|
||||||
|
|
||||||
After getting the AST we convert it to a more convenient intermediate
|
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
|
representation called [`chalk_rust_ir`][chalk_rust_ir]. This is sort of
|
||||||
[HIR] in Rust. The process of converting to IR is called *lowering*.
|
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"
|
The [`chalk::program::Program`][chalk-program] struct contains some "rust things"
|
||||||
but indexed and accessible in a different way. For example, if you have a
|
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
|
type like `Foo<Bar>`, we would represent `Foo` as a string in the AST but in
|
||||||
`rust_ir::Program`, we use numeric indices (`ItemId`).
|
`chalk::program::Program`, we use numeric indices (`ItemId`).
|
||||||
|
|
||||||
The [IR source code][ir-code] contains the complete definition.
|
The [IR source code][ir-code] contains the complete definition.
|
||||||
|
|
||||||
|
|
@ -120,14 +121,14 @@ 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
|
Similar to [`chalk::program::Program`][chalk-program] which has "rust-like
|
||||||
things", chalk_ir defines [`ProgramEnvironment`] which which is "pure logic".
|
things", chalk_ir defines [`ProgramEnvironment`] which which is "pure logic".
|
||||||
The main field in that struct is `program_clauses`, which contains the
|
The main field in that struct is `program_clauses`, which contains the
|
||||||
[`ProgramClause`]s generated by the rules module.
|
[`ProgramClause`]s generated by the rules module.
|
||||||
|
|
||||||
#### Rules
|
### Rules ([chalk_rules])
|
||||||
|
|
||||||
The `rules` module ([source code][rules-src]) defines the logic rules we use
|
The `chalk_rules` crate ([source code][chalk_rules]) defines the logic rules we use
|
||||||
for each item in the Rust IR. It works by iterating over every trait, impl,
|
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.
|
etc. and emitting the rules that come from each one.
|
||||||
|
|
||||||
|
|
@ -136,13 +137,13 @@ etc. and emitting the rules that come from each one.
|
||||||
#### Well-formedness checks
|
#### Well-formedness checks
|
||||||
|
|
||||||
As part of lowering to logic, we also do some "well formedness" checks. See
|
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.
|
the [`chalk_rules::wf` source code][rules-wf-src] for where those are done.
|
||||||
|
|
||||||
*See also: [Well-formedness checking][wf-checking]*
|
*See also: [Well-formedness checking][wf-checking]*
|
||||||
|
|
||||||
#### Coherence
|
#### Coherence
|
||||||
|
|
||||||
The function `record_specialization_priorities` in the `coherence` module
|
The method `CoherenceSolver::specialization_priorities` in the `coherence` module
|
||||||
([source code][coherence-src]) checks "coherence", which means that it
|
([source code][coherence-src]) checks "coherence", which means that it
|
||||||
ensures that two impls of the same trait for the same type cannot exist.
|
ensures that two impls of the same trait for the same type cannot exist.
|
||||||
|
|
||||||
|
|
@ -158,18 +159,19 @@ queries is called the *solver*.
|
||||||
|
|
||||||
Chalk's functionality is broken up into the following crates:
|
Chalk's functionality is broken up into the following crates:
|
||||||
- [**chalk_engine**][chalk_engine]: Defines the core [SLG solver][slg].
|
- [**chalk_engine**][chalk_engine]: Defines the core [SLG solver][slg].
|
||||||
|
- [**chalk_rust_ir**][chalk_rust_ir], containing the "HIR-like" form of the AST
|
||||||
- [**chalk_ir**][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**][chalk_solve]: Combines `chalk_ir` and `chalk_engine`,
|
- [**chalk_solve**][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**][chalk_parse]: Defines the raw AST and a parser.
|
- [**chalk_parse**][chalk_parse]: Defines the raw AST and a parser.
|
||||||
|
- [**chalk_rules**][chalk_rules]: which implements logic rules converting
|
||||||
|
`chalk_rust_ir` to `chalk_ir`
|
||||||
|
- Defines the `coherence` module, which implements coherence rules
|
||||||
- [**chalk**][doc-chalk]: Brings everything together. Defines the following
|
- [**chalk**][doc-chalk]: Brings everything together. Defines the following
|
||||||
modules:
|
modules:
|
||||||
- [`rust_ir`][rust_ir], containing the "HIR-like" form of the AST
|
- `chalk::lowering`, which converts AST to `chalk_rust_ir`
|
||||||
- `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.
|
- Also includes [chalki][chalki], chalk's REPL.
|
||||||
|
|
||||||
[Browse source code on GitHub](https://github.com/rust-lang/chalk)
|
[Browse source code on GitHub](https://github.com/rust-lang/chalk)
|
||||||
|
|
@ -188,7 +190,7 @@ which is expected to lower to logic successfully, and a set of queries
|
||||||
tests support specifying only a prefix of the output.
|
tests support specifying only a prefix of the output.
|
||||||
|
|
||||||
**Lowering tests** check the stages that occur before we can issue queries
|
**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
|
to the solver: the [lowering to chalk_rust_ir][chalk-test-lowering], and the
|
||||||
[well-formedness checks][chalk-test-wf] that occur after that.
|
[well-formedness checks][chalk-test-wf] that occur after that.
|
||||||
|
|
||||||
### Testing internals
|
### Testing internals
|
||||||
|
|
@ -229,29 +231,28 @@ Likewise, lowering tests use the [`lowering_success!` and
|
||||||
[universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification
|
[universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification
|
||||||
|
|
||||||
[`ProgramClause`]: https://rust-lang.github.io/chalk/doc/chalk_ir/enum.ProgramClause.html
|
[`ProgramClause`]: https://rust-lang.github.io/chalk/doc/chalk_ir/enum.ProgramClause.html
|
||||||
[`ProgramEnvironment`]: https://rust-lang.github.io/chalk/doc/chalk_ir/struct.ProgramEnvironment.html
|
[`ProgramEnvironment`]: http://rust-lang.github.io/chalk/doc/chalk/program_environment/struct.ProgramEnvironment.html
|
||||||
[chalk_engine]: https://rust-lang.github.io/chalk/doc/chalk_engine/index.html
|
[chalk_engine]: https://rust-lang.github.io/chalk/doc/chalk_engine/index.html
|
||||||
[chalk_ir]: https://rust-lang.github.io/chalk/doc/chalk_ir/index.html
|
[chalk_ir]: https://rust-lang.github.io/chalk/doc/chalk_ir/index.html
|
||||||
[chalk_parse]: https://rust-lang.github.io/chalk/doc/chalk_parse/index.html
|
[chalk_parse]: https://rust-lang.github.io/chalk/doc/chalk_parse/index.html
|
||||||
[chalk_solve]: https://rust-lang.github.io/chalk/doc/chalk_solve/index.html
|
[chalk_solve]: https://rust-lang.github.io/chalk/doc/chalk_solve/index.html
|
||||||
|
[chalk_rules]: https://rust-lang.github.io/chalk/doc/chalk_rules/index.html
|
||||||
|
[chalk_rust_ir]: https://rust-lang.github.io/chalk/doc/chalk_rust_ir/index.html
|
||||||
[doc-chalk]: https://rust-lang.github.io/chalk/doc/chalk/index.html
|
[doc-chalk]: https://rust-lang.github.io/chalk/doc/chalk/index.html
|
||||||
[engine-context]: https://rust-lang.github.io/chalk/doc/chalk_engine/context/index.html
|
[engine-context]: https://rust-lang.github.io/chalk/doc/chalk_engine/context/index.html
|
||||||
[rust_ir-program]: https://rust-lang.github.io/chalk/doc/chalk/rust_ir/struct.Program.html
|
[chalk-program]: http://rust-lang.github.io/chalk/doc/chalk/program/struct.Program.html
|
||||||
[rust_ir]: https://rust-lang.github.io/chalk/doc/chalk/rust_ir/index.html
|
|
||||||
|
|
||||||
[binders-struct]: https://github.com/rust-lang/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L661
|
[binders-struct]: http://rust-lang.github.io/chalk/doc/chalk_ir/struct.Binders.html
|
||||||
[chalk-ast]: https://github.com/rust-lang/chalk/blob/master/chalk-parse/src/ast.rs
|
[chalk-ast]: http://rust-lang.github.io/chalk/doc/chalk_parse/ast/index.html
|
||||||
[chalk-test-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115
|
[chalk-test-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115
|
||||||
[chalk-test-lowering-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs#L8-L31
|
[chalk-test-lowering-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs#L8-L31
|
||||||
[chalk-test-lowering]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs
|
[chalk-test-lowering]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs
|
||||||
[chalk-test-wf]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf/test.rs#L1
|
[chalk-test-wf]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf/test.rs#L1
|
||||||
[chalki]: https://rust-lang.github.io/chalk/doc/chalki/index.html
|
[chalki]: https://rust-lang.github.io/chalk/doc/chalki/index.html
|
||||||
[clause]: https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md#clause
|
[clause]: https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md#clause
|
||||||
[coherence-src]: https://github.com/rust-lang/chalk/blob/master/src/coherence.rs
|
[coherence-src]: http://rust-lang.github.io/chalk/doc/chalk_rules/coherence/index.html
|
||||||
[ir-code]: https://github.com/rust-lang/chalk/blob/master/src/rust_ir.rs
|
[ir-code]: http://rust-lang.github.io/chalk/doc/chalk_rust_ir/
|
||||||
[rules-environment]: https://github.com/rust-lang/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/rules.rs#L9
|
[rules-wf-src]: http://rust-lang.github.io/chalk/doc/chalk_rules/wf/index.html
|
||||||
[rules-src]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules.rs
|
|
||||||
[rules-wf-src]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf.rs
|
|
||||||
[solve_goal]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L85
|
[solve_goal]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L85
|
||||||
[test-lowering-macros]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test_util.rs#L21-L54
|
[test-lowering-macros]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test_util.rs#L21-L54
|
||||||
[test-macro]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L33
|
[test-macro]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L33
|
||||||
|
|
|
||||||
|
|
@ -28,10 +28,10 @@ comment like so:
|
||||||
// Rule Foo-Bar-Baz
|
// Rule Foo-Bar-Baz
|
||||||
|
|
||||||
The reference implementation of these rules is to be found in
|
The reference implementation of these rules is to be found in
|
||||||
[`chalk/src/rules.rs`][chalk_rules]. They are also ported in rustc in the
|
[`chalk/chalk-rules/src/clauses.rs`][chalk_rules]. They are also ported in
|
||||||
[`librustc_traits`][librustc_traits] crate.
|
rustc in the [`librustc_traits`][librustc_traits] crate.
|
||||||
|
|
||||||
[chalk_rules]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rules.rs
|
[chalk_rules]: https://github.com/rust-lang/chalk/blob/master/chalk-rules/src/clauses.rs
|
||||||
[librustc_traits]: https://github.com/rust-lang/rust/tree/master/src/librustc_traits
|
[librustc_traits]: https://github.com/rust-lang/rust/tree/master/src/librustc_traits
|
||||||
|
|
||||||
## Lowering where clauses
|
## Lowering where clauses
|
||||||
|
|
|
||||||
|
|
@ -11,14 +11,14 @@ to prove it using the lowered rules we described in the
|
||||||
[lowering rules](./lowering-rules.md) chapter. If we are able to prove it, we
|
[lowering rules](./lowering-rules.md) chapter. If we are able to prove it, we
|
||||||
say that the construct is well-formed. If not, we report an error to the user.
|
say that the construct is well-formed. If not, we report an error to the user.
|
||||||
|
|
||||||
Well-formedness checking happens in the [`src/rules/wf.rs`][wf] module in
|
Well-formedness checking happens in the [`chalk/chalk-rules/src/wf.rs`][wf]
|
||||||
chalk. After you have read this chapter, you may find useful to see an
|
module in chalk. After you have read this chapter, you may find useful to see
|
||||||
extended set of examples in the [`src/rules/wf/test.rs`][wf_test] submodule.
|
an extended set of examples in the [`chalk/src/test/wf.rs`][wf_test] submodule.
|
||||||
|
|
||||||
The new-style WF checking has not been implemented in rustc yet.
|
The new-style WF checking has not been implemented in rustc yet.
|
||||||
|
|
||||||
[wf]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rules/wf.rs
|
[wf]: https://github.com/rust-lang/chalk/blob/master/chalk-rules/src/wf.rs
|
||||||
[wf_test]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rules/wf/test.rs
|
[wf_test]: https://github.com/rust-lang/chalk/blob/master/src/test/wf.rs
|
||||||
|
|
||||||
We give here a complete reference of the generated goals for each Rust
|
We give here a complete reference of the generated goals for each Rust
|
||||||
declaration.
|
declaration.
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue