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.