Module flux_middle::fhir
source · 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§
- “Lift” HIR types into FHIR types.
Structs§
<qself as path>::name- These are types of things that may be refined with indices or existentials
- A map between rust definitions and flux annotations in their desugared
fhirform. - An
ItemLocalIduniquely identifies something within a given “item-like”. - See [
rustc_hir::def::PartialRes] - Information about the refinement parameters associated with an adt (struct/enum).
- A predicate required to hold before calling a function.
- The source-order index of a variant in a type.
Enums§
- A boolean-like enum used to mark whether some code should be checked for overflows
- Owner version of
FluxLocalDefId - A boolean-like enum used to mark whether a piece of code is ignored.
- Inference mode for a parameter.
- 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.
- How a parameter was declared in the surface syntax.
- A boolean-like enum used to mark whether some code should be trusted.
- Not represented directly in the AST; referred to by name through a
ty_path.