Merge pull request #406 from detrumi/book-improvements

Book improvements

Author: detrumi

README.md

@@ -7,6 +7,8 @@
 A [Prolog-ish][Prolog] interpreter written in Rust, intended perhaps for use in
 the compiler, but also for experimentation.
 
+See the [Chalk book](https://rust-lang.github.io/chalk/book/) for more information.
+
 ## FAQ
 
 **How does chalk relate to rustc?** The plan is to have rustc use the `chalk-engine` crate (in this repo), which defines chalk's solver. The rest of chalk can then be considered an elaborate unit testing harness. For more details, see [the Traits chapter of the rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/traits/index.html).
@@ -51,8 +53,9 @@ Unique; substitution [], lifetime constraints []
 If you'd like to contribute, consider joining the [Traits Working Group][working-group].
 We hang out on the [rust-lang zulip][rust-lang-zulip] in the [#wg-traits][wg-traits-stream] stream.
 
-See [CONTRIBUTING.md](CONTRIBUTING.md) for more info.
+See [the contributing chapter][contributing] in the chalk book for more info.
 
 [working-group]: https://rust-lang.github.io/compiler-team/working-groups/traits/
 [rust-lang-zulip]:https://rust-lang.zulipchat.com
 [wg-traits-stream]: https://rust-lang.zulipchat.com/#narrow/stream/144729-wg-traits
+[contributing]: https://rust-lang.github.io/chalk/book/contributing.html

book/src/SUMMARY.md

@@ -2,17 +2,15 @@
 
 - [What is Chalk?](./what_is_chalk.md)
     - [Crates](./what_is_chalk/crates.md)
+    - [REPL](./what_is_chalk/repl.md)
 - [Contribution guide](./contribution_guide.md)
-- [REPL](./repl.md)
-- [Representing and manipulating Rust types](./types.md)
-    - [The role of the `Interner`](./types/role_of_interner.md)
-    - [Controlling representation with `Interner`](./types/how_to_control_repr.md)
+- [Representing and manipulating types](./types.md)
+    - [The `Interner`](./types/role_of_interner.md)
     - [Rust types](./types/rust_types.md)
         - [Application types](./types/rust_types/application_ty.md)
     - [Rust lifetimes](./types/rust_lifetimes.md)
     - [Operations](./types/operations.md)
         - [Fold and the Folder trait](./types/operations/fold.md)
-- [Representing traits, impls, and other parts of Rust programs](./rust_ir.md)
 - [Lowering Rust IR to logic](./clauses.md)
     - [Goals and clauses](./clauses/goals_and_clauses.md)
     - [Type equality and unification](./clauses/type_equality.md)
@@ -21,7 +19,7 @@
     - [Well-formedness checking](./clauses/wf.md)
 - [Canonical queries](./canonical_queries.md)
     - [Canonicalization](./canonical_queries/canonicalization.md)
-- [How does the engine work](./engine.md)
+- [Chalk engine](./engine.md)
     - [Major concepts](./engine/major_concepts.md)
     - [Logic](./engine/logic.md)
         - [Coinduction](./engine/logic/coinduction.md)

book/src/contribution_guide.md

@@ -1 +1,75 @@
 # Contribution guide
+
+Thank you for your interest in contributing to chalk! There are many ways to
+contribute, and we appreciate all of them.
+
+* [Bug Reports](#bug-reports)
+* [Running and Debugging](#running-and-debugging)
+* [Pull Requests](#pull-requests)
+* [Writing Documentation](#writing-documentation)
+
+If you'd like to contribute, consider joining the [Traits Working Group][traits-working-group].
+We hang out on the [rust-lang zulip][rust-lang-zulip] in the [#wg-traits][wg-traits-stream] stream.
+
+As a reminder, all contributors are expected to follow our [Code of Conduct][coc].
+
+[traits-working-group]: https://rust-lang.github.io/compiler-team/working-groups/traits/
+[rust-lang-zulip]:https://rust-lang.zulipchat.com
+[wg-traits-stream]: https://rust-lang.zulipchat.com/#narrow/stream/144729-wg-traits
+[coc]: https://www.rust-lang.org/conduct.html
+
+## Bug Reports
+[bug-reports]: #bug-reports
+
+While bugs are unfortunate, they're a reality in software. We can't fix what we
+don't know about, so please report liberally. If you're not sure if something
+is a bug or not, feel free to file a bug anyway.
+
+If you have the chance, before reporting a bug, please search existing issues,
+as it's possible that someone else has already reported your error. This doesn't
+always work, and sometimes it's hard to know what to search for, so consider
+this extra credit. We won't mind if you accidentally file a duplicate report.
+
+Sometimes, a backtrace is helpful, and so including that is nice. To get
+a backtrace, set the `RUST_BACKTRACE` environment variable to a value
+other than `0`. The easiest way to do this is to invoke `chalk` like this:
+
+```bash
+$ RUST_BACKTRACE=1 chalk ...
+```
+
+## Running and Debugging
+[running-and-debugging]: #running-and-debugging
+There is a repl mainly for debugging purposes which can be run by `cargo run`. Some basic examples are in [libstd.chalk](https://github.com/rust-lang/chalk/blob/master/libstd.chalk):
+```bash
+$ cargo run
+?- load libstd.chalk
+?- Vec<Box<i32>>: Clone
+Unique; substitution [], lifetime constraints []
+```
+
+More logging can be enabled by setting the `CHALK_DEBUG` environment variable. Set `CHALK_DEBUG=1` to see `info!(...)` output, and `CHALK_DEBUG=2` to see `debug!(...)` output as well.
+
+## Pull Requests
+[pull-requests]: #pull-requests
+
+Pull requests are the primary mechanism we use to change Rust. GitHub itself
+has some [great documentation][pull-request-documentation] on using the Pull Request feature.
+We use the "fork and pull" model [described here][development-models], where
+contributors push changes to their personal fork and create pull requests to
+bring those changes into the source repository.
+
+Please make pull requests against the `master` branch.
+
+[pull-request-documentation]: https://help.github.com/articles/about-pull-requests/
+[development-models]: https://help.github.com/articles/about-collaborative-development-models/
+
+## Writing Documentation
+[writing-documentation]: #writing-documentation
+
+Documentation improvements are very welcome. Documentation pull requests
+function in the same way as other pull requests.
+
+You can find documentation style guidelines in [RFC 1574][rfc1574].
+
+[rfc1574]: https://github.com/rust-lang/rfcs/blob/master/text/1574-more-api-documentation-conventions.md#appendix-a-full-conventions-text

book/src/rust_ir.md

@@ -1,5 +1,23 @@
 # Representing and manipulating Rust types
 
+## Intermediate representations
+
+Intermediate representations (IR) are used to represent parts of Rust programs such as traits and impls.
+
+Chalk contains three levels of IR:
+
+- The **AST**. This is used purely for writing test cases
+  with a Rust-like syntax. This is consumed by **lowering** code, which
+  takes AST and products **Rust IR** (the next bullet point).
+- The **Rust IR**. This is a "HIR-like" notation that defines the
+  interesting properties of things like traits, impls, and structs.
+  It is an input to the **rules** code, which produces
+- The **Chalk IR**. This is most "Prolog-like" of the various IRs. It
+  contains the definition of **types** as well as prolog-like concepts
+  such as goals (things that must be proven true) and clauses (things
+  that are assumed to be true).
+
+
 ## Goal of the chalk-ir crate
 
 To have an ergonomic, flexible library that can abstractly represent
@@ -44,8 +62,8 @@ Chalk as of today to match this document:
 * Extract `TypeName` into something opaque to chalk-ir.
 * Dyn type equality should probably be driven by entailment.
 * Projections need to be renamed to aliases.
-* The variant we use for impl traits should be removed and folded into type aliases. 
+* The variant we use for impl traits should be removed and folded into type aliases.
 * Remove placeholders and projection placeholders from apply and create placeholder types.
 * Move `Error` from a `TypeName` to its own variant.
 * Introduce `GeneratorWitness` into chalk
-* Complete transition from `ForAll` to `Fn` in chalk 
+* Complete transition from `ForAll` to `Fn` in chalk

book/src/types.md

@@ -5,7 +5,7 @@ Most everything in the IR is parameterized by the [`Interner`] trait:
 [`Interner`]: http://rust-lang.github.io/chalk/chalk_ir/interner/trait.Interner.html
 
 ```rust,ignore
-trait Interner: Copy + Clone + Debug + Eq + Ord { 
+trait Interner: Copy + Clone + Debug + Eq + Ord {
     ..
 }
 ```
@@ -16,3 +16,72 @@ the interner is defined by the embedded and can be used to control
 other things in memory. For example, the `Interner` trait could be
 used to intern all the types, as rustc does, or it could be used to
 `Box` them instead, as the chalk testing harness currently does.
+
+### Controlling representation with `Interner`
+
+The purpose of the [`Interner`] trait is to give control over how
+types and other bits of chalk-ir are represented in memory. This is
+done via an "indirection" strategy. We'll explain that strategy here
+in terms of [`Ty`] and [`TyData`], the two types used to represent
+Rust types, but the same pattern is repeated for many other things.
+
+[`Interner`]: http://rust-lang.github.io/chalk/chalk_ir/interner/trait.Interner.html
+[`Ty`]: http://rust-lang.github.io/chalk/chalk_ir/struct.Ty.html
+[`TyData`]: http://rust-lang.github.io/chalk/chalk_ir/enum.TyData.html
+
+Types are represented by a [`Ty<I>`] type and the [`TyData<I>`] enum.
+There is no *direct* connection between them. The link is rather made
+by the [`Interner`] trait, via the [`InternedTy`] associated type:
+
+[`Ty<I>`]: http://rust-lang.github.io/chalk/chalk_ir/struct.Ty.html
+[`TyData<I>`]: http://rust-lang.github.io/chalk/chalk_ir/enum.TyData.html
+[`InternedTy`]: http://rust-lang.github.io/chalk/chalk_ir/interner/trait.Interner.html#associatedtype.InternedType
+
+```rust,ignore
+struct Ty<I: Interner>(I::InternedTy);
+enum TyData<I: Interner> { .. }
+```
+
+The way this works is that the [`Interner`] trait has an associated
+type [`InternedTy`] and two related methods, [`intern_ty`] and [`ty_data`]:
+
+[`intern_ty`]: http://rust-lang.github.io/chalk/chalk_ir/interner/trait.Interner.html#tymethod.intern_ty
+[`ty_data`]: http://rust-lang.github.io/chalk/chalk_ir/interner/trait.Interner.html#tymethod.ty_data
+
+```rust,ignore
+trait Interner {
+    type InternedTy;
+
+    fn intern_ty(&self, data: &TyData<Self>) -> Self::InternedTy;
+    fn ty_data(data: &Self::InternedTy) -> &TyData<Self>;
+}
+```
+
+However, as a user you are not meant to use these directly. Rather,
+they are encapsulated in methods on the [`Ty`] and [`TyData`] types:
+
+```rust,ignore
+impl<I: Interner> Ty<I> {
+  fn data(&self) -> &TyData<I> {
+    I::lookup_ty(self)
+  }
+}
+```
+
+and
+
+```rust,ignore
+impl<I: Interner> TyData<I> {
+  fn intern(&self, I: &I) -> Ty<I> {
+    Ty(i.intern_ty(self))
+  }
+}
+```
+
+Note that there is an assumption here that [`ty_data`] needs no
+context. This effectively constrains the [`InternedTy`] representation
+to be a `Box` or `&` type. To be more general, at the cost of some
+convenience, we could make that a method as well, so that one would
+invoke `ty.data(i)` instead of just `ty.data()`. This would permit us
+to use (for example) integers to represent interned types, which might
+be nice (e.g., to permit using generational indices).

book/src/types/how_to_control_repr.md

@@ -206,7 +206,7 @@ Likewise, lowering tests use the [`lowering_success!` and
 ## More Resources
 
 * [Chalk Source Code](https://github.com/rust-lang/chalk)
-* [Chalk Glossary](https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md)
+* [Chalk Glossary](glossary.md)
 
 [goals-and-clauses]: ./clauses/goals_and_clauses.html
 [HIR]: https://rustc-dev-guide.rust-lang.org/hir.html

book/src/types/role_of_interner.md

@@ -17,7 +17,7 @@ other programs:
 
 The following crate is an implementation detail, used internally by `chalk-solve`:
 
-* The `chalk-engine` crate, which defines the actual engine that solves logical predicate. This 
+* The `chalk-engine` crate, which defines the actual engine that solves logical predicate. This
   engine is quite general and not really specific to Rust.
 * The `chalk-derive` crate defines custom derives for the `chalk_ir::fold::Fold` trait and other
   such things.
@@ -35,3 +35,42 @@ define a kind of "minimal embedding" of chalk.
   `chalk-rust-ir` by a process called "lowering'.
 * Finally, the main `chalk` crate, along with the testing crate in the
   `tests` directory, define the actual entry points.
+
+## The chalk-solve crate
+
+| The `chalk-solve` crate | |
+|---|--- |
+| Purpose:  | to solve a given goal |
+| Depends on IR:  | chalk-ir and rust-ir   |
+| Context required:  | `RustIrDatabase` |
+
+The `chalk-solve` crate exposes a key type called `Solver`.  This is a
+solver that, given a goal (expressed in chalk-ir) will solve the goal
+and yield up a `Solution`. The solver caches intermediate data between
+invocations, so solving the same goal twice in a row (or solving goals
+with common subgoals) is faster.
+
+The solver is configured by a type that implements the
+`RustIrDatabase` trait. This trait contains some callbacks that
+provide needed context for the solver -- notably, the solver can ask:
+
+- **What are the program clauses that might solve given rule?** This
+  is answered by the code in the chalk-solve crate.
+- **Is this trait coinductive?** This is answered by the chalk-ir.
+
+
+## The chalk-engine crate
+
+| The `chalk-engine` crate  |   |
+|---|--- |
+| Purpose:  | define the base solving strategy |
+| IR:  | none   |
+| Context required:  | `Context` trait |
+
+For the purposes of chalk, the `chalk-engine` crate is effectively
+encapsulated by `chalk-solve`.  It defines the base SLG engine. It is
+written in a very generic style that knows next to nothing about Rust
+itself. The engine can be configured via the traits defined in
+`chalk_engine::context::Context`, which contain (for example)
+associated types that define what a goal or clause is, as well as
+functions that operate on those things.

book/src/what_is_chalk.md

@@ -0,0 +1,9 @@
+# REPL
+
+There is a repl mainly for debugging purposes which can be run by `cargo run`. Some basic examples are in [libstd.chalk](https://github.com/rust-lang/chalk/blob/master/libstd.chalk):
+```bash
+$ cargo run
+?- load libstd.chalk
+?- Vec<Box<i32>>: Clone
+Unique; substitution [], lifetime constraints []
+```