From 90716dc9da1a4d72507d3dea24caab286657df32 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Mon, 29 Oct 2018 21:59:17 -0500 Subject: [PATCH 1/6] Add section on chalk structure --- src/traits/chalk-overview.md | 65 ++++++++++++++++++++++++++++++++++++ 1 file changed, 65 insertions(+) diff --git a/src/traits/chalk-overview.md b/src/traits/chalk-overview.md index 3473a0764..029b1460e 100644 --- a/src/traits/chalk-overview.md +++ b/src/traits/chalk-overview.md @@ -16,6 +16,71 @@ 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. +## Chalk Structure +Chalk has two main "products". The first of these is the +[`chalk_engine`][doc-chalk-engine] crate, which defines the core [SLG +solver][slg]. This is the part rustc uses. + +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. + +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-tests]. + +[chalk-tests]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115 + +### Crates +- [**chalk_engine**][doc-chalk-engine]: Defines the core [SLG solver][slg]. +- [**chalk_ir**][doc-chalk-ir]: Defines chalk's internal representation of + types, lifetimes, and goals. +- [**chalk_solve**][doc-chalk-solve]: Combines `chalk_ir` and `chalk_engine`, + effectively. + - [`chalk_engine::context`][engine-context] provides the necessary hooks. +- [**chalk_parse**][doc-chalk-parse]: Defines the raw AST and a parser. +- [**chalk**][doc-chalk]: Brings everything together. Defines the following + modules: + - [`rust_ir`][doc-chalk-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][doc-chalki], chalk's REPL. + +[Browse source on GitHub](https://github.com/rust-lang-nursery/chalk) + +[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-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-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-rust-ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rules/index.html +[doc-chalki]: https://rust-lang-nursery.github.io/chalk/doc/chalki/index.html + ## Resources * [Chalk Source Code](https://github.com/rust-lang-nursery/chalk) From b62fe76a354ec60835d6e83d6a6ff70b17515fc3 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Mon, 29 Oct 2018 22:19:58 -0500 Subject: [PATCH 2/6] Move Resources to bottom --- src/traits/chalk-overview.md | 34 +++++++++++++++------------------- 1 file changed, 15 insertions(+), 19 deletions(-) diff --git a/src/traits/chalk-overview.md b/src/traits/chalk-overview.md index 029b1460e..20a71ef87 100644 --- a/src/traits/chalk-overview.md +++ b/src/traits/chalk-overview.md @@ -50,7 +50,7 @@ Ambiguous; no inference guidance You can see more examples of programs and queries in the [unit tests][chalk-tests]. -[chalk-tests]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115 +Next we'll go through each stage required to produce the output above. ### Crates - [**chalk_engine**][doc-chalk-engine]: Defines the core [SLG solver][slg]. @@ -80,22 +80,7 @@ You can see more examples of programs and queries in the [unit tests][chalk-test [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 [doc-chalki]: https://rust-lang-nursery.github.io/chalk/doc/chalki/index.html - -## Resources - -* [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) - -### 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/) +[chalk-tests]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115 ## Parsing @@ -190,9 +175,20 @@ 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. -## Solver +## 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 -See [The SLG Solver][slg]. +* [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 From d2238c30b7837ec1bd6411b5a01ef3c8e2807604 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Mon, 29 Oct 2018 22:22:14 -0500 Subject: [PATCH 3/6] Move Crates section down Nest existing content under Chalk Structure. I think it reads better this way. --- src/traits/chalk-overview.md | 73 ++++++++++++++++++++---------------- 1 file changed, 40 insertions(+), 33 deletions(-) diff --git a/src/traits/chalk-overview.md b/src/traits/chalk-overview.md index 20a71ef87..4abe0ac02 100644 --- a/src/traits/chalk-overview.md +++ b/src/traits/chalk-overview.md @@ -17,6 +17,7 @@ expressive, which should behave better in corner cases, and be much easier to extend. ## Chalk Structure + Chalk has two main "products". The first of these is the [`chalk_engine`][doc-chalk-engine] crate, which defines the core [SLG solver][slg]. This is the part rustc uses. @@ -52,37 +53,9 @@ You can see more examples of programs and queries in the [unit tests][chalk-test Next we'll go through each stage required to produce the output above. -### Crates -- [**chalk_engine**][doc-chalk-engine]: Defines the core [SLG solver][slg]. -- [**chalk_ir**][doc-chalk-ir]: Defines chalk's internal representation of - types, lifetimes, and goals. -- [**chalk_solve**][doc-chalk-solve]: Combines `chalk_ir` and `chalk_engine`, - effectively. - - [`chalk_engine::context`][engine-context] provides the necessary hooks. -- [**chalk_parse**][doc-chalk-parse]: Defines the raw AST and a parser. -- [**chalk**][doc-chalk]: Brings everything together. Defines the following - modules: - - [`rust_ir`][doc-chalk-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][doc-chalki], chalk's REPL. - -[Browse source on GitHub](https://github.com/rust-lang-nursery/chalk) - -[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-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-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-rust-ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rules/index.html -[doc-chalki]: https://rust-lang-nursery.github.io/chalk/doc/chalki/index.html [chalk-tests]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115 -## Parsing +### Parsing 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 @@ -98,7 +71,7 @@ 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 +### Lowering After parsing, there is a "lowering" phase. This aims to convert traits/impls into "program clauses". A [`ProgramClause` (source code)][programclause] is @@ -136,7 +109,7 @@ 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 +#### Well-formedness checks 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 @@ -144,7 +117,7 @@ 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) +### Intermediate Representation (IR) The second intermediate representation in chalk is called, well, the "ir". :) The [IR source code][ir-code] contains the complete definition. The @@ -159,7 +132,7 @@ In addition to `ir::Program` which has "rust-like things", there is also `program_clauses` which contains the `ProgramClause`s that we generated previously. -## Rules +### Rules 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 @@ -167,6 +140,40 @@ most up-to-date reference on that. The `ir::ProgramEnvironment` is created [in this module][rules-environment]. +### Solver + +See [The SLG Solver][slg]. + +## Crates + +Chalk's functionality is broken up into the following crates: +- [**chalk_engine**][doc-chalk-engine]: Defines the core [SLG solver][slg]. +- [**chalk_ir**][doc-chalk-ir]: Defines chalk's internal representation of + types, lifetimes, and goals. +- [**chalk_solve**][doc-chalk-solve]: Combines `chalk_ir` and `chalk_engine`, + effectively. + - [`chalk_engine::context`][engine-context] provides the necessary hooks. +- [**chalk_parse**][doc-chalk-parse]: Defines the raw AST and a parser. +- [**chalk**][doc-chalk]: Brings everything together. Defines the following + modules: + - [`rust_ir`][doc-chalk-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][doc-chalki], chalk's REPL. + +[Browse source on GitHub](https://github.com/rust-lang-nursery/chalk) + +[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-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-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-rust-ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rules/index.html +[doc-chalki]: https://rust-lang-nursery.github.io/chalk/doc/chalki/index.html + ## Testing TODO: Basically, [there is a macro](https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/solve/test.rs#L112-L148) From b5024c3a7328eecdccb37edbfe376c6ac99f2004 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Mon, 29 Oct 2018 22:31:59 -0500 Subject: [PATCH 4/6] Chalk Overview: Update old content --- src/traits/chalk-overview.md | 99 +++++++++++++++++++++--------------- 1 file changed, 59 insertions(+), 40 deletions(-) diff --git a/src/traits/chalk-overview.md b/src/traits/chalk-overview.md index 4abe0ac02..5e0f147ca 100644 --- a/src/traits/chalk-overview.md +++ b/src/traits/chalk-overview.md @@ -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 -### Parsing +### 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 @@ -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 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`, 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 && ...` @@ -93,8 +105,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 {} @@ -109,54 +121,61 @@ 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. -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 + +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 -### Intermediate Representation (IR) +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 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: [Well-formedness checking][wf-checking]* -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`). +[rules-wf-src]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf.rs -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. +#### Coherence -### Rules +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. -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-src]: https://github.com/rust-lang-nursery/chalk/blob/master/src/coherence.rs -The `ir::ProgramEnvironment` is created [in this module][rules-environment]. +### Solver ([chalk_solve]) -### Solver +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 [The SLG Solver][slg]. +*See also: [The SLG Solver][slg]* ## Crates Chalk's functionality is broken up into the following crates: - [**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. - [**chalk_solve**][doc-chalk-solve]: Combines `chalk_ir` and `chalk_engine`, effectively. - [`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 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` - `rules`, which implements logic rules converting `rust_ir` to `chalk_ir` - `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 [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-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-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 ## Testing @@ -201,15 +221,14 @@ is the function that is ultimately called. [chalk]: https://github.com/rust-lang-nursery/chalk [lowering-to-logic]: ./lowering-to-logic.html [lowering-rules]: ./lowering-rules.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 [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 +[ir-code]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rust_ir.rs [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 From 7f14c8254e501a418836f8c1fe979d746e847df2 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Tue, 30 Oct 2018 17:20:29 -0500 Subject: [PATCH 5/6] Chalk Overview: Organize and sort links --- src/traits/chalk-overview.md | 67 +++++++++++++++++------------------- 1 file changed, 32 insertions(+), 35 deletions(-) diff --git a/src/traits/chalk-overview.md b/src/traits/chalk-overview.md index 5e0f147ca..1a6e72bec 100644 --- a/src/traits/chalk-overview.md +++ b/src/traits/chalk-overview.md @@ -19,7 +19,7 @@ extend. ## Chalk Structure Chalk has two main "products". The first of these is the -[`chalk_engine`][doc-chalk-engine] crate, which defines the core [SLG +[`chalk_engine`][chalk_engine] crate, which defines the core [SLG solver][slg]. This is the part rustc uses. The rest of chalk can be considered an elaborate testing harness. Chalk is @@ -53,8 +53,6 @@ You can see more examples of programs and queries in the [unit tests][chalk-test 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 - ### Parsing ([chalk_parse]) Chalk is designed to be incorporated with the Rust compiler, so the syntax and @@ -134,10 +132,6 @@ 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 As part of lowering to logic, we also do some "well formedness" checks. See @@ -145,16 +139,12 @@ the [`rules::wf` source code][rules-wf-src] for where those are done. *See also: [Well-formedness checking][wf-checking]* -[rules-wf-src]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf.rs - #### Coherence 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. -[coherence-src]: https://github.com/rust-lang-nursery/chalk/blob/master/src/coherence.rs - ### Solver ([chalk_solve]) Finally, when we've collected all the program clauses we care about, we want @@ -166,10 +156,10 @@ queries is called the *solver*. ## Crates Chalk's functionality is broken up into the following crates: -- [**chalk_engine**][doc-chalk-engine]: Defines the core [SLG solver][slg]. +- [**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**][doc-chalk-solve]: Combines `chalk_ir` and `chalk_engine`, +- [**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. @@ -179,20 +169,9 @@ Chalk's functionality is broken up into the following crates: - `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][doc-chalki], chalk's REPL. - -[Browse source on GitHub](https://github.com/rust-lang-nursery/chalk) - -[engine-context]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/context/index.html + - Also includes [chalki][chalki], chalk's REPL. -[doc-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 -[doc-chalk-solve]: https://rust-lang-nursery.github.io/chalk/doc/chalk_solve/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 -[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 +[Browse source code on GitHub](https://github.com/rust-lang-nursery/chalk) ## Testing @@ -217,19 +196,37 @@ is the function that is ultimately called. * [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 +[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://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-tests]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115 +[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 -[goals-and-clauses]: ./goals-and-clauses.html +[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 -[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 -[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 From cf2682ae86e6f026395e7bdfc3ed1bf3a34e6d5b Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Tue, 30 Oct 2018 18:03:42 -0500 Subject: [PATCH 6/6] Chalk Overview: Fill in testing section --- src/traits/chalk-overview.md | 39 +++++++++++++++++++++++++++++------- 1 file changed, 32 insertions(+), 7 deletions(-) diff --git a/src/traits/chalk-overview.md b/src/traits/chalk-overview.md index 1a6e72bec..59572479d 100644 --- a/src/traits/chalk-overview.md +++ b/src/traits/chalk-overview.md @@ -49,7 +49,8 @@ No possible solution. Ambiguous; no inference guidance ``` -You can see more examples of programs and queries in the [unit tests][chalk-tests]. +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. @@ -175,11 +176,29 @@ Chalk's functionality is broken up into the following crates: ## 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]. + +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. + +**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 @@ -222,7 +241,10 @@ is the function that is ultimately called. [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-tests]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115 +[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 @@ -230,3 +252,6 @@ is the function that is ultimately called. [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