numerous edits
This commit is contained in:
Niko Matsakis
parent
53115310f7
commit
95f9957277
|
|
@ -24,11 +24,11 @@
|
|||
- [Trait solving (new-style)](./traits.md)
|
||||
- [Lowering to logic](./traits-lowering-to-logic.md)
|
||||
- [Goals and clauses](./traits-goals-and-clauses.md)
|
||||
- [Lowering rules](./traits-lowering-rules.md)
|
||||
- [Equality and associated types](./traits-associated-types.md)
|
||||
- [Region constraints](./traits-regions.md)
|
||||
- [Canonical queries](./traits-canonical-queries.md)
|
||||
- [Canonicalization](./traits-canonicalization.md)
|
||||
- [Equality and associated types](./traits-associated-types.md)
|
||||
- [Region constraints](./traits-regions.md)
|
||||
- [Lowering rules](./traits-lowering-rules.md)
|
||||
- [Well-formedness checking](./traits-wf.md)
|
||||
- [The SLG solver](./traits-slg.md)
|
||||
- [Bibliography](./traits-bibliography.md)
|
||||
|
|
|
|||
|
|
@ -31,10 +31,12 @@ LTO | Link-Time Optimizations. A set of optimizations offer
|
|||
[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))
|
||||
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)
|
||||
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.
|
||||
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.
|
||||
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](./background.html#quantified)
|
||||
|
|
@ -49,6 +51,7 @@ span | a location in the user's source code, used for error
|
|||
substs | the substitutions for a given generic type or item (e.g. the `i32`, `u32` in `HashMap<i32, u32>`)
|
||||
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))
|
||||
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.
|
||||
|
|
|
|||
|
|
@ -20,6 +20,8 @@ that syntax is expanded during
|
|||
["type collection"](./type-checking.html) into the explicit form,
|
||||
though that is something we may want to change in the future.)
|
||||
|
||||
<a name=normalize>
|
||||
|
||||
In some cases, associated type projections can be **normalized** --
|
||||
that is, simplified -- based on the types given in an impl. So, to
|
||||
continue with our example, the impl of `IntoIterator` for `Option<T>`
|
||||
|
|
|
|||
|
|
@ -12,12 +12,14 @@ a few new superpowers.
|
|||
In Rust's solver, **goals** and **clauses** have the following forms
|
||||
(note that the two definitions reference one another):
|
||||
|
||||
Goal = DomainGoal
|
||||
Goal = DomainGoal // defined in the section below
|
||||
| Goal && Goal
|
||||
| Goal || Goal
|
||||
| exists<K> { Goal } // existential quantification
|
||||
| forall<K> { Goal } // universal quantification
|
||||
| if (Clause) { Goal } // implication
|
||||
| true // something that's trivially true
|
||||
| ambiguous // something that's never provable
|
||||
|
||||
Clause = DomainGoal
|
||||
| Clause :- Goal // if can prove Goal, then Clause is true
|
||||
|
|
@ -39,9 +41,11 @@ gives the details.
|
|||
|
||||
## Domain goals
|
||||
|
||||
<a name=trait-ref>
|
||||
|
||||
To define the set of *domain goals* in our system, we need to first
|
||||
introduce a few simple formulations. A **trait reference** consists of
|
||||
the name of a trait allow with a suitable set of inputs P0..Pn:
|
||||
the name of a trait along with a suitable set of inputs P0..Pn:
|
||||
|
||||
TraitRef = P0: TraitName<P1..Pn>
|
||||
|
||||
|
|
@ -50,7 +54,9 @@ IntoIterator`. Note that Rust surface syntax also permits some extra
|
|||
things, like associated type bindings (`Vec<T>: IntoIterator<Item =
|
||||
T>`), that are not part of a trait reference.
|
||||
|
||||
A **projection** consists of a an associated item reference along with
|
||||
<a name=projection>
|
||||
|
||||
A **projection** consists of an associated item reference along with
|
||||
its inputs P0..Pm:
|
||||
|
||||
Projection = <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>
|
||||
|
|
@ -77,7 +83,9 @@ Given that, we can define a `DomainGoal` as follows:
|
|||
to [implied bounds].
|
||||
- `ProjectionEq(Projection = Type)` -- the given associated type `Projection` is equal
|
||||
to `Type`; see [the section on associated types](./traits-associated-types.html)
|
||||
- `Normalize(Projection -> Type)` -- the given associated type `Projection` can be normalized
|
||||
- in general, proving `ProjectionEq(TraitRef::Item = Type)` also
|
||||
requires proving `Implemented(TraitRef)`
|
||||
- `Normalize(Projection -> Type)` -- the given associated type `Projection` can be [normalized][n]
|
||||
to `Type`
|
||||
- as discussed in [the section on associated types](./traits-associated-types.html),
|
||||
`Normalize` implies `ProjectionEq` but not vice versa
|
||||
|
|
@ -85,6 +93,8 @@ Given that, we can define a `DomainGoal` as follows:
|
|||
*well-formed*
|
||||
- well-formedness is important to [implied bounds].
|
||||
|
||||
[n]: ./traits-associated-types.html#normalize
|
||||
|
||||
<a name=coinductive>
|
||||
|
||||
## Coinductive goals
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
# Lowering rules
|
||||
|
||||
This section gives the complete lowering rules for Rust traits into
|
||||
[program clauses][pc]. These rules reference the [domain goals][dg] defined in
|
||||
an earlier section.
|
||||
[program clauses][pc]. It is a kind of reference. These rules
|
||||
reference the [domain goals][dg] defined in an earlier section.
|
||||
|
||||
[pc]: ./traits-goals-and-clauses.html
|
||||
[dg]: ./traits-goals-and-clauses.html#domain-goals
|
||||
|
|
@ -22,7 +22,7 @@ definitions; these macros reference other sections within this chapter.
|
|||
|
||||
## Lowering where clauses
|
||||
|
||||
When used in a goal position, where clauses can be mapped directly
|
||||
When used in a goal position, where clauses can be mapped directly to
|
||||
[domain goals][dg], as follows:
|
||||
|
||||
- `A0: Foo<A1..An>` maps to `Implemented(A0: Foo<A1..An>)`.
|
||||
|
|
@ -72,12 +72,12 @@ inside the `{}`.
|
|||
### Trait header
|
||||
|
||||
From the trait itself we mostly make "meta" rules that setup the
|
||||
relationships between different kinds of domain goals. The first dush
|
||||
relationships between different kinds of domain goals. The first such
|
||||
rule from the trait header creates the mapping between the `FromEnv`
|
||||
and `Implemented` predicates:
|
||||
|
||||
forall<Self, P1..Pn> {
|
||||
Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn)
|
||||
Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)
|
||||
}
|
||||
|
||||
<a name="implied-bounds">
|
||||
|
|
@ -114,7 +114,7 @@ to be **well-formed**:
|
|||
|
||||
// For each where clause WC:
|
||||
forall<Self, P1..Pn> {
|
||||
WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>), WellFormed(WC)
|
||||
WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
|
||||
}
|
||||
|
||||
This `WellFormed` rule states that `T: Trait` is well-formed if (a)
|
||||
|
|
@ -150,7 +150,7 @@ one of those:
|
|||
|
||||
This `WellFormed` predicate is only used when proving that impls are
|
||||
well-formed -- basically, for each impl of some trait ref `TraitRef`,
|
||||
we must that `WellFormed(TraitRef)`. This in turn justifies the
|
||||
we must show that `WellFormed(TraitRef)`. This in turn justifies the
|
||||
implied bounds rules that allow us to extend the set of `FromEnv`
|
||||
items.
|
||||
|
||||
|
|
@ -170,9 +170,10 @@ where WC
|
|||
}
|
||||
```
|
||||
|
||||
We will produce a number of program clases. The first two define
|
||||
We will produce a number of program clauses. The first two define
|
||||
the rules by which `ProjectionEq` can succeed; these two clauses are discussed
|
||||
in detail in the [section on associated types](./traits-associated-types.html).
|
||||
in detail in the [section on associated types](./traits-associated-types.html),,
|
||||
but reproduced here for reference:
|
||||
|
||||
// ProjectionEq can succeed by normalizing:
|
||||
forall<Self, P1..Pn, Pn+1..Pm, U> {
|
||||
|
|
@ -180,7 +181,8 @@ in detail in the [section on associated types](./traits-associated-types.html).
|
|||
Normalize(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> -> U)
|
||||
}
|
||||
|
||||
// ProjectionEq can succeed by skolemizing:
|
||||
// ProjectionEq can succeed by skolemizing, see "associated type"
|
||||
// chapter for more:
|
||||
forall<Self, P1..Pn, Pn+1..Pm> {
|
||||
ProjectionEq(
|
||||
<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> =
|
||||
|
|
@ -188,13 +190,13 @@ in detail in the [section on associated types](./traits-associated-types.html).
|
|||
) :-
|
||||
// But only if the trait is implemented, and the conditions from
|
||||
// the associated type are met as well:
|
||||
Implemented(Self: Trait<P1..Pn>),
|
||||
WC1
|
||||
Implemented(Self: Trait<P1..Pn>)
|
||||
&& WC1
|
||||
}
|
||||
|
||||
The next rule covers implied bounds for the projection. In particular,
|
||||
the `Bounds` declared on the associated type must be proven to hold to
|
||||
show that the impl is well-formed, and hence we can rely on them from
|
||||
show that the impl is well-formed, and hence we can rely on them
|
||||
elsewhere.
|
||||
|
||||
// XXX how exactly should we set this up? Have to be careful;
|
||||
|
|
@ -237,7 +239,7 @@ Given an impl that contains:
|
|||
impl<P0..Pn> Trait<A1..An> for A0
|
||||
where WC
|
||||
{
|
||||
type AssocType<Pn+1..Pm>: Bounds where WC1 = T;
|
||||
type AssocType<Pn+1..Pm> where WC1 = T;
|
||||
}
|
||||
```
|
||||
|
||||
|
|
@ -246,13 +248,12 @@ We produce the following rule:
|
|||
forall<P0..Pm> {
|
||||
forall<Pn+1..Pm> {
|
||||
Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :-
|
||||
WC, WC1
|
||||
WC && WC1
|
||||
}
|
||||
}
|
||||
|
||||
Note that `WC` and `WC1` both encode where-clauses that the impl can
|
||||
rely on, whereas the bounds `Bounds` on the associated type are things
|
||||
that the impl must prove (see the well-formedness checking).
|
||||
rely on.
|
||||
|
||||
<a name=constant-vals>
|
||||
|
||||
|
|
|
|||
|
|
@ -33,6 +33,9 @@ Prolog-like notation, as follows:
|
|||
```
|
||||
Clone(usize).
|
||||
Clone(Vec<?T>) :- Clone(?T).
|
||||
|
||||
// The notation `A :- B` means "A is true if B is true".
|
||||
// Or, put another way, B implies A.
|
||||
```
|
||||
|
||||
In Prolog terms, we might say that `Clone(Foo)` -- where `Foo` is some
|
||||
|
|
@ -82,20 +85,20 @@ let's turn our focus a bit towards **type-checking**. Type-checking is
|
|||
interesting because it is what gives us the goals that we need to
|
||||
prove. That is, everything we've seen so far has been about how we
|
||||
derive the rules by which we can prove goals from the traits and impls
|
||||
in the program; but we are also interesting in how derive the goals
|
||||
in the program; but we are also interested in how to derive the goals
|
||||
that we need to prove, and those come from type-checking.
|
||||
|
||||
Consider type-checking the function `foo()` here:
|
||||
|
||||
```rust
|
||||
fn foo() { bar::<usize>() }
|
||||
fn bar<U: Eq>() { }
|
||||
fn bar<U: Eq<U>>() { }
|
||||
```
|
||||
|
||||
This function is very simple, of course: all it does is to call
|
||||
`bar::<usize>()`. Now, looking at the definition of `bar()`, we can see
|
||||
that it has one where-clause `U: Eq`. So, that means that `foo()` will
|
||||
have to prove that `usize: Eq` in order to show that it can call `bar()`
|
||||
that it has one where-clause `U: Eq<U>`. So, that means that `foo()` will
|
||||
have to prove that `usize: Eq<usize>` in order to show that it can call `bar()`
|
||||
with `usize` as the type argument.
|
||||
|
||||
If we wanted, we could write a Prolog predicate that defines the
|
||||
|
|
@ -103,7 +106,7 @@ conditions under which `bar()` can be called. We'll say that those
|
|||
conditions are called being "well-formed":
|
||||
|
||||
```
|
||||
barWellFormed(?U) :- Eq(?U).
|
||||
barWellFormed(?U) :- Eq(?U, ?U).
|
||||
```
|
||||
|
||||
Then we can say that `foo()` type-checks if the reference to
|
||||
|
|
@ -118,7 +121,7 @@ If we try to prove the goal `fooTypeChecks`, it will succeed:
|
|||
|
||||
- `fooTypeChecks` is provable if:
|
||||
- `barWellFormed(usize)`, which is provable if:
|
||||
- `Eq(usize)`, which is provable because of an impl.
|
||||
- `Eq(usize, usize)`, which is provable because of an impl.
|
||||
|
||||
Ok, so far so good. Let's move on to type-checking a more complex function.
|
||||
|
||||
|
|
@ -132,8 +135,8 @@ can be provide. To see what I'm talking about, let's revamp our previous
|
|||
example to make `foo` generic:
|
||||
|
||||
```rust
|
||||
fn foo<T: Eq>() { bar::<T>() }
|
||||
fn bar<U: Eq>() { }
|
||||
fn foo<T: Eq<T>>() { bar::<T>() }
|
||||
fn bar<U: Eq<U>>() { }
|
||||
```
|
||||
|
||||
To type-check the body of `foo`, we need to be able to hold the type
|
||||
|
|
@ -145,8 +148,8 @@ this like so:
|
|||
fooTypeChecks :-
|
||||
// for all types T...
|
||||
forall<T> {
|
||||
// ...if we assume that Eq(T) is provable...
|
||||
if (Eq(T)) {
|
||||
// ...if we assume that Eq(T, T) is provable...
|
||||
if (Eq(T, T)) {
|
||||
// ...then we can prove that `barWellFormed(T)` holds.
|
||||
barWellFormed(T)
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue