Crate hax_frontend_exporter Copy item path
Summary Source pub use crate::id_table ;
pub use hax_frontend_exporter_options as options;
pub use crate ::*;
pub use crate::prelude ::*;
pub use crate::state ::*;
body 🔒 comments constant_utils 🔒 deterministic_hash 🔒 Stolen from https://github.com/Wassasin/deterministic-hash/blob/main/src/lib.rs id_table index_vec 🔒 mir_kinds Enumerates the kinds of Mir bodies. TODO: use const generics
instead of an open list of types. prelude 🔒 rustc rustc_utils 🔒 sinto 🔒 state traits 🔒 types 🔒 utils 🔒 cfg_feature_rustc 🔒 schema_for Generates a RootSchema
for the given type using default settings. sinto_as_usize sinto_todo AdtDef Reflects ty::AdtDef
AdtExpr Reflects thir::AdtExpr
Alias This type merges the information from
rustc_type_ir::AliasKind
and ty::AliasTy
AnonConst Reflects [hir::AnonConst
] Arm Reflects thir::Arm
Ascription Reflects thir::Ascription
AssocItem Reflects ty::AssocItem
AttrItem Reflects [rustc_hir::AttrItem
] BasicBlockData Binder Reflects ty::Binder
BindingMode Reflects rustc_ast::ast::BindingMode
Block Reflects thir::Block
BoundRegion Reflects ty::BoundRegion
BoundTy Reflects ty::BoundTy
CORE_EXTRACTION_MODE 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
ConstArg Reflects [hir::ConstArg
] ConstOperand The contents of Operand::Const
. ConstantFieldExpr CopyNonOverlapping Decorated Generic container for decorating items with a type, a span,
attributes and other meta-data. DefId Reflects rustc_hir::def_id::DefId
DefIdContents DelimArgs Reflects rustc_ast::ast::DelimArgs
DisambiguatedDefPathItem Reflects [rustc_hir::definitions::DisambiguatedDefPathData
] DiscriminantValue Reflects ty::util::Discr
EarlyParamRegion Reflects ty::EarlyParamRegion
ExistentialProjection Reflects [rustc_type_ir::ExistentialProjection
] ExistentialTraitRef Reflects [rustc_type_ir::ExistentialTraitRef
] FieldDef Reflects ty::FieldDef
FieldExpr A field expression: a field name along with a value FieldPat A field pattern: a field name along with a pattern FnDecl Reflects [hir::FnDecl
] FnDef Function definition FnHeader Reflects [hir::FnHeader
] FnSig Reflects [hir::FnSig
] ForeignItem Reflects [hir::ForeignItem
] FruInfo Field Record Update (FRU) informations, this reflects thir::FruInfo
FullDef Gathers a lot of definition information about a rustc_hir::def_id::DefId
. GenericParam Reflects [hir::GenericParam
] GenericParamDef Reflects ty::GenericParamDef
GenericPredicates Reflects ty::GenericPredicates
Generics Reflects [hir::Generics
] HashMap A hash map implemented with quadratic probing and SIMD lookup. HirFieldDef Reflects [hir::FieldDef
] HirId Reflects [hir::hir_id::HirId
] Impl Reflects [hir::Impl
]. 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. ImplExpr An ImplExpr
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. ImplInfos Meta-informations about an impl<GENERICS[: PREDICATES]> TRAIT for TYPE where PREDICATES {}
ImplItem Reflects [hir::ImplItem
] IndexVec Item Reflects [hir::Item
] (and [hir::ItemId
]) ItemAttributes LateParamRegion Reflects ty::LateParamRegion
Loc Reflects rustc_span::Loc
LocalDecl LocalIdent Reflects thir::LocalVarId
MacroDef Reflects ast::MacroDef
MetaItemLit Reflects rustc_ast::MetaItemLit
MirBody 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. Param Reflects thir::Param
ParamConst Reflects ty::ParamConst
ParamEnv The combination of type generics and related predicates. ParamTy Reflects ty::ParamTy
PatRange Reflects thir::PatRange
PathBuf An owned, mutable path (akin to String
). PathSegment Reflects [hir::PathSegment
] Place Placeholder Reflects ty::Placeholder
Predicate Reflects ty::Predicate
and adds a hash-consed predicate identifier. PredicateId A PredicateId
is a unique identifier for a clause or a
predicate. It is computed by hashing predicates and clause in a
uniform and deterministic way. PredicateSearcher Stores a set of predicates along with where they came from. ProjectionPredicate Expresses a constraints over an associated type. PromotedConstant Part of a MIR body that was promoted to be a constant. PromotedId Rc A single-threaded reference-counting pointer. ‘Rc’ stands for ‘Reference
Counted’. Region Reflects ty::Region
ReprOptions Reflects [ty::ReprOptions
] ScalarInt Scope Reflects rustc_middle::middle::region::Scope
SourceInfo SourceScopeData Span Reflects rustc_span::Span
Spanned Reflects rustc_span::source_map::Spanned
Statement Stmt Reflects thir::Stmt
SubtypePredicate Reflects ty::SubtypePredicate
Terminator TraitItem Reflects [hir::TraitItem
] TraitPredicate Reflects ty::TraitPredicate
TraitRef Reflects ty::TraitRef
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>
. UsePath Reflects [hir::UsePath
] UserArgs Reflects ty::UserArgs
UserSelfTy Reflects ty::UserSelfTy
Variant Reflects [hir::Variant
] VariantDef Reflects ty::VariantDef
VariantInformations Describe a variant RDefId A DefId
identifies a particular definition , by combining a crate
index and a def index. RLocalDefId A LocalDefId
is equivalent to a DefId
with krate == LOCAL_CRATE
. Since
we encode this information in the type, we can ensure at compile time that
no DefId
s from upstream crates get thrown into the mix. There are quite a
few cases where we know that only DefId
s from the local crate are expected;
a DefId
from a different crate would signify a bug somewhere. This
is when LocalDefId
comes in handy. ROwnerId AdtExprBase AdtFlags AdtKind Reflects ty::AdtKind
AggregateKind AliasKind Reflects [ty::AliasKind
] AliasRelationDirection Reflects [ty::AliasRelationDirection
] Align AssertMessage AssocItemContainer AssocItemKind Reflects [hir::AssocItemKind
] AssocKind Reflects ty::AssocKind
AttrArgs Reflects [rustc_hir::AttrArgs
] AttrStyle Reflects rustc_ast::AttrStyle
Attribute Reflects rustc_ast::Attribute
AttributeKind Reflects [rustc_attr_data_structures::AttributeKind
] BasicBlock BinOp Reflects rustc_middle::mir::BinOp
BlockSafety Reflects thir::BlockSafety
BorrowKind Reflects rustc_middle::mir::BorrowKind
BoundRegionKind Reflects ty::BoundRegionKind
BoundTyKind Reflects ty::BoundTyKind
BoundVariableKind Reflects ty::BoundVariableKind
ByRef Reflects rustc_ast::ast::ByRef
CanonicalTyVarKind Reflects [rustc_middle::infer::canonical::CanonicalTyVarKind
] CanonicalVarInfo Reflects [rustc_middle::infer::canonical::CanonicalVarKind
] CastKind ClauseKind Reflects ty::ClauseKind
ClosureKind Reflects [ty::ClosureKind
] CoercionSource CommentKind Reflects rustc_ast::token::CommentKind
ConstArgKind Reflects [hir::ConstArgKind
] ConstOperandKind ConstantExprKind The subset of Expr that corresponds to constants. ConstantInt ConstantLiteral Constness Reflects [hir::Constness
] CoverageKind CtorKind Reflects [hir::def::CtorKind
] CtorOf Reflects [hir::def::CtorOf
] DefKind Reflects [rustc_hir::def::DefKind
] DefPathItem Reflects [rustc_hir::definitions::DefPathData
] Defaultness Reflects [hir::Defaultness
] DelimSpan Delimiter Reflects rustc_ast::token::Delimiter
DiscriminantDefinition Reflects ty::VariantDiscr
DynKind Reflects [ty::DynKind
] ErrorGuaranteed ExistentialPredicate A predicate without Self
, for use in dyn Trait
. ExprKind Reflects thir::ExprKind
ExternAbi Reflects [rustc_abi::ExternAbi
] FakeBorrowKind Reflects rustc_middle::mir::FakeBorrowKind
FakeReadCause FieldIdx FileName Reflects rustc_span::FileName
FloatTy Reflects [rustc_type_ir::FloatTy
] FnRetTy Reflects [hir::FnRetTy
] ForeignItemKind Reflects [hir::ForeignItemKind
] FullDefKind Imbues [rustc_hir::def::DefKind
] with a lot of extra information.
Important: the owner_id()
must be the id of this definition. FunOperand A value of type fn<...> A -> B
that can be called. GenericArg Reflects both ty::GenericArg
and ty::GenericArgKind
GenericParamDefKind Reflects ty::GenericParamDefKind
GenericParamKind Reflects [hir::GenericParamKind
] HeaderSafety HirGenericArgs HostEffectPredicate ImplAssocItemValue ImplExprAtom 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
. ImplExprPathChunk ImplItemKind Reflects [hir::ImplItemKind
], inlining the body of the items. ImplPolarity Reflects hir::ImplPolarity
ImplTraitInTraitData Reflects ty::ImplTraitInTraitData
ImplicitSelfKind Reflects [hir::ImplicitSelfKind
] InferTy Reflects partially [ty::InferTy
] InlineAsm InlineAsmOperand InlineAsmOptions InlineAsmTemplatePiece InlineAttr Reflects [rustc_attr_data_structures::InlineAttr
] IntTy Reflects [rustc_type_ir::IntTy
] IntegerType InvisibleOrigin IsAsync Reflects [hir::IsAsync
] IsAuto Reflects hir::IsAuto
ItemKind Reflects [hir::ItemKind
] LateParamRegionKind Reflects ty::LateParamRegionKind
LifetimeParamKind Reflects [hir::LifetimeParamKind
] LintLevel Reflects thir::LintLevel
LitFloatType Reflects ast::LitFloatType
LitIntType Reflects both ty::GenericArg
and ty::GenericArgKind
LitKind Reflects rustc_ast::ast::LitKind
Local LogicalOp Reflects thir::LogicalOp
MacroKind Reflects rustc_span::hygiene::MacroKind
MissingLifetimeKind Movability Reflects [hir::Movability
] MutBorrowKind Reflects rustc_middle::mir::MutBorrowKind
NonDivergingIntrinsic NonMacroAttrKind Reflects [hir::def::NonMacroAttrKind
] NormalizesTo NullOp Operand OwnerId ParamName Reflects [hir::ParamName
] PatKind Reflects thir::PatKind
PatRangeBoundary Reflects thir::PatRangeBoundary
PlaceKind PointerCoercion Reflects ty::adjustment::PointerCoercion
PredicateKind Reflects ty::PredicateKind
PrimTy Reflects [hir::PrimTy
] ProjectionElem ProjectionElemFieldKind QPath RangeEnd Reflects [hir::RangeEnd
] RawPtrKind RealFileName Reflects rustc_span::RealFileName
RegionKind Reflects ty::RegionKind
ReprFlags Res Reflects [hir::def::Res
] RetagKind Rvalue Safety Reflects [hir::Safety
] ScalarInt ScalarTy ScopeData Reflects rustc_middle::middle::region::ScopeData
SourceScope StatementKind StmtKind Reflects thir::StmtKind
StrStyle Reflects rustc_ast::ast::StrStyle
Term Reflects ty::Term
TerminatorKind TraitItemKind Reflects [hir::TraitItemKind
] TyKind Reflects ty::TyKind
UintTy Reflects [rustc_type_ir::UintTy
] UnOp Reflects rustc_middle::mir::UnOp
UnwindAction UnwindTerminateReason UseKind Reflects [hir::UseKind
] UserType Reflects ty::UserType
: this is currently
disabled, and everything is printed as debug in the
UserType::Todo
variant. UserTypeAnnotationIndex UserTypeProjection Variance Reflects [ty::Variance
] VariantData Reflects [hir::VariantData
] VariantKind Describe the kind of a variant Visibility Reflects ty::Visibility
WhereEqPredicate WhereRegionPredicate Deserialize A data structure that can be deserialized from any data format supported
by Serde. ExprKindExt HasParamEnv IsBody IsMirKind JsonSchema A type which can be described as a JSON Schema document. SExpect SInto Serialize A data structure that can be serialized into any data format supported
by Serde. SubstBinder ToPolyTraitRef TypeMapper Defines a mapping from types to types. body_from_id const_value_to_constant_expr erase_and_norm eval_mir_constant Evaluate a mir::Const
. eval_ty_constant Evaluate a ty::Const
. get_closest_parent_type Gets the closest ancestor of id
that is the id of a type. get_def_kind Gets the kind of the definition. get_def_span Gets the attributes of the definition. get_thir implied_predicates The predicates that can be deduced from the presence of this item in a signature. We only
consider predicates implied by traits here, not implied bounds such as &'a T
implying T: 'a
. E.g. make_fn_def predicates_defined_on Returns a list of type predicates for the definition with ID def_id
, including inferred
lifetime constraints. This is the basic list of predicates we use for essentially all items. required_predicates The predicates that must hold to mention this item. E.g. self_clause_for_item Retrieve the Self: Trait
clause for a trait associated item. self_predicate The special “self” predicate on a trait. solve_item_and_parents_required_traits Like solve_item_required_traits
, but also includes predicates coming from the parent items. solve_item_implied_traits Solve the trait obligations for implementing a trait (or for trait associated type bounds) in
the current context. solve_item_required_traits Solve the trait obligations for a specific item use (for example, a method call, an ADT, etc.)
in the current context. solve_trait This is the entrypoint of the solving. super_clause_to_clause_and_impl_expr 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 an ImplExpr
. translate_constant_reference Attempts to translate a ty::UnevaluatedConst
into a constant expression. This handles cases
of references to top-level or associated constants. Returns None
if the input was not a named
constant. translate_span BasicBlocks 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 EnumDef Expr FirstStatementIndex GlobalIdent Ident Reflects rustc_span::symbol::Ident
ItemLocalId Mutability Pat Path PlaceholderConst Reflects ty::PlaceholderConst
PlaceholderRegion Reflects ty::PlaceholderRegion
PlaceholderType Reflects ty::PlaceholderType
PolyFnSig Reflects ty::PolyFnSig
RegionOutlivesPredicate Reflects ty::RegionOutlivesPredicate
RegionVid Symbol ThirBody TokenStream Reflects rustc_ast::tokenstream::TokenStream
as a plain
string. If you need to reshape that into Rust tokens or construct,
please use, e.g., syn
. TypeOutlivesPredicate Reflects ty::TypeOutlivesPredicate
UniverseIndex VariantIdx AdtInto AdtInto
derives a
SInto
instance. This helps at transporting a algebraic data type A
to
another ADT B
when A
and B
shares a lot of structure.Deserialize JsonSchema Serialize TypeMappable