Crate chalk_ir

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

• impl_debugs 🔒
• interned_slice 🔒
• interned_slice_common 🔒
• try_break
  Unwraps a ControlFlow or propagates its Break value. This replaces the Try implementation that would be used with std::ops::ControlFlow.

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 associated_ty_data method.
• Binders
  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.
• BindersIntoIterator
  IntoIterator for binders.
• BoundVar
  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.
• 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 (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.
• Constraints
  List of interned elements.
• CoroutineId
  Id for Rust coroutines.
• 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 for<T> { (T: Clone) :- (T: Copy) }, then T would be represented as a BoundVar(0) (as the for is the innermost binder).
• DynTy
  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.
• 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 self.ty
• FnSig
  A function signature.
• FnSubst
  A wrapper for the substs on a Fn.
• ForeignDefId
  Id for foreign types.
• GenericArg
  A generic argument, see GenericArgData for more information.
• 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 'a: 'b checks that the lifetime 'a is a superset of the value of 'b.
• 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 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.
• OpaqueTy
  An opaque type opaque type T<..>: Trait = HiddenTy.
• 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 consequence :- conditions where conditions = cond_1 && cond_2 && ... is the conjunction of the individual conditions.
• ProgramClauses
  List of interned elements.
• ProjectionTy
  A projection <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>.
• QuantifiedWhereClauses
  List of interned elements.
• SubstFolder 🔒
• Substitution
  List of interned elements.
• SubtypeGoal
  Subtype goal: tries to prove that a is a subtype of b
• TraitId
  The id of a trait definition; could be used to load the trait datum by invoking the trait_datum method.
• 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 TyKind.
• TyData
  Contains the data for a Ty
• TypeFlags
  Contains flags indicating various properties of a Ty
• TypeOutlives
  Type outlives, which for T: 'a checks that the type T lives at least as long as the lifetime 'a
• UCanonical
  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.
• 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: 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.
• UniverseMap
  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).
• 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 Fallible and Floundered.
• 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 forall and exists.
• 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 PhantomData.
• 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 GenericArgs that signifies that it can applied as a substituion to a value
• 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 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.
• UnificationDatabase
  Logic to decide the Variance for a given subst

Type Aliases

• 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 forall<> or exists<> quantifiers.