Module conv

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:

1. Names are bound correctly.
2. Refinement parameters appear in allowed positions. This is particularly important for refinement predicates, aka abstract refinements, since the syntax in rty has syntactic restrictions on predicates.
3. Refinements are well-sorted.

Modules

errors 🔒

struct_compat

Check whether two refinemnt types/signatures are structurally compatible.

Structs

AfterSortck 🔒

ConvCtxt

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 🔒

LookupResult 🔒

ParamEntry 🔒

Enums

LayerKind 🔒

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.

LookupResultKind 🔒

Traits

ConvPhase

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.

WfckResultsProvider

An interface to the information elaborated during sort checking. We mock these results in the first conversion phase during sort checking.

Functions

conv_adt_sort_def 🔒

conv_constant 🔒

conv_constant_expr 🔒

conv_default_type_parameter 🔒

conv_defn 🔒

conv_func_decl

conv_generic_param_kind 🔒

conv_generics 🔒

conv_invariants 🔒

conv_qualifier 🔒

conv_refinement_generics 🔒

conv_un_op 🔒

def_id_to_param_const 🔒

def_id_to_param_ty 🔒

prim_ty_to_bty 🔒

ty_param_name 🔒

ty_param_owner 🔒

variant_idx 🔒