Struct PolyFuncSort

pub struct PolyFuncSort {
    params: List<SortParamKind>,
    fsort: FuncSort,
}

A polymorphic function sort parametric over sorts or bit-vector sizes.

Parameterizing over bit-vector sizes is a bit of a stretch, because smtlib doesn’t support full parametric reasoning over them. As long as we used functions parameterized over a size monomorphically we should be fine. Right now, we can guarantee this, because size parameters are not exposed in the surface syntax and they are only used for predefined (interpreted) theory functions.

Fields

params: List<SortParamKind>

The list of parameters including sorts and bit vector sizes

fsort: FuncSort

Implementations

impl PolyFuncSort

pub fn new(params: List<SortParamKind>, fsort: FuncSort) -> Self

pub fn skip_binders(&self) -> FuncSort

pub fn instantiate_identity(&self) -> FuncSort

pub fn expect_mono(&self) -> FuncSort

pub fn params(&self) -> impl ExactSizeIterator<Item = SortParamKind> + '_

pub fn instantiate(&self, args: &[SortArg]) -> FuncSort

Trait Implementations

impl Clone for PolyFuncSort

fn clone(&self) -> PolyFuncSort

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for PolyFuncSort

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<__D: TyDecoder> Decodable<__D> for PolyFuncSort

fn decode(__decoder: &mut __D) -> Self

impl<__E: TyEncoder> Encodable<__E> for PolyFuncSort

fn encode(&self, __encoder: &mut __E)

impl Hash for PolyFuncSort

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for PolyFuncSort

fn eq(&self, other: &PolyFuncSort) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Pretty for PolyFuncSort

fn fmt(&self, cx: &PrettyCx<'_>, f: &mut Formatter<'_>) -> Result

fn default_cx(tcx: TyCtxt<'_>) -> PrettyCx<'_>

impl TypeFoldable for PolyFuncSort

fn try_fold_with<F: FallibleTypeFolder>( &self, folder: &mut F, ) -> Result<Self, F::Error>

fn fold_with<F: TypeFolder>(&self, folder: &mut F) -> Self

fn normalize_projections<'tcx>( &self, genv: GlobalEnv<'_, 'tcx>, infcx: &InferCtxt<'tcx>, callsite_def_id: DefId, ) -> QueryResult<Self>

fn normalize(&self, defns: &SpecFuncDefns) -> Self

Normalize expressions by applying beta reductions for tuples and lambda abstractions.

fn replace_holes( &self, f: impl FnMut(&[BoundVariableKinds], HoleKind) -> Expr, ) -> Self

Replaces all holes with the result of calling a closure. The closure takes a list with all the layers of bound variables at the point the hole was found. Each layer corresponds to the list of bound variables at that level. The list is ordered from outermost to innermost binder, i.e., the last element is the binder closest to the hole.

fn with_holes(&self) -> Self

Remove all refinements and turn each underlying BaseTy into a TyKind::Exists with a TyKind::Constr and a hole. For example, Vec<{v. i32[v] | v > 0}>[n] becomes {n. Vec<{v. i32[v] | *}>[n] | *}.

fn replace_evars(&self, evars: &EVarSol) -> Self

fn shift_in_escaping(&self, amount: u32) -> Self

fn shift_out_escaping(&self, amount: u32) -> Self

fn erase_regions(&self) -> Self

impl TypeVisitable for PolyFuncSort

fn visit_with<V: TypeVisitor>(&self, visitor: &mut V) -> ControlFlow<V::BreakTy>

fn has_escaping_bvars(&self) -> bool

fn has_escaping_bvars_at_or_above(&self, binder: DebruijnIndex) -> bool

Returns true if self has any late-bound vars that are either bound by binder or bound by some binder outside of binder. If binder is ty::INNERMOST, this indicates whether there are any late-bound vars that appear free.

fn fvars(&self) -> FxHashSet<Name>

Returns the set of all free variables. For example, Vec<i32[n]>{v : v > m} returns {n, m}.

impl Eq for PolyFuncSort

impl StructuralPartialEq for PolyFuncSort