From 0130cf34413feedf15c91f90fded196632db3495 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Thu, 10 May 2018 15:22:12 -0700 Subject: [PATCH] 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: