Walkthrough

This section shows a sample session in the chalk repl, and then gives a tour through the code to give you an idea of the phases involved.

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

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 of testing to be able to run chalk on its own, so chalk includes a parser for a 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). You can find the complete definition of the 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.

Rust Intermediate Representation (chalk_solve::rust_ir)

After getting the AST we convert it to a more convenient intermediate representation called chalk_rust_ir. This is sort of analogous to the HIR in Rust. The process of converting to IR is called lowering.

The chalk::program::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 chalk::program::Program, we use numeric indices (ItemId).

The IR source 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 && ...
• A universally quantified clause of the form forall<T> { consequence :- conditions }
  • forall<T> { ... } is used to represent universal quantification. See the section on Lowering to logic 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<Trait> { u32: Trait } which would say "u32 implements all traits". You can however say forall<T> { T: Trait } meaning "Trait is implemented by all types".
  • forall<T> { ... } is represented in the code using the Binders<T> struct.

See also: Goals and Clauses

This is where we encode the rules of the trait system into logic. For example, if we have the following Rust:

impl<T: Clone> Clone for Vec<T> {}

We generate the following program clause:

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

Similar to chalk::program::Program which has "rust-like things", chalk_ir defines ProgramEnvironment which is "pure logic". The main field in that struct is program_clauses, which contains the ProgramClauses generated by the rules module.

Rules (chalk_solve)

The chalk_solve crate (source code) 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

Well-formedness checks

As part of lowering to logic, we also do some "well formedness" checks. See the chalk_solve::wf source code for where those are done.

See also: Well-formedness checking

Coherence

The method CoherenceSolver::specialization_priorities in the coherence module (source code) checks "coherence", which means that it ensures that two impls of the same trait for the same type cannot exist.

Solver (chalk_solve)

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 also: The SLG Solver

Crates

Chalk's functionality is broken up into the following crates:

• chalk_engine: Defines the core SLG solver.
• chalk_ir: Defines chalk's internal representation of types, lifetimes, and goals.
• chalk_solve: Combines chalk_ir and chalk_engine, effectively, which implements logic rules converting chalk_rust_ir to chalk_ir
  • Contains the rust_ir module, which defines the "HIR-like" Rust IR
  • Defines the coherence module, which implements coherence rules
  • chalk_engine::context provides the necessary hooks.
• chalk_parse: Defines the raw AST and a parser.
• chalk: Brings everything together. Defines the following modules:
  • chalk::lowering, which converts AST to chalk_rust_ir
  • Also includes chalki, chalk's REPL.

Browse source code on GitHub

Testing

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.

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. 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 chalk_rust_ir, and the well-formedness checks that occur after that.

Testing internals

Goal tests use a 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.

Likewise, lowering tests use the lowering_success! and lowering_error! macros.

More Resources

• Chalk Source Code
• Chalk Glossary