Crate hax_frontend_exporter

Source

Re-exports§

pub use crate::id_table;
pub use hax_frontend_exporter_options as options;
pub use crate::*;
pub use crate::prelude::*;
pub use crate::state::*;

Modules§

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 🔒

Macros§

cfg_feature_rustc 🔒
schema_for
Generates a RootSchema for the given type using default settings.
sinto_as_usize
sinto_todo

Structs§

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 DefIds from upstream crates get thrown into the mix. There are quite a few cases where we know that only DefIds 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

Enums§

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

Traits§

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.

Functions§

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

Type Aliases§

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

Derive Macros§

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

Trait Aliases§

TypeMappable