rusttyc

Struct TcKey

Source 
pub struct TcKey { /* private fields */ }
Expand description

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§

Source§

impl TcKey

Source

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

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

Examples found in repository?
examples/parametrized_function.rs (line 157)
123fn tc_expr(tc: &mut VarlessTypeChecker<Variant>, expr: &Expression) -> Result<TcKey, TcErr<Variant>> {
124    use Expression::*;
125    let key_result = tc.new_term_key(); // will be returned
126    match expr {
127        ConstInt(c) => {
128            let width = (128 - c.leading_zeros()).try_into().unwrap();
129            tc.impose(key_result.concretizes_explicit(Variant::Integer(width)))?;
130        }
131        ConstFixed(i, f) => {
132            let int_width = (64 - i.leading_zeros()).try_into().unwrap();
133            let frac_width = (64 - f.leading_zeros()).try_into().unwrap();
134            tc.impose(key_result.concretizes_explicit(Variant::Fixed(int_width, frac_width)))?;
135        }
136        ConstBool(_) => tc.impose(key_result.concretizes_explicit(Variant::Bool))?,
137        Conditional { cond, cons, alt } => {
138            let key_cond = tc_expr(tc, cond)?;
139            let key_cons = tc_expr(tc, cons)?;
140            let key_alt = tc_expr(tc, alt)?;
141            tc.impose(key_cond.concretizes_explicit(Variant::Bool))?;
142            tc.impose(key_result.is_meet_of(key_cons, key_alt))?;
143        }
144        PolyFn { name: _, param_constraints, args, returns } => {
145            // Note: The following line cannot be replaced by `vec![param_constraints.len(); tc.new_key()]` as this
146            // would copy the keys rather than creating new ones.
147            let params: Vec<(Option<Variant>, TcKey)> =
148                param_constraints.iter().map(|p| (*p, tc.new_term_key())).collect();
149            &params;
150            for (arg_ty, arg_expr) in args {
151                let arg_key = tc_expr(tc, arg_expr)?;
152                match arg_ty {
153                    ParamType::ParamId(id) => {
154                        let (p_constr, p_key) = params[*id];
155                        // We need to enforce that the parameter is more concrete than the passed argument and that the
156                        // passed argument satisfies the constraints imposed on the parametric type.
157                        tc.impose(p_key.concretizes(arg_key))?;
158                        if let Some(c) = p_constr {
159                            tc.impose(arg_key.concretizes_explicit(c))?;
160                        }
161                    }
162                    ParamType::Abstract(at) => tc.impose(arg_key.concretizes_explicit(*at))?,
163                };
164            }
165            match returns {
166                ParamType::Abstract(at) => tc.impose(key_result.concretizes_explicit(*at))?,
167                ParamType::ParamId(id) => {
168                    let (constr, key) = params[*id];
169                    if let Some(c) = constr {
170                        tc.impose(key_result.concretizes_explicit(c))?;
171                    }
172                    tc.impose(key_result.equate_with(key))?;
173                }
174            }
175        }
176    }
177    Ok(key_result)
178}
Source

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.

Examples found in repository?
examples/parametrized_function.rs (line 172)
123fn tc_expr(tc: &mut VarlessTypeChecker<Variant>, expr: &Expression) -> Result<TcKey, TcErr<Variant>> {
124    use Expression::*;
125    let key_result = tc.new_term_key(); // will be returned
126    match expr {
127        ConstInt(c) => {
128            let width = (128 - c.leading_zeros()).try_into().unwrap();
129            tc.impose(key_result.concretizes_explicit(Variant::Integer(width)))?;
130        }
131        ConstFixed(i, f) => {
132            let int_width = (64 - i.leading_zeros()).try_into().unwrap();
133            let frac_width = (64 - f.leading_zeros()).try_into().unwrap();
134            tc.impose(key_result.concretizes_explicit(Variant::Fixed(int_width, frac_width)))?;
135        }
136        ConstBool(_) => tc.impose(key_result.concretizes_explicit(Variant::Bool))?,
137        Conditional { cond, cons, alt } => {
138            let key_cond = tc_expr(tc, cond)?;
139            let key_cons = tc_expr(tc, cons)?;
140            let key_alt = tc_expr(tc, alt)?;
141            tc.impose(key_cond.concretizes_explicit(Variant::Bool))?;
142            tc.impose(key_result.is_meet_of(key_cons, key_alt))?;
143        }
144        PolyFn { name: _, param_constraints, args, returns } => {
145            // Note: The following line cannot be replaced by `vec![param_constraints.len(); tc.new_key()]` as this
146            // would copy the keys rather than creating new ones.
147            let params: Vec<(Option<Variant>, TcKey)> =
148                param_constraints.iter().map(|p| (*p, tc.new_term_key())).collect();
149            &params;
150            for (arg_ty, arg_expr) in args {
151                let arg_key = tc_expr(tc, arg_expr)?;
152                match arg_ty {
153                    ParamType::ParamId(id) => {
154                        let (p_constr, p_key) = params[*id];
155                        // We need to enforce that the parameter is more concrete than the passed argument and that the
156                        // passed argument satisfies the constraints imposed on the parametric type.
157                        tc.impose(p_key.concretizes(arg_key))?;
158                        if let Some(c) = p_constr {
159                            tc.impose(arg_key.concretizes_explicit(c))?;
160                        }
161                    }
162                    ParamType::Abstract(at) => tc.impose(arg_key.concretizes_explicit(*at))?,
163                };
164            }
165            match returns {
166                ParamType::Abstract(at) => tc.impose(key_result.concretizes_explicit(*at))?,
167                ParamType::ParamId(id) => {
168                    let (constr, key) = params[*id];
169                    if let Some(c) = constr {
170                        tc.impose(key_result.concretizes_explicit(c))?;
171                    }
172                    tc.impose(key_result.equate_with(key))?;
173                }
174            }
175        }
176    }
177    Ok(key_result)
178}
Source

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

Declares that self is at least as concrete as bound.

Examples found in repository?
examples/parametrized_function.rs (line 129)
123fn tc_expr(tc: &mut VarlessTypeChecker<Variant>, expr: &Expression) -> Result<TcKey, TcErr<Variant>> {
124    use Expression::*;
125    let key_result = tc.new_term_key(); // will be returned
126    match expr {
127        ConstInt(c) => {
128            let width = (128 - c.leading_zeros()).try_into().unwrap();
129            tc.impose(key_result.concretizes_explicit(Variant::Integer(width)))?;
130        }
131        ConstFixed(i, f) => {
132            let int_width = (64 - i.leading_zeros()).try_into().unwrap();
133            let frac_width = (64 - f.leading_zeros()).try_into().unwrap();
134            tc.impose(key_result.concretizes_explicit(Variant::Fixed(int_width, frac_width)))?;
135        }
136        ConstBool(_) => tc.impose(key_result.concretizes_explicit(Variant::Bool))?,
137        Conditional { cond, cons, alt } => {
138            let key_cond = tc_expr(tc, cond)?;
139            let key_cons = tc_expr(tc, cons)?;
140            let key_alt = tc_expr(tc, alt)?;
141            tc.impose(key_cond.concretizes_explicit(Variant::Bool))?;
142            tc.impose(key_result.is_meet_of(key_cons, key_alt))?;
143        }
144        PolyFn { name: _, param_constraints, args, returns } => {
145            // Note: The following line cannot be replaced by `vec![param_constraints.len(); tc.new_key()]` as this
146            // would copy the keys rather than creating new ones.
147            let params: Vec<(Option<Variant>, TcKey)> =
148                param_constraints.iter().map(|p| (*p, tc.new_term_key())).collect();
149            &params;
150            for (arg_ty, arg_expr) in args {
151                let arg_key = tc_expr(tc, arg_expr)?;
152                match arg_ty {
153                    ParamType::ParamId(id) => {
154                        let (p_constr, p_key) = params[*id];
155                        // We need to enforce that the parameter is more concrete than the passed argument and that the
156                        // passed argument satisfies the constraints imposed on the parametric type.
157                        tc.impose(p_key.concretizes(arg_key))?;
158                        if let Some(c) = p_constr {
159                            tc.impose(arg_key.concretizes_explicit(c))?;
160                        }
161                    }
162                    ParamType::Abstract(at) => tc.impose(arg_key.concretizes_explicit(*at))?,
163                };
164            }
165            match returns {
166                ParamType::Abstract(at) => tc.impose(key_result.concretizes_explicit(*at))?,
167                ParamType::ParamId(id) => {
168                    let (constr, key) = params[*id];
169                    if let Some(c) = constr {
170                        tc.impose(key_result.concretizes_explicit(c))?;
171                    }
172                    tc.impose(key_result.equate_with(key))?;
173                }
174            }
175        }
176    }
177    Ok(key_result)
178}
Source

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.

Examples found in repository?
examples/parametrized_function.rs (line 142)
123fn tc_expr(tc: &mut VarlessTypeChecker<Variant>, expr: &Expression) -> Result<TcKey, TcErr<Variant>> {
124    use Expression::*;
125    let key_result = tc.new_term_key(); // will be returned
126    match expr {
127        ConstInt(c) => {
128            let width = (128 - c.leading_zeros()).try_into().unwrap();
129            tc.impose(key_result.concretizes_explicit(Variant::Integer(width)))?;
130        }
131        ConstFixed(i, f) => {
132            let int_width = (64 - i.leading_zeros()).try_into().unwrap();
133            let frac_width = (64 - f.leading_zeros()).try_into().unwrap();
134            tc.impose(key_result.concretizes_explicit(Variant::Fixed(int_width, frac_width)))?;
135        }
136        ConstBool(_) => tc.impose(key_result.concretizes_explicit(Variant::Bool))?,
137        Conditional { cond, cons, alt } => {
138            let key_cond = tc_expr(tc, cond)?;
139            let key_cons = tc_expr(tc, cons)?;
140            let key_alt = tc_expr(tc, alt)?;
141            tc.impose(key_cond.concretizes_explicit(Variant::Bool))?;
142            tc.impose(key_result.is_meet_of(key_cons, key_alt))?;
143        }
144        PolyFn { name: _, param_constraints, args, returns } => {
145            // Note: The following line cannot be replaced by `vec![param_constraints.len(); tc.new_key()]` as this
146            // would copy the keys rather than creating new ones.
147            let params: Vec<(Option<Variant>, TcKey)> =
148                param_constraints.iter().map(|p| (*p, tc.new_term_key())).collect();
149            &params;
150            for (arg_ty, arg_expr) in args {
151                let arg_key = tc_expr(tc, arg_expr)?;
152                match arg_ty {
153                    ParamType::ParamId(id) => {
154                        let (p_constr, p_key) = params[*id];
155                        // We need to enforce that the parameter is more concrete than the passed argument and that the
156                        // passed argument satisfies the constraints imposed on the parametric type.
157                        tc.impose(p_key.concretizes(arg_key))?;
158                        if let Some(c) = p_constr {
159                            tc.impose(arg_key.concretizes_explicit(c))?;
160                        }
161                    }
162                    ParamType::Abstract(at) => tc.impose(arg_key.concretizes_explicit(*at))?,
163                };
164            }
165            match returns {
166                ParamType::Abstract(at) => tc.impose(key_result.concretizes_explicit(*at))?,
167                ParamType::ParamId(id) => {
168                    let (constr, key) = params[*id];
169                    if let Some(c) = constr {
170                        tc.impose(key_result.concretizes_explicit(c))?;
171                    }
172                    tc.impose(key_result.equate_with(key))?;
173                }
174            }
175        }
176    }
177    Ok(key_result)
178}
Source

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.

Source

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.

Source

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§

Source§

impl Clone for TcKey

Source§

fn clone(&self) -> TcKey

Returns a duplicate of the value. Read more
1.0.0 · Source§

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

Performs copy-assignment from source. Read more
Source§

impl Debug for TcKey

Source§

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

Formats the value using the given formatter. Read more
Source§

impl Hash for TcKey

Source§

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

Feeds this value into the given Hasher. Read more
1.3.0 · Source§

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

Feeds a slice of this type into the given Hasher. Read more
Source§

impl Ord for TcKey

Source§

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

This method returns an Ordering between self and other. Read more
1.21.0 · Source§

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

Compares and returns the maximum of two values. Read more
1.21.0 · Source§

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

Compares and returns the minimum of two values. Read more
1.50.0 · Source§

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

Restrict a value to a certain interval. Read more
Source§

impl PartialEq for TcKey

Source§

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

Tests for self and other values to be equal, and is used by ==.
1.0.0 · Source§

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

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

impl PartialOrd for TcKey

Source§

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

This method returns an ordering between self and other values if one exists. Read more
1.0.0 · Source§

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

Tests less than (for self and other) and is used by the < operator. Read more
1.0.0 · Source§

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

Tests less than or equal to (for self and other) and is used by the <= operator. Read more
1.0.0 · Source§

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

Tests greater than (for self and other) and is used by the > operator. Read more
1.0.0 · Source§

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

Tests greater than or equal to (for self and other) and is used by the >= operator. Read more
Source§

impl Copy for TcKey

Source§

impl Eq for TcKey

Source§

impl StructuralPartialEq for TcKey

Auto Trait Implementations§

§

impl Freeze for TcKey

§

impl RefUnwindSafe for TcKey

§

impl Send for TcKey

§

impl Sync for TcKey

§

impl Unpin for TcKey

§

impl UnwindSafe for TcKey

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> CloneToUninit for T
where T: Clone,

Source§

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from self to dest. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T> ToOwned for T
where T: Clone,

Source§

type Owned = T

The resulting type after obtaining ownership.
Source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
Source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

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

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.