Struct rusttyc::TcKey

pub struct TcKey { /* fields omitted */ }

An inexpensive and simple indexing mechanism using during the type checking procedure.

It can that can be copied, checked for equality, and hashed, however, it is not ordered. A TcKey offers functions for relating them to other keys or types, symmetrically or asymmetrically, by creating constraints. These constraints only serve one purpose: They can be passed to the type checker’s crate::TypeChecker::impose() function.

Example

There are several kinds of constraints that can be generated for a key. Assume the following data structures exist:

use rusttyc::{Variant, TcKey, TypeChecker, TcVar, TcErr, Partial, Arity};

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
enum MyVariant {
    Top,
    Numeric,
    UInt,
    U8,
    String,
}

impl Variant for MyVariant {
    type Err = String;
    fn meet(lhs: Partial<Self>, rhs: Partial<Self>) -> Result<Partial<Self>, Self::Err> {
        use MyVariant::*;
        let variant = match (lhs.variant, rhs.variant) {
            (Top, x) | (x, Top) => Ok(x),
            (String, String) => Ok(String),
            (String, _) | (_, String) => Err("string can only be met with string.".to_string()),
            (Numeric, x) | (x, Numeric) => Ok(x), // x can only be Numeric, UInt, or U8.
            (UInt, x) | (x, UInt) => Ok(x),       // x can only be UInt or U8.
            (U8, U8) => Ok(U8),
        }?;
        Ok(Partial { variant, least_arity: 0 })
    }
    fn top() -> Self {
        Self::Top
    }
    fn arity(&self) -> Arity {
        Arity::Fixed(0)
    }
}
#[derive(PartialEq, Eq, Hash, Clone, Copy, Debug)]
struct MyVar(u8);
impl TcVar for MyVar {}

The type checking procedure can then proceed as follows.

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
enum MyVariant {
    Top,
    Numeric,
    UInt,
    U8,
    String,
}

impl Variant for MyVariant {
    type Err = String;
    fn meet(lhs: Partial<Self>, rhs: Partial<Self>) -> Result<Partial<Self>, Self::Err> {
        use MyVariant::*;
        let variant = match (lhs.variant, rhs.variant) {
            (Top, x) | (x, Top) => Ok(x),
            (String, String) => Ok(String),
            (String, _) | (_, String) => Err("string can only be met with string.".to_string()),
            (Numeric, x) | (x, Numeric) => Ok(x), // x can only be Numeric, UInt, or U8.
            (UInt, x) | (x, UInt) => Ok(x),       // x can only be UInt or U8.
            (U8, U8) => Ok(U8),
        }?;
        Ok(Partial { variant, least_arity: 0 })
    }
    fn top() -> Self {
        Self::Top
    }
    fn arity(&self) -> Arity {
        Arity::Fixed(0)
    }
}
#[derive(PartialEq, Eq, Hash, Clone, Copy, Debug)]
struct MyVar(u8);
impl TcVar for MyVar {}

let mut tc: TypeChecker<MyVariant, MyVar> = TypeChecker::new();
let key1 = tc.new_term_key();
let key2 = tc.new_term_key();
let key3 = tc.new_term_key();
let key4 = tc.new_term_key();

tc.impose(key1.concretizes_explicit(MyVariant::Numeric))?;  // key1 is numeric.
// key2 is at least as concrete as k1, i.e. it will also be numeric.
tc.impose(key2.concretizes(key1))?;
tc.impose(key3.equate_with(key2))?; // key3 is the same type as key2, i.e., numeric

let tt = tc.clone().type_check_preliminary()?;
assert_eq!(tt[&key1].variant, MyVariant::Numeric);
assert_eq!(tt[&key2].variant, MyVariant::Numeric);
assert_eq!(tt[&key3].variant, MyVariant::Numeric);
// we did not impose a constraint on it, yet, so its the top element.
assert_eq!(tt[&key4].variant, MyVariant::Top);

// Concretize key3 to be a UInt.  Also affects key2 due to unification.  
// key1 is unaffected because of the asymmetric relation between key1 and key2,
// which translates to an asymmetric relation between key1 and key3 as well.
tc.impose(key3.concretizes_explicit(MyVariant::UInt))?;

let tt = tc.clone().type_check_preliminary()?;
assert_eq!(tt[&key1].variant, MyVariant::Numeric);
assert_eq!(tt[&key2].variant, MyVariant::UInt);
assert_eq!(tt[&key3].variant, MyVariant::UInt);
assert_eq!(tt[&key4].variant, MyVariant::Top);

// key4 is more concrete than both key2 (and transitively key3), and key1, so it becomes a UInt.
tc.impose(key4.is_meet_of(key2, key1))?;
// Make key2 and key3 U8.  key4 depends on them, so it becomes U8 as well.  key1 is unaffected.
tc.impose(key2.concretizes_explicit(MyVariant::U8))?;
let key5 = tc.new_term_key();
tc.impose(key5.concretizes_explicit(MyVariant::String))?; // key5 is a string.

let tt = tc.clone().type_check_preliminary()?;
assert_eq!(tt[&key1].variant, MyVariant::Numeric);
assert_eq!(tt[&key2].variant, MyVariant::U8);
assert_eq!(tt[&key3].variant, MyVariant::U8);
assert_eq!(tt[&key4].variant, MyVariant::U8);
assert_eq!(tt[&key5].variant, MyVariant::String);

let key6 = tc.new_term_key();
// key6 is the meet of all other keys.
tc.impose(key6.is_meet_of_all(&[key1, key2, key3, key4, key5]))?;

let res = tc.type_check_preliminary();
// The meet of numeric types and strings will fail, so key6 cannot be resolved.
assert!(res.is_err());  

Implementations

impl TcKey

pub fn concretizes<V: ContextSensitiveVariant>(
    self,
    bound: Self
) -> Constraint<V>

Connects two keys asymmetrically. Refining bound refines self whereas refining self leaves bound unaffected.

pub fn equate_with<V: ContextSensitiveVariant>(
    self,
    other: Self
) -> Constraint<V>

Equates two keys, i.e., they refer to the same type and are thus symmetrically connected. Refining one will refine the other as well.

pub fn concretizes_explicit<V: ContextSensitiveVariant>(
    self,
    bound: V
) -> Constraint<V>

Declares that self is at least as concrete as bound.

pub fn is_meet_of<V: ContextSensitiveVariant>(
    self,
    left: Self,
    right: Self
) -> Constraint<V>

Declares that self is the meet of left and right.
This binds self to both left and right asymmetrically.

pub fn is_meet_of_all<V: ContextSensitiveVariant>(
    self,
    elems: &[Self]
) -> Constraint<V>

Declares that self is the meet of all elements contained in elems.
This binds self to all of these keys asymmetrically.

pub fn is_sym_meet_of<V: ContextSensitiveVariant>(
    self,
    left: Self,
    right: Self
) -> Constraint<V>

Declares that self is the symmetric meet of left and right.
This binds self to both left and right symmetrically.

pub fn is_sym_meet_of_all<V: ContextSensitiveVariant>(
    self,
    elems: &[Self]
) -> Constraint<V>

Declares that self is the symmetric meet of all elements contained in elems.
This binds self to all of these keys symmetrically.

Trait Implementations

impl Clone for TcKey

fn clone(&self) -> TcKey

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for TcKey

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

Formats the value using the given formatter.

impl Hash for TcKey

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, 

Feeds a slice of this type into the given Hasher.

impl Ord for TcKey

fn cmp(&self, other: &TcKey) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

Restrict a value to a certain interval.

impl PartialEq<TcKey> for TcKey

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

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

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

This method tests for !=.

impl PartialOrd<TcKey> for TcKey

fn partial_cmp(&self, other: &TcKey) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

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

This method tests less than (for self and other) and is used by the < operator.

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

This method tests less than or equal to (for self and other) and is used by the <= operator.

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

This method tests greater than (for self and other) and is used by the > operator.

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

This method tests greater than or equal to (for self and other) and is used by the >= operator.

impl Copy for TcKey

impl Eq for TcKey

impl StructuralEq for TcKey

impl StructuralPartialEq for TcKey