Restructure some chapters

Author: detrumi

book/src/SUMMARY.md

@@ -2,11 +2,10 @@
 
 - [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)
@@ -21,7 +20,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/types/how_to_control_repr.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/role_of_interner.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/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 []
+```