Crate chalk_ir[−][src]
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 GenericArgs that signifies
that it can applied as a substituion to a value
Utility 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.