Skip to main content Module hax Copy item path Source pub use rustc_trait_elaboration as elaboration;pub use crate::hax ::*;pub use crate::hax::state ::*;constant_utils 🔒 index_vec 🔒 mir_kinds Enumerates the kinds of Mir bodies. TODO: use const generics
instead of an open list of types. options prelude 🔒 rustc rustc_utils 🔒 sinto 🔒 state traits 🔒 types 🔒 utils 🔒 sinto_as_usize sinto_reexport sinto_todo Alias This type merges the information from
[ty::AliasTyKind] and [ty::AliasTy]. Align Reflects [rustc_abi::Align], but directly stores the number of bytes as a u64. AssocItem Reflects [ty::AssocItem] Binder Reflects [ty::Binder] BoundRegion Reflects [ty::BoundRegion] BoundTy Reflects [ty::BoundTy] Canonical Reflects [rustc_middle::infer::canonical::Canonical] CanonicalUserTypeAnnotation Reflects [ty::CanonicalUserTypeAnnotation] Clause Reflects [ty::Clause] and adds a hash-consed predicate identifier. ClosureArgs Reflects [ty::ClosureArgs] CoercePredicate Reflects [ty::CoercePredicate] ConstOperand The contents of Operand::Const. ConstantFieldExpr Decorated Generic container for decorating items with a type, a span,
attributes and other meta-data. DefId Reflects rustc_hir::def_id::DefId DefIdContents DisambiguatedDefPathItem Reflects [rustc_hir::definitions::DisambiguatedDefPathData] DiscriminantValue Reflects [ty::util::Discr] DynBinder A representation of exists<T: Trait1 + Trait2>(value): we create a fresh type id and the
appropriate trait clauses. The contained value may refer to the fresh ty and the in-scope trait
clauses. This is used to represent types related to dyn Trait. EarlyParamRegion Reflects [ty::EarlyParamRegion] ElaborationCtx ExistentialProjection Reflects [rustc_type_ir::ExistentialProjection] ExistentialTraitRef Reflects [rustc_type_ir::ExistentialTraitRef] FieldDef Reflects [ty::FieldDef] FullDef Gathers a lot of definition information about a rustc_hir::def_id::DefId GenericParamDef Reflects [ty::GenericParamDef] GenericPredicate GenericPredicates Reflects [ty::GenericPredicates] HashMap A hash map implemented with quadratic probing and SIMD lookup. ImplAssocItem An associated item in a trait impl. This can be an item provided by the trait impl, or an item
that reuses the trait decl default value. ImplAssocItemValue The item is provided by the trait impl. IndexVec ItemPredicate ItemPredicates ItemRef Reference to an item, with generics. Basically any mention of an item (function, type, etc)
uses this. ItemRefContents Contents of ItemRef. LateParamRegion Reflects [ty::LateParamRegion] OutlivesPredicate Reflects [ty::OutlivesPredicate] as a named struct
instead of a tuple struct. This is because the script converting
JSONSchema types to OCaml doesn’t support tuple structs, and this
is the only tuple struct in the whole AST. ParamConst Reflects [ty::ParamConst] ParamEnv The combination of type generics and related predicates. ParamTy Reflects [ty::ParamTy] PathBuf An owned, mutable path (akin to String Placeholder Reflects [ty::Placeholder] Predicate Reflects [ty::Predicate] and adds a hash-consed predicate identifier. ProjectionPredicate Expresses a constraints over an associated type. Rc A single-threaded reference-counting pointer. ‘Rc’ stands for ‘Reference
Counted’. Region Reflects [ty::Region] ReprFlags The representation flags without the ones irrelevant outside of rustc. ReprOptions Reflects [rustc_abi::ReprOptions]. SubtypePredicate Reflects [ty::SubtypePredicate] SyntheticItemData TraitItemBinder The binding context to use when translating a trait impl associated item. TraitPredicate Reflects [ty::TraitPredicate] TraitProofContents Ty Reflects [rustc_middle::ty::Ty] TyFnSig Reflects [ty::FnSig] TyGenerics Reflects [ty::Generics] TypeAndMut Reflects [ty::TypeAndMut] TypeMap A map that maps types to values in a generic manner: we store for each type T a value of
type M::Value<T>. UserArgs Reflects [ty::UserArgs] UserSelfTy Reflects [ty::UserSelfTy] VariantDef Reflects [ty::VariantDef] VirtualImplAssocItem VirtualTraitImpl Partial data for a trait impl, used for fake trait impls that we generate ourselves such as
FnOnce and Drop impls. ByteSymbol Like Symbol, but for byte strings. ByteSymbol is used less widely, so
it has fewer operations defined than Symbol. FieldIdx The source-order index of a field in a variant. MacroKinds A set of macro kinds, for macros that can have more than one kind PromotedId RDefId A DefId identifies a particular definition , by combining a crate
index and a def index. Span A compressed span. Spanned Symbol An interned UTF-8 string. VariantIdx The source-order index of a variant in a type. AdtFlags AdtKind Reflects [ty::AdtKind] AliasKind Reflects [rustc_middle::ty::AliasTyKind]. AliasRelationDirection Reflects [ty::AliasRelationDirection] AssocItemContainer AssocItemResolution AssocKind Reflects [ty::AssocKind] AssocTypeData Reflects [ty::AssocTypeData] BoundRegionKind Reflects [ty::BoundRegionKind] BoundTyKind Reflects [ty::BoundTyKind] BoundVarIndexKind Reflects [ty::BoundVarIndexKind] BoundVariableKind Reflects [ty::BoundVariableKind] BuiltinTraitData ClauseKind Reflects [ty::ClauseKind] ClosureKind Reflects [ty::ClosureKind] ConstKind The kind of a constant item. ConstOperandKind ConstantExprKind The subset of expressions that corresponds to constants. ConstantInt ConstantLiteral DefIdBase DefKind Reflects rustc_hir::def::DefKind DefPathItem Reflects [rustc_hir::definitions::DefPathData] DestructData DiscriminantDefinition Reflects [ty::VariantDiscr] ErrorGuaranteed ExistentialPredicate A predicate without Self, for use in dyn Trait. FloatTy Reflects [rustc_type_ir::FloatTy] FullDefKind Imbues rustc_hir::def::DefKind GenericArg Reflects both [ty::GenericArg] and [ty::GenericArgKind] GenericParamDefKind Reflects [ty::GenericParamDefKind] GenericPredicateId Uniquely identifies a predicate. HostEffectPredicate ImplTraitInTraitData Reflects [ty::ImplTraitInTraitData] InferTy Reflects partially [ty::InferTy] InlineAttr Reflects [rustc_hir::attrs::InlineAttr] IntTy Reflects [rustc_type_ir::IntTy] ItemPredicateId Uniquely identifies a predicate. LateParamRegionKind Reflects [ty::LateParamRegionKind] LitIntType Reflects both [ty::GenericArg] and [ty::GenericArgKind] NormalizesTo Pattern PredicateDirection PredicateKind Reflects [ty::PredicateKind] RegionKind Reflects [ty::RegionKind] SyntheticItem We create some extra DefIds to represent things that rustc doesn’t have a DefId for. This
makes the pipeline much easier to have “real” def_ids for them.
We generate fake struct-like items for each of: arrays, slices, and tuples. This makes it
easier to emit trait impls for these types, especially with monomorphization. This enum tracks
identifies these builtin types. Term Reflects [ty::Term] TraitProofImpliedPredicate TraitProofKind The source of a particular trait implementation. Most often this is either Concrete for a
concrete impl Trait for Type {} item, or LocalBound for a context-bound where T: Trait. TyKind Reflects [ty::TyKind] UintTy Reflects [rustc_type_ir::UintTy] UnsizingMetadata The metadata to attach to the newly-unsized ptr. UserType Reflects [ty::UserType]: this is currently
disabled, and everything is printed as debug in the
UserType::Todo Variance Reflects [ty::Variance] VariantKind Describe the kind of a variant Visibility Reflects [ty::Visibility] CtorKind What kind of constructor something is. CtorOf Encodes if a DefKind::Ctor is the constructor of an enum variant or a struct. ExternAbi ABI we expect to see within extern "{abi}" Mutability RDefKind What kind of definition something is; e.g., mod vs struct.
enum DefPathData may need to be updated if a new variant is added here. Safety IsMirKind ItemId The identifier of an item; generalizes over rustc’s DefId to allow for virtual items. SExpect SInto SubstBinder ToPolyTraitRef TypeMapper Defines a mapping from types to types. assoc_tys_for_trait Generates a list of <trait_ref>::Ty type aliases for each non-gat associated type of the
given trait and its parents, in a specific order. closure_once_shim compute_unsizing_metadata const_value_to_constant_expr drop_glue_shim dyn_self_ty Generates a dyn Trait<Args.., Ty = <Self as Trait>::Ty..> type for the given trait ref. erase_and_norm erase_free_regions Erase free regions from the given value. Largely copied from tcx.erase_and_anonymize_regions, but also
erases bound regions that are bound outside value, so we can call this function inside a
Binder. eval_ty_constant Evaluate a ty::Const. get_foreign_mod_children Gets the children of an extern block. Empty if the block is not defined in the current crate. get_method_sig The signature of a method impl may be a subtype of the one expected from the trait decl, as in
the example below. For correctness, we must be able to map from the method generics declared in
the trait to the actual method generics. Because this would require type inference, we instead
simply return the declared signature. This will cause issues if it is possible to use such a
more-specific implementation with its more-specific type, but we have a few other issues with
lifetime-generic function pointers anyway so this is unlikely to cause problems. get_mod_children Gets the children of a module. get_promoted_mir Retrieve the MIR for a promoted body. inst_binder name_of_local normalize Normalize a value. param_env_from_clauses Make a new ParamEnv from a list of clauses. self_clause_for_item Retrieve the Self: Trait clause for a trait associated item. self_predicate The special “self” predicate on a trait. solve_destruct Solve the T: Destruct predicate. solve_item_implied_traits Solve the trait obligations for implementing a trait (or for trait associated type bounds) in
the current context. solve_sized Solve the T: Sized predicate. solve_trait This is the entrypoint of the solving. substitute super_clause_to_clause_and_trait_proof Given a clause clause in the context of some impl block impl_did, susbts correctly Self
from clause and (1) derive a Clause and (2) resolve a TraitProof. translate_item_ref Translate a reference to an item, resolving the appropriate trait clauses as needed. BoundVar CanonicalUserType Reflects [ty::CanonicalUserType] ConstantExpr Rustc has different representation for constants: one for MIR
([rustc_middle::mir::Const]), one for the type system
([rustc_middle::ty::ConstKind]). For simplicity hax maps those
two construct to one same ConstantExpr type. ConstantKind DebruijnIndex Ident Reflects [rustc_span::symbol::Ident] PlaceholderConst Reflects [ty::PlaceholderConst] PlaceholderRegion Reflects [ty::PlaceholderRegion] PlaceholderType Reflects [ty::PlaceholderType] PolyFnSig Reflects [ty::PolyFnSig] PredicateSearcher RegionOutlivesPredicate Reflects [ty::RegionOutlivesPredicate] RegionVid TraitProof A TraitProof describes the full data of a trait implementation. Because of generics, this may
need to combine several concrete trait implementation items. For example, ((1u8, 2u8), "hello").clone() combines the generic implementation of Clone for (A, B) with the
concrete implementations for u8 and &str, represented as a tree. TraitRef Reflects [ty::TraitRef]
Contains the def_id and arguments passed to the trait. The first type argument is the Self
type. The trait proofs are the required predicate for this trait; currently they are always
empty because we consider all trait predicates as implied.
self.in_trait is always None because a trait can’t be associated to another one. TypeOutlivesPredicate Reflects [ty::TypeOutlivesPredicate] AdtInto AdtIntoSIntoA to
another ADT B when A and B shares a lot of structure.TypeMappable