Module flux_fhir_analysis::conv
source · Expand description
Conversion from types in fhir to types in rty
Conversion assumes well-formedness and will panic if type are not well-formed. Among other things, well-formedness implies:
- Names are bound correctly.
- Refinement parameters appear in allowed positions. This is particularly important for
refinement predicates, aka abstract refinements, since the syntax in
rtyhas syntactic restrictions on predicates. - Refinements are well-sorted.
Modules§
- errors 🔒
- Check whether two refinemnt types/signatures are structurally compatible.
Structs§
- Wrapper over a type implementing
ConvPhase. We have this to implement most functionality as inherent methods instead of defining them as default implementation in the trait definition. - Env 🔒
- Layer 🔒
Enums§
- Whether the list of parameters in a layer is converted into a list of bound variables or coalesced into a single parameter of adt sort.
Traits§
- We do conversion twice: once before sort checking when we don’t have elaborated information and then again after sort checking after all information has been elaborated. This is the interface to configure conversion for both phases.
- An interface to the information elaborated during sort checking. We mock these results in the first conversion phase during sort checking.
Functions§
- conv_
lit 🔒