Crate chalk_ir[−][src]
Expand description
Defines the IR for types and logical predicates.
Re-exports
pub use crate::debug::SeparatorTraitRef; |
Modules
cast | Upcasts, to avoid writing out wrapper types. |
could_match | Fast matching check for zippable values. |
debug | Debug impls for types. |
fold | Traits for transforming bits of IR. |
interner | Encapsulates the concrete representation of core types such as types and goals. |
visit | Traits for visiting bits of IR. |
zip | Traits for “zipping” types, walking through two structures and checking that they match. |
Macros
try_break | Unwraps a |
Structs
AdtId | The id for an Abstract Data Type (i.e. structs, unions and enums). |
AliasEq | Proves equality between an alias and a type. |
AnswerSubst | The resulting substitution after solving a goal. |
AssocTypeId | The id for the associated type member of a trait. The details of the type
can be found by invoking the |
Binders | Indicates that the |
BindersIntoIterator |
|
BoundVar | Identifies a particular bound variable within a binder.
Variables are identified by the combination of a |
Canonical | Wraps a “canonicalized item”. Items are canonicalized as follows: |
CanonicalVarKinds | List of interned elements. |
ClauseId | Id for a specific clause. |
ClosureId | Id for Rust closures. |
ConcreteConst | Concrete constant, whose value is known (as opposed to inferred constants and placeholders). |
Const | Constants. |
ConstData | Constant data, containing the constant’s type and value. |
ConstrainedSubst | Combines a substitution ( |
Constraints | List of interned elements. |
DebruijnIndex | 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 |
DynTy | A “DynTy” represents a trait object ( |
Environment | The set of assumptions we’ve made so far, and the current number of universal (forall) quantifiers we’re within. |
EqGoal | Equality goal: tries to prove that two values are equal. |
Floundered | Indicates that the complete set of program clauses for this goal cannot be enumerated. |
FnDefId | Function definition id. |
FnPointer | for<’a…’z> X – all binders are instantiated at once,
and we use deBruijn indices within |
FnSig | A function signature. |
FnSubst | A wrapper for the substs on a Fn. |
ForeignDefId | Id for foreign types. |
GeneratorId | Id for Rust generators. |
GenericArg | A generic argument, see |
Goal | A general goal; this is the full range of questions you can pose to Chalk. |
Goals | List of interned elements. |
ImplId | The id for an impl. |
InEnvironment | A goal with an environment to solve it in. |
InferenceVar | A type, lifetime or constant whose value is being inferred. |
Lifetime | A Rust lifetime. |
LifetimeOutlives | Lifetime outlives, which for |
NoSolution | Indicates that the attempted operation has “no solution” – i.e., cannot be performed. |
Normalize | Proves that the given type alias normalizes to the given
type. A projection |
OpaqueTy | An opaque type |
OpaqueTyId | Id for an opaque type. |
PlaceholderIndex | 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. |
ProgramClause | A program clause is a logic expression used to describe a part of the program. |
ProgramClauseData | Contains the data for a program clause. |
ProgramClauseImplication | Represents one clause of the form |
ProgramClauses | List of interned elements. |
ProjectionTy | A projection |
QuantifiedWhereClauses | List of interned elements. |
Substitution | List of interned elements. |
SubtypeGoal | Subtype goal: tries to prove that |
TraitId | The id of a trait definition; could be used to load the trait datum by
invoking the |
TraitRef | A trait reference describes the relationship between a type and a trait. This can be used in two forms: |
Ty | A Rust type. The actual type data is stored in |
TyData | Contains the data for a Ty |
TypeFlags | Contains flags indicating various properties of a Ty |
TypeOutlives | Type outlives, which for |
UCanonical | A “universe canonical” value. This is a wrapper around a
|
UniverseIndex | 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:
|
UniverseMap | Maps the universes found in the |
VariableKinds | List of interned elements. |
Variances | List of interned elements. |
WithKind | A value with an associated variable kind. |
Enums
AliasTy | An alias, which is a trait indirection such as a projection or opaque type. |
ClausePriority | Specifies how important an implication is. |
ConstValue | A constant value, not necessarily concrete. |
Constraint | A constraint on lifetimes. |
DomainGoal | 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. |
FallibleOrFloundered | A combination of |
FloatTy | Different kinds of float types. |
FromEnv | Checks whether a type or trait ref can be derived from the contents of the environment. |
GenericArgData | Generic arguments data. |
GoalData | A general goal; this is the full range of questions you can pose to Chalk. |
IntTy | Different signed int types. |
LifetimeData | Lifetime data, including what kind of lifetime it is and what it points to. |
Mutability | Whether a type is mutable or not. |
QuantifierKind | Kinds of quantifiers in the logic, such as |
Safety | Whether a function is safe or not. |
Scalar | Types of scalar values. |
TyKind | Type data, which holds the actual type information. |
TyVariableKind | Represents some extra knowledge we may have about the type variable. |
UintTy | Different unsigned int types. |
VariableKind | The “kind” of variable. Type, lifetime or constant. |
Variance | Variance |
Void | Uninhabited (empty) type, used in combination with |
WellFormed | Checks whether a type or trait ref is well-formed. |
WhereClause | Where clauses that can be written by a Rust programmer. |
Traits
AsParameters | Convert a value to a list of parameters. |
Substitute | An extension trait to anything that can be represented as list of |
ToGenericArg | 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 |
UnificationDatabase | Logic to decide the Variance for a given subst |
Type Definitions
CanonicalVarKind | A variable kind with universe index. |
Fallible | Many of our internal operations (e.g., unification) are an attempt to perform some operation which may not complete. |
QuantifiedWhereClause | A where clause that can contain |