Struct TypeChecker

pub struct TypeChecker<S: Sort> { /* private fields */ }

Implementations

impl<S: Sort> TypeChecker<S>

pub fn new() -> TypeChecker<S>

pub fn new_type_variable(&mut self, span: Span) -> TypeRef<S>

pub fn new_attached_type_variable( &mut self, span: Span, pointer: *mut Option<GroundSort<S>>, ) -> TypeRef<S>

pub fn assert_equal<A: Into<TypeRef<S>>, B: Into<TypeRef<S>>>( &mut self, expected: A, given: B, )

Add a new constraint to the type checker.

Even of the system is not satisfiable, this function never fail. Type errors are detected with the TypeChecker::resolve method.

pub fn var(&self, index: usize) -> &TypeRef<S>

pub fn push<T: Into<TypeRef<S>>>(&mut self, ty: T)

pub fn pop(&mut self, len: usize)

pub fn enter(&mut self, span: Span)

pub fn leave(&mut self)

pub fn location(&self) -> Span

pub fn representant(&self, id: usize) -> (usize, TypeRef<S>)

pub fn redirected(&self, ty: &TypeRef<S>) -> TypeRef<S>

pub fn unify( &self, expected: TypeRef<S>, given: TypeRef<S>, root: bool, span: Span, ) -> Result<(TypeRef<S>, Vec<Constraint<S>>), SortMissmatch<S>>

pub fn resolve(&mut self) -> Result<(), S>

Resolve all the constraints.

pub unsafe fn apply(&self) -> Result<(), S>

Apply the resolved types.