[][src]Crate rusttyc

This crate provides an interface to perform lattice-based type checking on arbitrary structures structures.

The TypeChecker struct constitutes the main struct. It provides functions to create new TcKeys.
These keys represent typed entities such as terms or variables in programming languages. TcKey provides a set of functions generating constraints such as 'the type behind key a is more concrete than the type behind key b' or 'type X is an upper bound of the type behind key a'.

The user needs to supply a type lattice by implementing the Abstract trait.

Then, iterate over your data structure, e.g. your abstract syntax tree, generate keys for terms and variables, and impose constraints on the keys. Lastly, generate a type table mapping keys to their resolved types. The type table itself can be Reifiable if the abstract type can be transformed into a concrete type.

Example

Consider a type lattice consisting of a boolean type and an integer type, where the integer type is a variable bit length.

#[derive(PartialEq, Eq, Clone, Debug)]
enum MyType {
    Integer(usize),
    Boolean,
    Unknown,
    Error,
}

Implement the Abstract type for the enum. This requires two additional types: an error type and a variant tag. The latter indicates what kind of variant a certain type has. This is a minor inconvenience required for constructing and destructing incomplete types. The tag provides information about its arity, i.e., the number of subtypes relevant for this type. As an example consider an Option-like type. As a monad, it has arity 1. Scalar types have arity 0. Note that non-leaf types, i.e., types that are not resolved yet such as MyVariant::Unknown, do not provide a tag.

type MyTypeErr = String;
#[derive(PartialEq, Eq, Clone, Copy, Debug)]
enum MyVariant { Integer, Boolean }
impl Abstract for MyType {
    type Err = MyTypeErr;
    type VariantTag = MyVariant;
    fn variant(&self) -> Option<Self::VariantTag> {
        match self {
            MyType::Integer(_) => Some(MyVariant::Integer),
            MyType::Boolean => Some(MyVariant::Boolean),
            MyType::Unknown => None,
        }
    }
    fn unconstrained() -> Self { MyType::Unknown }
    fn meet(&self, other: &Self) -> Result<Self, Self::Err> {
        match (self, other) {
            (MyType::Unknown, x) | (x, MyType::Unknown) => Ok(x.clone()),
            (MyType::Boolean, MyType::Boolean) => Ok(MyType::Boolean),
            (MyType::Integer(a), MyType::Integer(b)) => Ok(MyType::Integer(usize::max(*a, *b))),
            _ => Err(String::from("Cannot combine Boolean and Integer")),
        }
    }
    fn variant_arity(tag: Self::VariantTag) -> usize { 0 }
    fn from_tag(tag: Self::VariantTag, children: Vec<Self>) -> Self {
        match tag {
            MyVariant::Integer => MyType::Integer(0),
            MyVariant::Boolean => MyType::Boolean,
        }
    }
}
#[derive(PartialEq, Eq, Hash, Clone, Copy, Debug)]
struct MyVariable(u8);
impl TcVar for MyVariable {}

let mut tc: TypeChecker<MyType, MyVariable> = TypeChecker::new();
// We type check `x = 0b111 ^ 0b11010`, so x needs 5 bits.
let t1 = tc.new_term_key();
// The term is an int with at least a width of 3 bits.
tc.impose(t1.more_concrete_than_explicit(MyType::Integer(3)))?;
let t2 = tc.new_term_key();
// The term is an int with at least a width of 5 bits.
tc.impose(t2.more_concrete_than_explicit(MyType::Integer(5)))?;
let tx = tc.new_term_key(); // t3 is the combination of t1 and t2, e.g. addition.
tc.impose(tx.is_meet_of(t1, t2))?; // Addition is the meet of both types.
let type_table = tc.type_check()?;
assert_eq!(type_table[tx], MyType::Integer(5));
}

Additional Examples

Check the documentation of TcKey for all possible constraints imposable on keys and their effects. Check the RustTyC examples on github for more elaborate examples.

Modules

types

This mod contains everything related to types and collections of types (type tables).

Structs

TcKey

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

TypeChecker

The TypeChecker is the main interaction point for the type checking procedure.

Enums

TcErr

Represents an error during the type check procedure.

Traits

TcVar

Represents a re-usable variable in the type checking procedure.