Module flux_middle::rty

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 evars::EVar;
• pub use evars::EVarGen;
• pub use crate::fhir::InferMode;
• pub use flux_rustc_bridge::ty::Region::*;
• pub use SortInfer::*;

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}.
• evars
• expr 🔒
• fold
  This modules follows the implementation of folding in rustc. For more information read the documentation in rustc_middle::ty::fold.
• normalize 🔒
• pretty 🔒
• projections
• 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 🔒
• AliasReft
• AliasTy
• AssocRefinement
• AssocRefinements
• Binder
• BoundReft
• BoundRegion
• BvSizeVid
  A bit vector size vvariable id
• Clause
• Const
• CoroutineObligPredicate
• ESpan
• 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
• LateParamRegion
• 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; i.e. should be < than the number of params.
• Path
• PolyFuncSort
  A polymorphic function sort parametric over sorts or bit-vector sizes.
• ProjectionPredicate
• Qualifier
• Real
• RefineParam
• RefinementGenerics
• SortVid
  A sort vvariable id
• SpecFunc
• SpecFuncDecl
• SpecFuncDefns
• 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
• 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
• 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
• Mutability
• UintTy

Constants

• SELF_PARAM_TY
• FIRST_VARIANT
  Equivalent to VariantIdx(0).
• INNERMOST

Statics

• INT_TYS
• UINT_TYS

Traits

• GenericArgsExt
• RefineArgsExt

Functions

• int_invariants 🔒
• slice_invariants 🔒
  returns the same invariants as for usize which is the length of a slice
• uint_invariants 🔒

Type Aliases

• BoundVariableKinds
• Clauses
• GenericArgs
• ItemLocalMap
• List
• PolyExistentialPredicate
• PolyExistentialTraitRef
• PolyFnSig
• PolyProjectionPredicate
• PolyTraitPredicate
• PolyTraitRef
• PolyVariant
• PolyVariants
• RefineArgs
• SubsetTyCtor
  A type constructor meant to be used as generic a argument of kind base. This is just an alias to Binder<SubsetTy>, but we expect the binder to have a single bound variable of the sort of the underlying base type.
• TyCtor
• TypeOutlivesPredicate