Struct erg_compiler::ty::RefinementType

pub struct RefinementType {
    pub var: Str,
    pub t: Box<Type>,
    pub pred: Box<Predicate>,
}

e.g.

{I: Int | I >= 0}
{_: StrWithLen N | N >= 0}
{T: (Int, Int) | T.0 >= 0, T.1 >= 0}

Fields

var: Str

t: Box<Type>

pred: Box<Predicate>

Implementations

impl RefinementType

pub fn new(var: Str, t: Type, pred: Predicate) -> Self

pub fn deconstruct(self) -> (Str, Type, Predicate)

pub fn invert(self) -> Self

{None}.invert() == {x: Obj | x != None}

Trait Implementations

impl Clone for RefinementType

fn clone(&self) -> RefinementType

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for RefinementType

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

Formats the value using the given formatter.

impl Display for RefinementType

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

Formats the value using the given formatter.

impl From<RefinementType> for Type

fn from(refine: RefinementType) -> Self

Converts to this type from the input type.

impl Hash for RefinementType

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 LimitedDisplay for RefinementType

fn limited_fmt<W: Write>(&self, f: &mut W, limit: isize) -> Result

If limit was set to a negative value, it will be displayed without abbreviation. FIXME:

fn to_string_unabbreviated(&self) -> String

impl PartialEq for RefinementType

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

This method tests for self and other values to be equal, and is used by ==.

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

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

impl<'a> TryFrom<&'a Type> for &'a RefinementType

type Error = ()

The type returned in the event of a conversion error.

fn try_from(t: &'a Type) -> Result<&'a RefinementType, ()>

Performs the conversion.

impl Eq for RefinementType

impl StructuralPartialEq for RefinementType