From 05e67188737682ae191b5df35f12268f918d0fac Mon Sep 17 00:00:00 2001 From: Mark Mansi Date: Wed, 23 May 2018 12:30:10 -0500 Subject: fix remaining links --- src/doc/rustc-dev-guide/src/SUMMARY.md | 6 +- src/doc/rustc-dev-guide/src/appendix/glossary.md | 30 ++--- src/doc/rustc-dev-guide/src/chalk-overview.md | 148 --------------------- src/doc/rustc-dev-guide/src/mir/borrowck.md | 12 +- src/doc/rustc-dev-guide/src/mir/index.md | 4 +- src/doc/rustc-dev-guide/src/mir/passes.md | 2 +- src/doc/rustc-dev-guide/src/mir/regionck.md | 8 +- .../rustc-dev-guide/src/trait-specialization.md | 42 ------ .../rustc-dev-guide/src/traits/canonicalization.md | 2 +- .../rustc-dev-guide/src/traits/chalk-overview.md | 148 +++++++++++++++++++++ src/doc/rustc-dev-guide/src/traits/index.md | 2 +- .../rustc-dev-guide/src/traits/specialization.md | 42 ++++++ src/doc/rustc-dev-guide/src/type-checking.md | 2 +- src/doc/rustc-dev-guide/src/variance.md | 2 +- 14 files changed, 225 insertions(+), 225 deletions(-) delete mode 100644 src/doc/rustc-dev-guide/src/chalk-overview.md delete mode 100644 src/doc/rustc-dev-guide/src/trait-specialization.md create mode 100644 src/doc/rustc-dev-guide/src/traits/chalk-overview.md create mode 100644 src/doc/rustc-dev-guide/src/traits/specialization.md (limited to 'src/doc/rustc-dev-guide') diff --git a/src/doc/rustc-dev-guide/src/SUMMARY.md b/src/doc/rustc-dev-guide/src/SUMMARY.md index a2b7d3e1302..8efe304b73f 100644 --- a/src/doc/rustc-dev-guide/src/SUMMARY.md +++ b/src/doc/rustc-dev-guide/src/SUMMARY.md @@ -26,7 +26,7 @@ - [Higher-ranked trait bounds](./traits/hrtb.md) - [Caching subtleties](./traits/caching.md) - [Specialization](./traits/specialization.md) -- [Trait solving (new-style)](./traits.md) +- [Trait solving (new-style)](./traits/index.md) - [Lowering to logic](./traits/lowering-to-logic.md) - [Goals and clauses](./traits/goals-and-clauses.md) - [Equality and associated types](./traits/associated-types.md) @@ -38,12 +38,12 @@ - [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) + - [An Overview of Chalk](./traits/chalk-overview.md) - [Bibliography](./traits/bibliography.md) - [Type checking](./type-checking.md) - [Method Lookup](./method-lookup.md) - [Variance](./variance.md) -- [The MIR (Mid-level IR)](./mir.md) +- [The MIR (Mid-level IR)](./mir/index.md) - [MIR construction](./mir/construction.md) - [MIR visitor and traversal](./mir/visitor.md) - [MIR passes: getting the MIR for a function](./mir/passes.md) diff --git a/src/doc/rustc-dev-guide/src/appendix/glossary.md b/src/doc/rustc-dev-guide/src/appendix/glossary.md index a37f1b22fc0..ad2604e63cf 100644 --- a/src/doc/rustc-dev-guide/src/appendix/glossary.md +++ b/src/doc/rustc-dev-guide/src/appendix/glossary.md @@ -7,18 +7,18 @@ them better. Term | Meaning ------------------------|-------- AST | the abstract syntax tree produced by the syntax crate; reflects user syntax very closely. -binder | a "binder" is a place where a variable or type is declared; for example, the `` is a binder for the generic type parameter `T` in `fn foo(..)`, and \|`a`\|` ...` is a binder for the parameter `a`. See [the background chapter for more](./appendix-background.html#free-vs-bound) -bound variable | a "bound variable" is one that is declared within an expression/term. For example, the variable `a` is bound within the closure expession \|`a`\|` a * 2`. See [the background chapter for more](./appendix-background.html#free-vs-bound) +binder | a "binder" is a place where a variable or type is declared; for example, the `` is a binder for the generic type parameter `T` in `fn foo(..)`, and \|`a`\|` ...` is a binder for the parameter `a`. See [the background chapter for more](./appendix/background.html#free-vs-bound) +bound variable | a "bound variable" is one that is declared within an expression/term. For example, the variable `a` is bound within the closure expession \|`a`\|` a * 2`. See [the background chapter for more](./appendix/background.html#free-vs-bound) codegen unit | when we produce LLVM IR, we group the Rust code into a number of codegen units. Each of these units is processed by LLVM independently from one another, enabling parallelism. They are also the unit of incremental re-use. completeness | completeness is a technical term in type theory. Completeness means that every type-safe program also type-checks. Having both soundness and completeness is very hard, and usually soundness is more important. (see "soundness"). -control-flow graph | a representation of the control-flow of a program; see [the background chapter for more](./appendix-background.html#cfg) +control-flow graph | a representation of the control-flow of a program; see [the background chapter for more](./appendix/background.html#cfg) cx | we tend to use "cx" as an abbrevation for context. See also `tcx`, `infcx`, etc. DAG | a directed acyclic graph is used during compilation to keep track of dependencies between queries. ([see more](incremental-compilation.html)) -data-flow analysis | a static analysis that figures out what properties are true at each point in the control-flow of a program; see [the background chapter for more](./appendix-background.html#dataflow) +data-flow analysis | a static analysis that figures out what properties are true at each point in the control-flow of a program; see [the background chapter for more](./appendix/background.html#dataflow) DefId | an index identifying a definition (see `librustc/hir/def_id.rs`). Uniquely identifies a `DefPath`. Double pointer | a pointer with additional metadata. See "fat pointer" for more. Fat pointer | a two word value carrying the address of some value, along with some further information necessary to put the value to use. Rust includes two kinds of "fat pointers": references to slices, and trait objects. A reference to a slice carries the starting address of the slice and its length. A trait object carries a value's address and a pointer to the trait's implementation appropriate to that value. "Fat pointers" are also known as "wide pointers", and "double pointers". -free variable | a "free variable" is one that is not bound within an expression or term; see [the background chapter for more](./appendix-background.html#free-vs-bound) +free variable | a "free variable" is one that is not bound within an expression or term; see [the background chapter for more](./appendix/background.html#free-vs-bound) 'gcx | the lifetime of the global arena ([see more](ty.html)) generics | the set of generic type parameters defined on a type or item HIR | the High-level IR, created by lowering and desugaring the AST ([see more](hir.html)) @@ -32,36 +32,36 @@ IR | Intermediate Representation. A general term in compil local crate | the crate currently being compiled. LTO | Link-Time Optimizations. A set of optimizations offered by LLVM that occur just before the final binary is linked. These include optmizations like removing functions that are never used in the final program, for example. _ThinLTO_ is a variant of LTO that aims to be a bit more scalable and efficient, but possibly sacrifices some optimizations. You may also read issues in the Rust repo about "FatLTO", which is the loving nickname given to non-Thin LTO. LLVM documentation: [here][lto] and [here][thinlto] [LLVM] | (actually not an acronym :P) an open-source compiler backend. It accepts LLVM IR and outputs native binaries. Various languages (e.g. Rust) can then implement a compiler front-end that output LLVM IR and use LLVM to compile to all the platforms LLVM supports. -MIR | the Mid-level IR that is created after type-checking for use by borrowck and trans ([see more](./mir.html)) +MIR | the Mid-level IR that is created after type-checking for use by borrowck and trans ([see more](./mir/index.html)) miri | an interpreter for MIR used for constant evaluation ([see more](./miri.html)) -normalize | a general term for converting to a more canonical form, but in the case of rustc typically refers to [associated type normalization](./traits-associated-types.html#normalize) +normalize | a general term for converting to a more canonical form, but in the case of rustc typically refers to [associated type normalization](./traits/associated-types.html#normalize) newtype | a "newtype" is a wrapper around some other type (e.g., `struct Foo(T)` is a "newtype" for `T`). This is commonly used in Rust to give a stronger type for indices. -NLL | [non-lexical lifetimes](./mir-regionck.html), an extension to Rust's borrowing system to make it be based on the control-flow graph. +NLL | [non-lexical lifetimes](./mir/regionck.html), an extension to Rust's borrowing system to make it be based on the control-flow graph. node-id or NodeId | an index identifying a particular node in the AST or HIR; gradually being phased out and replaced with `HirId`. -obligation | something that must be proven by the trait system ([see more](trait-resolution.html)) -projection | a general term for a "relative path", e.g. `x.f` is a "field projection", and `T::Item` is an ["associated type projection"](./traits-goals-and-clauses.html#trait-ref) -promoted constants | constants extracted from a function and lifted to static scope; see [this section](./mir.html#promoted) for more details. +obligation | something that must be proven by the trait system ([see more](traits/resolution.html)) +projection | a general term for a "relative path", e.g. `x.f` is a "field projection", and `T::Item` is an ["associated type projection"](./traits/goals-and-clauses.html#trait-ref) +promoted constants | constants extracted from a function and lifted to static scope; see [this section](./mir/index.html#promoted) for more details. provider | the function that executes a query ([see more](query.html)) -quantified | in math or logic, existential and universal quantification are used to ask questions like "is there any type T for which is true?" or "is this true for all types T?"; see [the background chapter for more](./appendix-background.html#quantified) +quantified | in math or logic, existential and universal quantification are used to ask questions like "is there any type T for which is true?" or "is this true for all types T?"; see [the background chapter for more](./appendix/background.html#quantified) query | perhaps some sub-computation during compilation ([see more](query.html)) region | another term for "lifetime" often used in the literature and in the borrow checker. sess | the compiler session, which stores global data used throughout compilation side tables | because the AST and HIR are immutable once created, we often carry extra information about them in the form of hashtables, indexed by the id of a particular node. sigil | like a keyword but composed entirely of non-alphanumeric tokens. For example, `&` is a sigil for references. -skolemization | a way of handling subtyping around "for-all" types (e.g., `for<'a> fn(&'a u32)`) as well as solving higher-ranked trait bounds (e.g., `for<'a> T: Trait<'a>`). See [the chapter on skolemization and universes](./mir-regionck.html#skol) for more details. +skolemization | a way of handling subtyping around "for-all" types (e.g., `for<'a> fn(&'a u32)`) as well as solving higher-ranked trait bounds (e.g., `for<'a> T: Trait<'a>`). See [the chapter on skolemization and universes](./mir/regionck.html#skol) for more details. soundness | soundness is a technical term in type theory. Roughly, if a type system is sound, then if a program type-checks, it is type-safe; i.e. I can never (in safe rust) force a value into a variable of the wrong type. (see "completeness"). span | a location in the user's source code, used for error reporting primarily. These are like a file-name/line-number/column tuple on steroids: they carry a start/end point, and also track macro expansions and compiler desugaring. All while being packed into a few bytes (really, it's an index into a table). See the Span datatype for more. substs | the substitutions for a given generic type or item (e.g. the `i32`, `u32` in `HashMap`) tcx | the "typing context", main data structure of the compiler ([see more](ty.html)) 'tcx | the lifetime of the currently active inference context ([see more](ty.html)) -trait reference | the name of a trait along with a suitable set of input type/lifetimes ([see more](./traits-goals-and-clauses.html#trait-ref)) +trait reference | the name of a trait along with a suitable set of input type/lifetimes ([see more](./traits/goals-and-clauses.html#trait-ref)) token | the smallest unit of parsing. Tokens are produced after lexing ([see more](the-parser.html)). [TLS] | Thread-Local Storage. Variables may be defined so that each thread has its own copy (rather than all threads sharing the variable). This has some interactions with LLVM. Not all platforms support TLS. trans | the code to translate MIR into LLVM IR. trait reference | a trait and values for its type parameters ([see more](ty.html)). ty | the internal representation of a type ([see more](ty.html)). UFCS | Universal Function Call Syntax. An unambiguous syntax for calling a method ([see more](type-checking.html)). -variance | variance determines how changes to a generic type/lifetime parameter affect subtyping; for example, if `T` is a subtype of `U`, then `Vec` is a subtype `Vec` because `Vec` is *covariant* in its generic parameter. See [the background chapter](./appendix-background.html#variance) for a more general explanation. See the [variance chapter](./variance.html) for an explanation of how type checking handles variance. +variance | variance determines how changes to a generic type/lifetime parameter affect subtyping; for example, if `T` is a subtype of `U`, then `Vec` is a subtype `Vec` because `Vec` is *covariant* in its generic parameter. See [the background chapter](./appendix/background.html#variance) for a more general explanation. See the [variance chapter](./variance.html) for an explanation of how type checking handles variance. Wide pointer | a pointer with additional metadata. See "fat pointer" for more. [LLVM]: https://llvm.org/ diff --git a/src/doc/rustc-dev-guide/src/chalk-overview.md b/src/doc/rustc-dev-guide/src/chalk-overview.md deleted file mode 100644 index 76c119a5ed3..00000000000 --- a/src/doc/rustc-dev-guide/src/chalk-overview.md +++ /dev/null @@ -1,148 +0,0 @@ -# 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][rustc-issues] 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. (See [*Lowering to Logic*][lowering-to-logic] and -[*Lowering Rules*][lowering-rules]) Its goal is to be an executable, highly -readable specification of the Rust trait system. - -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. - -## 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. 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)][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]. - -*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: - -```rust,ignore -impl Clone for Vec {} -``` - -We generate the following program clause: - -```rust,ignore -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 struct 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. See [Lowering Rules][lowering-rules] for 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/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. - -## Solver - -See [The SLG Solver][slg]. - -[rustc-issues]: https://github.com/rust-lang-nursery/rustc-guide/issues -[chalk]: https://github.com/rust-lang-nursery/chalk -[lowering-to-logic]: traits-lowering-to-logic.html -[lowering-rules]: traits-lowering-rules.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 -[universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification -[lowering-forall]: https://rust-lang-nursery.github.io/rustc-guide/traits-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]: traits-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/blob/master/src/ir.rs -[HIR]: hir.html -[binders-struct]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L661 -[rules-environment]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/rules.rs#L9 -[slg]: traits-slg.html diff --git a/src/doc/rustc-dev-guide/src/mir/borrowck.md b/src/doc/rustc-dev-guide/src/mir/borrowck.md index 51a6c6cbf26..cd83843f89d 100644 --- a/src/doc/rustc-dev-guide/src/mir/borrowck.md +++ b/src/doc/rustc-dev-guide/src/mir/borrowck.md @@ -21,7 +21,7 @@ Doing borrow checking on MIR has two key advantages: can see [a list of bugs that the MIR-based borrow checker fixes here][47366].) - Even more importantly, using the MIR enables ["non-lexical lifetimes"][nll], - which are regions derived from the control-flow graph. + which are regions derived from the control-flow graph. [47366]: https://github.com/rust-lang/rust/issues/47366 [nll]: http://rust-lang.github.io/rfcs/2094-nll.html @@ -43,17 +43,17 @@ The overall flow of the borrow checker is as follows: include references to the new regions that we are computing. - We then invoke `nll::replace_regions_in_mir` to modify this copy C. Among other things, this function will replace all of the regions in - the MIR with fresh [inference variables](./appendix-glossary.html). - - (More details can be found in [the regionck section](./mir-regionck.html).) + the MIR with fresh [inference variables](./appendix/glossary.html). + - (More details can be found in [the regionck section](./mir/regionck.html).) - Next, we perform a number of [dataflow - analyses](./appendix-background.html#dataflow) + analyses](./appendix/background.html#dataflow) that compute what data is moved and when. The results of these analyses are needed to do both borrow checking and region inference. - Using the move data, we can then compute the values of all the regions in the MIR. - - (More details can be found in [the NLL section](./mir-regionck.html).) + - (More details can be found in [the NLL section](./mir/regionck.html).) - Finally, the borrow checker itself runs, taking as input (a) the results of move analysis and (b) the regions computed by the region checker. This allows us to figure out which loans are still in scope at any particular point. - + diff --git a/src/doc/rustc-dev-guide/src/mir/index.md b/src/doc/rustc-dev-guide/src/mir/index.md index 81bbf6bd686..838048b81a4 100644 --- a/src/doc/rustc-dev-guide/src/mir/index.md +++ b/src/doc/rustc-dev-guide/src/mir/index.md @@ -26,7 +26,7 @@ Some of the key characteristics of MIR are: - It does not have nested expressions. - All types in MIR are fully explicit. -[cfg]: ./appendix-background.html#cfg +[cfg]: ./appendix/background.html#cfg ## Key MIR vocabulary @@ -244,4 +244,4 @@ but [you can read about those below](#promoted)). [mir]: https://github.com/rust-lang/rust/tree/master/src/librustc/mir [mirmanip]: https://github.com/rust-lang/rust/tree/master/src/librustc_mir [mir]: https://github.com/rust-lang/rust/tree/master/src/librustc/mir -[newtype'd]: appendix-glossary.html +[newtype'd]: appendix/glossary.html diff --git a/src/doc/rustc-dev-guide/src/mir/passes.md b/src/doc/rustc-dev-guide/src/mir/passes.md index 64e72f06e45..a5b5df10a99 100644 --- a/src/doc/rustc-dev-guide/src/mir/passes.md +++ b/src/doc/rustc-dev-guide/src/mir/passes.md @@ -174,4 +174,4 @@ alternatives in [rust-lang/rust#41710]. [rust-lang/rust#41710]: https://github.com/rust-lang/rust/issues/41710 [mirtransform]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/transform/ [`NoLandingPads`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/transform/no_landing_pads/struct.NoLandingPads.html -[MIR visitor]: mir-visitor.html +[MIR visitor]: mir/visitor.html diff --git a/src/doc/rustc-dev-guide/src/mir/regionck.md b/src/doc/rustc-dev-guide/src/mir/regionck.md index e67e91138c0..90f6fa2749f 100644 --- a/src/doc/rustc-dev-guide/src/mir/regionck.md +++ b/src/doc/rustc-dev-guide/src/mir/regionck.md @@ -35,7 +35,7 @@ The MIR-based region analysis consists of two major functions: - More details to come, though the [NLL RFC] also includes fairly thorough (and hopefully readable) coverage. -[fvb]: appendix-background.html#free-vs-bound +[fvb]: appendix/background.html#free-vs-bound [NLL RFC]: http://rust-lang.github.io/rfcs/2094-nll.html ## Universal regions @@ -131,7 +131,7 @@ the type of `foo` the type `bar` expects We handle this sort of subtyping by taking the variables that are bound in the supertype and **skolemizing** them: this means that we replace them with -[universally quantified](appendix-background.html#quantified) +[universally quantified](appendix/background.html#quantified) representatives, written like `!1`. We call these regions "skolemized regions" -- they represent, basically, "some unknown region". @@ -148,7 +148,7 @@ what we wanted. So let's work through what happens next. To check if two functions are subtypes, we check if their arguments have the desired relationship -(fn arguments are [contravariant](./appendix-background.html#variance), so +(fn arguments are [contravariant](./appendix/background.html#variance), so we swap the left and right here): ```text @@ -187,7 +187,7 @@ Here, the root universe would consist of the lifetimes `'static` and the same concept to types, in which case the types `Foo` and `T` would be in the root universe (along with other global types, like `i32`). Basically, the root universe contains all the names that -[appear free](./appendix-background.html#free-vs-bound) in the body of `bar`. +[appear free](./appendix/background.html#free-vs-bound) in the body of `bar`. Now let's extend `bar` a bit by adding a variable `x`: diff --git a/src/doc/rustc-dev-guide/src/trait-specialization.md b/src/doc/rustc-dev-guide/src/trait-specialization.md deleted file mode 100644 index 671e5e01682..00000000000 --- a/src/doc/rustc-dev-guide/src/trait-specialization.md +++ /dev/null @@ -1,42 +0,0 @@ -# Specialization - -**TODO**: where does Chalk fit in? Should we mention/discuss it here? - -Defined in the `specialize` module. - -The basic strategy is to build up a *specialization graph* during -coherence checking (recall that coherence checking looks for overlapping -impls). Insertion into the graph locates the right place -to put an impl in the specialization hierarchy; if there is no right -place (due to partial overlap but no containment), you get an overlap -error. Specialization is consulted when selecting an impl (of course), -and the graph is consulted when propagating defaults down the -specialization hierarchy. - -You might expect that the specialization graph would be used during -selection – i.e. when actually performing specialization. This is -not done for two reasons: - -- It's merely an optimization: given a set of candidates that apply, - we can determine the most specialized one by comparing them directly - for specialization, rather than consulting the graph. Given that we - also cache the results of selection, the benefit of this - optimization is questionable. - -- To build the specialization graph in the first place, we need to use - selection (because we need to determine whether one impl specializes - another). Dealing with this reentrancy would require some additional - mode switch for selection. Given that there seems to be no strong - reason to use the graph anyway, we stick with a simpler approach in - selection, and use the graph only for propagating default - implementations. - -Trait impl selection can succeed even when multiple impls can apply, -as long as they are part of the same specialization family. In that -case, it returns a *single* impl on success – this is the most -specialized impl *known* to apply. However, if there are any inference -variables in play, the returned impl may not be the actual impl we -will use at trans time. Thus, we take special care to avoid projecting -associated types unless either (1) the associated type does not use -`default` and thus cannot be overridden or (2) all input types are -known concretely. diff --git a/src/doc/rustc-dev-guide/src/traits/canonicalization.md b/src/doc/rustc-dev-guide/src/traits/canonicalization.md index 37a59026b42..f87de5f814f 100644 --- a/src/doc/rustc-dev-guide/src/traits/canonicalization.md +++ b/src/doc/rustc-dev-guide/src/traits/canonicalization.md @@ -41,7 +41,7 @@ trait query: `?A: Foo<'static, ?B>`, where `?A` and `?B` are unbound. This query contains two unbound variables, but it also contains the lifetime `'static`. The trait system generally ignores all lifetimes and treats them equally, so when canonicalizing, we will *also* -replace any [free lifetime](./appendix-background.html#free-vs-bound) with a +replace any [free lifetime](./appendix/background.html#free-vs-bound) with a canonical variable. Therefore, we get the following result: ```text diff --git a/src/doc/rustc-dev-guide/src/traits/chalk-overview.md b/src/doc/rustc-dev-guide/src/traits/chalk-overview.md new file mode 100644 index 00000000000..e737edcd912 --- /dev/null +++ b/src/doc/rustc-dev-guide/src/traits/chalk-overview.md @@ -0,0 +1,148 @@ +# 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][rustc-issues] 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. (See [*Lowering to Logic*][lowering-to-logic] and +[*Lowering Rules*][lowering-rules]) Its goal is to be an executable, highly +readable specification of the Rust trait system. + +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. + +## 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. 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)][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]. + +*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: + +```rust,ignore +impl Clone for Vec {} +``` + +We generate the following program clause: + +```rust,ignore +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 struct 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. See [Lowering Rules][lowering-rules] for 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/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. + +## Solver + +See [The SLG Solver][slg]. + +[rustc-issues]: https://github.com/rust-lang-nursery/rustc-guide/issues +[chalk]: https://github.com/rust-lang-nursery/chalk +[lowering-to-logic]: traits/lowering-to-logic.html +[lowering-rules]: traits/lowering-rules.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 +[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/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L721 +[clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause +[goals-and-clauses]: ./traits/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/blob/master/src/ir.rs +[HIR]: hir.html +[binders-struct]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L661 +[rules-environment]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/rules.rs#L9 +[slg]: ./traits/slg.html diff --git a/src/doc/rustc-dev-guide/src/traits/index.md b/src/doc/rustc-dev-guide/src/traits/index.md index 6aad2474d02..2dabd0b6967 100644 --- a/src/doc/rustc-dev-guide/src/traits/index.md +++ b/src/doc/rustc-dev-guide/src/traits/index.md @@ -4,7 +4,7 @@ [process of being implemented][wg]; this chapter serves as a kind of in-progress design document. If you would prefer to read about how the current trait solver works, check out -[this other chapter](./trait-resolution.html). (By the way, if you +[this other chapter](./traits/resolution.html). (By the way, if you would like to help in hacking on the new solver, you will find instructions for getting involved in the [Traits Working Group tracking issue][wg].) 🚧 diff --git a/src/doc/rustc-dev-guide/src/traits/specialization.md b/src/doc/rustc-dev-guide/src/traits/specialization.md new file mode 100644 index 00000000000..671e5e01682 --- /dev/null +++ b/src/doc/rustc-dev-guide/src/traits/specialization.md @@ -0,0 +1,42 @@ +# Specialization + +**TODO**: where does Chalk fit in? Should we mention/discuss it here? + +Defined in the `specialize` module. + +The basic strategy is to build up a *specialization graph* during +coherence checking (recall that coherence checking looks for overlapping +impls). Insertion into the graph locates the right place +to put an impl in the specialization hierarchy; if there is no right +place (due to partial overlap but no containment), you get an overlap +error. Specialization is consulted when selecting an impl (of course), +and the graph is consulted when propagating defaults down the +specialization hierarchy. + +You might expect that the specialization graph would be used during +selection – i.e. when actually performing specialization. This is +not done for two reasons: + +- It's merely an optimization: given a set of candidates that apply, + we can determine the most specialized one by comparing them directly + for specialization, rather than consulting the graph. Given that we + also cache the results of selection, the benefit of this + optimization is questionable. + +- To build the specialization graph in the first place, we need to use + selection (because we need to determine whether one impl specializes + another). Dealing with this reentrancy would require some additional + mode switch for selection. Given that there seems to be no strong + reason to use the graph anyway, we stick with a simpler approach in + selection, and use the graph only for propagating default + implementations. + +Trait impl selection can succeed even when multiple impls can apply, +as long as they are part of the same specialization family. In that +case, it returns a *single* impl on success – this is the most +specialized impl *known* to apply. However, if there are any inference +variables in play, the returned impl may not be the actual impl we +will use at trans time. Thus, we take special care to avoid projecting +associated types unless either (1) the associated type does not use +`default` and thus cannot be overridden or (2) all input types are +known concretely. diff --git a/src/doc/rustc-dev-guide/src/type-checking.md b/src/doc/rustc-dev-guide/src/type-checking.md index cb6d346e4c2..9a161abd211 100644 --- a/src/doc/rustc-dev-guide/src/type-checking.md +++ b/src/doc/rustc-dev-guide/src/type-checking.md @@ -6,7 +6,7 @@ draws heavily on the [type inference] and [trait solving].) [typeck]: https://github.com/rust-lang/rust/tree/master/src/librustc_typeck [type inference]: type-inference.html -[trait solving]: trait-resolution.html +[trait solving]: traits/resolution.html ## Type collection diff --git a/src/doc/rustc-dev-guide/src/variance.md b/src/doc/rustc-dev-guide/src/variance.md index 08399b5b3af..05a286c075c 100644 --- a/src/doc/rustc-dev-guide/src/variance.md +++ b/src/doc/rustc-dev-guide/src/variance.md @@ -2,7 +2,7 @@ For a more general background on variance, see the [background] appendix. -[background]: ./appendix-background.html +[background]: ./appendix/background.html During type checking we must infer the variance of type and lifetime parameters. The algorithm is taken from Section 4 of the paper ["Taming the -- cgit 1.4.1-3-g733a5