Struct move_model::ty::TypeUnificationAdapter

pub struct TypeUnificationAdapter { /* private fields */ }

Helper to unify types which stem from different generic contexts.

Both comparison side may have type parameters (equally named as #0, #1, …). The helper converts the type parameter from or both sides into variables and then performs unification of the terms. The resulting substitution is converted back to parameter instantiations.

Example: consider a function f which uses memory M<X, u64>, and invariant invariant which uses memory M<bool, X>. Using this helper to unify both memories will result in instantiations which when applied create f and invariant respectively.

Implementations

impl TypeUnificationAdapter

pub fn new_pair(
    lhs_type: &Type,
    rhs_type: &Type,
    treat_lhs_type_param_as_var: bool,
    treat_rhs_type_param_as_var: bool
) -> Self

Create a TypeUnificationAdapter with the goal of unifying a pair of types.

If treat_lhs_type_param_as_var is True, treat all type parameters on the LHS as variables. If treat_rhs_type_param_as_var is True, treat all type parameters on the RHS as variables.

pub fn new_vec(
    lhs_types: &[Type],
    rhs_types: &[Type],
    treat_lhs_type_param_as_var: bool,
    treat_rhs_type_param_as_var: bool
) -> Self

Create a TypeUnificationAdapter with the goal of unifying a pair of type tuples.

If treat_lhs_type_param_as_var is True, treat all type parameters on the LHS as variables. If treat_rhs_type_param_as_var is True, treat all type parameters on the RHS as variables.

pub fn unify(
    self,
    variance: Variance,
    shallow_subst: bool
) -> Option<(BTreeMap<u16, Type>, BTreeMap<u16, Type>)>

Consume the TypeUnificationAdapter and produce the unification result. If type unification is successful, return a pair of instantiations for type parameters on each side which unify the LHS and RHS respectively. If the LHS and RHS cannot unify, None is returned.