Struct SubsetTy

pub struct SubsetTy {
    pub bty: BaseTy,
    pub idx: Expr,
    pub pred: Expr,
}

A subset type is a simplified version of a type that has the form {b[e] | p} where b is a BaseTy, e a refinement index, and p a predicate.

These are mainly found under a Binder with a single variable of the base type’s sort. This can be interpreted as a type constructor or an existial type. For example, under a binder with a variable v of sort int, we can interpret {i32[v] | v > 0} as:

• A lambda λv:int. {i32[v] | v > 0} that “constructs” types when applied to ints, or
• An existential type ∃v:int. {i32[v] | v > 0}.

This second interpretation is the reason we call this a subset type, i.e., the type ∃v. {b[v] | p} corresponds to the subset of values of type b whose index satisfies p. These are the types written as B{v: p} in the surface syntax and correspond to the types supported in other refinement type systems like Liquid Haskell (with the difference that we are explicit about separating refinements from program values via an index).

The main purpose for subset types is to be used as generic arguments of kind base when interpreted as type constructors. They have two key properties that makes them suitable for this:

1. Syntacitc Restriction: Subset types are syntactically restricted, making it easier to relate them structurally (e.g., for subtyping). For instance, given two types S<λv. T1> and S<λ. T2>, if T1 and T2 are subset types, we know they match structurally (at least shallowly). In particularly, the syntactic restriction rules out complex types like S<λv. (i32[v], i32[v])> simplifying some operations.

2. Eager Canonicalization: Subset types can be eagerly canonicalized via strengthening during substitution. For example, suppose we have a function:

   fn foo<T>(x: T[@a], y: { T[@b] | b == a }) { }

   If we instantiate T with λv. { i32[v] | v > 0}, after substitution and applying the lambda (the indexing syntax T[a] corresponds to an application of the lambda), we get:

   fn foo(x: {i32[@a] | a > 0}, y: { { i32[@b] | b > 0 } | b == a }) { }

   Via strengthening we can canonicalize this to

   fn foo(x: {i32[@a] | a > 0}, y: { i32[@b] | b == a && b > 0 }) { }

   As a result, we can guarantee the syntactic restriction through substitution.

Fields

bty: BaseTy

The base type b in the subset type {b[e] | p}.

NOTE: This is mostly going to be under a Binder. It is not yet clear to me whether this BaseTy should be able to mention variables in the binder. In general, in a type ∃v. {b[e] | p}, it’s fine to mention v inside b, but since SubsetTy is meant to facilitate syntactic manipulation we may want to restrict this.

idx: Expr

The refinement index e in the subset type {b[e] | p}. This can be an arbitrary expression, which makes manipulation easier. However, since this is mostly found under a binder, we expect it to be Expr::nu().

pred: Expr

The predicate p in the subset type {b[e] | p}.

Implementations

impl SubsetTy

pub fn new(bty: BaseTy, idx: impl Into<Expr>, pred: impl Into<Expr>) -> Self

pub fn trivial(bty: BaseTy, idx: impl Into<Expr>) -> Self

pub fn strengthen(&self, pred: impl Into<Expr>) -> Self

pub fn to_ty(&self) -> Ty

Trait Implementations

impl Clone for SubsetTy

fn clone(&self) -> SubsetTy

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for SubsetTy

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

Formats the value using the given formatter.

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

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

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

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

impl Hash for SubsetTy

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 SubsetTy

fn eq(&self, other: &SubsetTy) -> 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 SubsetTy

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

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

impl<'tcx> ToRustc<'tcx> for SubsetTy

type T = Ty<'tcx>

fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Ty<'tcx>

impl TypeFoldable for SubsetTy

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 TypeSuperFoldable for SubsetTy

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

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

impl TypeVisitable for SubsetTy

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 SubsetTy

impl StructuralPartialEq for SubsetTy