Expand description
Defines the IR for types and logical predicates.
Re-exports
pub use crate::debug::SeparatorTraitRef;
Modules
Upcasts, to avoid writing out wrapper types.
Fast matching check for zippable values.
Debug impls for types.
Traits for transforming bits of IR.
Encapsulates the concrete representation of core types such as types and goals.
Traits for visiting bits of IR.
Traits for “zipping” types, walking through two structures and checking that they match.
Macros
Unwraps a
ControlFlow
or propagates its Break
value.
This replaces the Try
implementation that would be used
with std::ops::ControlFlow
.Structs
The id for an Abstract Data Type (i.e. structs, unions and enums).
Proves equality between an alias and a type.
The resulting substitution after solving a goal.
The id for the associated type member of a trait. The details of the type
can be found by invoking the
associated_ty_data
method.Indicates that the
value
is universally quantified over N
parameters of the given kinds, where N == self.binders.len()
. A
variable with depth i < N
refers to the value at
self.binders[i]
. Variables with depth >= N
are free.IntoIterator
for binders.Identifies a particular bound variable within a binder.
Variables are identified by the combination of a
DebruijnIndex
,
which identifies the binder, and an index within that binder.Wraps a “canonicalized item”. Items are canonicalized as follows:
List of interned elements.
Id for a specific clause.
Id for Rust closures.
Concrete constant, whose value is known (as opposed to
inferred constants and placeholders).
Constants.
Constant data, containing the constant’s type and value.
Combines a substitution (
subst
) with a set of region constraints
(constraints
). This represents the result of a query; the
substitution stores the values for the query’s unknown variables,
and the constraints represents any region constraints that must
additionally be solved.List of interned elements.
References the binder at the given depth. The index is a de
Bruijn index, so it counts back through the in-scope binders,
with 0 being the innermost binder. This is used in impls and
the like. For example, if we had a rule like
for<T> { (T: Clone) :- (T: Copy) }
, then T
would be represented as a
BoundVar(0)
(as the for
is the innermost binder).A “DynTy” represents a trait object (
dyn Trait
). Trait objects
are conceptually very related to an “existential type” of the form
exists<T> { T: Trait }
(another example of such type is impl Trait
).
DynTy
represents the bounds on that type.The set of assumptions we’ve made so far, and the current number of
universal (forall) quantifiers we’re within.
Equality goal: tries to prove that two values are equal.
Indicates that the complete set of program clauses for this goal
cannot be enumerated.
Function definition id.
for<’a…’z> X – all binders are instantiated at once,
and we use deBruijn indices within
self.ty
A function signature.
A wrapper for the substs on a Fn.
Id for foreign types.
Id for Rust generators.
A generic argument, see
GenericArgData
for more information.A general goal; this is the full range of questions you can pose to Chalk.
List of interned elements.
The id for an impl.
A goal with an environment to solve it in.
A type, lifetime or constant whose value is being inferred.
A Rust lifetime.
Lifetime outlives, which for
'a: 'b`` checks that the lifetime
’ais a superset of the value of
’b`.Indicates that the attempted operation has “no solution” – i.e.,
cannot be performed.
Proves that the given type alias normalizes to the given
type. A projection
T::Foo
normalizes to the type U
if we can
match it to an impl and that impl has a type Foo = V
where
U = V
.An opaque type
opaque type T<..>: Trait = HiddenTy
.Id for an opaque type.
Index of an universally quantified parameter in the environment.
Two indexes are required, the one of the universe itself
and the relative index inside the universe.
A program clause is a logic expression used to describe a part of the program.
Contains the data for a program clause.
Represents one clause of the form
consequence :- conditions
where
conditions = cond_1 && cond_2 && ...
is the conjunction of the individual
conditions.List of interned elements.
A projection
<P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>
.List of interned elements.
List of interned elements.
Subtype goal: tries to prove that
a
is a subtype of b
The id of a trait definition; could be used to load the trait datum by
invoking the
trait_datum
method.A trait reference describes the relationship between a type and a trait.
This can be used in two forms:
A Rust type. The actual type data is stored in
TyKind
.Contains the data for a Ty
Contains flags indicating various properties of a Ty
Type outlives, which for
T: 'a
checks that the type T
lives at least as long as the lifetime 'a
A “universe canonical” value. This is a wrapper around a
Canonical
, indicating that the universes within have been
“renumbered” to start from 0 and collapse unimportant
distinctions.An universe index is how a universally quantified parameter is
represented when it’s binder is moved into the environment.
An example chain of transformations would be:
forall<T> { Goal(T) }
(syntactical representation)
forall { Goal(?0) }
(used a DeBruijn index)
Goal(!U1)
(the quantifier was moved to the environment and replaced with a universe index)
See https://rustc-dev-guide.rust-lang.org/borrow_check/region_inference.html#placeholders-and-universes for more.Maps the universes found in the
u_canonicalize
result (the
“canonical” universes) to the universes found in the original
value (and vice versa). When used as a folder – i.e., from
outside this module – converts from “canonical” universes to the
original (but see the UMapToCanonical
folder).List of interned elements.
List of interned elements.
A value with an associated variable kind.
Enums
An alias, which is a trait indirection such as a projection or opaque type.
Specifies how important an implication is.
A constant value, not necessarily concrete.
A constraint on lifetimes.
A “domain goal” is a goal that is directly about Rust, rather than a pure
logical statement. As much as possible, the Chalk solver should avoid
decomposing this enum, and instead treat its values opaquely.
A combination of
Fallible
and Floundered
.Different kinds of float types.
Checks whether a type or trait ref can be derived from the contents of the environment.
Generic arguments data.
A general goal; this is the full range of questions you can pose to Chalk.
Different signed int types.
Lifetime data, including what kind of lifetime it is and what it points to.
Whether a type is mutable or not.
Kinds of quantifiers in the logic, such as
forall
and exists
.Whether a function is safe or not.
Types of scalar values.
Type data, which holds the actual type information.
Represents some extra knowledge we may have about the type variable.
Different unsigned int types.
The “kind” of variable. Type, lifetime or constant.
Variance
Uninhabited (empty) type, used in combination with
PhantomData
.Checks whether a type or trait ref is well-formed.
Where clauses that can be written by a Rust programmer.
Traits
Convert a value to a list of parameters.
An extension trait to anything that can be represented as list of
GenericArg
s that signifies
that it can applied as a substituion to a valueUtility for converting a list of all the binders into scope
into references to those binders. Simply pair the binders with
the indices, and invoke
to_generic_arg()
on the (binder, index)
pair. The result will be a reference to a bound
variable of appropriate kind at the corresponding index.Logic to decide the Variance for a given subst
Type Definitions
A variable kind with universe index.
Many of our internal operations (e.g., unification) are an attempt
to perform some operation which may not complete.
A where clause that can contain
forall<>
or exists<>
quantifiers.