Struct KVarGen

pub struct KVarGen {
    kvars: IndexVec<KVid, KVarDecl>,
    dummy: bool,
}

Fields

kvars: IndexVec<KVid, KVarDecl>

dummy: bool

If true, generate dummy holes instead of kvars. Used during shape mode to avoid generating unnecessary kvars.

Implementations

impl KVarGen

pub(crate) fn new(dummy: bool) -> Self

fn get(&self, kvid: KVid) -> &KVarDecl

pub fn fresh( &mut self, binders: &[BoundVariableKinds], scope: impl IntoIterator<Item = (Var, Sort)>, encoding: KVarEncoding, ) -> Expr

Generate a fresh kvar under several layers of binders. Each layer may contain any kind of bound variable, but variables that are not of kind BoundVariableKind::Refine will be filtered out.

The variables bound in the last layer (last element of the binders slice) is expected to have only BoundVariableKind::Refine and all its elements are used as the self arguments. The rest of the binders are appended to the scope.

Note that the returned expression will have escaping variables and it is up to the caller to put it under an appropriate number of binders.

Prefer using InferCtxt::fresh_kvar when possible.

fn fresh_inner<A>( &mut self, self_args: usize, args: A, encoding: KVarEncoding, ) -> Expr

where A: IntoIterator<Item = (Var, Sort)>,