Expand description
Flux High-Level Intermediate Representation
The fhir corresponds to the desugared version of source level flux annotations. The main difference with the surface syntax is that the list of refinement parameters is explicit in fhir. For example, the following signature
fn(x: &strg i32[@n]) ensures x: i32[n + 1]
desugars to
for<n: int, l: loc> fn(&strg<l: i32[n]>) ensures l: i32[n + 1].
The name fhir is borrowed (pun intended) from rustc’s hir to refer to something a bit lower than the surface syntax.
Modules§
Structs§
- Alias
Reft <qself as path>::name- Assoc
Item Constraint - Bare
FnTy - BaseTy
- These are types of things that may be refined with indices or existentials
- Const
Arg - EnumDef
- Expr
- FhirId
- A unique identifier for a node in the AST. Like
HirIdit is composed of anownerand alocal_id. We don’t generate ids for all nodes, but only for those we need to remember information elaborated during well-formedness checking to later be used during conversion intorty. - Field
Def - Field
Expr - Flux
Items - A map between rust definitions and flux annotations in their desugared
fhirform. - FnDecl
- FnOutput
- FnSig
- Foreign
Item - Func
Sort - Generic
Param - Generics
- Impl
- Impl
Assoc Reft - Impl
Item - Item
- Item
Local Id - An
ItemLocalIduniquely identifies something within a given “item-like”. - LetDecl
- MutTy
- Opaque
Ty - ParamId
- Partial
Res - See [
rustc_hir::def::PartialRes] - Path
- Path
Expr - Path
Segment - Poly
Func Sort - Poly
Trait Ref - Qualifier
- Range
- Refine
Param - Refined
By - Information about the refinement parameters associated with an adt (struct/enum).
- Requires
- A predicate required to hold before calling a function.
- Sort
Decl - Sort
Path - See
flux_syntax::surface::SortPath - Spec
Func - Spread
- Struct
Def - Trait
- Trait
Assoc Reft - Trait
Item - Ty
- TyAlias
- Variant
Def - Variant
Ret - Where
Bound Predicate - Variant
Idx - The source-order index of a variant in a type.
Enums§
- Assoc
Item Constraint Kind - Base
TyKind - BinOp
- Const
ArgKind - Ensures
- Expr
Kind - ExprRes
- Flux
Item - Flux
Owner Id - Owner version of
FluxLocalDefId - Foreign
Item Kind - Generic
Arg - Generic
Bound - Generic
Param Kind - Ignored
- A boolean-like enum used to mark whether a piece of code is ignored.
- Impl
Item Kind - Infer
Mode - Inference mode for a parameter.
- Item
Kind - Lifetime
- Our surface syntax doesn’t have lifetimes. To deal with them we create a hole for every lifetime which we then resolve when we check for structural compatibility against the rust type.
- Lit
- Node
- Owner
Node - Param
Kind - How a parameter was declared in the surface syntax.
- Prim
Sort - QPath
- Quant
Kind - Refinement
Kind - Res
- Sort
- SortRes
- Spec
Func Kind - Struct
Kind - Trait
Bound Modifier - Trait
Item Kind - Trusted
- A boolean-like enum used to mark whether some code should be trusted.
- TyKind
- UnOp
- Mutability
- PrimTy
- Not represented directly in the AST; referred to by name through a
ty_path.