Struct WKVarInstantiator 

pub struct WKVarInstantiator<'a> {
    args_to_param: &'a UnordMap<Expr, Expr>,
    self_args: &'a UnordSet<Expr>,
    any_self_args_used: bool,
    memo: &'a mut UnordMap<Expr, Expr>,
    current_index: DebruijnIndex,
}

Fields

args_to_param: &'a UnordMap<Expr, Expr>

Map from the actuals passed to this Weak KVar to its params

In theory this could be a Vecrty::Expr, but the instantiator is configured right now to only return a single solution.

self_args: &'a UnordSet<Expr>

Set of self args

any_self_args_used: bool

Were any of the self args used in the expr?

memo: &'a mut UnordMap<Expr, Expr>

In theory, this could (and probably should) map to multiple solutions, i.e. a Vecrty::Expr.

current_index: DebruijnIndex

Implementations

impl WKVarInstantiator<'_>

pub fn try_instantiate_wkvar_args( self_args: usize, wkvar_args: &[Expr], expr: &Expr, ) -> Option<Binder<Expr>>

If it succeeds: creates an expression that can replace the weak kvar, which when used as a refinement will produce the original expr in this branch after all substitutions have happened.

It requires that the expression uses at least one of the first self_args number of wkvar_args.

There are a lot of patches we put in this algorithm to get around the fact that it is purely syntactic. We currently try to eagerly eta reduce any Ctor/Tuples + eta expand any args which aren’t of that form

FIXME(ck): This does not properly deal with expressions that have bound variables: if the expression has a bound variable, we might fail the instantiation when it should succeed.

Trait Implementations

impl FallibleTypeFolder for WKVarInstantiator<'_>

type Error = Var

We fail instantiation if we can’t replace all free variables; return the name of the first unreplaceable free variable found.

fn try_enter_binder(&mut self, _vars: &BoundVariableKinds)

fn try_exit_binder(&mut self)

fn try_fold_expr(&mut self, e: &Expr) -> Result<Expr, Var>

fn try_fold_sort(&mut self, sort: &Sort) -> Result<Sort, Self::Error>

fn try_fold_ty(&mut self, ty: &Ty) -> Result<Ty, Self::Error>

fn try_fold_bty(&mut self, bty: &BaseTy) -> Result<BaseTy, Self::Error>

fn try_fold_subset_ty( &mut self, constr: &SubsetTy, ) -> Result<SubsetTy, Self::Error>

fn try_fold_region(&mut self, re: &Region) -> Result<Region, Self::Error>

fn try_fold_const(&mut self, c: &Const) -> Result<Const, Self::Error>