Skip to content

Update chalk overview #223

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Nov 2, 2018
Merged

Update chalk overview #223

Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
90716dc
Add section on chalk structure
tmandry Oct 30, 2018
b62fe76
Move Resources to bottom
tmandry Oct 30, 2018
d2238c3
Move Crates section down
tmandry Oct 30, 2018
b5024c3
Chalk Overview: Update old content
tmandry Oct 30, 2018
7f14c82
Chalk Overview: Organize and sort links
tmandry Oct 30, 2018
cf2682a
Chalk Overview: Fill in testing section
tmandry Oct 30, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
229 changes: 169 additions & 60 deletions src/traits/chalk-overview.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,23 +16,45 @@ 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.

## Resources
## Chalk Structure

* [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)
Chalk has two main "products". The first of these is the
[`chalk_engine`][chalk_engine] crate, which defines the core [SLG
solver][slg]. This is the part rustc uses.

### Blog Posts
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.

* [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/)
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<T> { }
| trait Clone { }
| impl<T> Clone for Vec<T> where T: Clone { }
| impl Clone for Foo { }

?- Vec<Foo>: Clone
Unique; substitution [], lifetime constraints []

?- Vec<Bar>: Clone
No possible solution.

?- exists<T> { Vec<T>: Clone }
Ambiguous; no inference guidance
```

You can see more examples of programs and queries in the [unit
tests][chalk-test-example].

## Parsing
Next we'll go through each stage required to produce the output above.

### 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
Expand All @@ -48,11 +70,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 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*.

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:
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
"if" and `conditions = cond1 && cond2 && ...`
Expand All @@ -70,8 +104,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<T: Clone> Clone for Vec<T> {}
Expand All @@ -86,63 +120,138 @@ forall<T> { (Vec<T>: Clone) :- (T: Clone) }
This rule dictates that `Vec<T>: 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.

#### 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]*

#### Well-formedness checks

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.

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.
*See also: [Well-formedness checking][wf-checking]*

## Intermediate Representation (IR)
#### Coherence

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.
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.

For example, if you have a type like `Foo<Bar>`, we would represent `Foo` as a
string in the AST but in `ir::Program`, we use numeric indices (`ItemId`).
### Solver ([chalk_solve])

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.
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*.

## Rules
*See also: [The SLG Solver][slg]*

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.
## Crates

The `ir::ProgramEnvironment` is created [in this module][rules-environment].
Chalk's functionality is broken up into the following crates:
- [**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**][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.
- [**chalk**][doc-chalk]: Brings everything together. Defines the following
modules:
- [`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
- Also includes [chalki][chalki], chalk's REPL.

[Browse source code on GitHub](https://github.com/rust-lang-nursery/chalk)

## 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].

## Solver
The main kind of tests in chalk are **goal tests**. They contain a program,
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I made this name up, but it seemed reasonable to me!

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.

See [The SLG Solver][slg].
**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.

[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
### 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

* [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

* [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/)

[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://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
[HIR]: ../hir.html

[`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-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
[ir-code]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rust_ir.rs
[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
[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