1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106
//! This crate provides an interface to perform lattice-based type checking on arbitrary structures. //! //! The [TypeChecker] struct constitutes the main struct. It provides functions to create new [TcKey]s. //! 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 [Variant] or [ContextSensitiveVariant] trait. The following documentation //! uses both traits interchangeably whenever possible without ambiguity. //! //! 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. These can either be [Variant]s with the keys representing their children, or //! _constructed_ types if [Variant] implements [Constructable]. //! //! # 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 MyVariant { //! Integer(usize), //! Boolean, //! Top, //! } //! ``` //! //! Implement the [Variant] type for the enum. This requires an additional error type, access to a [Variant::top()] element, and information whether //! or not the variant has a fixed or variable 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, tuples of undetermined length have variable arity. //! ``` //! # #[derive(PartialEq, Eq, Clone, Debug)] //! # enum MyVariant { //! # Integer(usize), //! # Boolean, //! # Top, //! # } //! # use rusttyc::{TcVar, TypeChecker, Variant, TcErr, Partial, Arity}; //! type MyTypeErr = String; //! impl Variant for MyVariant { //! type Err = MyTypeErr; //! fn arity(&self) -> Arity { Arity::Fixed(0) } //! fn top() -> Self { MyVariant::Top } //! fn meet(lhs: Partial<Self>, rhs: Partial<Self>) -> Result<Partial<Self>, Self::Err> { //! assert_eq!(lhs.least_arity, 0); //! assert_eq!(lhs.least_arity, 0); //! let variant = match (lhs.variant, rhs.variant) { //! (MyVariant::Top, x) | (x, MyVariant::Top) => Ok(x), //! (MyVariant::Boolean, MyVariant::Boolean) => Ok(MyVariant::Boolean), //! (MyVariant::Integer(a), MyVariant::Integer(b)) => Ok(MyVariant::Integer(usize::max(a, b))), //! (MyVariant::Boolean, MyVariant::Integer(_)) | (MyVariant::Integer(_), MyVariant::Boolean) => Err(String::from("Cannot combine Boolean and Integer")), //! }?; //! Ok(Partial { variant, least_arity: 0 }) //! } //! } //! #[derive(PartialEq, Eq, Hash, Clone, Copy, Debug)] //! struct MyVariable(u8); //! impl TcVar for MyVariable {} //! //! # fn main() -> Result<(), TcErr<MyVariant>> { //! let mut tc: TypeChecker<MyVariant, MyVariable> = TypeChecker::new(); //! // We type check `x = 0b111 ^ 0b11010`, so x needs 5 bits. //! let t1 = tc.new_term_key(); //! // The first term is an int with at least a width of 3 bits. //! tc.impose(t1.concretizes_explicit(MyVariant::Integer(3)))?; //! let t2 = tc.new_term_key(); //! // The second term is an int with at least a width of 5 bits. //! tc.impose(t2.concretizes_explicit(MyVariant::Integer(5)))?; //! let tx = tc.new_term_key(); // tx is the combination of t1 and t2, e.g. xor or addition. //! tc.impose(tx.is_meet_of(t1, t2))?; // The result is the meet of both types. //! let type_table = tc.type_check_preliminary()?; //! assert_eq!(type_table[&tx].variant, MyVariant::Integer(5)); //! # Ok(()) //! } //! ``` //! //! ## 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. //! #![deny( missing_docs, missing_debug_implementations, missing_copy_implementations, trivial_casts, trivial_numeric_casts, unsafe_code, unstable_features, unused_import_braces, unused_qualifications, broken_intra_doc_links, unused_results )] pub(crate) mod constraint_graph; mod keys; #[cfg(test)] mod tests; mod type_checker; pub mod types; pub use keys::TcKey; pub use type_checker::{TcErr, TcVar, TypeChecker, VarlessTypeChecker}; pub use types::{ Arity, Constructable, ContextSensitiveVariant, Partial, Preliminary, PreliminaryTypeTable, TypeTable, Variant, };