[−][src]Struct rusttyc::TcKey
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]
self,
bound: AbsTy
) -> Constraint<AbsTy>
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]
self,
left: Self,
right: Self
) -> Constraint<AbsTy>
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]
self,
elems: &[Self]
) -> Constraint<AbsTy>
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]
self,
left: Self,
right: Self
) -> Constraint<AbsTy>
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]
self,
elems: &[Self]
) -> Constraint<AbsTy>
Declares that self
is the symmetric meet of all elements contained in elems
.
This binds self
to all of these keys symmetrically.
pub fn has_exactly_type<AbsTy: Abstract>(self, ty: AbsTy) -> Constraint<AbsTy>
[src]
Ensures that the type behind self
is exactly ty
. As a consequence, this implicitly imposes ty
as lower bound for self
.
pub fn concretizes_concrete<AbsTy: Abstract, CT>(
self,
conc: CT
) -> Constraint<AbsTy> where
CT: Generalizable<Generalized = AbsTy>,
[src]
self,
conc: CT
) -> Constraint<AbsTy> where
CT: Generalizable<Generalized = AbsTy>,
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]
fn hash<__H: Hasher>(&self, state: &mut __H)
[src]
fn hash_slice<H>(data: &[Self], state: &mut H) where
H: Hasher,
1.3.0[src]
H: Hasher,
impl<AbsTy: Abstract> Index<TcKey> for AbstractTypeTable<AbsTy>
[src]
type Output = AbsTy
The returned type after indexing.
fn index(&self, index: TcKey) -> &Self::Output
[src]
impl<Concrete> Index<TcKey> for ReifiedTypeTable<Concrete>
[src]
type Output = Concrete
The returned type after indexing.
fn index(&self, index: TcKey) -> &Self::Output
[src]
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]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,