Module rty

Expand description

Defines how flux represents refinement types internally. Definitions in this module are used during refinement type checking. A couple of important differences between definitions in this module and in crate::fhir are:

Types in this module use debruijn indices to represent local binders.
Data structures are interned so they can be cheaply cloned.

Re-exports§

pub use normalize::NormalizeInfo;
pub use normalize::NormalizedDefns;
pub use normalize::local_deps;
pub use crate::fhir::InferMode;
pub use SortInfer::*;
pub use flux_rustc_bridge::ty::Region::*;

Modules§

binder 🔒
canonicalize: A canonical type is a type where all existentials and constraint predicates are hoisted to the top level. For example, the canonical version of ∃a. {∃b. i32[a + b] | b > 0} is ∃a,b. {i32[a + b] | b > 0}.
expr 🔒
fold: This modules follows the implementation of folding in rustc. For more information read the documentation in rustc_middle::ty::fold.
normalize
pretty 🔒
refining: Refining is the process of generating a refined version of a rust type.
region_matching
subst

Macros§

Bool
Int
Ref
Uint

Structs§

AdtDef
AdtDefData
AdtSortDef: The definition of the data sort automatically generated for a struct or enum.
AdtSortDefData 🔒
AdtSortVariant
AliasReft
AliasTy
AssocRefinements
Binder
BoundReft
BoundRegion
BvSizeVid: A bit vector size vvariable id
Clause
Const
CoroutineObligPredicate
ESpan
EVid: Existential variable id
EarlyBinder
EarlyReftParam
ExistentialProjection
ExistentialTraitRef
Expr
FnOutput
FnSig
FnTraitPredicate
FuncSort
GenericParamDef
GenericPredicates
Generics
Invariant
KVar: In theory a kvar is just an unknown predicate that can use some variables in scope. In practice, fixpoint makes a difference between the first and the rest of the arguments, the first one being the kvar’s self argument. Fixpoint will only instantiate qualifiers that use the self argument. Flux generalizes the self argument to be a list. We call the rest of the arguments the scope.
KVid
Lambda: A lambda abstraction with an elaborated output sort. We need the output sort of lambdas for encoding into fixpoint
LocalTableInContext
LocalTableInContextMut
Name
NumVid: A numeric vvariable id
OutlivesPredicate
ParamSort: ParamSort is used for polymorphic sorts (Set, Map, etc.) and bit-vector size parameters. They should occur “bound” under a PolyFuncSort or an AdtSortDef. We assume there’s a single binder and a ParamSort represents a variable as an index into the list of variables bound by that binder, i.e., the representation doesnt’t support higher-ranked sorts.
Path
PolyFuncSort: A polymorphic function sort parametric over sorts or bit-vector sizes.
ProjectionPredicate
Qualifier
Real
RefineParam
RefinementGenerics
SortVid: A sort vvariable id
SubsetTy: A subset type is a simplified version of a type that has the form {b[e] | p} where b is a BaseTy, e a refinement index, and p a predicate.
TraitPredicate
TraitRef
Ty
VariantSig
WfckResults
AdtFlags
BoundVar
ConstVid: A const variable ID.
DebruijnIndex: A De Bruijn index is a standard means of representing regions (and perhaps later types) in a higher-ranked setting. In particular, imagine a type like this:
EarlyParamRegion
LateParamRegion: The parameter representation of late-bound function parameters, “some region at least as big as the scope fr.scope”.
ParamConst
ParamTy
RegionVid: A region variable ID.
ScalarInt: The raw bytes of a simple value.
TyVid: A type variable ID.
VariantIdx: The source-order index of a variant in a type.

Enums§

AggregateKind
AliasKind
BaseTy
BinOp
BoundReftKind
BoundVariableKind
BvSize: The size of a bit-vector
ClauseKind
Coercion
ConstKind
Constant
ConstantInfo
Ctor
Ensures
ExistentialPredicate
ExprKind
FieldProj
GenericArg
GenericParamDefKind
HoleKind: The position where a hole appears. This determines how it will be inferred. This is related to, but not the same as, an InferMode.
Loc
NumVarValue
Opaqueness: Option-like enum to explicitly mark that we don’t have information about an ADT because it was annotated with #[flux::opaque]. Note that only structs can be marked as opaque.
PtrKind
Region
Sort
SortArg: An argument for a generic parameter in a Sort which can be either a generic sort or a generic bit-vector size.
SortCtor
SortInfer: A placeholder for a sort that needs to be inferred
SortParamKind: See PolyFuncSort
TyKind
TyOrBase
TyOrCtor
UnOp
Var
BoundRegionKind
ClosureKind: Represents the various closure traits in the language. This will determine the type of the environment (self, in the desugaring) argument that the closure expects.
FloatTy
IntTy
LateParamRegionKind: When liberating bound regions, we map their BoundRegionKind to this as we need to track the index of anonymous regions. We otherwise end up liberating multiple bound regions to the same late-bound region.
Mutability
UintTy