[][src]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 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::{types::Abstract, TcKey, TypeChecker, TcVar, TcErr};

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

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

impl Abstract for MyType {
    type Err = String;
    fn with_children<I>(&self, children: I) -> Self
    where
        I: IntoIterator<Item = Self>,
    {
        assert!(children.into_iter().collect::<Vec<Self>>().is_empty());
        self.clone()
    }
    fn nth_child(&self, _: usize) -> &Self {
        panic!("will not be called")
    }
    fn meet(&self, other: &Self) -> Result<Self, Self::Err> {
        use MyType::*;
        match (*self, *other) {
            (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),
        }
    }
    fn unconstrained() -> Self {
        Self::Top
    }
    fn arity(&self) -> Option<usize> {
        match self {
            Self::String | Self::U8 => Some(0),
            _ => None,
        }
    }
}
#[derive(PartialEq, Eq, Hash, Clone, Copy, Debug)]
struct MyVar(u8);
impl TcVar for MyVar {}

The type checking procedure can then proceed as follows.

let mut tc: TypeChecker<MyType, 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(MyType::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()?;
assert_eq!(tt[key1], MyType::Numeric);
assert_eq!(tt[key2], MyType::Numeric);
assert_eq!(tt[key3], MyType::Numeric);
// we did not impose a constraint on it, yet, so its the top element.
assert_eq!(tt[key4], MyType::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(MyType::UInt))?;

let tt = tc.clone().type_check()?;
assert_eq!(tt[key1], MyType::Numeric);
assert_eq!(tt[key2], MyType::UInt);
assert_eq!(tt[key3], MyType::UInt);
assert_eq!(tt[key4], MyType::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(MyType::U8))?;
let key5 = tc.new_term_key();
tc.impose(key5.concretizes_explicit(MyType::String))?; // key5 is a string.

let tt = tc.clone().type_check()?;
assert_eq!(tt[key1], MyType::Numeric);
assert_eq!(tt[key2], MyType::U8);
assert_eq!(tt[key3], MyType::U8);
assert_eq!(tt[key4], MyType::U8);
assert_eq!(tt[key5], MyType::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.clone().type_check();
// The meet of numeric types and strings will fail, so key6 cannot be resolved.
assert!(res.is_err());  

Implementations

impl TcKey[src]

pub fn concretizes<AbsTy: Abstract>(self, bound: Self) -> Constraint<AbsTy>[src]

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

pub fn equate_with<AbsTy: Abstract>(self, other: Self) -> Constraint<AbsTy>[src]

equate_withs 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<AbsTy: Abstract>(
    self,
    bound: AbsTy
) -> Constraint<AbsTy>
[src]

Declares that self is at least as concrete as bound.

pub fn is_meet_of<AbsTy: Abstract>(
    self,
    left: Self,
    right: Self
) -> Constraint<AbsTy>
[src]

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<AbsTy: Abstract>(
    self,
    elems: &[Self]
) -> Constraint<AbsTy>
[src]

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<AbsTy: Abstract>(
    self,
    left: Self,
    right: Self
) -> Constraint<AbsTy>
[src]

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<AbsTy: Abstract>(
    self,
    elems: &[Self]
) -> Constraint<AbsTy>
[src]

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

pub fn concretizes_concrete<AbsTy: Abstract, CT>(
    self,
    conc: CT
) -> Constraint<AbsTy> where
    CT: Generalizable<Generalized = AbsTy>, 
[src]

Declares that self is at least as concrete as the abstracted version of conc.

Trait Implementations

impl Clone for TcKey[src]

impl Copy for TcKey[src]

impl Debug for TcKey[src]

impl Eq for TcKey[src]

impl Hash for TcKey[src]

impl<AbsTy: Abstract> Index<TcKey> for AbstractTypeTable<AbsTy>[src]

type Output = AbsTy

The returned type after indexing.

impl<Concrete> Index<TcKey> for ReifiedTypeTable<Concrete>[src]

type Output = Concrete

The returned type after indexing.

impl PartialEq<TcKey> for TcKey[src]

impl StructuralEq for TcKey[src]

impl StructuralPartialEq for TcKey[src]

Auto Trait Implementations

impl RefUnwindSafe for TcKey

impl Send for TcKey

impl Sync for TcKey

impl Unpin for TcKey

impl UnwindSafe for TcKey

Blanket Implementations

impl<T> Any for T where
    T: 'static + ?Sized
[src]

impl<T> Borrow<T> for T where
    T: ?Sized
[src]

impl<T> BorrowMut<T> for T where
    T: ?Sized
[src]

impl<T> From<T> for T[src]

impl<T, U> Into<U> for T where
    U: From<T>, 
[src]

impl<T> ToOwned for T where
    T: Clone
[src]

type Owned = T

The resulting type after obtaining ownership.

impl<T, U> TryFrom<U> for T where
    U: Into<T>, 
[src]

type Error = Infallible

The type returned in the event of a conversion error.

impl<T, U> TryInto<U> for T where
    U: TryFrom<T>, 
[src]

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.