From 0130cf34413feedf15c91f90fded196632db3495 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Thu, 10 May 2018 15:22:12 -0700 Subject: [PATCH 1/8] Added an overview of chalk --- src/SUMMARY.md | 1 + src/chalk-overview.md | 140 ++++++++++++++++++++++++++++++++++++++++++ src/traits-slg.md | 2 + 3 files changed, 143 insertions(+) create mode 100644 src/chalk-overview.md diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 1839f59c..4923d497 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -38,6 +38,7 @@ - [The lowering module in rustc](./traits-lowering-module.md) - [Well-formedness checking](./traits-wf.md) - [The SLG solver](./traits-slg.md) + - [An Overview of Chalk](./chalk-overview.md) - [Bibliography](./traits-bibliography.md) - [Type checking](./type-checking.md) - [Method Lookup](./method-lookup.md) diff --git a/src/chalk-overview.md b/src/chalk-overview.md new file mode 100644 index 00000000..63757f7b --- /dev/null +++ b/src/chalk-overview.md @@ -0,0 +1,140 @@ +# An Overview of Chalk + +> Chalk is under heavy development, so if any of these links are broken or if +> any of the information is inconsistent with the code or outdated, please open +> an issue so we can fix it. If you are able to fix the issue yourself, we would +> love your contribution! + +[Chalk][chalk] recasts Rust's trait system explicitly in terms of logic +programming by "lowering" Rust code into a kind of logic program we can then +execute queries against. Its goal is to be an executable, highly readable +specification of the Rust trait system.[^negativechalk] + +There are many expected benefits from this work. It will consolidate our +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.[^negativechalk] + +## 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/) + +## 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 +of testing to be able to run chalk on its own, so chalk includes a parser for a +Rust-like syntax. + +The parser takes that syntax and produces an [Abstract Syntax Tree (AST)][ast]. +You can find the [complete definition of the AST][chalk-ast] in the source code. + +The syntax contains things from Rust that we know and love for example traits, +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 + +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: + +* A [clause] of the form `consequence :- conditions` where `:-` is read as + "if" and `conditions = cond1 && cond2 && ...` +* A universally quantified clause of the form `forall { consequence :- conditions }` + * `forall { ... }` is used to represent [universal quantification]. See the + section on [Lowering to logic][lowering-forall] for more information. + * A key thing to note about `forall` is that we don't allow you to "quantify" + over traits, only types and regions (lifetimes). That is, you can't make a + rule like `forall { u32: Trait }` which would say "`u32` implements + all traits". You can however say `forall { T: Trait }` meaning "`Trait` + is implemented by all types". + * `forall { ... }` is represented in the code using the [`Binders` + struct][binders-struct]. + +This is the phase where we encode the rules of the trait system into logic. For +example, if we have: + +```rust +impl Clone for Vec {} +``` + +We generate: + +```rust +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 + +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. + +## 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 +`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`, we would represent `Foo` as a +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 +`ir::ProgramEnvironment` which is "pure logic". The main field in that is +`program_clauses` which contains the `ProgramClause`s that we generated +previously. + +## Rules + +The `rules` module works by iterating over every trait, impl, etc. and emitting +the rules that come from each one. The traits section of the rustc-guide (that +you are currently reading) contains the most up-to-date reference on that. + +The `ir::ProgramEnvironment` is created [in this module][rules-environment]. + +## Testing + +TODO: Basically, [there is a macro](https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/solve/test/mod.rs#L112-L148) +that will take syntax and run it through the full pipeline described above. +[This](https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/solve/test/mod.rs#L83-L110) +is the function that is ultimately called. + +## Solver + +See [The SLG Solver][slg]. + +[^negativechalk]: [*Negative reasoning in Chalk* by Aaron Turon](http://aturon.github.io/blog/2017/04/24/negative-chalk/) + +[chalk]: https://github.com/rust-lang-nursery/chalk +[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]: traits-lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses +[programclause]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/mod.rs#L721 +[clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause +[well-formedness-checks]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/lowering/mod.rs#L230-L232 +[ir-code]: https://github.com/rust-lang-nursery/chalk/blob/master/src/ir/mod.rs +[HIR]: hir.html +[binders-struct]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/mod.rs#L661 +[rules-environment]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/rules/mod.rs#L9 +[slg]: traits-slg.html diff --git a/src/traits-slg.md b/src/traits-slg.md index cdd52ece..1dc56e14 100644 --- a/src/traits-slg.md +++ b/src/traits-slg.md @@ -1 +1,3 @@ # The SLG solver + +TODO: From e34946fd9a8021545149e7531b1aa53b90383790 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Thu, 10 May 2018 15:43:18 -0700 Subject: [PATCH 2/8] Lines must be <= 80 characters UNLESS there is a link --- src/chalk-overview.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/chalk-overview.md b/src/chalk-overview.md index 63757f7b..8c5bc159 100644 --- a/src/chalk-overview.md +++ b/src/chalk-overview.md @@ -54,7 +54,8 @@ essentially one of the following: * A [clause] of the form `consequence :- conditions` where `:-` is read as "if" and `conditions = cond1 && cond2 && ...` -* A universally quantified clause of the form `forall { consequence :- conditions }` +* A universally quantified clause of the form + `forall { consequence :- conditions }` * `forall { ... }` is used to represent [universal quantification]. See the section on [Lowering to logic][lowering-forall] for more information. * A key thing to note about `forall` is that we don't allow you to "quantify" @@ -129,7 +130,7 @@ See [The SLG Solver][slg]. [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]: traits-lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses +[lowering-forall]: https://rust-lang-nursery.github.io/rustc-guide/traits-lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses [programclause]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/mod.rs#L721 [clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause [well-formedness-checks]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/lowering/mod.rs#L230-L232 From 9c8e72a6892a4b7a8b34202fc79d8b3192641938 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Thu, 10 May 2018 15:48:24 -0700 Subject: [PATCH 3/8] Ignoring code examples that aren't actually compile-able --- src/chalk-overview.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/chalk-overview.md b/src/chalk-overview.md index 8c5bc159..49f68514 100644 --- a/src/chalk-overview.md +++ b/src/chalk-overview.md @@ -69,13 +69,13 @@ essentially one of the following: This is the phase where we encode the rules of the trait system into logic. For example, if we have: -```rust +```rust,ignore impl Clone for Vec {} ``` We generate: -```rust +```rust,ignore forall { (Vec: Clone) :- (T: Clone) } ``` From a6b9870c6c3f8cba667fe37f8964101ee178c566 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Fri, 11 May 2018 17:14:26 -0700 Subject: [PATCH 4/8] Updating links to match latest code --- src/chalk-overview.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/chalk-overview.md b/src/chalk-overview.md index 49f68514..7cea6ace 100644 --- a/src/chalk-overview.md +++ b/src/chalk-overview.md @@ -115,9 +115,9 @@ The `ir::ProgramEnvironment` is created [in this module][rules-environment]. ## Testing -TODO: Basically, [there is a macro](https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/solve/test/mod.rs#L112-L148) +TODO: Basically, [there is a macro](https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/solve/test.rs#L112-L148) that will take syntax and run it through the full pipeline described above. -[This](https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/solve/test/mod.rs#L83-L110) +[This](https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/solve/test.rs#L83-L110) is the function that is ultimately called. ## Solver @@ -131,11 +131,11 @@ See [The SLG Solver][slg]. [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]: https://rust-lang-nursery.github.io/rustc-guide/traits-lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses -[programclause]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/mod.rs#L721 +[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 -[well-formedness-checks]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/lowering/mod.rs#L230-L232 -[ir-code]: https://github.com/rust-lang-nursery/chalk/blob/master/src/ir/mod.rs +[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/ir.rs [HIR]: hir.html -[binders-struct]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/mod.rs#L661 -[rules-environment]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/rules/mod.rs#L9 +[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]: traits-slg.html From 3f5ba4ee63848428563f824f0861af482a2ca59a Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Mon, 14 May 2018 10:52:21 -0700 Subject: [PATCH 5/8] Changes from review --- src/chalk-overview.md | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/chalk-overview.md b/src/chalk-overview.md index 7cea6ace..cd2c98b8 100644 --- a/src/chalk-overview.md +++ b/src/chalk-overview.md @@ -1,19 +1,20 @@ # An Overview of Chalk > Chalk is under heavy development, so if any of these links are broken or if -> any of the information is inconsistent with the code or outdated, please open -> an issue so we can fix it. If you are able to fix the issue yourself, we would +> any of the information is inconsistent with the code or outdated, please +> [open an issue][rustc-issues] so we can fix it. If you are able to fix the issue yourself, we would > love your contribution! [Chalk][chalk] recasts Rust's trait system explicitly in terms of logic programming by "lowering" Rust code into a kind of logic program we can then -execute queries against. Its goal is to be an executable, highly readable -specification of the Rust trait system.[^negativechalk] +execute queries against. (See [*Lowering to Logic*][lowering-to-logic] and +[*Lowering Rules*][lowering-rules]) Its goal is to be an executable, highly +readable specification of the Rust trait system. There are many expected benefits from this work. It will consolidate our 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.[^negativechalk] +extend. ## Resources @@ -124,9 +125,10 @@ is the function that is ultimately called. See [The SLG Solver][slg]. -[^negativechalk]: [*Negative reasoning in Chalk* by Aaron Turon](http://aturon.github.io/blog/2017/04/24/negative-chalk/) - +[rustc-issues]: https://github.com/rust-lang-nursery/rustc-guide/issues [chalk]: https://github.com/rust-lang-nursery/chalk +[lowering-to-logic]: traits-lowering-to-logic.html +[lowering-rules]: traits-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 From d9a22957a90ba7f1e7b1e54fbcdae39854fe6d96 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Mon, 14 May 2018 11:18:14 -0700 Subject: [PATCH 6/8] More review changes --- src/chalk-overview.md | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/src/chalk-overview.md b/src/chalk-overview.md index cd2c98b8..926c7f5a 100644 --- a/src/chalk-overview.md +++ b/src/chalk-overview.md @@ -2,8 +2,8 @@ > Chalk is under heavy development, so if any of these links are broken or if > any of the information is inconsistent with the code or outdated, please -> [open an issue][rustc-issues] so we can fix it. If you are able to fix the issue yourself, we would -> love your contribution! +> [open an issue][rustc-issues] so we can fix it. If you are able to fix the +> issue yourself, we would love your contribution! [Chalk][chalk] recasts Rust's trait system explicitly in terms of logic programming by "lowering" Rust code into a kind of logic program we can then @@ -42,7 +42,7 @@ Rust-like syntax. The parser takes that syntax and produces an [Abstract Syntax Tree (AST)][ast]. You can find the [complete definition of the AST][chalk-ast] in the source code. -The syntax contains things from Rust that we know and love for example traits, +The syntax contains things from Rust that we know and love, for example: traits, 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. @@ -67,14 +67,14 @@ essentially one of the following: * `forall { ... }` is represented in the code using the [`Binders` struct][binders-struct]. -This is the phase where we encode the rules of the trait system into logic. For -example, if we have: +Lowering is the phase 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 {} ``` -We generate: +We generate the following program clause: ```rust,ignore forall { (Vec: Clone) :- (T: Clone) } @@ -102,22 +102,23 @@ 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`). In addition to `ir::Program` which has "rust-like things", there is also -`ir::ProgramEnvironment` which is "pure logic". The main field in that is +`ir::ProgramEnvironment` which is "pure logic". The main field in that struct is `program_clauses` which contains the `ProgramClause`s that we generated previously. ## Rules The `rules` module works by iterating over every trait, impl, etc. and emitting -the rules that come from each one. The traits section of the rustc-guide (that -you are currently reading) contains the most up-to-date reference on that. +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]. ## 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 syntax and run it through the full pipeline described above. +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. From 71a66d2d7ca50b8fdf7a33d16df2d1f61b1c2449 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Mon, 14 May 2018 11:21:20 -0700 Subject: [PATCH 7/8] Even more review changes --- src/chalk-overview.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/chalk-overview.md b/src/chalk-overview.md index 926c7f5a..02e09429 100644 --- a/src/chalk-overview.md +++ b/src/chalk-overview.md @@ -37,7 +37,8 @@ extend. 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 of testing to be able to run chalk on its own, so chalk includes a parser for a -Rust-like syntax. +Rust-like syntax. This syntax is orthogonal to the Rust AST and grammar. It is +not intended to look exactly like it or support the exact same syntax. The parser takes that syntax and produces an [Abstract Syntax Tree (AST)][ast]. You can find the [complete definition of the AST][chalk-ast] in the source code. From e1cf1f67b27e090fcc5f3e3d8bf6298b9bd036a6 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Mon, 14 May 2018 11:26:15 -0700 Subject: [PATCH 8/8] Missed a few things because of GitHub's UI --- src/chalk-overview.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/chalk-overview.md b/src/chalk-overview.md index 02e09429..76c119a5 100644 --- a/src/chalk-overview.md +++ b/src/chalk-overview.md @@ -68,6 +68,8 @@ essentially one of the following: * `forall { ... }` is represented in the code using the [`Binders` struct][binders-struct]. +*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: @@ -137,6 +139,7 @@ See [The SLG Solver][slg]. [lowering-forall]: https://rust-lang-nursery.github.io/rustc-guide/traits-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]: traits-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/ir.rs [HIR]: hir.html