Struct TypeChecker

pub struct TypeChecker<V: ContextSensitiveVariant, Var: TcVar> { /* private fields */ }

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

The TypeChecker is the main interaction point for the type checking procedure. It provides functionality to obtain TcKeys, manage variables, impose constraints, and generate a type table.

Related Data Structures

• TcKey represent different entities during the type checking procedure such as variables or terms.
• TcVar represent variables in the external structure, e.g. in the AST that is type checked. A variable has exactly one associated key, even if it occurs several times in the external data structure. The type checker manages keys for variables.
• Constraints represent dependencies between keys and types. They can only be created using TcKeys.
• Variant is an external data type that constitutes a potentially unresolved type.
• TcErr is a wrapper for Variant::Err that contains additional information on what went wrong.
• TypeTable maps keys to Constructable::Type if Variant implements Constructable.
• PreliminaryTypeTable maps keys to Preliminary. This is only useful if Variant does not implement Constructable

Process

In the first step after creation, the TypeChecker generates keys and collects information. It may already resolve some constraints and reveal contradictions. This prompts it to return a negative result with a TcErr. When all information is collected, it resolves them and generates a type table that contains the least restrictive Variant type for each registered key.

Note:

The absence of errors does not entail that a constraint can be satisfied. Only the successful generation of a type table indicates that all constraints can be satisfied.

Example

See crate documentation.

Implementations

impl<V: Variant> TypeChecker<V, NoVars>

pub fn without_vars() -> VarlessTypeChecker<V>

Instantiates a new, empty type checker that does not require variables.

Examples found in repository

examples/parametrized_function.rs (line 184)

fn main() {
    // Build an expression to type-check.
    let expr = build_complex_expression_type_checks();
    // Create an empty type checker.
    let mut tc: VarlessTypeChecker<Variant> = TypeChecker::without_vars();
    // Type check the expression.
    let res = tc_expr(&mut tc, &expr).and_then(|key| tc.type_check().map(|tt| (key, tt)));
    match res {
        Ok((key, tt)) => {
            let res_type = tt[&key];
            // Expression `if true then 2.7^3 + 4.3 else 3` should yield type Fixed(3, 3) because the addition requires a
            // Fixed(2,3) and a Fixed(3,3), which results in a Fixed(3, 3).
            // Constructing an actual type yields Type::FixedPointI64F64.
            assert_eq!(res_type, Type::FixedPointI64F64);
        }
        Err(_) => panic!("Unexpected type error!"),
    }
}

impl<V: Variant, Var: TcVar> TypeChecker<V, Var>

pub fn new() -> Self

Creates a new, empty type checker.

impl<V: ContextSensitiveVariant, Var: TcVar> TypeChecker<V, Var>

pub fn with_context(context: V::Context) -> Self

Creates a new, empty type checker with the given context.

pub fn new_term_key(&mut self) -> TcKey

Generates a new key representing a term.

Examples found in repository

examples/parametrized_function.rs (line 125)

fn tc_expr(tc: &mut VarlessTypeChecker<Variant>, expr: &Expression) -> Result<TcKey, TcErr<Variant>> {
    use Expression::*;
    let key_result = tc.new_term_key(); // will be returned
    match expr {
        ConstInt(c) => {
            let width = (128 - c.leading_zeros()).try_into().unwrap();
            tc.impose(key_result.concretizes_explicit(Variant::Integer(width)))?;
        }
        ConstFixed(i, f) => {
            let int_width = (64 - i.leading_zeros()).try_into().unwrap();
            let frac_width = (64 - f.leading_zeros()).try_into().unwrap();
            tc.impose(key_result.concretizes_explicit(Variant::Fixed(int_width, frac_width)))?;
        }
        ConstBool(_) => tc.impose(key_result.concretizes_explicit(Variant::Bool))?,
        Conditional { cond, cons, alt } => {
            let key_cond = tc_expr(tc, cond)?;
            let key_cons = tc_expr(tc, cons)?;
            let key_alt = tc_expr(tc, alt)?;
            tc.impose(key_cond.concretizes_explicit(Variant::Bool))?;
            tc.impose(key_result.is_meet_of(key_cons, key_alt))?;
        }
        PolyFn { name: _, param_constraints, args, returns } => {
            // Note: The following line cannot be replaced by `vec![param_constraints.len(); tc.new_key()]` as this
            // would copy the keys rather than creating new ones.
            let params: Vec<(Option<Variant>, TcKey)> =
                param_constraints.iter().map(|p| (*p, tc.new_term_key())).collect();
            &params;
            for (arg_ty, arg_expr) in args {
                let arg_key = tc_expr(tc, arg_expr)?;
                match arg_ty {
                    ParamType::ParamId(id) => {
                        let (p_constr, p_key) = params[*id];
                        // We need to enforce that the parameter is more concrete than the passed argument and that the
                        // passed argument satisfies the constraints imposed on the parametric type.
                        tc.impose(p_key.concretizes(arg_key))?;
                        if let Some(c) = p_constr {
                            tc.impose(arg_key.concretizes_explicit(c))?;
                        }
                    }
                    ParamType::Abstract(at) => tc.impose(arg_key.concretizes_explicit(*at))?,
                };
            }
            match returns {
                ParamType::Abstract(at) => tc.impose(key_result.concretizes_explicit(*at))?,
                ParamType::ParamId(id) => {
                    let (constr, key) = params[*id];
                    if let Some(c) = constr {
                        tc.impose(key_result.concretizes_explicit(c))?;
                    }
                    tc.impose(key_result.equate_with(key))?;
                }
            }
        }
    }
    Ok(key_result)
}

pub fn get_var_key(&mut self, var: &Var) -> TcKey

Manages keys for variables. It checks if var already has an associated key. If so, it returns the key. Otherwise, it generates a new one.

pub fn get_child_key( &mut self, parent: TcKey, nth: usize, ) -> Result<TcKey, TcErr<V>>

Provides a key to the nth child of the type behind parent. This imposes the restriction that parent resolves to a type that has at least an arity of nth. If this imposition immediately leads to a contradiction, a TcErr is returned. Contradictions due to this constraint may only occur later when resolving further constraints. Calling this function several times on a parent with the same nth results in the same key.

pub fn impose(&mut self, constr: Constraint<V>) -> Result<(), TcErr<V>>

Imposes a constraint on keys. They can be obtained by using the associated functions of TcKey. Returns a TcErr if the constraint immediately reveals a contradiction.

Examples found in repository

examples/parametrized_function.rs (line 129)

fn tc_expr(tc: &mut VarlessTypeChecker<Variant>, expr: &Expression) -> Result<TcKey, TcErr<Variant>> {
    use Expression::*;
    let key_result = tc.new_term_key(); // will be returned
    match expr {
        ConstInt(c) => {
            let width = (128 - c.leading_zeros()).try_into().unwrap();
            tc.impose(key_result.concretizes_explicit(Variant::Integer(width)))?;
        }
        ConstFixed(i, f) => {
            let int_width = (64 - i.leading_zeros()).try_into().unwrap();
            let frac_width = (64 - f.leading_zeros()).try_into().unwrap();
            tc.impose(key_result.concretizes_explicit(Variant::Fixed(int_width, frac_width)))?;
        }
        ConstBool(_) => tc.impose(key_result.concretizes_explicit(Variant::Bool))?,
        Conditional { cond, cons, alt } => {
            let key_cond = tc_expr(tc, cond)?;
            let key_cons = tc_expr(tc, cons)?;
            let key_alt = tc_expr(tc, alt)?;
            tc.impose(key_cond.concretizes_explicit(Variant::Bool))?;
            tc.impose(key_result.is_meet_of(key_cons, key_alt))?;
        }
        PolyFn { name: _, param_constraints, args, returns } => {
            // Note: The following line cannot be replaced by `vec![param_constraints.len(); tc.new_key()]` as this
            // would copy the keys rather than creating new ones.
            let params: Vec<(Option<Variant>, TcKey)> =
                param_constraints.iter().map(|p| (*p, tc.new_term_key())).collect();
            &params;
            for (arg_ty, arg_expr) in args {
                let arg_key = tc_expr(tc, arg_expr)?;
                match arg_ty {
                    ParamType::ParamId(id) => {
                        let (p_constr, p_key) = params[*id];
                        // We need to enforce that the parameter is more concrete than the passed argument and that the
                        // passed argument satisfies the constraints imposed on the parametric type.
                        tc.impose(p_key.concretizes(arg_key))?;
                        if let Some(c) = p_constr {
                            tc.impose(arg_key.concretizes_explicit(c))?;
                        }
                    }
                    ParamType::Abstract(at) => tc.impose(arg_key.concretizes_explicit(*at))?,
                };
            }
            match returns {
                ParamType::Abstract(at) => tc.impose(key_result.concretizes_explicit(*at))?,
                ParamType::ParamId(id) => {
                    let (constr, key) = params[*id];
                    if let Some(c) = constr {
                        tc.impose(key_result.concretizes_explicit(c))?;
                    }
                    tc.impose(key_result.equate_with(key))?;
                }
            }
        }
    }
    Ok(key_result)
}

pub fn lift_into(&mut self, variant: V, sub_types: Vec<TcKey>) -> TcKey

Lifts a collection of keys as children into a certain recursive variant.

pub fn lift_partially( &mut self, variant: V, sub_types: Vec<Option<TcKey>>, ) -> TcKey

Lifts a collection of keys as subset of children into a certain recursive variant.

pub fn all_keys(&self) -> impl Iterator<Item = TcKey> + '_

Returns an iterator over all keys currently present in the type checking procedure.

pub fn update_context<F>(&mut self, update: F)

where F: FnOnce(&mut V::Context),

Updates the current context.

Applies the update function to the context of the current typechecker. The function may mutate the context.

Warning

This will not change any call retroactively, i.e. it only applies to future meet and equate calls. Proceed with caution.

pub fn type_check_preliminary(self) -> Result<PreliminaryTypeTable<V>, TcErr<V>>

Finalizes the type check procedure without constructing a full type table. Refer to TypeChecker::type_check if Variant implements Constructable. Calling this function indicates that all relevant information was passed on to the type checker. It will attempt to resolve all constraints and return a type table mapping each registered key to its minimally constrained Variants. For recursive types, the respective Preliminary provides access to crate::TcKeys refering to their children. If any constrained caused a contradiction, it will return a TcErr containing information about it.

impl<V, Var: TcVar> TypeChecker<V, Var>

where V: Constructable,

pub fn type_check(self) -> Result<TypeTable<V>, TcErr<V>>

Finalizes the type check procedure. Calling this function indicates that all relevant information was passed on to the type checker. It will attempt to resolve all constraints and return a type table mapping each registered key to its minimally constrained, constructed type, i.e. Constructable::Type. Refer to TypeChecker::type_check_preliminary() if Variant does not implement Constructable. If any constrained caused a contradiction, it will return a TcErr containing information about it.

Examples found in repository

examples/parametrized_function.rs (line 186)

fn main() {
    // Build an expression to type-check.
    let expr = build_complex_expression_type_checks();
    // Create an empty type checker.
    let mut tc: VarlessTypeChecker<Variant> = TypeChecker::without_vars();
    // Type check the expression.
    let res = tc_expr(&mut tc, &expr).and_then(|key| tc.type_check().map(|tt| (key, tt)));
    match res {
        Ok((key, tt)) => {
            let res_type = tt[&key];
            // Expression `if true then 2.7^3 + 4.3 else 3` should yield type Fixed(3, 3) because the addition requires a
            // Fixed(2,3) and a Fixed(3,3), which results in a Fixed(3, 3).
            // Constructing an actual type yields Type::FixedPointI64F64.
            assert_eq!(res_type, Type::FixedPointI64F64);
        }
        Err(_) => panic!("Unexpected type error!"),
    }
}

Trait Implementations

impl<V: Clone + ContextSensitiveVariant, Var: Clone + TcVar> Clone for TypeChecker<V, Var>

where V::Context: Clone,

fn clone(&self) -> TypeChecker<V, Var>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<V: Debug + ContextSensitiveVariant, Var: Debug + TcVar> Debug for TypeChecker<V, Var>

where V::Context: Debug,

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

Formats the value using the given formatter.

impl<V: Variant, Var: TcVar> Default for TypeChecker<V, Var>

fn default() -> Self

Returns the “default value” for a type.